Two-block parity vectors and Collatz cycles: a uniform Steiner-type theorem

For two parity words X and Y we study Collatz cycles whose parity vector is, cyclically, X^k Y^l with k, l ≥ 1. A 2 × 2 determinant D(X, Y), built from the two words' affine maps, controls integrality: an integral cycle of this shape has its modulus 2^N − 3^r dividing D times either block's geometric sum. Our main result has two hypotheses: the part of D prime to 6 is ±1, and the two blocks lie on opposite sides of the critical line. Under them, no word X^k Y^l is the parity vector of a non-trivial positive integer cycle. The threshold this needs from Baker's theory is the same for every pair. Through the Christoffel (Stern–Brocot) tree this gives infinitely many explicit families: one for each pair of Farey parents on the path of log₂ 3. The first family is Steiner's circuits (1977), and the second is Mimuro's one-run family (2005). For the later families, a recent preprint (rStation's collatz_57) excludes every two-block word over a pair of total length at most 4.3 · 10^10, assuming the verification of the conjecture to 3 · 2^69. Our proof needs the verification only below 2^37, and for larger pairs the families are new as far as we have found. We then allow s alternations X^(k₁) Y^(l₁) ⋯ X^(kₛ) Y^(lₛ). Deeper pairs allow more alternations: up to 18 at depths 3 and 4, and about 93 at depth 5. From pair size 2.5 · 10^5 on, Baker's theory alone excludes words with up to half the pair product of alternations. With the verification below 2^71, the m-cycle method of Simons–de Weger and Hercher carries over to alternations over a pair. It excludes up to 2,599 alternations at depth 5 and up to 545,184 at depth 16. All of these are instances of one bound: a periodic stretch that starts low in a cycle forces a 2-adic congruence, which brings the cycle too close to the critical line. Sections 1–5, Section 6 up to Theorem 6.5, and Section 7 up to Proposition 7.4 are formally verified in Lean 4 with Mathlib. The cited bounds (Ellison, Laurent, Rhin, Eliahou, and the verification of the conjecture) enter as explicit hypotheses, never as axioms. Every formalized result depends only on Lean's three standard axioms (propext, Classical.choice, Quot.sound). The code is at https://github.com/vaidmanworks/two-block-collatz-lean, where an automatic build compiles the proofs from scratch and checks the axioms on every change. A snapshot of the code is attached to this record.