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

An extension to baker cycles showing two parity words X and Y are effectively X^k Y^l (k, l ≥ 1). This is the parity vector of a non-trivial positive integer cycle, for the pair's 2×2 minor is ±(a power of 2 times a power of 3). This gives an explicit family for every pair of Farey parents on the type of log₂ 3. This includes families such as Steiner's circuits and Mimuro's one-run family. Sections 1–5, Section 6 up to Theorem 6.5, and Section 7 up to Theorm 7.4 are formally verified in Lean 4 with Mathlib. 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. A snapshot of the code is attached to this record.File is currently restricted due to issues in the PDF, lean remains working and is available in the git files.