Multiplier obstructions for Legendre pairs of length 9p

A Legendre pair of odd length n consists of two ±1 sequences whose periodic autocorrelations sum to −2 at every nonzero shift; it gives a Hadamard matrix of order 2n + 2. Searches for such pairs often assume that a group of multipliers fixes both sequences. We show that at length 9p, for an odd prime p ≠ 3, such a group must be small: if it has odd order h ≥ 19 and its multipliers are congruent to 1 modulo 9, then p ≥ 6h² − 4h + 1. A first-moment argument gives only p ≥ h(h − 1)/2 + 1. The proof compresses the pair to length nine. Each compressed sequence is Z + 2hY, where the sequences Z form a Legendre pair of length nine and the integer residuals Y have sum zero. A variance bound shows that small residuals would have constant combined autocorrelation off the zero shift. A divisibility theorem for pairs of integer sequences of length nine, which follows from a lemma of Arasu and Xiang and a lemma of Ma, rules this out. Integer solutions at p = 6h² + 1 show that the leading coefficient six is the best that the compressed pair equation alone can give. We also show that no Legendre pair of length 279 has both sequences fixed by the multiplier 64, and we prove an analogous bound at lengths ℓ²p for primes ℓ ≡ 3 (mod 4) when h exceeds an explicit threshold. All numbered results are also proved in Lean 4. This record holds the article and its source archive, supplement.zip. The source archive contains the manuscript and bibliography; the Lean proofs, with files that state each final theorem with no proof inside; the claim map, which gives each of the eight claims with its hypotheses, status and limits; the pinned versions of the formal tools and the replay commands; the record and receipt of a passing formal replay; and a check script. The replay compiled the first-party Lean modules afresh, audited their axioms, replayed them in the Lean kernel and checked the exported dependencies with the independent Lean proof checker nanoda. The check script uses only the Python 3 standard library and covers finite arithmetic and source consistency, not a fresh formal replay. The article and its LaTeX source, the documentation and the data files are licensed under CC BY 4.0, and the programs and the Lean development under the MIT License; LICENSES.md assigns each file. Cited works, Lean, Mathlib, lean4export and nanoda keep their own terms and are not included. The PDF embeds subsets of the Latin Modern fonts (GUST Font License) and the AMS fonts (SIL Open Font License), which keep their own terms. Use of generative AI. Generative AI tools, including ChatGPT, Codex and Claude, assisted with the mathematics, proofs, programs and text. The author is responsible for all content.