A prime-square multiplier obstruction for Legendre pairs: verification package

Abstract

This record accompanies A prime-square multiplier obstruction for Legendre pairs, version 1.3.0. A Legendre pair consists of two cyclic sign sequences whose periodic autocorrelations sum to −2 at every nonzero shift. For odd length n = p²q, where p is an odd prime and q is a positive integer, neither row of a Legendre pair can be invariant under i ↦ (1 + pq)i + c, for any offset c modulo n. No symmetry is required of the companion row. A short odd-cycle argument gives individually sharp autocorrelation bounds, including for sequences of sum 1. The general direct obstruction was previously stated publicly under the GitHub handle byclaude. This note supplies a self-contained proof with sharp bounds, derives the affine consequence, and provides formal verification. Applications include lengths 117 and 333. The result excludes specified symmetries; it neither decides existence of Legendre pairs at length 333 nor refutes the prescribed-compression conjecture. Version 1.3.0 revises the exposition, attribution, and explanation of scope. The mathematical statements and Lean proofs are unchanged from version 1.2.0. Files include the article PDF, reader package, formal-verification package, arXiv source archive, and build record. The accompanying Lean 4 development formally verifies every original mathematical result stated in the article. Literature priority and the cited subgroup-table transcription remain outside that verification. The article discloses generative-AI use. Licensing is file-class specific: article and documentation under CC BY 4.0; original executable, build, and verification material under MIT. Factual and third-party material is not relicensed. See the packages’ license map.