Sparse primes for fixed compressions of Legendre pairs, and feasible low-degree relaxations

A Legendre pair of odd length n consists of two ±1 sequences whose periodic autocorrelations add to −2 at every nonzero shift. At a length mp, with p prime, we ask which compressions of the two sequences to length m can occur as p varies. For fixed odd m > 1, a fixed compression to length m occurs for at most O(X/(log X)^(3/2)) primes p ≤ X. The proof turns the fixed compression into a relative norm equation in a cyclotomic field and sieves the primes. As consequences, for almost all p, both compressions to length m of every Legendre pair of length mp have an entry of absolute value larger than a fixed small power of log p, and every group of multipliers congruent to 1 modulo m that fixes one of its sequences has order O(√p). For compressions to length nine we decide when a pair of symmetric integer sequences can have the same combined spectrum, and we count such pairs. Separately, at every odd length we construct a degree-five Sherali–Adams functional for the Legendre-pair equations whose degree-four part is a sum-of-squares functional, so neither relaxation certifies nonexistence. At length 117 the relaxations remain feasible with the two compressions to length 13 prescribed by Kotsireas, Gómez and Gómez-Pérez, and they do not force the symmetry under multiplication by 64 that the known pair with these compressions has. The arithmetic results restrict compressions and symmetries; they exclude no Legendre-pair length. This record holds the article and its source archive. The source archive contains the manuscript, the claim map, the length-117 witness, the Lean sources with a command that compiles them from a clean state and replays every proof in the Lean kernel and in the independent checker nanoda, the receipt of a passing replay, and Python and C++ checks using exact integer and rational arithmetic. Every numbered theorem, lemma, proposition, corollary and remark is also proved in Lean 4 with Mathlib, with one exception: Corollary 4.3 is proved for rows on Z/mZ × Z/pZ, and its identification with the cyclic statement by the Chinese remainder isomorphism is formalized only for m = 9. The receipt states what the replay trusts, and the finite checks do not prove the unbounded assertions. The article and its LaTeX source, the README and other prose documentation, the data and the replay receipt are licensed under CC BY 4.0. The programs with their claim map and build entry point, the Lean sources, the replay profile, the component map and the two Lean runners (the version that produced the replay receipt and the later shared runner) are licensed under the MIT License, except 23 Lean files adapted from PrimeNumberTheoremAnd and the module-replay body that the later runner embeds from Lean, which are licensed under Apache-2.0, as LICENSES.md states. The fonts embedded in the PDF and the cited works 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.