Prove δ* — complete research dossier for the RS proximity-gap prize (successor to #407)

[lalalune]

🔁 CLOSED — continued in #464

This issue has been superseded by a fresh consolidated dossier: #464 — Prove δ* — complete research dossier (v2).

#464 folds in everything from this thread (all 1,190 comments) plus the predecessors (#407/#389/#371/#357/#334/#232), the in-tree substrate, the external number-theory literature, and the post-2026-06-17 synthesis (the Shaw value, the Arithmetic Uncertainty Principle, the Wraparound Variance Law, the Jacobi-turnover tool, bad-prime localization). It states all open angles/directions, all unexplored math, the full closed/no-go ledger, every discovery and first, and the complete substrate context for continuing the δ* work.

Canonical in-tree copy: docs/kb/deltastar-DOSSIER-v2-2026-06-22.md.

➡️ Post new findings and continue the work in #464. The body below is the prior (frozen) dossier, retained for history.

---

Prove δ* — complete research dossier for the RS proximity-gap prize (working successor to #407)

📋 Consolidated digest — comments folded as of 2026-06-16T19:30Z (384 comments → this body; incl. the DECISIVE ON-BGK verdict). This body is the single current source of truth: §0.0 the ON-BGK verdict, §5 landed, §6 LIVE open paths, §7 out-of-regime candidates, §8 dead/refuted ledger (with where each failed), §11 audit. Post new findings as comments; folded next pass.

This is the canonical, self-contained account of the Grand Proximity Prize (proximityprize.org; companion Open Problems in List Decoding and Correlated Agreement, Arnon–Boneh–Chen–Fenzi–… 2026 = ePrint 2026/680, "ABF26"). It consolidates the #407 campaign (348 comments) + this issue's 359-comment multi-agent grind + the KB dossiers + every probe/brick. Start here. #389/#371/#357/#334/#232 are archival predecessors.

Mission. Pin δ* — the mutual-correlated-agreement (= list-decoding) threshold — for explicit smooth-domain Reed–Solomon codes in the window interior (1−√ρ, 1−ρ−Θ(1/log n)), worst-case, with a closed proof (reducing only to known-proven math). This solves both grand challenges (Grand-MCA and Grand-list-decoding; one threshold). Honesty contract: axiom-clean Lean (#print axioms ⊆ {propext, Classical.choice, Quot.sound}, 0 sorryAx) per declaration, or reproducible probes only; refutations → DISPROOF_LOG.md; never fabricate closure; the core is a recognized open problem.

---

⭐ 2026-06-17 (late) — comprehensive re-mine of all 570 comments (1219 findings): dossier confirmed current; the genuinely-new verified items

A full structured fan-out over all 570 comments (1219 deduped findings: 648 landed-substrate, 120 open-frontier, 117 refuted, 116 external-lit, 74 corrections) confirms the picture below is current and accurate. Genuinely-new/updated verified items folded here:

• ★ I031 ↔ Solve the Grand Proximity Prize directly: pin δ* in the prize regime (successor to #389) #407 reduction arc (REAL, axiom-clean, verified): Frontier/I031MFromConstantIndexConjecture.i031_M_le_logTarget_of_constantIndexConjecture (sorry:0; commits 888952d03/89c3fdeb2/7b4824b8a) — the prize object M(μ_n) ≤ √(2n·log(q/n)) now follows from the Solve the Grand Proximity Prize directly: pin δ* in the prize regime (successor to #389) #407 ConstantIndexSubGaussianPeriodBound conjecture, and the I031 union-bound Prop and the Solve the Grand Proximity Prize directly: pin δ* in the prize regime (successor to #389) #407 pointwise period bound are proven to deliver the same prize-target through one chain. NOT a closure — ConstantIndexSubGaussianPeriodBound IS the BGK/Lamzouri wall (a Prop, never asserted). A clean unification of two named-open objects onto the wall.
• ⚖️ The LIVE empirical tension — does K_eff saturate or creep? K_eff(n) := (E_r/Wick)^{1/r} at the optimal depth, β=4: one measurement (O506) finds it creeping up 0.608→0.625→0.675 (n=32→64→128, peak-r marching 12→14→18 toward r≈89) — prize-threatening if it crosses; the newest (NubsCarson, n=256) finds it saturating ≈0.67 (plateau, energy/moment route tight ~9% loss) — floor-favorable. This is the decisive compute-bound question (does the char-p energy ratio stay bounded to r≈ln q at n=2³⁰, or creep past?), and it sits exactly at the edge of feasibility (n=256). The char-0 anchor is decisive downward (K_eff→1 from below, a_r≤1 Lam–Leung); the open part is the char-p deep-r creep — i.e. the wall, now with mixed-but-mostly-favorable n≤256 evidence.
• di-Benedetto beat refinement (O267): the beat (0.9583) is good-prime-conditional — the all-n No-Excess at the prize prime does NOT follow from Lam–Leung (the bad-prime ceiling is exponential ~6^{n/2}), confirming the "good-prime-only at char-p" verdict.
• External confirmation (IDX=102): comprehensive Burgess-crossing / Bourgain-arsenal research (13 facets) — NO crossing of the Burgess barrier at n=p^{1/4}, NO Bourgain technique transfers; the Burgess exponent is exactly 1 at β=4 (structural). The wall is "the unfinished part of Bourgain's program." Independent confirmation the external input does not exist.
• ⚠️ S1/S6 "most hopeful" bricks flagged PHANTOM (see §11): lalalune's "prize reduced by two axiom-clean theorems" (prize_of_transfer_slack, the S6 bounded-Betti Deligne brick) are not on any branch; the S1 reduction's math is sound but is the wall re-framed; the S6 Deligne avenue is refuted on the math (μ_n-subgroup trap — §11).

⭐ 2026-06-17 UPDATE — two distinct targets: protocol SOUNDNESS above Johnson is now RESOLVED (ePrint 2026/858); δ* / the proximity gap is still OPEN

A real, verified paper changes the protocol landscape while leaving this issue's δ* mission open. ePrint 2026/858 (Chai–Fan, IoTeX, "FRI Soundness Above the Johnson Bound via Threshold Halving", Apr 2026; PDF read in full, 48pp) proves the first UNCONDITIONAL soundness theorem above Johnson for FRI/STIR/WHIR on deployed plain RS: for every δ∈(δ_J,1−ρ), ε_FRI ≤ nR/|F| + (1−δ/2)^q.

• Mechanism = threshold halving (RVW13): analyze soundness at the halved radius δ/2. For the whole open window δ/2 < (1−ρ)/2 < δ_J, so the round-1 fold is in the unique-decoding regime where BCIKS 2025 proves the proximity gap unconditionally. Verified valid (δ-far ⟹ δ/2-far ⟹ BCIKS@δ/2 preserves ⟹ rejection ≥1−(1−δ/2)^q). Cost: a ~2× query overhead, proven optimal within the CA framework. Their half-threshold CA core is Lean-verified (zero sorry) in their repo.
• ⚠️ It does NOT pin δ* — and the paper says so. Its own claim map (§1.9): "does not claim the original zero-loss proximity gap"; "Original up-to-capacity MCA / zero-loss proximity gap: Not solved here." OP1 (zero-loss CA) "resolved within CA framework" but vacuous at FRI scale (C(n,w)/|F|); OP2 deployment regime (c≥3) is Conjecture 41, open; the M=0 form refuted. Threshold halving sidesteps δ* (gives soundness regardless of where δ* sits, at 2× cost); it does not determine the MCA threshold.

⟹ Split the goal cleanly: (A) protocol soundness above Johnson = RESOLVED unconditionally (2026/858, 2× query cost); (B) δ* / the zero-loss correlated-agreement / MCA proximity gap = STILL OPEN = this dossier's mission = the BGK/Paley wall (§0.0 below). (A claimed "prize pinned unconditionally" reading of 2026/858 conflates A with B; corrected — comment 4726439961. The cited writeup prize-RESOLVED-threshold-halving-2026-858.md is not in the tree.)

⭐ 2026-06-16 (late) MAJOR UPDATE — the (δ*/zero-loss) prize is ON-BGK; the wall is real and two-sided (read this first)

A 359-comment fan-out + a ~95-brick formal campaign reconciled the long-running on/off-BGK tension and concluded the prize is ON-BGK (the wall is real). The "off-BGK combinatorial escape" hope of the previous fold is closed:

(0) ★ DECISIVE: the prize is ON-BGK — every off-BGK route refuted/capped (axiom-clean)

The contested on/off-BGK pieces are now reconciled — all three are right, and they compose to "the wall is real":
(Provenance flag: the 17:00 verdict comment cited several brick names that are NOT in the tree/any branch — _DstarGrowthLaw, _OPSingleOrbit, _DyadicRecursionDstar, PrizeEquivalencePin, FloorResonanceEnergyBridge are PHANTOM, see §11. The conclusion rests only on the VERIFIED bricks named here + standing numeric facts.)

• The over-determined distinct-γ count D* is p-independent as a char-0 census (D*(16,3)=97) — BUT super-budget inside the window: the over-det closed form OverdetIncidenceMaxClosedForm = 2m³−2m²+1 = Θ(n³) (REAL, in-tree) overshoots budget n by Θ(n²) (≈10¹⁶ at n=2³⁰). So the over-det contribution collapses to Johnson (the specific dStar3_gt_budget axiom-clean brick claimed for this is phantom; the Θ(n³) fact itself is real), forcing the window-interior δ* onto the under-determined char-sum M(n) ≤ C√(n log m) = BGK.
• No off-BGK escape: the complete-homogeneous count is super-polynomial (KambireDeepBandFloor.two_pow_le_multichoose_deep_band + KambireExponentialGap, REAL: multichoose s s ≥ 2^{s−1}), so the char-free F6 lower bound at its cliff M_cross=n/4 is Johnson-side — the char-free floor does NOT reach the window interior. (The single-orbit O_P=1 and dyadic-recursion escapes were also refuted, but numerically; their cited Lean bricks are phantom.)
• The decisive mechanism (numeric/conceptual): binding-count = (char-0 distinct count) − (mod-p collision defect); the ONLY way δ* enters the window interior is the mod-p defect = BGK char-sum cancellation (confirmed p-dependent). ⟹ prize is ON-BGK.
• Two-sided & tight (REAL bricks): _EnergyRatioMonotoneReduction proves ERM-at-r ⟺ max_c‖η_c‖² ≤ (2r+1)·n, so the energy route at prize depth r≈ln q is literally the BGK sup-norm bound (floor lower-bound = moment upper-bound, one object). Method-necessity is _MomentLadderExceedsPrize.moment_ladder_exceeds_prize (no second-order route at any depth).

THE SINGLE OPEN CORE (everything funnels here, proven two-sided): EnergyRatioGrowth at r≈log m ⟺ char-p transfer of Lam–Leung E_r(μ_n) ≤ (2r−1)‼·n^r to r≈ln q≈89 ⟺ M(μ_n) ≤ C√(n log m). Proven char-0 (all r); numerically verified for n≲40 (all accessible r); OPEN at n=2³⁰ = the BGK/Paley √-cancellation at the Burgess barrier (25-year-open analytic NT). Mildly favorable to the floor being TRUE: the char-0 anchor K_eff(n)→1 strictly from below (gap 1/n), and a_r ≤ 1 is a Lam–Leung theorem; the prize can fail only via a char-p DC-defect at deep r.

The earlier-fold framing — "(B) the true open core is now p-INDEPENDENT and combinatorial, more hopeful than BGK" — is therefore RETRACTED: the p-independent over-det object is real but super-budget (→ Johnson), and the window-interior δ* is governed by the p-dependent BGK char-sum. Docs: deltastar-444-onBGK-vs-offBGK-2026-06-16.md, deltastar-444-concrete-rungs-2026-06-16.md.

The supporting corrections since the last fold:

(1) ⚠️ "prize ⟺ BCHKS Conjecture 1.12 (tight)" is RETRACTED — the in-tree Prop is FALSE/vacuous

The earlier headline (commit 1c1712743, "prize ⟺ BCHKS proven TIGHT") was self-corrected by commit e56715bf0 and KB doc deltastar-444-BCHKS-correct-object-and-attack-2026-06-16.md. The in-tree BCHKS1_12 Prop states ∃ r ≤ c·log s, |Σ_r(μ_s)| ≤ budget≈s, where Σ_r is the distinct r-fold subset-sum count. This is FALSE: exact computation (probe probe_subsetsum_grows_refutes_bchks.py, independently re-run) shows |Σ_r| grows monotonically and is always ≫ budget:

• n=s=8: |Σ_r| = 33, 96, 225, 456, 833, 1408, 2241 (r=2..8) — never ≤ 8.
• n=s=16: |Σ_r| = 129, 704, 2945, 10128, 29953, 78592, 185617 — never ≤ 16.

So the ∃ m, BCHKSBudget hypothesis is unsatisfiable, and prize_reduces_to_BCHKS is vacuously true on a false hypothesis — it proves nothing about the prize. The mis-statement put the sumset |H^{(+r)}| = |Σ_r| (a budget multiplier) on the wrong side of the inequality.

(2) The CORRECT floor — Sumset-Extremality (ABF26 §4), with a char-free leading order

|F| is taken LARGE (not fixed at n·2^128); soundness error is #bad/|F|, and δ* is the radius where #bad crosses from poly(n) to super-poly. The open floor:

Sumset-Extremality. For every affine line (f,g) and every δ below threshold, #{λ : Δ(f+λg, C) ≤ δ} ≤ poly(n)·|H^{(+r)}|, with r the ⌊δn⌋-related depth.

The new, more-attackable decomposition (re-targets the proof — this is the current frontier):

• (a) CHAR-FREE leading order [the bulk — most landable]. The worst CHAR-FREE direction is complete-homogeneous, count h_j = C(s+r−1, r), NOT the subset-sum ceiling e_j = C(s,r) (which is not tight: log(h_j/e_j)/s → 0.26, a strictly larger leading exponent). The poly/super-poly crossing of poly(n)·C(s+r−1,r) vs ε*·|F| gives the leading δ*. In-tree pieces: SchurLagrangeBridge (dividedDifferencePow_eq_schurH), _CoreA5.monomial_dir_maximizes_overdet (worst direction is monomial), forced-γ count per (k+1)-subset = h_{a−k}(R).
• (b) GOOD-PRIME existence [Linnik]. A prime where the r-sums are distinct mod p (giving polynomially-many distinct λ); bad primes divide Res(Φ_s, ΣXⁱ−ΣXʲ) (≤ log₄ s per pair). Reduces to quantitative Linnik / effective Chebotarev (the Spur_r(p) count, _AvW2).
• (c) CHAR-p ANOMALY [exponent-0, the irreducible BGK residual]. E_r(μ_n) ≤ (2r−1)‼·n^r transferred to char-p at r≈log q. char-0 PROVEN (Lam–Leung structural; E_2..E_7 exact in-tree); char-p excess W_r=0 for p > onset-threshold(r) (VERIFIED r≤4 at prize scale). Does not move the leading δ*, but is needed for the exact constant — and at depth r≈log q≈89 it IS the BGK wall.

So: exact δ* = char-free complete-homogeneous crossing (provable bulk) + Linnik good-prime (effective PNT) + char-p exponent-0 anomaly (deep-r energy transfer = the genuine open residual). The leading order is char-free and attackable; the wall is the sub-leading exact-constant correction.

This re-targeting is FORMALIZED (commit 479bbe5af): _BchksF3_RetargetedReduction.prize_reduces_to_SumsetExtremality derives the window-interior from one open Prop SumsetExtremality (+ subsetSumBudget_unsat); _BchksF6_ExplicitDeltaStarLower.explicit_deltaStar_lower_bound lands the explicit char-free δ* lower bound modulo three named residuals. ⚠️ But (per §0.0) the char-free leading order does NOT reach the prize: the complete-homogeneous count is super-polynomial (O234/O235) and the F6 lower bound at its cliff M_cross=n/4 is Johnson-side — it reproduces the proxy. So the residual that actually decides the window interior is (c), the char-p excess = the BGK wall (§6.1). The Sumset-Extremality reduction is a correct, tighter bookkeeping of the same wall, not an escape from it.

(3) The over-det distinct-γ count is p-INDEPENDENT but SUPER-BUDGET (→ Johnson; not the prize)

The over-determined distinct-γ far-line count D*(m) = |⋃_R {γ_R}| is a p-independent char-0 census (verified identical across primes p > n⁴, n=8–64; ResolveFieldIndependent). But it is Θ(n³) ≫ budget n (_DstarGrowthLaw.dStar3_gt_budget), so it collapses δ* to Johnson and does NOT govern the window interior. The window-interior δ* is forced onto the p-DEPENDENT under-determined char-sum (BGK), via the mod-p collision defect (§0.0). The p-independence is real and was a genuine discovery, but it is the easy (proxy) part; the hard part is the p-dependent BGK cancellation that drags the count to budget.

(4) SOTA IMPROVED + the di Benedetto T₃ conditional DISCHARGED at prize scale

Specializing di Benedetto Thm 3.1 (arXiv:2003.06165) to μ_n with Sidon-floor energies T_2=3n²−3n, T_3=15n³−45n²+40n=O(n³) gives H_exp=7, hence max_a|Σ_{x∈μ_n} e_p(ax)| ≪ |H|^{1−1/24} p^{1/72}:

• β=4: exponent 0.9583, beating di Benedetto's generic 0.9892 (~3.9× the saving) — and the generic bound vanishes at β=4. β=5: H^{35/36} nontrivial where the generic bound vanishes. T₃ char-0 input now an UNCONDITIONAL theorem (this session, verified axiom-clean): _AvL_T3ClosedForm.rEnergy_mu_three_eq proves rEnergy(μ_{2^k},3)=15n³−45n²+40n on the actual rEnergy object — closing the "mechanical-only char-0 gap" and discharging the exactE3 hypothesis of gaussianEnergyBound_muN_three_of_exactE3. (char-p: W_3=0 for p≳n⁴, ONSET-THRESHOLD not Fermat.) The beat itself stays good-prime-restricted at char-p (W₄ dichotomy, §0.0).
• ⚠️ but the beat has a finite validity edge: the saving DIES at β = 191/40 = 4.775 (the di Benedetto Thm 3.1 β-window closes), and the 1/24 saving is UNREACHED at every finite n (the realised finite-n exponent is strictly larger). So 0.9583 is an asymptotic in-window value; honest scope: ≫ 1/2, SOTA-closeness, NOT closure (reaching 1/2 = beating the p^{1/4} prefactor = the BGK wall).

(5) ⚠️ AUDIT — verified bugs / retractions / phantom bricks (full list §11)

• The "δ* climbs to capacity / m*~log n" cascade is an ARTIFACT — RETRACTED (engine b<s direction-cap). Full-direction orbcount: far-line δ* = 1/2 + 1/n → 1/2 = Johnson, m* = n/4 − 1 (LINEAR). The far-line is a Johnson-locked Plotkin PROXY; there is no in-tree evidence the worst-case MCA δ* climbs to capacity.
• Master gap identity off-by-one FIXED: capacity − δ* = m*/n (not (m*−1)/n); δ* = 1−s/n (orbcount's 1−(s−1)/n was a display bug). _BridgeB01/B02/B04 rebuilt.
• D*(1) is p-DEPENDENT (3936@p=65537 vs 3984@p=1048609) — was laundered as p-independent; only the over-det m≥2 binding count is p-independent.
• PHANTOM bricks: _DefectOnsetOvershoot and SubsetSumThreePowExact were cited as landed but were ABSENT — since re-created with honest content under _AttackDefectOnset_EnergySandwich / _AttackThreePow_SubsetSumExact (the latter proves 3^{n/2} is an UPPER bound, not exact). ⚠️ Audit-doc over-correction caught: the audit flagged Sweep_A41…A49 as phantom, but they have since landed (dfd092069, ~1700 lines, each carrying one sorry = the named residual) — they are NOT phantom in the current tree (verify per-declaration). _AntipodalPlotkinHalfCap larp retracted. _Close27_* "decides opposite horns" = prose-only tautologies. LamLeungUnconditionalQ proves the structural foundation, not the full Wick bound (still open).

---

1. The problem — exact target & governing law

• Domain: dyadic FFT subgroup μ_n, n = 2^μ, a proper multiplicative subgroup μ_n ⊊ F_q* (n ∣ q−1).
• Prize regime: q = n^β prime, β ≈ 4–5 (the Burgess barrier), ε* = 2⁻¹²⁸, so q ≈ n·2¹²⁸ ≫ n³, budget q·ε* ≈ n, fixed index m = (q−1)/n = 2¹²⁸. THIN: n = q^{1/4..1/5}, n ≪ √q, prize n ~ 2³⁰.
• Rate ρ = k/n ∈ {1/2, 1/4, 1/8, 1/16}; window (1−√ρ, 1−ρ−Θ(1/log n)), strictly between Johnson (achievable) and capacity (proven impossible with poly soundness, ePrint 2025/2046).
• ⚠️ NEVER validate on the full group n = q−1 (special additive structure → false positives — the Cyclotomic coset-rigidity: bound #distinct e_1 over e_2=0 subsets of μ_n (the combinatorial core of the δ* prize, off the analytic wall) #400 trap). Always proper subgroups, large prime, multiple primes, exclude correlated directions X^{n/2}=±1.

Governing law (exact identity, in-tree): δ* = sup{ δ : I(δ) ≤ q·ε* }, I(δ) = max far-line incidence = max_{u₀,u₁} #{γ : u₀+γu₁ is δ-close to RS[k]}. (badScalars_eq_explainable + epsMCA = ⨆_u Pr_γ[mcaEvent] = max(#bad)/q.) Extremal lines are monomial directions (X^a, X^b) (Z/n dilation symmetry; _wf3D4 proves monomial is the unique dilation-eigenvector far direction).

Status of the endpoints: Johnson 1−√ρ achievable (ACFY24/Hab25 prove RS-MCA exactly up to Johnson); capacity 1−ρ proven impossible; KKH26/Kambiré (arXiv:2604.09724) give the CEILING δ*≤(1−ρ)−Θ(1/log n) via one bad family (easy direction, rate-locked at r=k+1) — confirming the window location but not the floor. The floor (worst-case list small for ALL words) is the open direction.

---

2. The single open core — ONE object, ~20 equivalent faces

CORE. M(n) = max_{b≢0(p)} |Σ_{x∈μ_n} e_p(bx)| ≤ C·√(n·log m), C = O(1), at p ~ 2¹⁶⁰, m = 2¹²⁸, for the binding low-exponent direction. (Per §0.0 this is both necessary and sufficient — the prize is proven two-sided onto exactly this BGK char-sum; equivalently the char-p energy E_r ≤ (2r−1)‼·n^r at r≈ln q.)

M(n) = the thin-subgroup BGK/Paley √-cancellation wall = λ₂(Cay(F_q, μ_n)) (generalized-Paley 2nd eigenvalue) = house of a degree-m algebraic integer = Gauss-period max = DFT sup-norm. Every analytic face (F1–F20) reduces here. Proven floor M ≥ √(n(q−n)/(q−1)) ≈ √n (Parseval, GaussPeriodParsevalFloor; the prize graph is NOT Ramanujan — fresh exact data §3 gives M/(2√n) = 1.34…2.43, far above 1); the ceiling M ≤ C√(n log m) is the wall.

Master reduction chain (axiom-clean): Σ_b η_b^r = q·N₀(G,r); Parseval DC-subtracted identity Σ_{b≠0}|η_b|^{2r} = p·E_r − n^{2r} (verified through r=6); dyadic split N₀(G,r)=2·N₀(H,r)+crossCell(H,ζ,r), exact crossCell(n,4)=3n²/2.

⚠️ MANDATORY FORM: raw E_r ≤ Wick = (2r−1)‼·n^r is FALSE at the prize (the DC term n^{2r}/q dominates for n≥64). Only the DC-subtracted A_r = E_r − n^{2r}/q ≤ Wick is non-vacuous (DCEnergyEssential). A_r ≤ Wick is proven char-0 for all r (Lam–Leung structural); the wall is char-p validity at depth r ≈ ln q ≈ 89.

---

3. SOTA — exactly how close, the Burgess barrier, and fresh exact data

• BGK (Bourgain–Glibichuk–Konyagin): M ≤ n^{1−o(1)}, non-effective, doesn't reach n^{1/2}.
• di Benedetto et al. (arXiv:2003.06165): generic n^{0.989}, range needs H > p^{1/4} — the prize point β=4 is exactly the Burgess barrier. ⭐ BEAT (this campaign): specializing to μ_n gives |H|^{1−1/24} p^{1/72}, β=4 exponent 0.9583 (3.9× the saving, nontrivial where generic vanishes), β=5 H^{35/36}. T₃-conditional now discharged at prize scale (§0.4). SOTA-closeness, not closure.
• Kowalski (arXiv:2401.04756, 2024): expository, re-proves the ineffective BGK n^{1−o(1)} (no rate). Best additive energy E(μ_n) ≪ n^{5/2} (Stepanov) — √-lossy. No 2023–26 paper crosses n^{0.989} → n^{1/2} at β=4 (4+ literature sweeps incl. a fresh 3-pass deep-search this fold: Shparlinski's 2024–26 list has nothing on thin 2-power-order subgroups near p^{1/4}; Alsetri–Shao arXiv:2509.07765 treats rank-2 additive GAPs not subgroups and does not break p^{1/4}; Podestá–Videla generalized-Paley spectra cover only index k≤5). The missing analytic input does not exist in the literature.
• The wall: a full half-power gap (0.989 → 0.5) at the single hardest point.
• Effective literature lever (named open input): the named hypothesis KKH26ThornerZaman.TZPrimeSupply n β supply (Thorner–Zaman effective PNT-in-APs) is the single input to close the KKH26 s=128 ceiling rows; consumer kkh26_mcaDeltaStar_le_of_TZ + concrete discharges tzPrimeSupply_{8,16,32,64,128,256}_* are in Frontier/ThornerZamanS128.lean / ThornerZamanInstance.lean (both sorry=0). The hypothesis itself is NOT Mathlib-formalizable today (needs log-free zero-density for Dirichlet L). (Earlier drafts mis-named this EffectiveTZLowerBound/effectiveTZ_to_supply — those identifiers do not exist; corrected this pass.)
• Hab25 (ePrint 2025/2110, MCA-for-RS): proves RS MCA exactly UP TO Johnson; vacuous AT Johnson — NOT a bypass.
• Chai–Fan 2026/858 (threshold halving): unconditional FRI/STIR/WHIR soundness above Johnson ε_FRI ≤ nR/|F|+(1−δ/2)^q at ~2× query cost — resolves the protocol question but sidesteps δ* (analyzes at δ/2 below Johnson); explicitly "does not claim the original zero-loss proximity gap" (§0 above). Companion 2026/861 (action-orbit) keeps δ* conjectural (Conj 41, c≥3 deployment regime open). BCIKS 2025 proves the proximity gap unconditionally below Johnson (the input threshold-halving leans on). Crites–Stewart 2025/2046 + Kambiré 2604.09724 disprove the zero-loss CA at capacity (the ceiling).

Fresh exact wall-constant data (2026-06-16, M(n)=max_{b≠0}‖η_b‖, smallest p≡1 mod n with p≥n⁴):

n	p	M(n)	M/√(n·log(p/n))	M(2n)/M(n)	M/(2√n)
8	4129	7.558	1.069	—	1.34
16	65537	13.838	1.199	1.831	1.73
32	1048609	22.983	1.260	1.660	2.03
64	16777601	38.529	1.363	1.677	2.41
128	268437889	55.064	1.276	1.429	2.43

The constant C = M/√(n·log(q/n)) is non-monotonic ≈1.07–1.36 (n=64 was a local high; n=128 pulled back to 1.28, near the Wick value ≈1.21), the doubling ratio decays toward √2, and M < √(2n ln q) throughout. Mildly favorable to a bounded C (prize-consistent) — but 5 oscillating points cannot rule out an n^{−o(1)}-slow divergence. Re-confirms: numerics cannot decide the prize; a proof needs genuine analytic equidistribution at fixed p.

GPU list-size measurement (2026-06-17, Nebius H200, ladder engine, self-test GPU=CPU MATCH): explicit worst-case list L(δ) = #{deg-<k RS codewords agreeing with a gapped worst-case word on ≥(1−δ)n pts}, MAX over candidate words, at n=64, ρ=1/8 (Johnson δ=0.646, capacity δ=0.875): L=0 across the whole window interior δ∈[0.64,0.80]; L=35 (bounded) at δ=0.81–0.83; explodes 6459→6643 only at the capacity edge δ≥0.844. ⟹ floor SUPPORTED at the fresh n=64=2⁶ octave — worst-case list bounded (≤35, no jump/OVERFLOW) deep in the window interior to δ*≈0.83, exploding only within ~0.03 of capacity, exactly the floor structure. (8×H200 failed to hold RUNNING — Nebius capacity; 1×H200 ran it, both destroyed/billing-stopped. ρ=1/4/k=16 and n=128 need the 8-GPU parallelism, infeasible on 1 GPU — not reported, no fabricated data.) In-regime evidence for the floor; does NOT prove the n→2³⁰ asymptotic (= the wall).

---

4. THE META-THEOREM — why every second-order method is dead (route-elimination)

For the deterministic period family {η_i} with Σ η_i² = p−n: bounding max|η_i| below √Σ admits exactly two equivalent routes — (a) high moments Σ η_i^{2r} to depth r ≍ log m, (b) a uniform individual tail ≡ (a). There is no third route.

_MomentMethodNoGo / _MetaTheoremSecondOrderFloor (axiom-clean): EVERY second-order method caps at Johnson/√p via (q·E_r)^{1/2r} ≥ n. Eliminates as a theorem: additive energy (any order), L²/Parseval, spectral λ₂, SDP/Delsarte-LP (phase-blind ⟹ L¹ triangle = trivial n), cumulant-2, the Shaw operator.

No third route: LP/SDP dual certificates are all moment polynomials; 6 EVT/RMT/arithmetic lenses confirm the meta-theorem. 3-property NECESSARY CONDITION on any winning method: simultaneously (a) b-sensitive, (b) deterministic-archimedean (not probabilistic-EVT), (c) genuinely L-infinity (sup, not RMS). Probabilistic-EVT crown killed: periods are exchangeable white-noise (Cov(η_a,η_b) = −Var/(m−1), distance-independent) → kills FHK / GMC / BRW / Coulomb-gas. (2026-06-16) Wall is provably archimedean: the period-polynomial discriminant disc(Ψ) is class-field-theory-fixed (= p^{m−1}·f²), so every symmetric/discriminant constraint gives only a LOWER bound on M — the "disc lower bound ⇒ house upper bound" lever is pruned (discnogo).

(2026-06-16) TETRACHOTOMY — a self-derived structural reason the wall is irreducible by elementary means. Any bound on max_b|η_b| for the flat 0-dimensional μ_n is necessarily one of four branches: (i) a symmetric function of the periods = a moment = BGK (Newton's identities force it: period-polynomial coefficients, SOS/Positivstellensatz certificates, phase-matrix singular values, b-orbit averages, and any sum-coincidence count by orthogonality are all symmetric functions of {η_b}, hence polynomials in the power-sum moments); (ii) a completion/Gauss-sum handle carrying a full √q factor (Hasse–Davenport b↦b², Weil — too big at the prize); (iii) a distributional/EVT/mixing statement (fails the deterministic-archimedean leg; mixing = equidistribution = BGK); (iv) a genuinely new evaluation of η_b not routing through a coincidence count. Branches (i)–(iii) are dead. Branch (iv) also closes for the dyadic prize object specifically: motivic/Tannakian relations express η_b via its Galois conjugates (= symmetric = (i)) and the one escape — a conductor factorization — is unavailable since n=2^a has an irreducible 2-power conductor; Bost–Connes/KMS free energy is circular (the KMS expectation of the b-character is η_b/n); p-adic↔archimedean transfer (Coleman/Coates–Wiles beyond the b-invariant Gross–Koblitz) is genuinely impossible because the period is a partial subgroup sum (not one Gauss sum), so its two places are independent; and house-from-minimal-polynomial is either wrong-direction (Schinzel–Zassenhaus/Dimitrov/Smyth bound the house below) or = coefficients = moments (Cauchy → trivial √p). ⟹ the only genuinely non-reducing object is the open analytic-NT evaluation itself — there is no fifth branch. This is why 250+ generated conjectures + a solo round all collapse, and it pins the prize to exactly the recognized open Gauss-period/BGK problem.

(2026-06-16) The STRUCTURED-PRIME lever is quantified-dead (the prize is forced into the high-v₂ regime, so this is decisive). Since n=2³⁰ ∣ p−1, every prize prime has v₂(p−1) ≥ 30 — the prize lives inside the "structured / 2-power" regime empirically shown to be worst-case (lowest onset r₀, the explicit Fermat W₄ defect). A dedicated round attacked exactly this regime, where the 2-adic / Stickelberger / complete-splitting machinery is strongest. Result (axiom-clean, verified this pass, _wf5M2_stickelberger_depth.lean, commit 473202e5f, #print axioms ⊆ {propext, Classical.choice, Quot.sound}): the depth-R Stickelberger / prime-splitting ceiling is p ≤ w^{n/(4R)} — non-vacuous only at R ≈ n/8 (the full window), and super-polynomial (zero constraint on p=n^β) at the prize deep-moment depth R ≈ β·ln n ≪ n/8. So the maximal-structure 2-adic lever gives an exact route-refutation, not an escape: it proves the wall holds in the regime it is strongest, it does not bound M. (Companion empirics, reproduced first-hand: the wall-constant ρ = M/√(n log m) is non-monotone in v₂ and stays bounded ~1.3 < √2 across a prize-faithful v₂-sweep — worst at the Fermat-like prime but never divergent; C=O(1) confirmed, proof unmoved. 2-power-order Gauss-sum evaluation gives per-character magnitudes but the sum over φ(2^k)/2 free phases re-incurs full √-cancellation = BGK; Stickelberger/2-adic-Γ constrain valuations, not the archimedean L∞ sup the meta-theorem demands.)

---

5. LANDED — actionable substrate (import + build on these; do NOT redo)

→ Full API: docs/kb/deltastar-444-LANDED-bricks-API-2026-06-15.md. Build idiom: scripts/pg-warm.sh once, then scripts/pg-iterate.sh <path> (no lock). Note: several core files carry exactly one sorry = the named open residual (the convention is modularity); the cited O### EXTEND-proven sub-lemmas are each axiom-clean {propext, Classical.choice, Quot.sound}.

Foundational bricks (unchanged): OpenCoreConditionalPin.WorstCaseIncidenceBounded (faithfully isolates the core), MetaTheoremSecondOrderCap, GaussPeriodParsevalFloor, IncidencePeriodBridge, CoshMGFIdentity (Σ_b cosh(η_b y)=q·Φ(y)), DCEnergyEssential/DCSubtractedMoment/DCMomentSupBound, SubgroupGaussSumMoment, _wf3D4/_wf3D5/_wf3D6 (monomial-worst / Lam–Leung orbit backbone / over-det Johnson-lock), MCADeltaStarListReduction (sqrt-free super-code bridge), OverdetIncidenceMaxClosedForm (2m³−2m²+1), ResolveFieldIndependent, OrbitCountCrossingLaw.crossing_law (D=z+S·O, crossing ⟺ O ≤ gcd(b−a,n)), ConverseLamLeung2Power, PrizeStructuralConstant (Λ²=max_b‖η_b‖²), E2W4CyclotomicNonCollision, DeltaStarExactPinF5/*F17* (exact pins), GranularityLadderRS (δ*=j/n bands), SchurLagrangeBridge (complete-homog = dividedDifferencePow_eq_schurH).

NEW since the fold (O196–O233 + lanes — all axiom-clean EXTEND-proofs unless noted):

• ★ Re-targeted floor reduction (commit 479bbe5af): _BchksF3_RetargetedReduction (prize_reduces_to_SumsetExtremality, subsetSumBudget_unsat, oldForm_vacuous_newForm_satisfiable), _BchksF6_ExplicitDeltaStarLower (explicit_deltaStar_lower_bound modulo 3 residuals), SumsetExtremalityReduction, CharSumBudgetVacuity (O223), _MasterGapOffByOneCorrected (capacity−δ*=m*/n). The whole new strategy's reduction skeleton is in-tree.
• ★ Poisson-MGF route FORECLOSED (NEW, verified + COMMITTED 913552cc0): _AvL_PoissonMGFForeclosure.lean (poissonAvg_ge_log: E[ρ_R] ≥ log q unconditionally; poissonAvg_gt_one; self-authored + verified axiom-clean, 0 sorryAx). The "softest form of the wall" (Poisson(log q)-averaged energy-MGF vs √q slack = the scalar E[ρ_R]≤1) is FALSE closed-form — the trivial r=1 Parseval anchor (ρ_1=q via the proven rEnergy_one) alone forces ≥ log q ≫ 1. Forecloses the route permanently.
• ★ I031↔Solve the Grand Proximity Prize directly: pin δ* in the prize regime (successor to #389) #407 reduction (NEW, verified): Frontier/I031MFromConstantIndexConjecture.i031_M_le_logTarget_of_constantIndexConjecture (sorry:0, commit 888952d03) — prize M(μ_n) from the Solve the Grand Proximity Prize directly: pin δ* in the prize regime (successor to #389) #407 ConstantIndexSubGaussianPeriodBound (= the wall). Unifies two named-open objects onto the wall.
• ★ Unconditional char-0 E₃ census (NEW, verified + COMMITTED ac9e7be5c): _AvL_T3ClosedForm.lean (rEnergy_mu_three_eq: rEnergy(μ_{2^k},3)=15n³−45n²+40n, + negSymCount_eq_closed, rEnergy_three_eq_negSymCount, exists_neg_transversal; independently verified #print axioms ⊆ {propext, Classical.choice, Quot.sound}, 0 sorryAx, pg-iterate ✅ ×3). Closes the "mechanical-only char-0 gap"; discharges exactE3 of the conditional gaussianEnergyBound_muN_three_of_exactE3.
• ★ di-Benedetto energy input grounded (NEW, verified + COMMITTED 31dcb5025): _AvL_DiBenedettoEnergyGrounded.lean (rEnergy_three_eq_energyThree: (rEnergy μ_n 3 : ℝ) = energyThree(|μ_n|); rEnergy_three_le: (rEnergy μ_n 3 : ℝ) ≤ 15|μ_n|³; axiom-clean verified) — bridges the genuine rEnergy to the di-Benedetto envelope, removing the abstract BalancedCount conditional for μ_n. Scope: grounds the char-0 energy input only; the beat stays di-Benedetto-Thm-3.1-conditional, good-prime-only at char-p, realised finite-n saving strictly below 1/24.
• ★ Structured-prime wall quantification (NEW, verified): _wf5M2_stickelberger_depth.lean (stickelberger_depth_bound, depth_prod_le_pow; commit 473202e5f, axiom-clean, pg-iterate ✅ 37s): the depth-R Stickelberger prime ceiling p ≤ w^{n/(4R)} — proves the maximal 2-adic/splitting lever is non-vacuous only at R≈n/8 and vacuous at prize depth R≈β ln n. Plus cdf8d8efe (E₃≤15n³ conditional on the char-0 census, char-p onset pinned at depth 3) and 59e92376b (di-Benedetto shortfall = Θ(1/log n), exact constant (2 log 15 + (log 3)/2)/72).
• ★ ON-BGK two-sided substrate (VERIFIED bricks only): _MomentLadderExceedsPrize.moment_ladder_exceeds_prize (no second-order route, any depth), _EnergyRatioMonotoneReduction (gaussianEnergyBound_of_ERM; ERM-at-r ⟺ max‖η‖²≤(2r+1)n = sup-norm — the two-sidedness), KambireDeepBandFloor/KambireExponentialGap (complete-homog count super-poly multichoose s s ≥ 2^{s−1}, O234/O235), OverdetIncidenceMaxClosedForm (over-det count 2m³−2m²+1 = Θ(n³) ≫ budget). Together with the standing numeric facts (proxy→Johnson, mod-p defect = BGK), these give: the prize is two-sided onto the BGK wall. ⚠️ The 17:00 verdict comment ALSO cited _DstarGrowthLaw/_OPSingleOrbit/_DyadicRecursionDstar/PrizeEquivalencePin/FloorResonanceEnergyBridge as axiom-clean — those are phantom (§11); do not consume them.
• char-0 face: _CharZeroMGFBesselBound (sorry=0, commit 74ad183f9): besselI0Two_le_exp_sq/besselI0Two_pow_le_exp prove I₀(2y)^m ≤ exp(m·y²) (the analytic char-0 MGF bound, from termwise 1/(k!)²≤1/k!). char-0 term-by-term E_r ≤ Wick is via GaussianEnergyFromPairing.gaussianEnergyBound_of_pairing + ConverseLamLeung2Power (Lam–Leung antipodal pairing) + _CollisionExcessPartition (genuineExcessCount=0 ⟹ bound); the all-r single theorem is §6.0 (near-term landable). r=2 rung unconditional & thinness-essential: GaussianEnergyBoundMuNDepthTwo.gaussianEnergyBound_muN_two.
• Energy ladder extended to E₇: _AvL1_E6ClosedForm (sorry=0), _AvL2_E7ClosedForm (sorry=0; E_7=135135n⁷−2837835n⁶+…+471556800n, leading (2·7−1)‼, SOS deficit cert, cross-validated E_7(8)=16993726464). E₈ is the next "producer" rung.
• Dilation-orbit reduction (I031): I031DilationOrbitReduction/I031SubGaussianMaxBridge — η_b is orbit-invariant, F_p* partitions into (p−1)/n size-n orbits, the sup collapses to a transversal of (p−1)/n reps (metric-entropy reduction log p → log(p/n)). Substrate axiom-clean; the chaining constant is the open lead (§6.8).
• Orbit-count growth: _OrbitSizeEqN (O197, odd-card carrier orbit size EXACTLY n), _OrbitCountGrowthLaw (O196, shallow-rung counts super-linear oc₃~n²/32, oc₄~n³/512). Spectrum generating function Sweep_A50 + alternating-sum Σ(−1)^r N_r=(−1)^{m+1}(m−1).
• Subset-sum SPECTRUM structure (constrains the BCHKS object): |μ_n| ∣ |spectrum_r \ {0}| (O231, freeness discharged), spectrum multiplicatively rigid / μ_n-orbit union (O229), negation-closed at central depth r=n/2 (O230), EVEN nonzero cardinality at r=n/2 (O233), peak (3^m+1)/2 at center, total mass 3^{m−1}(m+3). Constraints on |spectrum_r|, not a bound on it (still open).
• char-p r=3 DC-Wick rung κ6_charp = 40n + S with gate S ≤ 45n²−40n (O204); exact char-0 Lam–Leung SLACK Slack_2=3n, Slack_3=45n²−40n (O216, the wf-P2 headroom producer); SHARP max-fiber energy ceiling E_r(G) ≤ R_r·|G|^r (O227); GaussianStepLaw E_{r+1} ≤ (2r+1)·n·E_r (_AvL3).
• Determinantal / minor-degree route (_CoreA6deep/_AvL4): minor-degree budget SHARPENED for complete-homog readouts — |forcedGammaImage| ≤ b−1 < C(n,k+2), HALF the generic 2n margin (O208–O210), composed to DISCHARGE MinorImageLeBudget (O209). Residual-ratio permutation-invariance ⟹ #ratioImage ≤ C(n,k+1) (O207, (k+1)!-fold tightening).
• GV fibre rep-count is a polynomial root count of the shifted-power poly, r(c) ≤ deg gcd(Xⁿ−1,(X+1)ⁿ−C(cⁿ)) (O213/O214, the Stepanov-consumable bridge).
• dilation-pencil counts: sunflower common-M-core r(r−M)+M ≤ |G| (O202), general-pairwise Bonferroni count, M≥2 Johnson-collapse threshold (O232).
• KKH26 supply strictly decays along an s-step fold (O228); char-sum→incidence budget is VACUOUS at prize budget (O223, turns the prose correction into a theorem); δ* monotone in ε* (O224); orbit-count NECESSITY delimiter (O222, honest mirror of OpenCoreConditionalPin).
• √q ceilings: unconditional Λ² ≤ (√q−(√q−1)/t)² < q (O219), DepthLogSubGaussian confined to thin regime (O220), explicit Stepanov–Weil |V| ≤ (deg g+2)·⌊√q⌋ (O218); the classical Gauss-sum completion anchor is NON-PROVING on thin subgroups (O218, margin-collapse ~n/q→0).
• Multi-point (S-block) puncture pigeonhole transfer + transfer-BACK (O226); unique decoding ℓ=1 below half min-distance (BallDisjointUniqueDecoding, classical regime — not prize-relevant but axiom-clean).
• CensusDomination sufficiency (O206, the two census sub-obligations imply the consumed Prop) + multiplicity caps (O203).
• Structured single-line floor s* ≥ 5n/8 at ρ=1/4 for all μ (O199) — super-Johnson but explicitly bracketed SingleLineNotList away from CORE (single-line s*, NOT list-radius δ*).

⚠️ do NOT cite as landed: _DefectOnsetOvershoot (re-created as _AttackDefectOnset_EnergySandwich), SubsetSumThreePowExact (re-created as _AttackThreePow_SubsetSumExact, 3^{n/2} is an UPPER bound not exact), N9 |V_4|=48 point-count, _Close27_* "decision" (prose-only tautologies), LamLeungUnconditionalQ full Wick bound (only the structural foundation is proven). Correction: Sweep_A41…A49 (the char-0 dyadic-rigidity chain) DID land (dfd092069); the audit's "phantom" flag was stale (pre-merge to fork/main) — they exist, each with one named-residual sorry.

---

6. LIVE open research paths (the current frontier — none reaches closure; that is the prize)

🔑 The prize is ONE inequality, proven two-sided (§0.0): the char-p Lam–Leung transfer E_r(μ_n) ≤ (2r−1)‼·n^r at r≈ln q = M(n) ≤ C√(n log m) = BGK at the Burgess barrier. Everything below is either (i) the char-0 face of this (provable, near-closure — §6.0), (ii) the genuine open wall (char-p transfer — §6.4, now the SINGLE core), or (iii) reframings/levers shown to reduce to it. The off-BGK combinatorial routes (6.1–6.3) are confirmed to collapse to Johnson / equal the wall and are listed for completeness, not as escapes.

6.0-FLOOR ★ The FLOOR-proving frontier — ONE object, FOUR propositionally-equal faces, all the wall (verified 2026-06-17)

A dedicated attack on proving the floor (the hard lower-bound direction: worst-case list/δ* bounded in the window interior for ALL words) localized it sharply, and every angle reduces to the same wall — now with four in-tree, propositionally-linked names:

• (F1) Far-line incidence OpenCoreConditionalPin.WorstCaseIncidenceBounded C δ B (= BCHKS Conj 1.12): floor ⟸ this + the BGK sup-bound (NubsCarson prizeFloor_window_of_BGK_and_incidence, on a branch not yet on main — content corroborated). The sup-bound ALONE is vacuous (only sup→incidence route pays naive q·B ≈ |G|).
• (F2) Orbit-count ≤ d (OrbitCountPinNecessity, verified): coprime_pin_requires_single_orbit forces a SINGLE orbit (O≤1) at the binder; not_worstCaseIncidenceBounded_of_orbitCount_gt makes the pin provably FALSE whenever O>d. Converts the analytic floor to a combinatorial orbit-count statement.
• (F3) Union-growth law (unionGrowth_iff_orbitGrowth, _LaneB…, verified): the distinct-γ union floor is propositionally EQUAL to the orbit-count growth law (orbit size divided out) — two open laws are literally one.
• (F4) EVT concentration (_EVTFloorRoute.prizeFloor_of_EVTConcentration, verified sorry=0): the de-Finetti substrate is PROVEN (mean-pinned Σηᵦ=−|G|, real periods, Parseval variance qn−n²); the entire residual is EVTConcentration (‖η_b‖ ≤ C√(n log(q/n))) — a named-never-asserted open input (the BGK wall as a Gumbel-max concentration).
• ★ The decisive L²→L∞-over-offset verdict (verified, the freshest localization): the operative input (F1) is PROVEN in L²-mean over the offset s₀ (IncidenceDevL2Offset, branch: ∑_{s₀}‖D(s₀)‖² = q·∑_{b∈dev}‖η_b‖² exact). The remaining gap is L²→L∞ — and it is provably the wall, not a free lever: TwoDAnnihilatorLineParseval.lineEta_image_eq_globalImage (verified sorry=0) proves the offset-magnitude SET {‖D(s₀)‖} EQUALS the global set {‖η_b‖}, so max_{s₀}‖D(s₀)‖ = B exactly. And sum_reindex_mul_unit forces #dev = q−1 (the WHOLE nonzero spectrum, via the unit-multiplication bijection t↦t·b₀) — the hoped-for #dev=O(log) is structurally impossible. So bounding the worst offset literally is bounding B = the BGK/Paley sup-norm.
• Net (honest): all four faces + the L²→L∞ gap = the SAME object = BCHKS 1.12 = the char-p Lam–Leung transfer = the BGK/Paley wall (proven n^{1−o(1)}, prize needs √n, gap = full half-power = Paley). The mechanism is uniform: every proven input is L²/aggregate (Parseval √q·B cancellation EXACT; orbit-count super-linear at shallow rungs; antipodal sub-count constant), and the floor needs the L∞ max — the L²→L∞ collapse at the deep binding rung r~log n IS the wall. No genuine non-wall floor-proving path exists (verified; moment/energy, good-prime, dyadic-tower-saving-preserving, reducible-tower-wrong-lane all dead). GPU n=64 (§3) shows the floor empirically holds; proving it = this L∞ bound.

6.0 The char-0 half is ALREADY CLOSED for all r (verified this pass) — the residual is purely char-p

• Status. _CharZeroWickEnergy.gaussianEnergyBound_dyadic (sorry=0, axiom-clean) already proves E_r(G) ≤ (2r−1)‼·|G|^r for all r, any char-0 field, G ⊆ μ_{2^k} — via the Lam–Leung antipodal-pairing (ConverseLamLeung2Power) + _CollisionExcessPartition (the char-0 face has genuineExcessCount = 0 identically) + the pairing census. The Bessel face _CharZeroMGFBesselBound (I₀(2y)^m ≤ exp(my²), sorry=0) gives the same bound analytically. The exact char-0 census at r=3 is now also closed on rEnergy (_AvL_T3ClosedForm.rEnergy_mu_three_eq = 15n³−45n²+40n, verified axiom-clean this session). (A separate grind re-derived the all-r bound as _CharZeroEnergyAllR, confirming axiom-cleanliness, then found it duplicated gaussianEnergyBound_dyadic — not landed, to avoid redundancy.)
• Consequence. There is nothing left to do on the char-0 side: the entire open problem is precisely genuineExcessCount(μ_n, r) ≤ (char-0 slack) at r≈ln q at the prize prime — i.e. the char-p excess (§6.1). The char-0 slack is positive and Θ(n^{r−1})-large (e.g. Wick₂−E₂=3n, Wick₃−E₃=45n²−40n), so the prize does NOT need W_r=0, only W_r ≤ slack_r — but bounding the char-p excess at deep r IS the BGK wall.

6.1 ★ THE SINGLE CORE — char-p transfer of A_r ≤ (2r−1)‼·n^r at r≍log q (the BGK wall)

• Statement. The prize, sharpest form: genuineExcessCount(μ_n, r) = 0 (equivalently W_r = E_r(F_p)−E_r(ℂ) = 0, equivalently the DC-subtracted A_r ≤ Wick) at the prize prime for r ≈ ln q ≈ 89. Equivalently the saddle Φ_p(y*) ≤ exp(ny*²/2), y*=√(2 log q/n). Use DC-subtracted A_r (raw E_r ≤ Wick FALSE at prize).
• Status. char-0 = 0 identically (Lam–Leung; §6.0). W_r=0 ⟺ p > onset-threshold(r); W_3=0 at prize scale, W_4=0 at generic prize-scale primes; the deep-r onset at the fixed prize prime is the wall. No in-tree escape: ERM-at-r ⟺ M ≤ √((2r+1)n), so the energy route at this depth IS the sup-norm bound (two-sided). Numerically verified n≲40, OPEN at n=2³⁰. Floor-true evidence (computed this pass, two independent runs): at the structured Fermat prime 65537 (n=16) E_r ≤ Wick holds r=2..5 with A_r/Wick decreasing (0.94→0.82→0.68→0.52, W_4=4480); at a generic prime p=65617 it is cleaner — W_r=0 for r=2,3,4 (onset between r=4 and 5), then TINY (W_5/slack_5=0.022%, W_6/slack_6=0.146%), Wick holding with 3–4 orders of magnitude headroom. The wall-constant C(n)=M/√(n log(p/n)) stays in [1.20,1.36] (mean 1.285) with NO upward drift n=16→256, doubling ratios scatter between √2 and 2 (no approach to 2). Favorable to a bounded C (floor TRUE), not decisive — no finite r/n reaches the asymptotic depth r≈log m where the wall lives.
• Next (honest). This is the 25-year-open BGK/Paley problem at the Burgess barrier; a complete proof needs a genuinely new analytic-NT / effective-equidistribution / monodromy input that does not exist in the literature. In-tree, the only forward motions are characterizing the onset-threshold growth law and extending the E_r ladder (E₈+).

6.2 Char-free complete-homogeneous floor — CONFIRMED collapses to Johnson (not an escape)

• The complete-homogeneous count h_j=C(s+r−1,r) is the worst CHAR-FREE bad-scalar count, but it is super-polynomial (O234/O235: multichoose s s ≥ 2^{s−1}), so poly(n)·h_j ≫ ε*·|F| — the char-free crossing is Johnson-side (F6 at M_cross=n/4). The window interior needs the mod-p defect (BGK). Useful as tight bookkeeping (_BchksF3/F6), not an escape.

6.3 ★ Determinantal / Open-Set Rank route — NOW EXTERNALLY PUBLISHED (Chai–Fan 2026/858 §7, Conjecture 41) — the genuine non-BGK δ* handle

• The external result. 2026/858's structural track (§7) is the published, empirically-verified-to-n=40 form of the dossier's determinantal lever. The worst-case list size M_true (= the δ* object) has a codimension phase diagram: c=1 saturating; c=2 exponential M_true ~ 0.66·1.36ⁿ (PROVEN, Möbius Lemma 37 + Thm 38); c≥3 (the deployment regime, c=Θ(n)) conjecturally LINEAR M_true ≤ ⌊(2D−1)/c⌋ = O(1) — Conjecture 41 (Open-Set Rank Lemma).
• The reduction (verified). M_true(s) = m ⟹ m ≤ ⌊(2D−1)/c⌋ follows from full rank of the explicit constraint matrix A = [N_Ei | γi N_Ei]_{i} ∈ F_p^{mc×2D} (N_Ei = the c error-locator normals of support E_i, Lemma 25; distinct γi). The ONLY obstruction to full rank is the (w+1)-clique (all size-w subsets of a (w+1)-vertex set), which produces a row dependency — but only at small primes p < p0(n,k,c) (the K3 triangle at c=2/p=113, the K4 tetrahedron at c=3/n=12/p=61 are the witnesses). Conjecture 41 asserts p0(n,k,c) is polynomial in n (an effective Schwartz–Zippel bound on the clique-obstruction resultant).
• Why this is genuinely OFF BGK (not the sup-norm wall). It is a rank / resultant-divisibility statement, not a character sum: prize-δ* ⟸ Conj 41 ⟸ "the (w+1)-clique obstruction determinant has norm dividing only primes < poly(n)" — the determinantal + good-prime/Linnik levers (= §6.5), NOT the BGK sup-norm (§6.1). It does not reduce via orthogonality to a moment (it's a worst-case Nullstellensatz statement, not a coincidence-count). This is the strongest in-tree candidate's external validation: the dossier's determinantal lever (_CoreA6deep: D*(2) ≤ 2·span, bezout_beats_choose_two, plueckerMinor_ne_subsetSum) and the minor-degree bricks (O207–O214) are the in-tree substrate for exactly this matrix-rank argument.
• ATTACKED + VERIFIED (2026-06-17) — genuine route, but NOT a prize closure as posed. A focused attack + my own independent exact-ℚ rank computation settle the crux: the (w+1)-clique row-dependency is IDENTICALLY-ZERO over every field (not a mod-p coincidence). Exact rational Gaussian elimination of A=[N_{E_α}|γ_α N_{E_α}] for the clique E_α=W∖{α}: rank = D+c−1 exactly (never full min(mc,2D)), kerdim = w+1, robust across node/γ choices, at c=2 (K3: 5/6), c=3 (K4: 8/12), c=4 (K5: 11/16); disjoint/non-clique supports give full rank. In-tree the same fact is axiom-clean (Conjecture41CliqueKernelStructure.clique_kernel_mem, Conjecture41CliqueRelationModule.relation_factor_sum_twisted — via the char-free nodal identity (X−α)Λ_{E_α}=Λ_W) + an integer-coefficient PTE witness (E1={0,1,5,8,12,21}…, cyclic kernel over ℚ). ⟹ There is NO p0 for the rank statement — the "poly p0 via effective Schwartz–Zippel ⟹ prize" narrative is a category error (it conflates the obstruction polynomial's poly(n) degree with the integer height of its specialized value). The clique branch ALWAYS fails (structurally like the proven-EXPONENTIAL c=2 Möbius case), so Conj 41 lives entirely in its degeneracy escape clause.
• Net verdict (honest). Conj 41 is a genuine non-BGK route (vindicated — determinantal/resultant, no orthogonality to a moment; corroborated by the p-INDEPENDENCE smoking gun D=89 identical across 4 primes while BGK's B varies) — but REFUTED as a payoff: the easy structural half (clique = unique rank obstruction, full rank generic off-clique) is done in-tree; the prize relocates to TWO orthogonal, genuinely-open arithmetic layers, both showing exponential resistance: (i) prove every persistent char-0 rank-deficient syndrome is degenerate (a false positive supported on the (w+1)-set with NOT all error values nonzero, hence not a real V_E^{-1}s(γ) list member — Conj 41's own c≥3 escape clause, OPEN); and/or (ii) bound the log-HEIGHT of the all-nonzero-realizability resultant by poly(n) — where every proven in-tree height is the crude exponential 4^{φ(n)}=2^n (CyclotomicResultantBound, E2W4CyclotomicNonCollision: "vacuous at the prize point 2^{2^30}≫2^158"), and even the conjectured-tight (n/2−1)^{n/4} is exponential and fails at n=128 (tight_height_keeps_n128_wall_real). This is the E2W4 residual replicated at codim c≥3, NOT discharged — SOTA-adjacent route-clarification, not closure. (Lean target banked-able: the char-0 clique-rank fact "rank [N|γN]_clique=D+c−1 over any field" is half-built in Conjecture41CliqueKernelStructure; welding it to a single headline permanently banks the "identically-zero, not mod-p" verdict that kills the prize-favorable reading.)

6.3b Determinantal / Bézout minor count, in-tree substrate (_CoreA6deep)

• D*(2) ≤ 2·span via the degree-2 minor polynomial, bezout_beats_choose_two (2n < C(n,2) ∀n≥6); machine-certified DIFFERENT from BCHKS subset-sum (plueckerMinor_ne_subsetSum: the 2×2 minor is −xy, a product not a sum). Caveat: a Bézout ROOT-count, not a Lang–Weil point-count — V_r is 0-dim so Lang–Weil is VACUOUS; the bound is real, the point-count framing is the overreach trap. This is the in-tree machinery for §6.3's Conjecture-41 attack.

6.4 Dedup-strictness at log depth (_CoreA3, _AvL5)

• Statement. BCHKS ⟹ WeakestSuff holds unconditionally via D ≤ Σ_r; whether the dedup is strict at m≈log n (strict ⟹ prize needs less than full BCHKS; equal ⟹ wall) is the precise p-independent open question. The dedup N_r < C(n,r) is STRICT but fractionally vanishing at r=log₂n (survival ceiling C(2m,r)−C(m,r)2^r → 1, O211). In-tree evidence leans wall; the toy "escape" theorems are vacuous — do not cite as escapes.

6.5 Effective-Chebotarev / Linnik good-prime count of Spur_r(p) (_AvW2)

• Statement. Prove a good prime exists where r-sums are distinct mod p (giving poly-many distinct λ), bounding the bad-prime set by Res(Φ_s,·) divisor count ≤ log₄ s per pair. weight-4 spurious collisions exist at p=17 (m=4) and Fermat 641 (m=5) — bad primes are finite & small. Reduces to quantitative Linnik / effective Chebotarev (Lagarias–Odlyzko; p≡1 mod 8 density-1/4 surviving class = the prize-prime class).

6.6 Distinct-γ union-count growth law |⋃_R {γ_R}| (the reframed combinatorial core)

• Statement. Generating-function / polynomial-method bound on the p-independent distinct-γ count. Shallow-rung growth is super-linear (O196); deg(#bad_r) < r for general r (the growing-slack mechanism) would give the decay. The subset-sum spectrum structure bricks (O229–O233) constrain but do not yet bound |spectrum_r|.
• Why open. Numerics PROVABLY cannot separate bounded-m* from log₂n below n≥256; the plateau-width law w(n) of the worst-dir cascade is the single most decision-relevant computation (bounded w ⟹ m*=O(log n)). n=64 GPU min_m D*(m) (via the orbit-count recursion) is the decisive test.

6.7 Proxy ↔ true-MCA δ* relationship across rates (largely RESOLVED → reduces to §0.0)

• What it asked. Whether the far-line "proxy" δ*_farline→1/2 is a valid upper bound on the true MCA δ* across rates (it can't be at ρ<1/4, where proven MCA-up-to-Johnson gives δ*_MCA ≥ 1−√ρ > 1/2).
• Resolution. The §0.0 reconciliation answers this: the far-line over-det census is a p-independent count Θ(n³) ≫ budget that collapses to Johnson (it is a lower envelope realized only when the mod-p defect is absent), so it is NOT an upper bound on the true MCA floor; the window-interior δ* is governed by the p-dependent BGK char-sum. So "escape the proxy" = exactly the ON-BGK wall, not a separate lever. (A clean rate-swept orbcount at ρ∈{1/8,1/16} would still be a nice confirmation, but the conceptual question is settled.)

6.8 I031 dilation-quotient chaining (the surviving empirical non-BGK lead)

• Statement. M(n) = max_b‖η_b‖ ≤ C·E[sup|G_b|] over the (p−1)/n dilation-orbit representatives — chaining on F_p*/μ_n collapses the metric entropy log p → log(p/n). The orbit-reduction substrate is fully axiom-clean (I031DilationOrbitReduction: free action, partition into (p−1)/n size-n orbits, sup-transversal collapse).
• Why open / why notable. The DECIDER probe shows the normalized constant M/√(n·log(p/n)) stable in [1.15,1.40] and slightly DECREASING at the prize β=4, with no upward trend to n=256 — the campaign's strongest single empirical signal for a bounded constant. Next: attempt a union bound at depth (Lamzouri-type) over the collapsed (p−1)/n index set, and verify whether log(p/n) vs log p actually changes the achievable constant. (Equivalent to the BGK wall but with reduced entropy — the open question is whether the entropy reduction is exploitable.)

---

7. Out-of-regime candidates — failed/limited at non-prize scale, still worth PRIZE-REGIME testing

(Not refuted, not wall-reductions; hit a compute/scale ceiling or validated only out of regime. Re-test at thin prize n=2^30, q=n^β, multi-prime.)

• GPU exact over-det worst-direction scan at n=64,128 (m* growth distinguisher / plateau-width w(n)) — the single most-cited decisive computation, char-0 and OFF BGK. Needs the orbit-count recursion (brute is GPU-infeasible).
• Deep-rung moment A_r/Wick trajectory at r*~log m, n≥128 (worst bad prime) — all exact probing confined to r≤6 at sub-prize p; consistent with BOTH prize-true and BGK-tight.
• M2 Stickelberger/Chebotarev — failed generically, but the p≡1 mod 8 (m≥3) surviving class (density 1/4) is the prize-prime class; divisibility count there untested.
• Wasserstein / Kowalski–Untrau (KU25) effective equidistribution — no-go was at thick scale; the W₁ extreme-value upgrade of the Gauss-period family law untested in the thin regime.
• Thin-Sidon depth → sup-norm bootstrap (§7.2 of Solve the Grand Proximity Prize directly: pin δ* in the prize regime (successor to #389) #407) — every conversion gate ratio M_thin/M_random stays flat ~0.93–0.96 (β-invariant); a valid bootstrap must explain why MORE depth buys NO sup-norm saving. Run n=32 β=5 sup-sweep.
• Bilinear/dispersion n^{2/3} & M10 n^{3/4} towers — the bilinear lane is the ONLY one yielding a non-trivial unconditional exponent from a self-contained subgroup identity with NO external sum-product input; stalls (per-level loss multiplicative).
• Promising external tools (need a prize-regime test): Murphy–Rudnev–Shkredov 49/20 energy (arXiv:1712.00410), OSV short-Weil curve-blend (arXiv:2211.07739), Liu–Zhou subgroup-restriction eigenvalue recursion up the dyadic tower, theta-FE for x↦x² (metaplectic self-similarity), FKMS bilinear-below-PV.

---

8. DEAD / REFUTED ledger — do NOT re-attempt, grouped by WHERE it failed

⛔ Reduces to the BGK/Paley sup-norm wall (real machinery, NOT a bypass)

• Line-decoding / collinearity route (ABF26 Thm 4.21) as a BCHKS-free escape — both the MCA bad-count AND non-collinear line-packing reduce to the SAME far-line incidence.
• BCHKS-1.12 |Σ_r|≤budget as the prize object — |Σ_r| grows ≫ budget (vacuous); and as ABF26 states it, Conj 1.12 is the failure direction (strengthens the CEILING). The real floor is Sumset-Extremality (§0.2).
• crossCell dyadic-tower iteration — floors at log₂M ~ log₂n ⟹ trivial M≤n, never √(n log m).
• Even-moment / additive-energy face A_r — thin μ_n A_r == neg-closed-random A_r exactly; E_{2r}(thin)/E_{2r}(random) GROWS with r (thin LARGER).
• restriction/extension (Mockenhaupt–Tao), Gross–Koblitz / p-adic Γ_p / Newton-polygon (b-invariant unit phases), theta/AFE + de Finetti, circle method (minor arcs → L²/Parseval RMS), Elekes–Szabó / sum-product (√-lossy energy→δ*), polynomial method / slice-rank (n^{0.92}), hyper-Kloosterman/FKM (conductor ~n too large), List-decoding/HOMDS/Schur-at-roots (vanishing sums), random-RS capacity transfer (Schwartz–Zippel unavailable for explicit points), cosh-MGF/Bessel-saddle (caps at ~1.03× floor), deep-r Wick-deficit compounding (W_r→1 FASTER than knife-edge), phase-alignment/per-coset descent (−1∈μ_n forces real, a SIGN not a phase mechanism), bilinear/cube/free-prob/RMT, tropical/BKK/Croot–Sisask/Rankin–Selberg, Carlitz/FF-RH/quantum-group, LP/SDP "third route", 50-/100-/140-conjecture sweeps (0 survivors), negacyclic crossCell calculus / transfer operator (non-contracting α≥1), theta/ideal-lattice (rank φ(n)=n/2 ⟹ exp(Θ(n/2)) weight count = the √n-deficit in geometry-of-numbers clothing).
• discnogo (2026-06-16): the period-polynomial discriminant disc(Ψ)=p^{m−1}·f² is class-field-theory-fixed ⟹ every symmetric/discriminant constraint gives only a LOWER bound on M (the wall is provably archimedean).
• Stepanov lever FULLY CLOSED (2026-06-16, commit 61187fbe0): the last open Stepanov direction (I015 multivariate digit-recursion) collapses — μ_n's coordinate ring is an n-dim univariate (rational-curve) space and μ_n ⊂ F_p kills Frobenius; order-m vanishing-constraint rank saturates at exactly n. With the two prior stalls (M=1→degree, Weil √q vacuous on thin μ_n since √q ≥ n at β≥2), the entire curve/Stepanov door is permanently shut for 0-dimensional μ_n.
• Even/odd dyadic descent (G1/G2), non-symmetric tower descent, antipodal-tower descent — saving-NEUTRAL at every octave; telescopes to the μ_2 base (μ_1 degenerate); reduces to the BGK dyadic-lacunary char-p defect.
• Completion-sum cancellation Σ_j G_j — EQUALS the open BGK content (phase-blind); not a separately-capturable lever (O221).
• OSV short-Weil curve-blend (arXiv:2211.07739) — floor p^{3/7} ≫ prize p^{1/4} (gap 5/28); door shut at the prize point.
• Band dichotomy — "consecutive lacunary x^{n−1}+x^{n−2} is worst" is FALSE (it is a benign contiguous band, agreement ≤ k+1); the floor witness must be GAPPED (the gap engages the cyclotomic/BGK wall).
• The off-BGK combinatorial escapes (2026-06-16): the p-independent over-det count D*(n,3)=Θ(n³) ≫ budget (OverdetIncidenceMaxClosedForm, collapses to Johnson); the complete-homogeneous floor is super-poly (KambireDeepBandFloor/KambireExponentialGap, O234/O235, axiom-clean) so its crossing is Johnson-side; the single-orbit O_P=1 and dyadic-recursion escapes refuted numerically (their cited Lean bricks _OPSingleOrbit/_DyadicRecursionDstar are phantom — §11). All confirm: no off-BGK route reaches the window interior.
• delsartelpnogo (2026-06-16): the Delsarte / LP / Beurling–Selberg method class provably cannot beat Parseval (phase-blind ⟹ L¹ triangle = trivial n) — a clean addition to the §4 LP/SDP no-third-route theorem.
• 10 "new-math" relocations (Terwilliger op-norm =M, Bourgain–Gamburd amenable, Amice/Iwasawa b-independent unit, Kelley–Meka/PFR wrong direction, Krawtchouk/FKM conductor, chaining entropy metric-blind, Croot–Sisask =floor excess, 2-adic Newton-polygon, Schur–Siegel–Smyth → Johnson, entropy-compression backwards) — deeper result: M(μ_n) is INTRINSIC (framing-independent).

⛔ Reduces to Johnson / Plotkin proxy

• Even/over-det far-line construction as off-BGK floor — the over-det s−k≥2 stratum is p-INDEPENDENT but PROVABLY reproduces Johnson: δ*_farline = 1/2+1/n → 1/2, m*=n/4−1 LINEAR (I(n) is a clean quartic ~1.37e-3·n⁴).
• Hab25 as a published bypass past Johnson — reaches NOTHING past it (ℓ→∞ at Johnson).
• Antipodal-domination / antipodal-tower "prize true beyond Johnson" — RETRACTED; char-0 antipodal binding pins δ*=Johnson+1/n (saturates AT Johnson).
• r=2 (L4) moment rung — A_2 char-0-fixed but its L4 ceiling ~n^{1.5} OVERSHOOTS the prize √(n log m).
• O191 plateau dichotomy "m* SUB-LINEAR (3,5,8,12)" — real and m*/n→0, but this is the PROXY face, NOT the real BGK wall; m*(64+) is recursion-extrapolated, not measured.

❌ REFUTED-FALSE (machine-countermodel)

• Odd/signed-moment thin-cancellation (thin RIGIDITY makes signed cancellation WORSE, A_r=−32^r through r=7); additive large sieve (RHS = 2× Parseval, wrong side); fewnomial/Khovanskii/Descartes on I(n) (over/undershoots); reverse LD⟹MCA (thickness-invariant); "worst-case window list constant L=2" (RETRACTED — that's the dilation-INVARIANT-word list only); char-0 δ*=(1−ρ)−log₂n/n (true law s*−k=n/4); base-case+monotonicity proof of A_r≤Wick (n=64 KILLS it, f(r) increases 1.000→1.911); CensusDomination via K (exceeds its own weld budget); wf-D3 pinch (constant Θ(1) gap ~1/8, doesn't shrink); shallow-band #bad/census ~0.26 (budget-conflation artifact); v2(p−1)-gated 2-adic law (M/√n tracks BGK once β fixed); C8 weight-bounded surrogate.

⚠️ Finite-size artifact (decays to 0 in n) — thin Sidon r_min advantage (DROPS 11→8 at n=64); decoupling crossing-depth c*=Θ(n) (actually O(1), constant in rate); Route 36 deep-hole sup (saturates p-independent cyclotomic).

🚫 Larp / vacuous — classical DFT-uncertainty (Donoho–Stark 0.8n above Johnson; Tao strong-UP holds only for n PRIME); N9 codim-2 cohomology (|V_4|=48 p-independent constant, no q-error). The retracted _AntipodalPlotkinHalfCap, the _Close27_* tautologies, and deltaStar_pin_mu6_dim4=59/64 (toy n=6, not prize) belong here (see §11).

↪️ Out-of-regime (see §7) — BChKS admissibility construction (dyadic + ε*=2⁻¹²⁸ defeat it at FRI params); e2=0 over-det census (thickness-invariant, rule-3 fail); E_r p-invariance universal (E_4 first fails at Fermat); di Benedetto/Paley shortcuts at H~p^{1/4}; effective Katz/Deligne at fixed q (discrepancy ~m/√q=2⁴⁸≫1).

⛔ Open-thread sweep (2026-06-17, all 495 comments re-mined → 5 threads, all attacked):

• PoissonAveragedMGF (the "softest form of the wall" — Poisson(log q)-averaged energy-MGF vs √q slack) — REDUCES TO WALL, closed-form (not compute-bound): the saddle gives Ψ(y*) ≤ q² ⟺ E[ρ_R] ≤ 1, but ρ_1 = q exactly (via proven rEnergy_one: E_1=|G|=Wick_1), so the r=1 Poisson term alone contributes ln q ≫ 1, at every n/prime/literal prize scale. β-uniform failure; the averaging is dominated by the trivial Parseval anchor and discards the char-0-subtracted excess that is the real object. (coshMGF_poisson_form axiom-clean; verified first-hand.)
• ≥2-D MCA incidence L²-measurability (would-be reframe: is the δ*-governing witness incidence B-blind?) — REDUCES TO WALL: the proven L²-blindness (lineEta_energy_eq = q·|G|, axiom-clean) is quarantined to the line-energy object, which is provably not δ*; lineEta_image_eq_globalImage proves the line's magnitude-set = the global set, so the L∞ sup along the δ*-governing direction IS B (lineIncidence_spectral: the surviving core is the worst-case incomplete char sum = an L∞ sup). Recoupling now a theorem (twoD_line_incidence_L2_blind_Linf_isWall).
• D*/m* far-line growth law — the p-independent distinct-γ count: COMPUTE-BOUND dispute (n=16,20,24 give 3,4,5 under both linear n/4−1 and log readings; only n≥32 separates, the documented slow/disputed point; n≥256 for clean separation) — the standing "numerics cannot decide" wall, not newly attackable. The growth law itself remains the sole genuinely off-BGK computable frontier (§6.6), undecidable at feasible n.
• Root-number / multiplicative-dual exact reduction — the wall in a multiplicative hat (Paley-conditional); a reframe face, not a bypass.
• Exact E₅/E₆ producers — char-0 combinatorial, largely subsumed by the landed E₇ (_AvL2_E7ClosedForm); doesn't touch the wall.

---

9. Tooling, build & reproduce

• Build: scripts/pg-warm.sh ONCE, then scripts/pg-iterate.sh <file> (lake env lean, ~30–75s, no lock, parallel). scripts/lake-locked.sh build <targets> for the real build. NEVER bare lake build. pg-iterate treats sorry as a WARNING — always read #print axioms for the specific declaration.
• δ* engines: scripts/rust-pg/ (parallel Rust far-line solver, δ*(μ₁₆,k=4)=9/16); scripts/cuda-pg/ (CUDA, n=32 in seconds, exact to n=38); mine (unified delta*-grind CLI, --live TUI). ⚠️ both compute the far-line upper bound (Plotkin proxy) — mind the b∈[k,s) direction-cap that produced the retracted "climb to capacity" artifact; use FULL-direction orbcount.
• Probes: scripts/probes/prize_workspace.py, probe_farline_incidence_exact.py, probe_subsetsum_grows_refutes_bchks.py, probe_dstar_pdependence_cliff.py, probe_spectrum_central_even_card.py, probe_dc_essential.py.
• Logs/docs: DISPROOF_LOG.md, docs/kb/deltastar-444-* (BCHKS-correct-object / prize-regime-established / audit-corrections / empirical-formulas-and-bridges / LANDED-bricks-API / wall-constant-trajectory), docs/wiki/residual-census.md. Cone guide: ProximityGap/CLAUDE.md.

---

10. How to attack (guidance for the next agent) + honesty contract

1. Read §0.0 (the ON-BGK verdict), §4 (meta-theorem), §8 (dead ledger), §11 (audit) FIRST. Do not re-run any second-order/moment/energy/phase-descent/census/thinness-gate method — all proven capped. Do not generate another "closed-form δ* conjecture" (190+ refuted) or another "off-BGK escape" (the over-det/combinatorial routes are PROVEN to collapse to Johnson or equal the wall, §0.0/§6.2–6.4).
2. The prize = ONE inequality (§6.1): char-p E_r(μ_n) ≤ (2r−1)‼·n^r at r≈ln q = M ≤ C√(n log m) = BGK at the Burgess barrier. The char-0 half is ALREADY closed for all r (gaussianEnergyBound_dyadic, §6.0) — so the entire residual is the char-p excess W_r ≤ slack_r at deep r, which has no in-tree handle (it IS the wall). Do not re-grind char-0.
3. Use the MANDATORY DC-subtracted A_r (§2). Numerics cannot decide the prize (§3): a closure needs a proof, and the proof needs external analytic NT.
4. Any winning method MUST be b-sensitive + deterministic-archimedean + genuinely L-infinity (§4) — and, by the two-sidedness (ERM-at-r ⟺ M ≤ √((2r+1)n)), must directly bound the char-p sup-norm at deep r. There is no in-tree shortcut.
5. Honesty is mandatory. Tag every claim PROVEN(axiom-clean per declaration)/REFUTED/CONJECTURE/probe-only; verify multi-prime at proper subgroups (never the full group); exclude X^{n/2}=±1; a refutation is a win; never call the core closed.

Bottom line (2026-06-16, late). The prize is OPEN and ON-BGK: the campaign's own exhaustive two-pronged assault (get around the wall / prove the wall is real) concluded, with axiom-clean bricks, that there is no way around the wall (every off-BGK route refuted or capped: the p-independent over-det count is Θ(n³) ≫ budget and collapses to Johnson; single-orbit and dyadic-recursion escapes refuted; the char-free complete-homogeneous count is super-poly so its crossing is Johnson-side) and the wall is real and two-sided (method-necessity proven; floor lower-bound and moment upper-bound shown to be the same object via ERM-at-r ⟺ M ≤ √((2r+1)n)). The prize is exactly the char-p Lam–Leung / BGK √-cancellation E_r(μ_n) ≤ (2r−1)‼·n^r at r≈ln q≈89, n=2³⁰ — proven in char 0 (Lam–Leung; E₂..E₇ exact + the Bessel I₀(2y)^m ≤ exp(my²) face) and numerically verified for n≲40, OPEN at prize scale. Honest stance: this is the 25-year-open analytic-NT wall at the Burgess barrier; no in-tree path to a complete proof exists — a genuinely new sum-product / effective-equidistribution / monodromy input is required, and none in the literature crosses n^{0.989}→n^{1/2} at β=4. What the campaign did achieve is decisive and rare: it eliminated every elementary/second-order/off-BGK route as a theorem, built the full axiom-clean substrate (energy ladder to E₇, the Bessel char-0 face, the spectrum-structure/minor-degree/orbit bricks, the necessary-condition theorem, the tight two-sided reduction), corrected the record (BCHKS-vacuous; capacity−δ*=m*/n; the proxy artifact; phantom bricks), and proved numerics cannot settle it. The evidence is mildly favorable to the floor being TRUE (char-0 K_eff→1 from below, a_r≤1 Lam–Leung, the wall-constant C≈1.25 non-divergent with the n=128 turn-down) — but "mildly favorable" is not a proof. The prize is open.

---

11. AUDIT — verified bugs, retractions, laundered values, phantom bricks

Full detail: docs/kb/deltastar-444-audit-corrections-2026-06-16.md. Items below independently re-verified this pass (commits resolve, files checked on disk).

Bugs fixed

• Master-gap off-by-one: capacity − δ* = m*/n (was (m*−1)/n in _BridgeB01/B04); δ* = 1−s/n (orbcount's 1−(s−1)/n was a display bug). Rebuilt in _MasterGapOffByOneCorrected (d92366552). ⚠️ Residual inconsistency: the freshly-landed _BchksF6 docstring still writes 1−ρ−(M_cross−1)/n — reconcile to m*/n.
• D*(1) p-DEPENDENCE: reported "exact p-independent 3936" is wrong (3936@65537 vs 3984@1048609). Only the over-det binding counts (D*(2)=89, D*(3)=9) and m* are p-independent.

Retractions (claims withdrawn)

• "δ* climbs to capacity / m*~log n" — engine b<s direction-cap artifact; far-line δ* is a Johnson-locked proxy (m*=n/4−1 LINEAR). The GPU growth law s*(n)=n/2+1−2(⌊log₂n⌋−3) and δ*→0.594 were the same artifact; the "dyadic-defect law" was a 3-point/3-parameter overfit (zero residual by construction). n=32 is genuinely DISPUTED (m*∈{4,5}, δ*∈{0.594,0.625}), C(32,s) enumeration times out ~77 min.
• "prize ⟺ BCHKS-1.12 (tight)" (1c1712743) — vacuous, superseded by Sumset-Extremality (§0).
• _AntipodalPlotkinHalfCap "δ*≥1/2 cap" — larp, docstring corrected to the Johnson-lock-proxy truth.
• Quadratic "plateau-floor failure mechanism" (n/4−1)² — premise FALSE (it's a shoulder, not a floor; the corrected picture is prize-favorable).
• "M→δ* exponent-transfer bridge axiom-clean" — does NOT compile; retracted.

Exhaustive citation sweep (this fold): ~90 cited identifiers verified — ~64 real-clean (0 sorry), ~9 real-with-named-residual-sorry (honest), 19 correctly-flagged-phantom; net exactly ONE new mis-citation: EffectiveTZLowerBound (with effectiveTZ_to_supply/WF407_B3_s128.lean) — does NOT exist; the REAL B3/s=128 artifacts are KKH26ThornerZaman.TZPrimeSupply + consumer kkh26_mcaDeltaStar_le_of_TZ in Frontier/ThornerZamanS128.lean/ThornerZamanInstance.lean (sorry=0). Fixed in §3; the KB doc wf407-B3-s128-thorner-zaman-ceiling.md needs the same rename. No false-phantoms (every phantom flag re-confirmed absent). Adversarial crack-check of the ON-BGK verdict returned ZERO cracks (necessity, second-order no-go, and char-sum vacuity all in-tree sorry-free; the open core is correctly carried as a named OPEN predicate).

Phantom bricks (cited as landed axiom-clean but ABSENT — verified absent this pass via git grep on all branches)

• ⚠️ The S1/S6 "char-p energy-transfer / most-hopeful-state" bricks (2026-06-17 comment, this pass): prize_of_transfer_slack, CharPEnergyTransferWithSlack, _wfS1_transfer_slack_prize, good_of_maxnorm_lt, and the S6 "bounded-Betti Deligne on the config variety" brick — none on any branch (git grep, 60+ refs). The S1 reduction's math is sound (E_r ≤ K^r·Wick uniform ⟹ M ≤ √(2eK·n·ln q) = prize, the standard moment consumer) — but it is the BGK wall re-framed positively (uniform K=O(1) energy bound = the char-p Wick bound = the two-sided sup-norm), and the claimed axiom-clean Lean theorems are unverifiable here. S6 is refuted on the math (not just phantom): V_r={x∈μ_n^{2r}:Σε_i x_i=0} with "bounded Betti C(2r,r)≤4^r independent of n,p ⟹ K~4" hits the μ_n-subgroup trap — imposing x_i∈μ_n makes V_r 0-dimensional (Deligne main-term is the count, vacuous), and dropping it forces the subgroup-indicator into m=(q−1)/n=2¹²⁸ characters whose sum reintroduces the n/q-dependence = the BGK wall ("completion-sum cancellation EQUALS the open BGK content"). Bounded Betti is real for one toric sum; the bridge to the μ_n energy is the m-character sum = the wall. (The empirical K_eff≈0.6 at n≤256 is real floor-favorable evidence; the proof of uniform-K is the wall.)
• ⚠️ The ON-BGK verdict's bricks (2026-06-16, comment, this pass): _DstarGrowthLaw (dStar3_gt_budget, offBGK_overdet_caps_below_window), _OPSingleOrbit (OP_single_orbit_refuted), _DyadicRecursionDstar, PrizeEquivalencePin (no_second_order_route, mcaThreshold_eq_iff, prizeFloor_eq_value_iff_bindingCount_brackets), FloorResonanceEnergyBridge — none exist on any branch. The ON-BGK conclusion stands on the VERIFIED bricks (_MomentLadderExceedsPrize, _EnergyRatioMonotoneReduction, KambireDeepBandFloor/KambireExponentialGap, OverdetIncidenceMaxClosedForm) + standing numerics, but the comment's specific axiom-clean citations were not landed. Treat the verdict's conclusion as well-supported, its brick names as partly phantom.
• Commits: 38e71fce8, 80047be6 (short-hashes, no object).
• Files: _DefectOnsetOvershoot, SubsetSumThreePowExact (re-created honestly as _AttackDefectOnset_EnergySandwich / _AttackThreePow_SubsetSumExact); _MomentMethodPrizeDepthNoGo, BadScalarsPinnedScalars, _wf5R2_KMEdgeMomentReduction, _wf6C1_chebotarev_badprime_count, _MultUpperAgreementBinom, _CoreR3SpurLamLeungGate, _RatioPerm, RepCountFiberGcdBound, LamLeungSlackExact, DeltaStarConditionalEntropyPin, DeepBandSpectrumCentralParity, _S2NonSymTower; the combined-range Sweep_A41-A45.lean / Sweep_A46-A48.lean (only the per-index Sweep_A41/A42/A44/A45/A46/A47/A48 files exist — those ARE present, so the "A41–A48 char-0 rigidity chain end-to-end" claim is partly supported, partly phantom). Docs BDERIV_FULL_108.md, deltastar-444-CLOSED-CONJECTURE-2026-06-15.md. Treat any result resting on these as unsupported until re-landed.

Overclaims softened

• LamLeungUnconditionalQ proves the Lam–Leung structural foundation (linearIndependent_pow_le), not the full E_r≤(2r−1)‼n^r bound (still open char-p).
• _Close27_* "decides opposite horns" = omega/decide/rfl tautologies — the "decision" is prose-only.
• A6 "Lang–Weil tractability" → the valid object is a Bézout/degree ROOT-count (V_r is 0-dim ⟹ Lang–Weil VACUOUS); the bound stands, the point-count framing is the trap.
• E_r > Wick ∀r≥4, "0/10 lenses refuted", M4 C_prize~0.5 — Fermat artifact (W_3=W_4=0 generically) / rate-limit-cut (4/10) / shallow-prescreen, respectively.
• RepThree threshold corrected 12^{n/4} → 52^{n/4} (the [5,1] degenerate zero-sum makes RepThree(μ_8) fail at p=313, O225).

_{🤖 Authored by Claude (Opus 4.8, 1M ctx) from a full mine of #407 (348 comments) + this issue's 359-comment grind (12-chunk fan-out + verification workflow) + the KB dossiers + git ground truth + independent re-verification (commits resolved, files checked, probes re-run). Cited Lean paths verified present; phantoms verified absent; results tagged by status; no fabricated closure.}