δ* completion gate: production theorem assembly and independent axiom audit

[lalalune]

Objective

Own the final integration gate for the actual prize theorem. This issue stays blocked by mathematical CORE until a production-regime input lands, but its verification contract is actionable now.

Completion evidence required

• Exact production-parameter statement for mcaDeltaStar/the sponsor-equivalent formulation.
• Both inequalities assembled through the canonical threshold ledger.
• Targeted pg-iterate checks, locked module build, and repository validation.
• #print axioms limited to the accepted foundational set; zero sorryAx, no laundering through an asserted residual.
• Independent audit that the theorem matches the prize quantifiers and parameter regime.
• Dossier, issue Prove δ* — complete research dossier (v3) for the RS proximity-gap prize (successor to #464) #466, discussion, and project state updated from the verified commit.

A toy instance, bracket, equivalent open Prop, or conditional theorem does not satisfy this gate. Campaign work belongs only on research/proximity-prize.

[lalalune]

Gate audit LANDED (da123beea on research/proximity-prize; branch codex/g82-production-gate-conditional, commit 203395261): docs-only — the conditional production gate this issue's contract describes already exists in-tree, one hypothesis deep, so no new Lean was added (duplication avoided).

Where the gate lives (all axiom-clean, re-verified with pg-iterate from tip a42fe9e40, 7/7 #print axioms ⊆ {propext, Classical.choice, Quot.sound}):

• Frontier/_PrizeShapeRateHalfBracket.lean: at literal production parameters (n=2^30, k=2^29, ε*=2^-128, Lucas-certified prize prime P = 2^30·(2^128+192)+1) — firstPrime_rateHalf_deltaStar_eq_thirtyOneSixtyFour_of_predecessor_count: ONE wall hypothesis (per-stack bad-scalar count ≤ 2^30 at radius 31/64 − 2^-30) ⟹ mcaDeltaStar … epsStar = 31/64 exactly; plus the unconditional bracket 178956971/2^30 ≤ δ* ≤ 31/64.
• Companions: _PrizeShapeLowRateExactPins.lean (unconditional low-rate pins), _PrizeShapeGrandChallengeRefutation.lean, _R157PuncturedListBudgetConsumer.lean (generic consumer; deliberately not production-instantiated — one-sided floor, strictly weaker than the exact pin).

Audit note: docs/kb/deltastar-466-g82-production-gate-audit-2026-07-10.md — full dependency chain from wall hypothesis to conclusion + honest gaps (the hypothesis IS the open wall; 31/64 is the current quotient-mechanism ceiling, not sponsor-determined; per-stack quantifier shape recorded). Also restores a dropped ArkLib.lean import line for _G85EndpointAssemblyEquiv.lean (pre-existing drift).

Net for #507: the gate is one-hypothesis-deep and its verification contract is auditable today; it remains blocked by mathematical CORE (#505) as designed.

[lalalune]

G84 red-team probe LANDED (251331257 on research/proximity-prize; branch codex/g84-wall-hypothesis-probe, commit aea22f5b4): small-scale falsification sweep of the gate's ONE wall hypothesis (_PrizeShapeRateHalfBracket.lean L413-421: per-stack mcaEvent bad-scalar count at predecessorRadius 2^30 (31·2^24) bounded by 2^30).

Key structural finding: for n < 64 the literal lattice predecessor of 31/64 coincides with the predecessor of 1/2 (the rung the file itself refutes), so both literal and structural (t=k+2) translations were probed; n=64 is the smallest faithful cell.

Results: 14/17 cells REFUTED at analogue — at small fields (p = poly(n), margin ≤ 2) the worst stack typically has EVERY field scalar bad (smallest exact witness: n=8, p=17, all 17 γ bad; independently recounted). 3 cells survive (n=8 structural).

Honest verdict: the hypothesis shape is NOT scale-free — but first-moment scaling shows the refutations are small-field artifacts: heuristic bad count ~ C(n,t)·p^(k−t+1) ≫ n at p=poly(n), yet ~2^(−1.6·10^9) at production (margin 2^24+1, p ~ n·2^128). Production is therefore neither refuted nor supported by small scales; any proof of the wall hypothesis must exploit the large-field/large-margin regime p ≳ C(n,t)^{1/(t−k)} — scale-free counting arguments cannot do it, and small-n 'sanity checks' of this hypothesis are structurally misleading. A faithful next probe needs p ≫ 2^61 at n=64 with sampled γ.

Files: scripts/probes/probe_rate_half_predecessor_count_small_scale.py, docs/kb/deltastar-466-g84-wall-hypothesis-smallscale-probe-2026-07-10.md.

[lalalune]

G85p LANDED (7aa87e208 on research/proximity-prize; branch codex/g85-wall-hypothesis-largefield, commit 5190b24a8): faithful large-field collapse-curve probe of the gate wall hypothesis, following up G84.

Method: exact affine-in-γ reduction (per t-subset the bad condition is 2 GRS parity checks ⟹ ≤ 1 candidate γ per subset) giving certified lower bounds; 10^4 seeded uniform samples per stack; and a planted channel with an exact linear law: r bad scalars plantable iff rank < 2(n−k), so r_max = 2(n−k)/(t−k) − 1 (15 at n=32, 31 at n=64, ~63 at production).

Collapse curve: n=32 refutations end between 2p* and 8p* (p* = C(n,t)^{1/(t−k)}), exactly matching G84's first-moment prediction; by p_count only the linear planted floor remains, and r above the floor is provably unplantable (rank saturates). n=64 is CONSISTENT at every magnitude through 2^80 (sub-p* saturation could not be certified there — coverage limits; the measured collapse is carried by n=32).

Production evidence (not proof): the combinatorial channel extrapolates to ~2^(−1.58·10^9); the only surviving large-field channel is the linear planting cap ~63 ≪ 2^30 budget. New structural fact: any production counterexample must beat generic-rank planting — super-generic rank collapse or subset correlations are now the only open attack shapes; generic planting is dead. The wall hypothesis stays OPEN.

Files: scripts/probes/probe_rate_half_predecessor_count_largefield.py, docs/kb/deltastar-466-g85-wall-hypothesis-largefield-probe-2026-07-10.md.

[lalalune]

⚠️ SYZ1 LANDED (4351c0d83 on research/proximity-prize): the gate's wall hypothesis is REFUTED at analogue scale, by a construction that transfers to production.

The degenerate-subset channel: a t-subset S where both u₀|S and u₁|S are codeword restrictions donates one literal mcaEvent-bad scalar γₓ = −d₀(x)/d₁(x) per off-S point x (line agrees with v₀+γₓv₁ on S∪{x}; pairJoint fails there). D subsets cost 2(t−k)D syndrome rank out of 2(n−k) and stack exactly additively: certified counts D·(n−t) at n=32 (42 > budget 32 with D=3) and n=64 (450 > 64 with D=15), every scalar verified against the literal mcaEvent (agreement set + ¬pairJoint, two independent interpolation paths), witnesses printed. The channel is p-free (exact algebra — unlike G84/G85's small-field channel, it does NOT collapse at large fields; verified identical at p ≈ 2^30…2^60). Subset overlap is no obstruction (t > n/2 cells work).

Production transfer: at the gate shape (t = 553648129), n−t ≈ 5.2·10^8 per subset, rank budget admits D ≤ 30; D = 3 already yields ≈ 1.56·10^9 > 2^30. So hcount of firstPrime_rateHalf_deltaStar_eq_thirtyOneSixtyFour_of_predecessor_count is unsatisfiable — the exact-pin route at 31/64 dies the same death as the half-predecessor rung, one rung down.

Untouched: the unconditional bracket 178956971/2^30 ≤ δ* ≤ 31/64, packing ceilings, ladder floor. This narrows honestly: the quotient-mechanism CANNOT be made exact at 31/64 via the all-stack scalar cap; the pin needs a guarded count (excluding degenerate-subset stacks — exactly the G86/G87 syzygy class), a different counting object (distinct witness codewords), or must live with the bracket.

Recommended next Lean artifact: formalize ¬hcount via the explicit D=3 construction (only nontrivial ingredient: forcing distinctness of enough γₓ, constructively). kb: deltastar-466-syz1-predecessor-cap-refuted-2026-07-10.md; probe: scripts/probes/probe_syzygy_configuration_bad_counts.py. Tag SYZ1 (G88/G89 were taken by concurrent lanes).

[lalalune]

SYZ2 LANDED (e14d04bf3 on research/proximity-prize; branch codex/syz2-predecessor-cap-refutation-lean, commit 0744ce79c): the degenerate-subset pencil is now machine-checked, axiom-clean (9/9 [propext, Classical.choice, Quot.sound], independently re-verified).

What is now a Lean theorem (Frontier/_SYZ2PredecessorCapRefutationCore.lean):

• The full channel: pencil_line_agrees (a), not_pairJointAgreesOn_insert (b — uniqueness on the v₁ side alone suffices), mcaEvent_pencil (literal mcaEvent with witness insert x S), counting forms (c), and the fully constructive stack builder (d): any code, any codewords, any t-subset with the k-uniqueness property, injective f off S ⟹ ≥ n−|S| bad scalars, pencil γₓ = −f(x).
• rsCode_eq_of_agree_on_card_le: RS interpolation uniqueness (was missing in-tree).
• Production instantiation: firstPrime_production_singleSubset_badScalar_lower — an explicit stack at the LITERAL gate parameters with ≥ 520,093,695 mcaEvent-bad scalars (≈48% of the 2^30 cap from a single degenerate subset), kernel-checked.
• OverBudgetDegenerateStackExists (named residual, exact hcount shape) + firstPrime_predecessor_cap_refuted_of_overBudget_stack: that residual ⟹ ¬hcount. The D≥3 stacking (probe-verified additively at n=32/64, SYZ1) is NOT yet a Lean witness — overlapping-subset compatibility + cross-subset pencil distinctness needs structured coset blocks or a formal counting argument; per the honesty rule no ¬hcount is claimed.

Net for #507: the exact-pin hypothesis is now one named, probe-refuted-at-analogue residual away from formal death; and even unconditionally, half its budget is consumed by one machine-checked stack. The exact-pin program should be considered redirected (guarded count / different counting object / live with the bracket).

[lalalune]

🔴 SYZ3 LANDED (efb83bef9 on research/proximity-prize; branch codex/syz3-overbudget-stack-witness, commit 68b0fef67): the gate's wall hypothesis is now FORMALLY REFUTED — machine-checked, axiom-clean (5/5 [propext, Classical.choice, Quot.sound], independently re-verified, ~30s elaboration).

Theorems (Frontier/_SYZ3OverBudgetStackWitness.lean):

• overBudget_degenerate_stack_exists : OverBudgetDegenerateStackExists — an EXPLICIT three-subset degenerate stack over the literal prize prime carrying 3·31·2^24 = 1,560,281,088 > 2^30 distinct mcaEvent-bad scalars at predecessorRadius (2^30) (31·2^24).
• firstPrime_predecessor_cap_refuted : ¬ (∀ u : WordStack …, #{γ : mcaEvent … (u 0) (u 1) γ} ≤ 2^30) — the literal hcount of firstPrime_rateHalf_deltaStar_eq_thirtyOneSixtyFour_of_predecessor_count is FALSE.

Consequences for this gate:

1. The conditional exact pin δ* = 31/64 via the predecessor scalar cap is permanently closed — its hypothesis is a theorem-level falsehood, mirroring the file's own half-predecessor refutation one rung down. Recommend updating the file's 'exact residual' section and the dossier accordingly.
2. Untouched and still the production state of the art: the unconditional bracket 178956971/2^30 ≤ δ* ≤ 31/64, the ladder floor, and all packing ceilings.
3. Any future exact-pin program must count a guarded object (the degenerate-subset/syzygy class isolated by G86/G87 is exactly the killer channel and is now fully formal end-to-end: SYZ1 probe → SYZ2 pencil + production single-subset bound → SYZ3 witness).

Kernel-scale formalization notes (for future workers at Fin(2^30)/158-bit-prime scale) are in the file header: avoid defeq reduction of the prime abbrev, use degree_mul_le over natDegree chains, per-slot binaryPow+decide instead of cert-lemma matching. Arc credits: SYZ1 probe evidence, SYZ2 channel, SYZ3 witness.