Fibre stabilizers and a mod-8 obstruction for Legendre pairs

We give a fibre-stabilizer formulation of order-six multiplier obstructions for Legendre pairs. Let q be prime with q ≡ 1 (mod 12). We exclude Legendre pairs of length 9q whose rows are each invariant, without translation, under a multiplier congruent to 4 or 7 modulo 9 and of multiplicative order six modulo q; the two multipliers may differ. After normalizing the row sums to 1 and compressing to length nine, the three fixed-fibre actions force the shift-one autocorrelation of each compressed row to be 5 modulo 8, contradicting the compressed pair equation. The argument reformulates earlier mod-8 and mod-24 obstructions and recovers their length-333 exclusions. A Lean 4 development formalizes the cyclic theorem and its supporting results. The supplement contains the manuscript and Lean proof sources, claim map, dependency pins and reproduction instructions. Article text and prose documentation are licensed under CC BY 4.0; original Lean, Python, C++ and reusable TeX sources are under MIT. See LICENSES.md for the full allocation and third-party terms. Use of generative AI. OpenAI's ChatGPT and Codex were used in developing the mathematics, writing and checking the programs, and preparing the text. Anthropic's Claude also provided review feedback. The author is responsible for the mathematical statements, computations and references.