Uniqueness of the Legendre pair of length 117 with prescribed 9-compression and multiplier 64

We classify the Legendre pairs of length 117 whose two rows are fixed by multiplication by 64 and whose 9-compression is (δ + 3χ13, δ − 3χ13). Here χ13 is the quadratic character modulo 13, with value 0 at zero, and δ is the indicator of zero. There are exactly 5832 ordered pairs in this family. They form one orbit under the group of order 11 664 of equivalences that preserve the 9-compression, and each pair has a stabilizer of order 2. We display one pair and verify its Legendre equations from 35 pairs of autocorrelation values. This establishes the (p, q) = (13, 3) case of Kotsireas's prescribed-compression conjecture and gives a Hadamard matrix of order 236. The classification reduces to 356 classes of integer 3-compressions and an exhaustive enumeration of their ±1 decompressions, carried out by two separately written programs. The proofs are verified in Lean, with the enumeration (C1) as the only hypothesis of the classification. Pairs with this 9-compression but without this symmetry are not classified. The source archive contains the pair, the 356 class representatives, the census and enumeration programs with the recorded outputs and receipts of both enumerations, the programs that check them, the Lean development and the LaTeX source. Its README gives a command for each check; verification/check_witnesses.py checks the pair in under a second with Python alone. The article and data are licensed under CC BY 4.0; the programs and the Lean development are licensed under MIT, as LICENSES.md in the archive states. Use of generative AI. OpenAI's ChatGPT and Codex, together with Anthropic's Claude, were used in developing the mathematics, writing and checking the programs and the Lean proofs, and preparing the text. The author is responsible for the mathematical statements, computations and references. Version 1.2.0. New title. Versions 1.0.0 and 1.1.0, titled An explicit prescribed Legendre pair of length 117, gave the pair without classifying the family; this version proves the classification.