δ* Proximity Prize — research coordination and verified state

[lalalune]

This is the coordination thread for the machine-checked δ* / smooth-domain Reed–Solomon proximity-prize campaign.

Current verified state (2026-07-10): the production conjecture is still open. Exact toy/deep-rung pins, threshold-ledger reductions, and a large no-go map are formalized, but no theorem yet supplies the required production square-root cancellation. After G73, the signed cross-cell relationAnomaly route is the sole unclosed off-BGK route; otherwise the core is ON-BGK/Paley.

Control plane:

• Canonical tracker: Prove δ* — complete research dossier (v3) for the RS proximity-gap prize (successor to #464) #466
• Live CORE task: δ* CORE: bound the single-embedding first-incidence weighted relation discrepancy #505
• State/documentation integrity: δ* campaign: refresh canonical state, residual census, and branch-local guide #506
• Final completion/audit gate: δ* completion gate: production theorem assembly and independent axiom audit #507
• Structural branch split: Cleanup master plan: full fork assessment — slop removal, prize-research isolation, and the road to an upstream PR #499
• Project board: δ* Proximity Prize

Branch contract: all campaign work lands on research/proximity-prize; never merge that branch into main. Every claimed advance must be axiom-clean Lean or a reproducible probe. Refutations belong in DISPROOF_LOG.md. A conditional theorem, renamed open Prop, bracket, or toy pin is not prize completion.

Use this discussion for mathematical proposals, literature leads, and independent review. Use the linked issues for executable work and verified acceptance criteria.

[lalalune]

#505 frontier narrowed from current Lean evidence

The live signed route cannot use four tempting mechanisms: R382 proves rotation-orbit sums are sign-coherent; R384 proves primitive-generator averaging has exactly no quantitative gain; R385 proves cross-generator covariance ignores the unique-root stratum; G75 proves raw Wick-deviation sign is the wrong centered test and identifies the exact DC allowance.

Accordingly #505 now accepts only a first-incidence weighted bound across genuinely distinct relation orbits, or a theorem proving that this remaining formulation is itself equivalent to the BGK/Paley wall. This prevents another wrapper/averaging cycle from being misreported as progress.

[lalalune]

Verified G76 / OC-EQUI update

540f6b5151 closes two proposed refinements of the signed route. Full Galois-stable pools are exactly equidistributed over primitive embeddings, so total transversal coverage is only an embedding-count multiple of the one-embedding census. Independently, all distinct-generator factorial moments of order at least two lose the Z=1 stratum and cannot reconstruct the centered coefficient.

Both results compile axiom-clean ([propext]), and the exact enumeration probe passes. The live question is therefore narrower: control the single-embedding, first-incidence weighted discrepancy across distinct relation orbits at production depth. Issue #505 has been renamed and rewritten around that exact target. δ* remains open.

[lalalune]

Frontier update through 85a7f074f0: G80Z completes the arithmetic character-bias → arc-deviation consumer; G83 proves the exact determinant half-height fence; G84S supplies the canonical core/padding slot equivalence for corrected decoder assembly. These are axiom-clean reductions, not prize closure. The production theorem remains OPEN / ON-BGK. Live obligations are (1) a genuinely non-Fourier arc anti-concentration certificate or equivalent single-embedding discrepancy bound, (2) the concrete cyclotomic determinant/divisibility/Hadamard instantiation, and (3) decoder surjectivity plus primitive-core counting.

[lalalune]

Milestone update: the finite factorial-corrected decoder is now complete through weighted collision-sector counting (G86–G90), and the authoritative remote discharges production maximal-cancellation depth three. Adaptive all-depth Wick allocation is also formalized, so the first decoder-side open production depth is four. G89 also rewrites the weighted shadow anomaly exactly as a raw-word single-embedding collision discrepancy. None of these bounds that discrepancy or supplies the non-Fourier pointwise arc/dilation estimate; production δ* remains OPEN / ON-BGK.

[lalalune]

Current verified frontier (bcb4956457): production depth three is discharged; depth four is reduced exactly to the HBK-scale bound (rEnergy G 2)^2 ≤ 128|G|^5. Raw all-depth cardinality caps are impossible, so centered relation-weighted masses are essential. The first-incidence functional equals the wall exactly, and unsigned sup-arc uniformity has an n^(2/3) cost floor. G80S instead reduces same-arc pairs to directional centered-strip concentration for shifted-subgroup dilates; G91 gives the exact maximal-cancellation bag/stabilizer decomposition. These are reductions/no-go maps, not the missing signed pointwise estimate. Production δ* remains OPEN / ON-BGK.