Two Trees in One Ball, version 4

Garrett's tree is built from the six quaternions of norm 5, 1 ± 2i, 1 ± 2j and 1 ± 2k. In the peel coordinate of VOTKP, a step that multiplies a ratio by z has Smith step Γ = (z − 1)/(z + 1) and hyperbolic length ln z, and steps compose by Einstein addition. Read that way, each generator is a Lorentz boost of length ln 5 along its own axis, and the whole tree sits in the Poincaré ball with exact rational coordinates. On the knot side, the Riley meridians of a two-bridge knot on its real curve are boosts of length 2x, and the knot relation closes the word walk into a loop. The paper sets the two trees side by side in one disk: one never closes, the other does. Main results. The ratio-z boosts generate a free group of rank 3 for every whole number z ≥ 2: by a residue argument when z has an odd divisor (Lean), and by a ping-pong at the prime 1 + i of the Gaussian integers when z is even. They form a Schottky group exactly above Γ² = 1/2 (z > 3 + 2√2); at ln 5 the commutator is a rotation of infinite order, so the group is free but not discrete. Two perpendicular steps leave a Thomas rotation with tan(θ/2) = Γ², for every ratio (Lean). The ln 5 boost group is not conjugate to the Lubotzky–Phillips–Sarnak group in PGL(2, ℚ₅), although both act simply transitively on the same 5-adic tree. At ln 7 the distance bound ℓ + (L − 1)δ ≤ d(O, wO) ≤ Lℓ holds with cosh δ = 9/7, and δ is optimal; the ping-pong is checked in Lean. For the knots, tr[a, b] = 2 − v((s − 1/s)² − v) (Lean): the meridian commutator turns only when the meridian axes cross, and below Γ² = 1/2 it always does; for T(2,3), T(2,5) and T(2,7) it never does (Lean). In a census of 26 two-bridge knots, 19 turn and 7 never do. The relator polygon has zero area on a whole geodesic, by a reflection symmetry. Files. The PDF (101 pages) and HTML carry the paper; their appendices print every Lean file and every script with its output. The zip holds the five core-Lean 4.34.1 files (159 theorems, no Mathlib, no sorry, no native_decide), six false controls, the audit script check_core.py, and every script behind Section 8 with its stored output. The interactive Knot Atlas in 3D (with the Commutator eye and Peel tree views) is a separate HTML page. The same files are on GitHub at dicipler-pixel/votkp-lean, folder two-trees/, checked by GitHub Actions on every push. Prepared with AI assistance (Claude, Anthropic); every Lean statement is kernel-checked and every number is reproduced by the included scripts.