An explicit prescribed Legendre pair of length 117

A Legendre pair consists of two cyclic sign sequences whose periodic autocorrelations sum to −2 at every nonzero shift. An explicit pair of length 117 is constructed whose sums over equal residues modulo 13 are 1 at residue zero and respectively 3χ(r) and −3χ(r) elsewhere, where χ is the quadratic character modulo 13. This verifies one case of Kotsireas’s prescribed lifting conjecture, without establishing the general conjecture or classifying all lifts. Both sequences are fixed by an involution that reflects one Chinese remainder coordinate. A short correlation table proves the pair identities and gives a Hadamard matrix of order 236. An accompanying Lean 4 development formally verifies every original mathematical result stated in this article. The code checks the construction and reproduces the search from the successful length-39 compressed pair. Contents (version 1.0.0). The ZIP contains the article PDF, a reader package with the manuscript and verification instructions, the formal verification package, arXiv source, and the release build record. The supplied programs reproduce the displayed pair from the successful parent; their reported counts are for that lift, not an exhaustive classification of binary lifts. Licensing. The article and explanatory text are licensed under Creative Commons Attribution 4.0 International (CC BY 4.0). Original code and Lean sources are licensed under the MIT License. See the included LICENSES.md files for the exact allocation and retained notices. Use of generative AI. OpenAI’s ChatGPT and Codex were used in developing the construction, writing and checking the programs, and preparing the text. The author is responsible for the mathematical statements, computations, and references.