diff --git a/incoming/claude-bundle-v3-native-copies-20260928/K3_SIDE24_LB/UPPER2D/H3_closure/H3_CLOSURE.md b/incoming/claude-bundle-v3-native-copies-20260928/K3_SIDE24_LB/UPPER2D/H3_closure/H3_CLOSURE.md new file mode 100644 index 000000000..49d8fab87 --- /dev/null +++ b/incoming/claude-bundle-v3-native-copies-20260928/K3_SIDE24_LB/UPPER2D/H3_closure/H3_CLOSURE.md @@ -0,0 +1,261 @@ +# H3 CLOSURE — the normalizer lower bound Z_r ≥ c_Z r² (U2D-UPPER) + +**Date:** 2026-09-13. **Verifier:** H3-closure line (adversarial verification mode). +**Candidate closure under test:** Theorem G.3.1 of +`/mnt/agents/output/SIDE24_gap_fill/SIDE24_GAP_FILL_SUPPLEMENT.md` (lines 1534–1567), +with Part G.1–G.2 (lines 1446–1532) and G.7 (lines 1632–1653) as its proof context. + +**VERDICT: CLOSED for the frozen upper-campaign law, at theorem grade, with one +named amendment and one named non-explicit constant.** + +- The supplement's Theorem G.3.1 *as printed* is stated for the **3D** side-24 + field (conventions line 9: `T^3_24`; weight line 11: `1{H_M≺0, ind(H_S)=2}`; + 8 raw pins). It does **not**, as a cited statement, cover the frozen 2D law. +- The **2D instance of the same theorem** is the manuscript's Theorem + 3.11(i)–(ii) (`manuscript_v2_2026-09-13.md` line 200–207, stated explicitly + "For the typed pair-Palm law (Preliminary 2.5)"), and its proof is the + dimension-generic Part-G argument re-run in dimension two. Every step of that + argument is verified or certified below (§2); nothing in the argument is + 3D-specific. +- The assembly's transcribed limit object + `c_0 = E[|α_M det Q_M|·|α_S det Q_S|·1{Q_M≺0, α_M<0} ∩ {ind_S=2}]` carries the + **3D index convention**: on the 2D field `ind_S=2` reads `H_S ≺ 0` (S a + *maximum*), whose limit probability is **0** — read literally, the transcribed + formula gives c_0 = 0 and does **not** close H3 (demonstrated, §4). The + correct 2D typing (S a saddle ⟺ `det H_S < 0` ⟺ index 1) gives the corrected + limit object, certified here at 60+ digits: + + c_0 = E[ U² · 1{U<0} ], U ~ N( −(6/5)·a₂ , a₄ − a₂² ), + c_0 ∈ [3.230978535287004948096246569018163150764858010558710998470, + 3.230978535287004948096246569018163150764858010558710998471] (±5e-97 tail) + + in particular **c_0 ≥ 3.230978535287004948096246569018163150765 > 0 + (certified, interval arithmetic with certified spectral tails)**. + +--- + +## 1. Scope verification (pin by pin) + +Frozen upper-campaign law (assembly H3): `Q_r` = continuous Gaussian regression +version of the six-pin conditioning `f(M)=b=6/5`, `f(S)=b−r³/6`, +`∇f(M)=∇f(S)=0` at `M=(−r/2,0)`, `S=(r/2,0)` on the normalized periodized +side-24 **2D** Bargmann–Fock field; `W_r = |det H_M det H_S|·1{M max, S saddle}`; +`Z_r = E_{Q_r} W_r`; `dP_r = W_r dQ_r / Z_r`. + +| Coordinate | Assembly H3 | Manuscript Preliminary 2.5 (2.7) | Supplement G.3.1 | Verdict | +|---|---|---|---|---| +| field | periodized BF, `T²_24`, weights `e^{−|k|²/2}` on `(π/12)Z²` | same (lines 13, 110) | `T³_24`, `(π/12)Z³` (line 9) | **G.3.1 3D; 2D instance = Thm 3.11** | +| stations | `M=(−r/2,0)`, `S=(r/2,0)` | identical (line 81) | `M=x−rt/2`, `S=x+rt/2`, `t∈S²` | match (2D axis-aligned frame) | +| pin count | 6 (value+gradient at M,S) | 6 (V_r, (2.7)) | 8 (3D) | match in 2D | +| pin values | `b=6/5`, `b−r³/6`, gradients 0 | identical (lines 81, 112–115) | `b`, `b−κr³/6` | match with κ=1 | +| pin basis | raw six pins ↔ corrected V_r | corrected basis V_r (2.7) | corrected basis (G.1.3) | **same σ-algebra: det B_r = r⁻⁵ ≠ 0** (§2.S1) | +| weight | `|det H_M det H_S|·1{type}` | `W_r = |det H_M det H_S| 1_type` (line 115) | same (line 1539) | match | +| typing | M max, S saddle (2D: `H_M≺0`, `det H_S<0`) | "maximum at M and a saddle at S" (line 110) | `H_M≺0, ind(H_S)=2` (3D index-2 saddle) | match in 2D convention; **the transcribed c_0 formula's `ind_S=2` is the 3D convention, wrong if read in 2D (§4)** | +| mark | `b=6/5>0`, κ=1: compact positive singleton | `b=6/5` standing (line 81) | "uniformly on compact positive (b,κ) sets" | covered (§2.S9) | +| RN structure | `P_r = W_r dQ_r/Z_r` | `dP⁰/dP = W_r/Z_r` (line 115) | (A.1) | match | + +The identification of this exact law with the campaign's estimand of record is +already adjudicated: `REVIEW_LPW/RA_R1_R6.md` §R1(a), items 1–7 (all exact +match; sole residue there — the GP-DER-118 body — is a provenance note, not a +mathematical input to H3). + +## 2. The assembled 2D proof of Theorem G.3.1(2D) — step grades + +Statement proved: for the frozen law, uniformly on compact positive (b,κ) sets +(in particular at (6/5, 1)): `c_Z r² ≤ Z_r ≤ C_Z r²` and `E_{Q_r}[W_r²] ≤ C r⁴` +for `0 < r ≤ r_max`, with `c_Z = c_0/2` explicit and `r_0 > 0` (the small-r +range) existential (see §5 for the exact honesty boundary). + +- **S1 — Basis invariance (machine-verified, symbolic).** The change of basis + `P6_r → V_r` has `det B_r = r⁻⁵ ≠ 0` for all `r>0`; Gaussian conditioning + depends only on the pin span (regression equivariance — analytic). Verified: + H2 `pin_transform.py` selftest P5 (re-run by this closure, both modes + byte-identical); independently, `REVIEW_LPW/RA_R1_R6.md` item 3 (12 fail-closed + checks, PASS), including pinned-value agreement + `(b,0,0,0,0,−1/6)` and `det T_r = −r⁻⁵`. **G.3.1's proof, which conditions on + V_r, therefore proves the theorem for Q_r (raw pins) unchanged.** +- **S2 — Endpoint kernels (machine-verified, dimension-free).** + `h(∓r/2) = ∓(1/r)∫(r/2∓s)h'(s)ds` on the zero-mean class: + `verify_palm_soft_factors.py` (K1), re-run by this closure: + `ALL_ASSERTIONS_PASS`, normal/`-O` byte-identical. +- **S3 — Soft factorization (machine-verified, dimension-free).** + `det H = rD`, `D = α det Q − r βᵀ adj(Q) β`; in 2D `Q=q` scalar, + `D = αq − rβ²`: script item (S1), same PASS. +- **S4 — Value window (machine-verified).** `f(S)−f(M) = ∫(w²/2−r²/8)g'''dw`, + kernel mass `−r³/12` (script item K2, PASS). Consequence: the corrected pin + forces `∂₁₁₁f(0) = 2κ` in the blow-up (`−(1/12)·∂₁₁₁f(0) = −κ/6`). +- **S5 — Corrected-pin floor (analytic + certified endpoint + numeric + corroboration).** 2D limit jet `V_0 = (f, ∂₁f, ∂₂f, ∂₁₁f, ∂₁₂f, ∂₁₁₁f)(0)`: + six **distinct** derivative functionals; Gram SPD by full spectral support + (manuscript Def 2.2 / Lemma 3.1 — certified there; analytic argument: + independence of exponentials/monomials, dimension-free, identical to + supplement G.1.1). Uniform floor on `(x,t,r)` compacta: continuity + + compactness (supplement G.1.3, dimension-free). **Certified endpoint of + record:** `λ_min(Γ_0) > 31/250 = 0.124` (ten exact Sylvester minors, + LPW_CONSTANT package, reproduced in its falsifier F2), with certified modulus + `‖Γ_r − Γ_0‖_F ≤ 19.071156·r` on `[0, 1e-5]` → uniform floor `0.12380…` on + `[0, 1e-5]`, inherited by the six-pin block (Cauchy interlacing). + This closure adds the explicit limit-Gram determinant certificate + `det G_0 = (a₄−a₂²)(a₂a₆−a₄²)a₂³ ∈ [12−2.4e-100, 12+2.5e-100] > 0` + (CK4, iv path) and NUMERIC corroboration: the 6×6 `Cov(V_r)` smallest + eigenvalue `≥ 0.0391` on `r ∈ {0.1,…,0.005}` (CK8a; labeled NUMERIC). +- **S6 — Upper bounds (analytic; independently derived for this law).** + `W_r ≤ r²|D_MD_S|` with bounded Gaussian conditional moments (S3 + S5 floors) + ⇒ `Z_r ≤ C_Z r²`, `E W_r² ≤ Cr⁴` (Cauchy–Schwarz). Independently derived for + exactly this six-pin 2D law in the LPW candidate §9 with `C_Z = 4B_3`, + reviewed PASS (RD_R4_R5 §R5(i), polarity confirmed). +- **S7 — Lower bound (analytic, verified line-by-line in 2D).** + `Z_r/r² = E|D_MD_S|1{type}`. The scaled soft variables converge in law under + `Q_r` (Gaussian regression continuous in the pin Gram — SPD by S5 — and in the + bounded pin values): `α_M → −κ`, `α_S → +κ` **deterministically** (the pins + fix `∂₁₁f(0)=0` and `∂₁₁₁f(0)=2κ`; the conditional variances of the α's are + `O(r²·poly)` → 0; NUMERIC: `Var(α_M|pins) = 1.2e-5` at `r=0.005`, monotone in + r, CK8 table), `β's → ∓(1/2)∂₁₁₂f(0)`, `q_M, q_S → U = ∂₂₂f(0)`. The type + events: M max ⟺ `q_M<0 ∧ D_M>0`; S saddle ⟺ `D_S<0`; both converge to the + single open event `{U<0}` (since `D_M→−κU`, `D_S→+κU`), whose boundary + `{U=0}` is null under the limit law (`s² = a₄−a₂² > 0` certified, CK5b). The + pinned directions `α_M=−κ<0`, `α_S=+κ>0` lie strictly inside the event — + the partial degeneracy of the limit law is harmless. Weak convergence + + uniform integrability (Gaussian tails dominate the degree-2 polynomial + integrand, uniformly via S5's ceilings) give `Z_r/r² → c_0`. Note: the + supplement's phrase "nondegenerate centered Gaussian" for the scaled-variable + limit is imprecise (the α-coordinates degenerate to ±κ); the load-bearing + nondegeneracy is that of the transverse block `U`, which holds and is + certified. Verified. +- **S8 — c_0 > 0 (machine-certified, this closure).** §3. +- **S9 — Compact-mark uniformity (analytic; coverage of b=6/5 confirmed).** + `c_0(b,κ) = κ²·E[U²1{U<0}]` with `U ~ N(−b a₂, a₄−a₂²)` is continuous in + `(b,κ)` and strictly positive on every compact positive mark set + (`s²>0` certified; `P(U<0) = Φ(ba₂/√(a₄−a₂²)) > 0`); the singleton + `(b,κ)=(6/5,1)` is compact positive. The remainder of the uniformity + argument (convergence continuous in marks; positivity of `Z_r/r²` at fixed + `r` under the nondegenerate pin law; compactness) is dimension-free and + applies verbatim. **Coverage of b=6/5: confirmed.** +- **S10 — A.4.4–A.4.6 audit.** These lemmas are the capture/escape arithmetic + feeding G.5/G.7, **not** the normalizer; their machine audit + (`verify_a44_a46_flow_v1.py`: 17 checks at R∈{1,2,5,50} + symbolic + Young/eigen-slope chains; re-run by this closure: PASS, both modes + byte-identical) supports the G.7 corollary chain only. The normalizer + theorem itself consumes no A.4.x step. + +## 3. The limit object c_0 — certified computation on the exact field + +By S7, `c_0 = E[|α_M q_M|·|α_S q_S|·1{type-limit}] = κ²·E[U² 1{U<0}]` with +`U = ∂₂₂f(0)` under the limit pins. Gaussian regression (the odd covariances +vanish exactly — sine sums at `s=0`, CK3): + +`m = E[U|V_0] = −(6/5)·a₂`, `s² = Var(U|V_0) = a₄ − a₂²`, + +with `a_{2m} = (1/Z₁)Σ_{k∈(π/12)Z} e^{−k²/2} k^{2m}` the **exact finite-torus +moments** (never planar: `1−a₂ = 9.65254179896e-123 > 0` certified, errata +2(b) of record). Closed form: + +`c_0 = (m²+s²)·Φ(−m/s) − m·s·φ(−m/s)`. + +**Certified value (iv path of `cov_exact.py`, 100 dps, certified spectral +tails carried; Φ by in-program certified power series with geometric tail +certificate):** + + c_0 ∈ [3.23097853528700494809624656901816315076485801055871099847056563983657866727484113533199277175345604743007, + 3.23097853528700494809624656901816315076485801055871099847056563983657866727484113533199277175345608823472] + +(interval width < 5e-97). **Certified lower bound: c_0 ≥ 3.230978535287004948096246569018163150765 > 0.** + +Cross-checks (all pass, see certificate/falsifier transcripts): +- planar diagnostic (`a₂=1, a₄=3`) gives `3.23097853528700494809624656901816315076485801055871099847057…`, + inside the certified interval (CK6d) — finite-torus correction `< 1e-95`; +- independent falsifier engine (direct lattice sum at N=96, certified tail + `4.1e-129`; Poisson/Hermite identity; `mpmath.ncdf`): reproduces + `c_0 = 3.2309785352870049480962465690181631507648580105587…` (F1); +- full 6×6 regression solve agrees with the 2×2 reduction to `<1e-85` (CK5d/e); +- the same regression structure appears independently in the LPW_CONSTANT + package: `E[J|U_0] = (−a₂b,0,0,0)`, `Cov(J|U_0) = diag(a₄−a₂²,…)` (matches); +- NUMERIC (labeled): finite-r Monte Carlo of `Z_r/r²` under the exact + conditional law (corrected-pin frame, two independent covariance + implementations — spectral and image-kernel): `3.206, 3.224, 3.229, 3.227` + at `r = 0.1, 0.05, 0.025, 0.0125` (σ≈0.0037), approaching `c_0`; typed-event + probability → `0.80` (`= Φ(−m/s) = 0.801928…`). + +## 4. The named amendment — the transcribed `ind_S=2` + +The assembly's H3 statement quotes the limit object with `1{…}∩{ind_S=2}`, +verbatim from the 3D supplement. On the 2D field, `ind_S=2` is `H_S ≺ 0` +(S a **maximum**), not a saddle. Since `α_S → +κ > 0` a.s. under the limit pin +law, the limit event `{H_S ≺ 0}` is empty up to a null boundary: the literal +formula evaluates to `c_0 = 0` and **cannot** close H3. Demonstrated +executably: at `r = 0.1, 0.05, 0.025, 0.0125`, zero occurrences of +`{H_S ≺ 0}` in `1.5e6×4` and `1.2e6×3` samples from the exact conditional law +(two engines), while the true saddle event occurs with frequency ≈ 0.79–0.80; +Cantelli bound `P(α_S<0|pins) ≤ 2.7e-5 → 0` (CK8c, F3). The assembly must +consume the 2D typing (`S` saddle ⟺ `det H_S<0` ⟺ index 1) and the corrected +limit object of §3. With that amendment the closure is exact — the assembly's +`W_r` typing ("M max, S saddle") already means the 2D event; only the quoted +c_0 display carried the 3D index. + +## 5. Honest grade + +- **Machine-certified (this closure, iv path, certified tails, both modes + byte-identical, mutations caught fail-closed):** exact-torus moments; exact + orthogonality structure; limit Gram determinant > 0; conditional law + `(m, s²)`; `s² > 0`; the certified interval for c_0 (hence c_0 > 0); + dependency hashes of the consumed H2 libraries. +- **Machine-verified (supplement/H2 scripts, re-run here, PASS, byte-identical + two-mode):** kernel identities (K1), value window (K2), soft factorization + (S1/S2), pin-basis determinants `det B_r = r⁻⁵`, `det T_r = −r⁻⁵` + (symbolic); A.4.4–A.4.6 arithmetic (not a normalizer input). +- **Analytic (dimension-free, verified step-by-step):** spectral independence + and compactness floors; regression equivariance; weak convergence + UI; + boundary-nullity; compact-mark uniformity; Cauchy–Schwarz upper bounds + (independently derived with `C_Z = 4B_3` for this law, reviewed PASS). +- **NUMERIC corroboration only (labeled, never load-bearing):** finite-r + Monte-Carlo tables; the V_r eigenfloor grid. + +**Grade: theorem-grade for the assembled 2D statement as written in §2–§3** +(every step either analytic-and-verified or machine-certified; no named +unproved premise is consumed by H3). Two explicit honesty boundaries: +(a) Theorem G.3.1 *as printed in the supplement* is the 3D instance — anyone +quoting it must quote the 2D instance (manuscript Theorem 3.11(i)–(ii)) or §2 +here; (b) `r_0` is existential in the record of record (the convergence S7 has +no certified modulus). A certified explicit radius is within reach of existing +instruments (the pin-block floor is already certified uniformly on +`[0, 1e-5]` via `λ_min ≥ 0.1238…`, LPW_CONSTANT) but certifying a modulus for +the *expectation* is an unexecuted extension — **not claimed**. The NUMERIC +evidence is consistent with `c_Z = c_0/2` already holding at `r ≤ 0.1`. + +## 6. Closure statement the assembly can consume + +> **H3 (2D normalizer lower bound).** Let `Q_r` be the continuous Gaussian +> regression version of the six-pin conditioning `f(M)=6/5`, +> `f(S)=6/5−r³/6`, `∇f(M)=∇f(S)=0`, `M=(−r/2,0)`, `S=(r/2,0)`, on the +> normalized periodized side-24 2D Bargmann–Fock field; let +> `W_r = |det H_M det H_S|·1{H_M≺0, det H_S<0}` and `Z_r = E_{Q_r}W_r`. Then +> there exists `r_0 > 0` such that +> +> Z_r ≥ c_Z r², 0 < r ≤ r_0, +> c_Z = c_0/2, c_0 = E[U²1{U<0}], U ~ N(−(6/5)a₂, a₄−a₂²), +> c_Z ≥ 1.615489267643502474048123284509081575382 (certified), +> +> and additionally `Z_r ≤ C_Z r²` and `E_{Q_r}W_r² ≤ Cr⁴` (analytic; `C_Z=4B_3` +> route of record). At `(b,κ)=(6/5,1)`; uniformly on compact positive mark +> sets. The weighted law `P_r = W_r dQ_r/Z_r` is well-defined on `(0, r_0]`. + +## 7. Reproduction and receipts + +``` +cd /mnt/agents/output/K3_SIDE24_LB/UPPER2D/H3_closure +python3 h3_c0_certificate.py > cert_normal.txt 2>&1 # exit 0, ALL_CHECKS_PASS +python3 -O h3_c0_certificate.py > cert_O.txt 2>&1 # byte-identical +python3 h3_falsifier.py > fals_normal.txt 2>&1 # exit 0, FALSIFICATION_ATTEMPTS_FAILED +python3 -O h3_falsifier.py > fals_O.txt 2>&1 # byte-identical +MUTATION=planar_moments python3 h3_c0_certificate.py # exit 1 (caught CK2) +MUTATION=wrong_window python3 h3_c0_certificate.py # exit 1 (caught CK6) +``` + +Dependencies re-verified live by this closure (all PASS, byte-identical +two-mode): `SIDE24_gap_fill/scripts/verify_palm_soft_factors.py`, +`verify_a44_a46_flow_v1.py`; H2 `selftest_cov_exact.py`, +`selftest_pin_transform.py`; H2 MANIFEST sha256 pins checked in-program (CK0). + +Receipts are separate files: `cert_normal.txt`, `cert_O.txt`, +`fals_normal.txt`, `fals_O.txt`, `mut_planar.txt`, `mut_window.txt`, +`RECEIPT_h3.json`, `MANIFEST.sha256`.