Cubic observations for four-point convolution reconstruction: universal two-coordinate bound and Lean proof archive

UNREVIEWED RESEARCH AND LEAN PROOF ARCHIVE. For every four-point support S in a finite cyclic group, the complete labelled ordered-convolution square determines a fibre of candidates. This archive proves that at most two fixed labelled coefficients of the ordered convolution cube separate that entire fibre. The two-coordinate worst-case bound is attained in C8. Pairs and triples are ordered, diagonals are included, labels are retained, and candidates are not identified up to affine transformations. The cost is the number of exact integer coefficient queries after the fibre is available; it excludes computing the fibre, selecting probes and acquiring samples. An integer response is not a binary membership answer. The proof combines joint square–cube injectivity for arbitrary complex cyclic functions, the actual rectangular structure of four-candidate support fibres, and separation of an injective real parallelogram by at most two coordinates. Cubic injectivity on the square fibre is proved through Fourier, rather than assumed. Six new Lean modules contain 26 theorems and eight definitions. The historical local Lean 4.29.0 reception records 301 audited declarations and 37 recompiled proof modules, with standard axioms only. It is not an official CI receipt. The 113-file archive includes the earlier written notes, all six new modules, all 31 baseline modules copied with exact lock matches from the public reconstruction deposit, raw historical logs, a C8 necessity witness, rejection tests and fresh publication checks. The previously private baseline source imports are now supplied directly. External Lean and Mathlib dependencies remain version-pinned. Fresh checks: all 38 locked source files and the archived 301-root axiom output match; all 37 module logs were inspected; eight audit-verifier tests pass; 15664 finite parallelograms and the complete C8 witness were recalculated; 1143 finite checks of the explicit odd-power family passed. No new Lean compilation or official CI execution occurred during publication. The earlier exhaustive C4..C48 campaign and negative Lean rejection are preserved as historical evidence, without a new replay. This supplements the reconstruction archive 10.5281/zenodo.23981750 and connects to the unified manuscript 10.5281/zenodo.23981308. Earlier notes retain their dated unformalised status; the later formal dossier supplies the subsequent proof. The uncompiled DecisionInterface.lean in the unified manuscript is a distinct file. No novelty or priority is established, and no independent human peer review is claimed. Exact identifiability does not establish noise robustness, sampling complexity, physical entanglement, an economic advantage or an FCI benefit. Substantial AI assistance was used. Rights: no new blanket reuse licence; existing explicit notices retain their scope. See README.txt.