Multiplier and reflection obstructions for Legendre pairs of length 9p with prescribed 9-compression

A binary Legendre pair of odd length n consists of two ±1 sequences whose periodic autocorrelations add to −2 at every nonzero shift. Kotsireas conjectured that for every odd prime p there is a Legendre pair of length 9p whose two compressions to length p are δ + 3χ and δ − 3χ, where χ is the quadratic character modulo p and δ the indicator of zero. For p ≠ 3 we prove restrictions on such pairs that have additional structure. We give a field-descent criterion under which a group of multipliers acting on the p-coordinate alone that fixes one row must also fix the other. With it we show that at length 261 a row cannot have an affine symmetry of order seven and, with a norm equation in a CM field, that at length 333 it cannot be fixed by the subgroup of order nine of these multipliers, whatever the other row is. Pairs with both rows fixed by the subgroup of index six of the multipliers that act on the p-coordinate alone exist exactly for p = 7 and 13. For p ≡ 3 (mod 4) the reflection of the p-coordinate exchanges the two compressions. If one row is the reflection of the other outside at most one of the p columns, then 9p + 1 = u² − uv + v² for integers u, v, which fails for almost all such primes. Further results treat two exceptional columns and several individual lengths. Of the 55 numbered results, 42 have Lean 4 proofs with Mathlib, checked by the Lean kernel and by the independent checker nanoda. These include the field-descent criterion, the exclusion at length 333, the norm condition with its density statement, the exclusions of that two-column case at lengths 63, 171 and 279, the dyadic identity with its four families, the recognition results at lengths 153 and 261, and the rank-one obstruction at length 117. Another 11 have written proofs with exact programs or searches and count as computer evidence, not formal proofs. These include the exclusions at length 261, the one-column result at lengths 171 and 207, and the exclusion of the two-column case at length 207. The remaining two are proved in the text with external dependencies. The index-six theorem uses Theorem 1.2 of the article Multiplier obstructions for Legendre pairs of length 9p at p = 31, and its case p = 19 rests on computer evidence. A proposition on the released control pairs at length 63 and the prescribed pairs at length 99 states its clause at 99 under the hypothesis that those pairs form one orbit, the conclusion of the released exhaustive search at length 99, which is not rerun here. This record holds the article and its source archive. The source archive contains the LaTeX source; the data, with witnesses, factor certificates and finite records compared with the replay outputs; the replay programs; the Lean sources, with their pinned replay profile, component map, replay runner and the receipt of the passing replay, which states its scope; the native entry points and the three-word search programs for length 153; the README, which gives each replay command, its source and data locators, controls and recorded cost; and PUBLIC_MANIFEST.json, which pins code and data from one source version. The command in the README authenticates those bytes and runs the routine check. That check reruns all declared finite censuses except two: the compiled three-word search at length 153, whose two runs have their own records, and the traversal of the empty closed balls for multiplier 233 at length 261, which a separate full replay performs. The Lean replay is also a separate command. The article and its LaTeX source, the README and other prose documentation, and the data are licensed under CC BY 4.0. The programs, settings and checker data, the two TeX support files, and the Lean sources and records are licensed under the MIT License. Reused material and the fonts embedded in the PDF keep their own terms, as LICENSES.md states. 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.