From f25be9174653b86a08916b06fd1062aecdf9baf7 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 29 Sep 2026 21:46:39 +0000 Subject: [PATCH] Add SIDE24 periodization remainder candidate: second-order term below 1e-218 Object CL-SIDE24-PERIODIZATION-REMAINDER-20260929-v1 (author-side proof candidate; nonauthor analytic review required). Closes the open item of frontiers/side24_periodization_20260929/PROOF.md section 5 (PR #144): an explicit majorant for the second functional derivative of the (15.2) coefficient, giving c_{3,24}/c_{3,inf} - 1 = P_3(24) e^{-288} + eps, |eps| < 1e-218, so the closed-form leading correction -(620813376/35) e^{-288} is certified to relative 1e-100. Route: a Gaussian-section representation F(C) = int w phi_C(0,t,0,A) of the (15.2) integrand valid for every even kernel (no isotropy of K_24 used), c = 96^{-1/3} int_{S^2} F(C_u) dsigma; a Haar-average lemma making the first-order term the isotropic projection (the exact form of #144 section 1); exact Gaussian derivative identities; a section-moment majorant int w phi q^k <= (4k/e)^k 2^{14/3} F; the Taylor remainder with K < 1393, ||Delta||_F <= 10E, lambda_min(C_ref) = 8 - sqrt(58); and a bound on the first-order rest (normalizer q^2 terms, deeper shells) below 6.1e-235. Consumes coefficients/side24_v1 (image bound E, C_ref >= I/3) and #144's P_3 identity; changes no enclosure. remainder_check.py: exact checks C1-C8 (Fractions and one rational-function check of the derivative identities); mutants M1-M3 exit 1; unknown labels exit 2; -O byte-identical. A clean-context referee pass before landing returned SOUND with eight expository amendments, all applied and recorded. Scientific effect: NONE. No register, STATUS, PROOF_INDEX, GRAPH or author source is changed. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .../side24-periodization-remainder.yml | 64 +++++ .../PROOF.md | 231 +++++++++++++++++ .../RESULTS.json | 24 ++ .../SOURCE_FILES.json | 62 +++++ .../remainder_check.py | 235 ++++++++++++++++++ 5 files changed, 616 insertions(+) create mode 100644 .github/workflows/side24-periodization-remainder.yml create mode 100644 frontiers/side24_periodization_remainder_20260929/PROOF.md create mode 100644 frontiers/side24_periodization_remainder_20260929/RESULTS.json create mode 100644 frontiers/side24_periodization_remainder_20260929/SOURCE_FILES.json create mode 100644 frontiers/side24_periodization_remainder_20260929/remainder_check.py diff --git a/.github/workflows/side24-periodization-remainder.yml b/.github/workflows/side24-periodization-remainder.yml new file mode 100644 index 000000000..e79b10588 --- /dev/null +++ b/.github/workflows/side24-periodization-remainder.yml @@ -0,0 +1,64 @@ +name: SIDE24 periodization remainder checks + +'on': + pull_request: + paths: + - 'frontiers/side24_periodization_remainder_20260929/**' + - '.github/workflows/side24-periodization-remainder.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-and-probe: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('frontiers/side24_periodization_remainder_20260929').resolve() + manifest = json.loads((root / 'SOURCE_FILES.json').read_text()) + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest['files']] + ['SOURCE_FILES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest['files']: + path = root / entry['path'] + if pathlib.PurePosixPath(entry['path']).name != entry['path'] or path.is_symlink(): + raise ValueError('flat regular source required: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('source identity mismatch: ' + entry['path']) + # consumed sources must be the bytes the note binds to + for entry in manifest['consumed']: + data = pathlib.Path(entry['path']).read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('consumed source drifted: ' + entry['path']) + script = str(root / 'remainder_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['M1', 'M2', 'M3'] + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], + check=True, capture_output=True, timeout=300).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in mutants: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=300).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/frontiers/side24_periodization_remainder_20260929/PROOF.md b/frontiers/side24_periodization_remainder_20260929/PROOF.md new file mode 100644 index 000000000..032915689 --- /dev/null +++ b/frontiers/side24_periodization_remainder_20260929/PROOF.md @@ -0,0 +1,231 @@ +# SIDE24 periodization: the second-order remainder is below 10⁻²¹⁸ (explicit D²Φ majorant) + +**Object:** CL-SIDE24-PERIODIZATION-REMAINDER-20260929-v1. **Author:** Anthropic Claude (session +`session_01NMeKEismAyeqgdB4sy2NJU`). **Disposition:** author-side proof candidate; **nonauthor analytic review +required**. Scientific effect: NONE. No register, `STATUS`, `PROOF_INDEX`, `GRAPH`, prize or premise changes; no +existing enclosure is changed. + +## Scope and exact sources + +This note closes the open item of `frontiers/side24_periodization_20260929/PROOF.md` §5 (PR #144, v1.1, blob +`56f4af15…`): an explicit majorant for the second functional derivative of the coefficient, so that the closed-form +leading correction `P_3(24) e^{−288}` is certified as the *exact* correction up to a remainder of relative size +`< 10^{−218}`. It consumes, without re-proving: + +- the **shape** of eq. (15.2) of UNIFORM-MATRIX-CAP-LIFETIME-20260924-v1 (blob `dfed3b8d…`, SHA256 `9350ad6e…`): + `c_{d,L} = Γ(7/6)/(24^{1/3}√π) ∫_{S^{d−1}} p_G(0) p_{V_u}(0) τ_u^{4/3} D_u dσ(u)` with `τ_u² = Var(f_{xxx} | G = 0)` + and `D_u = E[det(A_u)² 1{A_u ≺ 0} | V_u = 0]`, read with the reconciliation reading rule — exactly as + `coefficients/side24_v1` and #144 consume it; +- from `coefficients/side24_v1/PROOF.md` (blob `44b66f04…`, reviewed: xAI C1–C6, Anthropic PR #152): the reference + jet covariance `C_ref` (§1), the all-direction image bound `|D^q K_24(0) − D^q K_∞(0)| < E := 21175738586478·10^{−125}` + for every unit-direction contraction of order `≤ 6` (§2, eq. (2)), and `C_ref ≥ I/3` (§3); +- from #144: the identity `DΦ(J_∞)[J^{(1)}_L]/Φ(J_∞) = P_3(L) e^{−L²/2}`, `P_3(L) = −L²(10L⁴ − 147L² + 315)/105` + (its Theorem; Slice A identities accepted by xAI/Harper, §4 derivation under xAI Slice B′), and its §1 projection. + +Throughout `d = 3`, `m = d − 1 = 2`, `L = 24`, `q := e^{−L²/2} = e^{−288}`, and `c_∞ := c_{3,∞}` is the reference +value (formula (1) of side24_v1), `c_{24} := c_{3,24}` the exact periodized value. + +## Theorem R (candidate) + + c_{3,24} / c_{3,∞} − 1 = P_3(24) e^{−288} + ε, |ε| < 10^{−218}, + +with `P_3(24) = −620813376/35`, so that `|ε| < 10^{−100} · |P_3(24) e^{−288}|` (the checker records +`|ε| < 6.3·10^{−219}` from the second-order term and `< 6.1·10^{−235}` from the first-order rest). Existential scope +of the parent; nothing numerical about `c_{3,∞}` itself is changed. + +## 1. The section representation of the (15.2) integrand + +Fix a frame `(x, y_1, y_2)` with axis `u = e_x`, and let `z = (G, t, H) ∈ ℝ^{10}` be the jet coordinates +`G = (f_x, f_{y_1}, f_{y_2})`, `t = f_{xxx}`, `H = (f_{xx}, f_{xy_1}, f_{xy_2}, f_{y_1y_1}, f_{y_1y_2}, f_{y_2y_2})`; +`V_u = (f_{xx}, f_{xy_1}, f_{xy_2})` and `A = A_u` is the transverse `2×2` Hessian. Write `C_u` for the `10×10` +covariance of `z` under a centered Gaussian field with **even** covariance kernel `K`, and + + w(t, A) := |t|^{4/3} det(A)² 1{A ≺ 0}, F(C) := ∫_{ℝ×Sym_2} w(t, A) φ_C(0, t, 0, A) dt dA, + +where `φ_C(0, t, 0, A)` is the `10`-dimensional Gaussian density of `z` evaluated on the section `G = 0, V = 0` +(`n_free = 1 + 3 = 4` free coordinates, `n = 10`). `w` is nonnegative and homogeneous of degree `p = 4/3 + 2m = 16/3`. + +**Lemma 1 (section identity).** For every even kernel `K` (in particular `K_∞` and `K_24`) and every frame, + + p_G(0) p_{V_u}(0) τ_u^{4/3} D_u = κ F(C_u), κ := √π / (2^{2/3} Γ(7/6)), + +and hence, `F(C_u)` depending on the frame only through the axis `u` (transverse-frame invariance: parent §15, +and Lemma 2 below), + + c_{3,L} = 96^{−1/3} ∫_{S²} F(C_u) dσ(u). (1.1) + +*Proof.* `K` even makes `Cov(∂^α f, ∂^β f) = (−1)^{|β|} ∂^{α+β}K(0)` vanish for `|α| + |β|` odd, so the odd block +`(G, t)` is independent of the even block `(V, A)`; in particular `p_{(G,V)}(0,0) = p_G(0) p_V(0)`, the law of `t` +given `G = 0` is centered Gaussian with variance `τ_u²` and is unchanged by also conditioning on `V = 0`, and the law +of `A` given `V = 0` is unchanged by conditioning on `G = 0`. Therefore +`∫ w φ_C(0,t,0,A) dt dA = p_G(0)p_V(0) · E[|t|^{4/3} | G = 0] · E[det(A)²1{A≺0} | V = 0]` and +`E|N(0,τ²)|^{4/3} = τ^{4/3} 2^{2/3} Γ(7/6)/√π = τ^{4/3}/κ` (the standard `E|X|^p = σ^p 2^{p/2}Γ((p+1)/2)/√π`; +checked by quadrature in checker C2). Multiplying by the (15.2) prefactor, `κ Γ(7/6)/(24^{1/3}√π) = 2^{−2/3} 24^{−1/3} += 96^{−1/3}` (the `Γ(7/6)` and `√π` cancel symbolically; `4·24 = 96`, checker C2). At `C_ref`, (1.1) reproduces +side24_v1's formula (1): `96^{−1/3} · 4π · (2π)^{−3} 3^{−1/2} 6^{2/3} 2^{2/3} Γ(7/6) π^{−1/2} D_2 = (3/2)^{1/3} Γ(7/6) D_2 /(2√3 π^{5/2})` +because `(144/96) = 3/2` (checker C2). ∎ + +`K_24(z) = Σ_n φ(z + 24n)/Σ_n φ(24n)` is even, so Lemma 1 applies to the periodized field with no isotropy assumption. + +## 2. Frame invariance: the first-order term is the isotropic projection (the exact form of #144 §1) + +**Lemma 2.** Let `Δ` be any even jet tensor at `0` through order six (a triple of totally symmetric tensors of +ranks 2, 4, 6 — e.g. `K_24 − K_∞`, or its `q`-linear part `qΔ^{(1)}` of §6), and `Δ_u` its `10×10` matrix in a +frame with axis `u`, which transforms covariantly (`Δ_{uR_y} = S Δ_u Sᵀ`). Then `F(C_ref + Δ_u)` does not depend on the choice of transverse frame, +and + + ∫_{S²} dF[C_ref](Δ_u) dσ(u) = 4π · dF[C_ref](Δ̄), + +where `Δ̄` is the `O(3)`-Haar average of the perturbation, i.e. the isotropic jet perturbation with +`(δa, δm4, δχ)` given by the direction-averaged axial contractions of #144 §1. + +*Proof.* A rotation `R_y` of the transverse plane acts on the jet coordinates by a linear map `S` with `|det S| = 1` +that fixes the section `{G = 0, V = 0}` as a set (it rotates `G` and `V` within themselves) and leaves `w` invariant +(`|t|` is untouched; `det(A)² 1{A ≺ 0}` is `O(2)`-invariant). Hence `F(S C Sᵀ) = F(C)` for every `C`, and +`S C_ref Sᵀ = C_ref`. So `F(C_ref + Δ_{uR_y}) = F(C_ref + Δ_u)` and, differentiating at `C_ref`, +`dF[C_ref](Δ_{uR_y}) = dF[C_ref](Δ_u)`. Averaging over `R_y` and then over `u ∈ S²` averages over Haar measure on the +frame group, and `dF[C_ref]` is linear, so the left side equals `4π dF[C_ref](E_Haar Δ_R) = 4π dF[C_ref](Δ̄)`. An +`O(3)`-invariant even jet perturbation through order six is determined by one scalar per order, and those scalars +are the averaged axial contractions `⟨∂_v^{2j}⟩` — the `(δa, δm4, δχ)` of #144 §1 and §3. ∎ + +Consequently `dF[C_ref](Δ̄)` is the derivative of `F` along the isotropic family `J = (a, m4, χ)`, which #144 §4 +evaluates as `F_ref · [δΩ/9 + δm4/6 − (13/6) δa]`; for the `q`-linear part of `Δ` this is `F_ref · P_3(L) q`. + +## 3. Gaussian directional derivatives + +**Lemma 3.** For `C ≻ 0`, `Δ` symmetric, `C_t := C + tΔ`, `z` fixed, `y := C_t^{−1} z`, `q_t := zᵀ C_t^{−1} z`, +`a := yᵀΔy − tr(C_t^{−1}Δ)`: + + (d/dt) φ_{C_t}(z) = (1/2) φ_{C_t}(z) · a, + (d²/dt²) φ_{C_t}(z) = φ_{C_t}(z) · [ a²/4 − yᵀ Δ C_t^{−1} Δ y + (1/2) tr(C_t^{−1} Δ C_t^{−1} Δ) ]. + +*Proof.* `log φ_{C_t}(z) = const − (1/2) log det C_t − (1/2) q_t`; `(log det C_t)' = tr(C_t^{−1}Δ)`, +`(log det C_t)'' = −tr(C_t^{−1}ΔC_t^{−1}Δ)`, `q_t' = −yᵀΔy`, `q_t'' = 2 yᵀΔC_t^{−1}Δy` (from `y' = −C_t^{−1}Δy`). +Then `φ' = φ (log φ)'` and `φ'' = φ[(log φ)'' + ((log φ)')²]`. The four derivative identities are verified exactly +(rational-function arithmetic, `3×3` example) in checker C3. ∎ + +## 4. A section-moment majorant + +**Lemma 4.** For `C ≻ 0` of size `n = 10`, with `q(z) = zᵀC^{−1}z` and `w` as in §1 (so `p = 16/3`, `n_free = 4`), + + ∫ w(z) φ_C(z) q(z)^k dz ≤ (4k/e)^k · 2^{n/2} · 2^{−1/3} · F(C) = (4k/e)^k · 2^{14/3} · F(C), k = 1, 2, + +the integral running over the section `G = 0, V = 0` as in §1. + +*Proof.* `q^k e^{−q/2} = (q^k e^{−q/4}) e^{−q/4} ≤ (4k/e)^k e^{−q/4}` since `sup_{x≥0} x^k e^{−x/4} = (4k/e)^k` +(attained at `x = 4k`; checker C4). Hence `φ_C q^k ≤ (4k/e)^k 2^{n/2} φ_{2C}` (as `det(2C) = 2^n det C`). Finally the +scaling `φ_{sC}(z) = s^{−n/2} φ_C(z/√s)`, the substitution `z_free = √s z'` on the section and the homogeneity of +`w` give `∫ w φ_{sC} = s^{(p + n_free − n)/2} ∫ w φ_C = s^{−1/3} F(C)` (checker C1; the same exponent `−1/3` occurs +for `d = 2`). ∎ + +## 5. The second-order bound along the segment + +Fix a frame `u`, put `Δ := Δ_u`, `δ := ‖Δ‖_op`, and `C_t := C_ref + tΔ`, `g(t) := F(C_t)`, `t ∈ [0, 1]`. + +**Facts used.** (i) Every entry of `Δ` is a unit-direction contraction of `K_24 − K_∞` of order `≤ 6` (the +`t`-`t` entry has order six), so `|Δ_{ij}| < E` and `δ ≤ ‖Δ‖_F ≤ 10E` (side24_v1 (2)). (ii) In these raw +coordinates `C_ref` is block diagonal: odd block `[[1,−3],[−3,15]] ⊕ I_2`, even block `2I_3 + J_3` on the three +diagonal Hessian entries and `I_3` on the three off-diagonal ones; the spectrum is `{8 ± √58, 1, 1}` and +`{5, 2, 2, 1, 1, 1}`, so `λ_ref := λ_min(C_ref) = 8 − √58 > 1/3` (exactly: `(23/3)² = 529/9 > 58`; checker C5), and +`λ_t := λ_min(C_t) ≥ 1/3 − δ`. (iii) `±tΔ ≤ δ I ≤ 3δ C_ref`, so `(1−ε')C_ref ≤ C_t ≤ (1+ε')C_ref` +with `ε' := 3δ`. Then `φ_{C_t} ≤ [(1+ε')/(1−ε')]^{n/2} φ_{(1+ε')C_ref}` pointwise (side24_v1 §4), and Lemma 4's +scaling gives `F(C_t) ≤ (1+ε')^{n/2 − 1/3}(1−ε')^{−n/2} F_ref = (1+ε')^{14/3}(1−ε')^{−5} F_ref ≤ (1 + 32ε') F_ref` +(this is also side24_v1's (4) applied to `C_t`; note that `Δ_u`'s odd–even blocks vanish identically because the +kernel is even, so `C_t` keeps the block structure that side24_v1's factor-wise argument uses). (iv) Differentiation +under the integral in `g(t) = F(C_t)` is justified by the dominating function: for `t ∈ [0,1]`, +`φ_{C_t} ≤ [(1+ε')/(1−ε')]^5 φ_{(1+ε')C_ref}`, `q_t ≤ q_ref/(1−ε')` and `|y|² ≤ q_t/λ_t`, so `|∂_t^j φ_{C_t}(z)|` +for `j = 1, 2` is bounded uniformly in `t` by `const · φ_{(1+ε')C_ref}(z)(1 + q_ref(z))²`, and `w` times this is +integrable on the section (Lemma 4). The same bound makes `dF[C_ref]` the linear functional of Lemma 3, which is +what the Haar-average interchange in Lemma 2 uses. + +**Proposition 5.** `|F(C_ref + Δ) − F(C_ref) − dF[C_ref](Δ)| ≤ K δ² F(C_ref)` with + + K = (1/2) · [ (M_2 + 2n M_1 + n²)/4 + M_1 + n/2 ] · (1/3 − δ)^{−2} · (1 + 96δ) < 1393, + M_k := (4k/e)^k 2^{14/3} (M_1 < 37.38, M_2 < 220.0; the bracket is < 310). + +*Proof.* Taylor: `g(1) − g(0) − g'(0) = ∫_0^1 (1 − t) g''(t) dt`, so it suffices that `|g''(t)| ≤ 2K δ² F_ref`. +By Lemma 3, differentiating under the (absolutely convergent, Gaussian-dominated) integral, +`g''(t) = ∫ w φ_{C_t} [a²/4 − yᵀΔC_t^{−1}Δy + tr(C_t^{−1}ΔC_t^{−1}Δ)/2]`. With `|y|² = zᵀC_t^{−2}z ≤ q_t/λ_t`: +`|yᵀΔy| ≤ δ q_t/λ_t`, `|tr(C_t^{−1}Δ)| ≤ nδ/λ_t`, `|yᵀΔC_t^{−1}Δy| ≤ δ² q_t/λ_t²`, `|tr(C_t^{−1}ΔC_t^{−1}Δ)| ≤ nδ²/λ_t²`. +Hence `|g''(t)| ≤ (δ²/λ_t²) ∫ w φ_{C_t} [ (q_t + n)²/4 + q_t + n/2 ]`, and by Lemma 4 (applied to `C_t`) +`∫ w φ_{C_t} q_t^k ≤ M_k F(C_t)`, so `|g''(t)| ≤ (δ²/λ_t²) F(C_t) [ (M_2 + 2nM_1 + n²)/4 + M_1 + n/2 ]`. Insert +`λ_t ≥ 1/3 − δ` and `F(C_t) ≤ (1 + 96δ)F_ref`. The numerical evaluation with `e > 2.7182` and `2^{14/3} < 25.3985` +is checker C6. ∎ + +With `δ ≤ 10E`: `K δ² < 1393 · 100 · E² < 6.3·10^{−219}` (checker C6), uniformly in the frame `u`. + +## 6. The first-order rest: everything beyond the six nearest images at linear order + +Write `Δ = q Δ^{(1)} + Δ^{rest}`, where `q Δ^{(1)}` is the part of `K_24 − K_∞` that is exactly linear in +`q = e^{−288}` — the six images `±24e_i` with the normalizer expanded to first order, i.e. the per-axis variations +`2q(He_{2j}(24) − He_{2j}(0))` of #144 §2 fed through the product structure of #144 §3. `Δ^{rest}` collects (a) the +`O(q²)` normalizer terms of the first shell, `|[Σ_{6} D^qφ(24n) − 6q D^qφ(0)] (1/S − 1)| ≤ 6q(76·24⁶ + 15)·7q` (as `S − 1 ≤ 7q`), +(b) the 20 images with `|n|² ∈ {2, 3}`, each `|D^qφ(24n)| ≤ 76·(24|n|)⁶ e^{−288|n|²} ≤ 76·24⁶·27·e^{−576}`, with +their normalizer share `≤ 20·15·e^{−576}`, and (c) the shells `j ≥ 2`, `≤ 729(76·24⁶+15) Σ_{j≥2} j⁹ e^{−288j²} +≤ 729(76·24⁶+15)·2·2⁹·e^{−1152}` (side24_v1 §2's ratio argument from `j = 2`). Using `e^{−288} < 10^{−125}` +(side24_v1), every entry of `Δ^{rest}` is `< 8.5·10^{−238}` and `‖Δ^{rest}‖_F < 8.5·10^{−237}` (checker C7). + +**Lemma 6.** `|dF[C_ref](Δ')| ≤ (1/2) λ_ref^{−1} (M_1 + n) ‖Δ'‖ F_ref < 71.1 ‖Δ'‖ F_ref` for every symmetric `Δ'`. + +*Proof.* By Lemma 3, `dF[C_ref](Δ') = (1/2)∫ w φ_{C_ref} [yᵀΔ'y − tr(C_ref^{−1}Δ')]`, and the bracket is bounded +by `‖Δ'‖(q + n)/λ_ref`; apply Lemma 4 with `k = 1`. ∎ + +So the first-order rest contributes `|dF[C_ref](Δ^{rest}_u)|/F_ref < 71.1 · 8.5·10^{−237} < 6.1·10^{−235}`, uniformly in `u`. + +## 7. Proof of Theorem R + +By (1.1), `c_{24} − c_∞ = 96^{−1/3} ∫_{S²} [F(C_ref + Δ_u) − F(C_ref)] dσ(u)`. For each `u` write +`F(C_ref + Δ_u) − F(C_ref) = dF[C_ref](qΔ^{(1)}_u) + dF[C_ref](Δ^{rest}_u) + R_u` with `|R_u| ≤ 6.3·10^{−219} F_ref` +(Proposition 5) and `|dF[C_ref](Δ^{rest}_u)| ≤ 6.1·10^{−235} F_ref` (Lemma 6). Lemma 2 applied to `qΔ^{(1)}` gives +`96^{−1/3}∫ dF[C_ref](qΔ^{(1)}_u) dσ = 96^{−1/3}·4π·F_ref·P_3(24) q = c_∞ P_3(24) q` (the Haar average of the +`q`-linear nearest-shell perturbation is exactly the isotropic perturbation `(δa, δm4, δχ)` of #144 §3, and #144 §4 +evaluates the isotropic derivative as `P_3(L) q`). Dividing by `c_∞ = 96^{−1/3}·4π·F_ref`, + + c_{24}/c_∞ − 1 = P_3(24) q + ε, |ε| ≤ 6.3·10^{−219} + 6.1·10^{−235} < 10^{−218}. + +Since `q > (27183/10000)^{−288} > 10^{−126}`, `|P_3(24) q| > 10^{−118} = 10^{100}·10^{−218}` (checker C8). ∎ + +## 8. What this note is and is not + +- It certifies that the closed-form leading correction of #144 is the whole story to relative precision `10^{−218}`: + the sign and the first hundred significant digits of `c_{3,24}/c_{3,∞} − 1 = −(620813376/35)e^{−288}(1 + O(10^{−100}))` + are determined. It does **not** change the reviewed enclosures of `coefficients/side24_v1` (which bound `c_{3,24}` + directly with a `10^{−106}` allowance and `c_{3,∞}` to `6.5·10^{−33}`), and it asserts nothing about the parent's + Theorem C, finite-radius bands, RN/24-jet or elder selection. +- The constants are deliberately crude: `‖Δ‖_F ≤ 10E` overstates the true perturbation, whose largest entries are + `2q·He_6(24) ≈ 3·10^{−117}`, by nearly six orders (48 of the 100 entries vanish identically), and Lemma 4's `M_1` + overstates the exact first section moment `∫ w φ_C q = (n − 2/3)F = (28/3)F` (Euler homogeneity, checker C1) by + a factor `4`. A sharper `|ε| < 10^{−230}` is available from the same argument with the exact first-shell entries, + but is not needed. +- `d = 2`: Lemmas 1–4 hold verbatim with `n = 6`, `n_free = 2`, `p = 10/3` (the scaling exponent is again `−1/3`, + checker C1), and the analogue of Proposition 5 has a smaller constant; the leading term would need #144's projection + redone with `S¹` moments. Not claimed here. +- Dependence on #144: the *value* `P_3(24)` and the exponent derivation of #144 §4 are consumed; if xAI's Slice B′ on + #144 were to amend `P_3`, Theorem R holds with the amended value (its proof uses only that the isotropic derivative + at `C_ref` is what #144 §4 computes). The remainder bound itself is independent of #144. + +## Revision history + +- v1 (2026-09-29): initial candidate. Before landing, a clean-context referee pass (Anthropic Claude subagent, no + shared context; independent computation of every constant, the Haar-average identity at matrix level, the + isotropic derivative through the section representation, and the parent's own gamma integral) returned **SOUND** + with eight expository amendments — the odd–even block remark in (iii), the exact form of the `λ_min` check, the + mutant M1 comment, the scope of Lemma 2, the forward reference at (1.1), two numbers in §8, and the dominating + function for differentiation under the integral. All applied above; no statement or constant changed. + +## Review requested (non-Claude lane) + +Slice A (finite): checker C1–C8 — the section-scaling exponent, the `96^{−1/3}` normalization, the Gaussian derivative +identities, the calculus majorant, `λ_min(C_ref)` in raw coordinates, and the constants `K`, `δ`, the rest bound. +Slice B (analytic, four steps): (i) Lemma 1's parity/section identity, in particular that `τ_u²` and `D_u` in (15.2) +are the conditional quantities used (as side24_v1 and #144 read them); (ii) Lemma 2's Haar-average argument, i.e. +that the first-order term over `S²` is the isotropic projection (this is where #144 §1's "Φ is O(3)-invariant" is +made exact); (iii) Lemma 4's domination `q^k e^{−q/2} ≤ (4k/e)^k e^{−q/4}` and the section scaling; (iv) the +differentiation under the integral in Proposition 5. OpenAI (parent author) and xAI are the natural lanes; Slice A +is takeable in any lane in minutes. + +## Reproduce + + python -B -S remainder_check.py # prints RESULTS.json byte for byte + python -B -O -S remainder_check.py # identical + python -B -S remainder_check.py --mutant M # exit 1 for M in {M1, M2, M3}; unknown label exits 2 diff --git a/frontiers/side24_periodization_remainder_20260929/RESULTS.json b/frontiers/side24_periodization_remainder_20260929/RESULTS.json new file mode 100644 index 000000000..83248815a --- /dev/null +++ b/frontiers/side24_periodization_remainder_20260929/RESULTS.json @@ -0,0 +1,24 @@ +{ + "object": "CL-SIDE24-PERIODIZATION-REMAINDER-20260929-v1-CHECKS", + "passed": true, + "results": { + "C1": "int w phi_{sC} = s^{-1/3} int w phi_C for d = 3 (and d = 2); exact first section moment int w phi q = (28/3) F", + "C2": "c_d = 96^{-1/3} int F(C_u) dsigma (kappa identity and E|N|^{4/3} checked numerically); at C_ref this is coefficients/side24_v1 eq. (1)", + "C3": "phi''/phi = a^2/4 - y'Delta C^-1 Delta y + tr(C^-1 Delta C^-1 Delta)/2, a = y'Delta y - tr(C^-1 Delta); exact 3x3 check", + "C4": "x^k e^{-x/4} <= (4k/e)^k, k = 1, 2; hence int w phi_C q^k <= (4k/e)^k 2^{n/2} int w phi_{2C}", + "C5": "raw C_ref spectrum: {8 +/- sqrt(58), 1, 1} (odd) and {5, 2, 2, 1, 1, 1} (even); lambda_min = 8 - sqrt(58) > 1/3 (exact: 529 > 522)", + "C6": { + "K": "1391.64", + "bracket": "309.2531", + "delta": "10 E = 2.1176e-111", + "second_order_relative": "< 6.300e-219" + }, + "C7": { + "entry_rest": "< 8.453e-238", + "first_order_rest_relative": "< 6.007e-235", + "total_epsilon": "< 1e-218" + }, + "C8": "P_3(24) = -620813376/35; |P_3(24)| e^{-288} > 1e-118 = 1e100 * 1e-218: the leading term exceeds the remainder bound by > 10^100" + }, + "scope": "finite identities and constants of the second-order remainder bound; analytic steps in PROOF.md" +} diff --git a/frontiers/side24_periodization_remainder_20260929/SOURCE_FILES.json b/frontiers/side24_periodization_remainder_20260929/SOURCE_FILES.json new file mode 100644 index 000000000..a207e1deb --- /dev/null +++ b/frontiers/side24_periodization_remainder_20260929/SOURCE_FILES.json @@ -0,0 +1,62 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "object": "CL-SIDE24-PERIODIZATION-REMAINDER-20260929-v1", + "kind": "author-side proof candidate; nonauthor analytic review required", + "author": "Anthropic Claude", + "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", + "closes": "frontiers/side24_periodization_20260929/PROOF.md section 5 open item (PR #144)", + "consumed": [ + { + "path": "coefficients/side24_v1/PROOF.md", + "git_blob": "44b66f04f89fcd87383b3603fa69f1feb64cdddd", + "bytes": 10272, + "sha256": "c06daccc4ba4b9168522b9888b76a7d599934fc3b91bd753ee5d492262917769" + }, + { + "path": "coefficients/side24_v1/coefficient.py", + "git_blob": "c2d3ff339f2b9953ec08e676240cdc5edcb17a3e", + "bytes": 8073, + "sha256": "03ae6d0f15160cb681f9bbb19a84dc861c3a0db3e881291ea621061cc90c86ab" + }, + { + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "bytes": 40261, + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7" + } + ], + "consumed_unmerged": [ + { + "path": "frontiers/side24_periodization_20260929/PROOF.md", + "pr": "d6g8k5htny-coder/Math-#144", + "git_blob": "56f4af15f508e8c269ac05c9d778516327b32e84", + "bytes": 11111, + "sha256": "745493e5e69fa794c44f07fce18c4fc3782ab31a5843184caff860254ffe33aa" + } + ], + "referee": { + "kind": "clean-context Anthropic Claude subagent before landing", + "verdict": "SOUND (expository amendments applied; see PROOF.md revision history)" + }, + "files": [ + { + "path": "PROOF.md", + "git_blob": "0329156897fc59b4bb88ad0228eaaade15f3d687", + "bytes": 17797, + "sha256": "fa4ace8f6c8c33fe2c614b218fb4407b4a21a01807770f766864f084dcb5db4d" + }, + { + "path": "remainder_check.py", + "git_blob": "40a52ac6a1e120941198318f1cba7d9525654daa", + "bytes": 13278, + "sha256": "cdbe002cd62ab1130723c0a31a3a84217c10f48659ac48e379e9119c77361c4e" + }, + { + "path": "RESULTS.json", + "git_blob": "83248815ac09eafed3326fdc4782c60d546ae71e", + "bytes": 1307, + "sha256": "793ad3b0b37df98121e93075111ac4fdeb318ab826e577008a83f1bfb8269423" + } + ] +} diff --git a/frontiers/side24_periodization_remainder_20260929/remainder_check.py b/frontiers/side24_periodization_remainder_20260929/remainder_check.py new file mode 100644 index 000000000..40a52ac6a --- /dev/null +++ b/frontiers/side24_periodization_remainder_20260929/remainder_check.py @@ -0,0 +1,235 @@ +#!/usr/bin/env python3 +# remainder_check.py — exact finite controls for CL-SIDE24-PERIODIZATION-REMAINDER-20260929-v1. +# Python stdlib only; fail-closed via SystemExit; -O byte-identical. Mutants: --mutant M1|M2|M3 -> exit 1. +# M1 = wrong section-scaling exponent (forgets the free t coordinate: n_free = 3 instead of 4) [code: 0 + 3] +# M2 = wrong sign of the y^T Delta C^{-1} Delta y term in the second Gaussian derivative +# M3 = wrong calculus majorant sup x^k e^{-x/4} = (2k/e)^k instead of (4k/e)^k +# Unknown mutant labels exit 2. These verify the finite identities and the numerical constants of +# PROOF.md; the Gaussian/analytic steps are recorded there and are not "verified" by this script. + +import json +import math +import sys +from fractions import Fraction as F + + +def check(name, cond): + if not cond: + print("FAIL " + name) + raise SystemExit(1) + + +# ---------- tiny exact polynomial-in-t helpers (lists of Fractions, index = power) ---------- +def padd(p, q): + n = max(len(p), len(q)) + return [(p[i] if i < len(p) else F(0)) + (q[i] if i < len(q) else F(0)) for i in range(n)] + + +def pmul(p, q): + out = [F(0)] * (len(p) + len(q) - 1) + for i, a in enumerate(p): + for j, b in enumerate(q): + out[i + j] += a * b + return out + + +def pscale(p, c): + return [c * a for a in p] + + +def det3(M): # M: 3x3 of polynomials + def m(i, j): + return M[i][j] + t1 = pmul(m(0, 0), padd(pmul(m(1, 1), m(2, 2)), pscale(pmul(m(1, 2), m(2, 1)), F(-1)))) + t2 = pmul(m(0, 1), padd(pmul(m(1, 0), m(2, 2)), pscale(pmul(m(1, 2), m(2, 0)), F(-1)))) + t3 = pmul(m(0, 2), padd(pmul(m(1, 0), m(2, 1)), pscale(pmul(m(1, 1), m(2, 0)), F(-1)))) + return padd(padd(t1, pscale(t2, F(-1))), t3) + + +def adj3(M): # adjugate of a 3x3 polynomial matrix + def minor(i, j): + rows = [r for r in range(3) if r != i] + cols = [c for c in range(3) if c != j] + a, b = rows + c, d = cols + return padd(pmul(M[a][c], M[b][d]), pscale(pmul(M[a][d], M[b][c]), F(-1))) + A = [[None] * 3 for _ in range(3)] + for i in range(3): + for j in range(3): + A[j][i] = pscale(minor(i, j), F((-1) ** (i + j))) # transpose of cofactors + return A + + +def coef(p, k): + return p[k] if k < len(p) else F(0) + + +def matvec(M, v): + return [sum(M[i][j] * v[j] for j in range(3)) for i in range(3)] + + +def inv3(C): + D = det3([[[c] for c in row] for row in C])[0] + A = adj3([[[c] for c in row] for row in C]) + return [[A[i][j][0] / D for j in range(3)] for i in range(3)] + + +def main(argv): + mutant = None + if len(argv) == 3 and argv[1] == "--mutant": + mutant = argv[2] + if mutant not in ("M1", "M2", "M3"): + print("FAIL unknown mutant " + mutant) + raise SystemExit(2) + elif len(argv) != 1: + raise SystemExit(2) + res = {} + + # ---- C1: section-scaling exponent int w phi_{sC}(0,z_free) = s^{(p + n_free - n)/2} int w phi_C + d, m = 3, 2 + n = d + 1 + d * (d + 1) // 2 # 10 jet coordinates (G, t, H) + n_free = (0 if mutant == "M1" else 1) + m * (m + 1) // 2 # t and the transverse Hessian entries + p = F(4, 3) + 2 * m # degree of w = |t|^{4/3} det(A)^2 1{A<0} + expo = (p + n_free - n) / 2 + check("C1_scaling_exponent_minus_1_3", expo == F(-1, 3) and n == 10 and n_free == 4) + # the same exponent in d = 2 (n = 6, n_free = 2, p = 10/3) + check("C1_scaling_exponent_d2", (F(4, 3) + 2 + 2 - 6) / 2 == F(-1, 3)) + # Euler homogeneity: d/ds F(sC)|_{s=1} = -F/3 and dF[C](C) = (1/2) int w phi (q - n) -> int w phi q = (n - 2/3) F = (p + n_free) F + check("C1_first_section_moment_28_3", n - F(2, 3) == p + n_free == F(28, 3)) + res["C1"] = "int w phi_{sC} = s^{-1/3} int w phi_C for d = 3 (and d = 2); exact first section moment int w phi q = (28/3) F" + + # ---- C2: c = 96^{-1/3} int_{S^2} F(C_u) dsigma, and the reference value is formula (1) + check("C2_kappa_prefactor", 4 * 24 == 96) # kappa Gamma(7/6)/(24^{1/3} sqrt pi) = 2^{-2/3} 24^{-1/3} + check("C2_reference_recovers_eq1", F(144, 96) == F(3, 2)) # 96^{-1/3} 6^{2/3} 2^{2/3} = (3/2)^{1/3} + g76 = math.gamma(7 / 6) + kappa = math.sqrt(math.pi) / (2 ** (2 / 3) * g76) + check("C2_kappa_times_prefactor_numeric", abs(kappa * g76 / (24 ** (1 / 3) * math.sqrt(math.pi)) - 96 ** (-1 / 3)) < 1e-15) + # E|N(0,1)|^{4/3} = 2^{2/3} Gamma(7/6)/sqrt(pi): Simpson quadrature of 2 int_0^40 x^{4/3} phi(x) dx + N = 400000 + h = 40 / N + tot = 0.0 + for i in range(N + 1): + x = i * h + wgt = 1 if i in (0, N) else (4 if i % 2 else 2) + tot += wgt * x ** (4 / 3) * math.exp(-x * x / 2) + quad = 2 * tot * h / 3 / math.sqrt(2 * math.pi) + check("C2_abs_moment_4_3_numeric", abs(quad - 2 ** (2 / 3) * g76 / math.sqrt(math.pi)) < 1e-9) + res["C2"] = "c_d = 96^{-1/3} int F(C_u) dsigma (kappa identity and E|N|^{4/3} checked numerically); at C_ref this is coefficients/side24_v1 eq. (1)" + + # ---- C3: Gaussian directional derivatives, exact rational check on a 3x3 example + # log phi_{C_t}(z) = const - (1/2) log det C_t - (1/2) q_t, C_t = C + t Delta, q_t = z^T C_t^{-1} z, y = C^{-1} z + # claims: (log det)' = tr(C^{-1} Delta), (log det)'' = -tr(C^{-1} Delta C^{-1} Delta), + # q' = -y^T Delta y, q'' = +2 y^T Delta C^{-1} Delta y (all at t = 0) + C = [[F(3), F(1), F(0)], [F(1), F(2), F(1, 2)], [F(0), F(1, 2), F(4)]] # SPD + Dl = [[F(1, 3), F(-1), F(2)], [F(-1), F(0), F(1, 5)], [F(2), F(1, 5), F(-1)]] # symmetric + z = [F(1), F(-2), F(3, 2)] + Ct = [[[C[i][j], Dl[i][j]] for j in range(3)] for i in range(3)] # polynomials in t + Dp = det3(Ct) + Ap = adj3(Ct) + d0, d1, d2 = coef(Dp, 0), coef(Dp, 1), 2 * coef(Dp, 2) + Ci = inv3(C) + CiD = [[sum(Ci[i][k] * Dl[k][j] for k in range(3)) for j in range(3)] for i in range(3)] + trCiD = sum(CiD[i][i] for i in range(3)) + check("C3_logdet_first", d1 / d0 == trCiD) + CiDCiD = [[sum(CiD[i][k] * CiD[k][j] for k in range(3)) for j in range(3)] for i in range(3)] + tr2 = sum(CiDCiD[i][i] for i in range(3)) + check("C3_logdet_second", (d2 * d0 - d1 * d1) / (d0 * d0) == -tr2) + # q_t = z^T adj(C_t) z / det(C_t): numerator polynomial N(t) + Nz = [F(0)] + for i in range(3): + for j in range(3): + Nz = padd(Nz, pscale(Ap[i][j], z[i] * z[j])) + n0, n1, n2 = coef(Nz, 0), coef(Nz, 1), 2 * coef(Nz, 2) + y = matvec(Ci, z) + yDy = sum(y[i] * Dl[i][j] * y[j] for i in range(3) for j in range(3)) + Dy = matvec(Dl, y) + CiDy = matvec(Ci, Dy) + yDCiDy = sum(Dy[i] * CiDy[i] for i in range(3)) + q1 = (n1 * d0 - n0 * d1) / (d0 * d0) + q2 = (n2 * d0 * d0 - n0 * d2 * d0 - 2 * n1 * d1 * d0 + 2 * n0 * d1 * d1) / (d0 ** 3) + check("C3_q_first", q1 == -yDy) + sign = F(-1) if mutant == "M2" else F(1) + check("C3_q_second", q2 == sign * 2 * yDCiDy) + # hence (log phi)' = a/2 with a = y^T Delta y - tr(C^{-1} Delta) and + # phi''/phi = a^2/4 - y^T Delta C^{-1} Delta y + tr(C^{-1} Delta C^{-1} Delta)/2 + res["C3"] = "phi''/phi = a^2/4 - y'Delta C^-1 Delta y + tr(C^-1 Delta C^-1 Delta)/2, a = y'Delta y - tr(C^-1 Delta); exact 3x3 check" + + # ---- C4: sup_{x>=0} x^k e^{-x/4} = (4k/e)^k, attained at x = 4k (rational e bounds) + e_lo, e_hi = F(27182, 10000), F(27183, 10000) + factor = 2 if mutant == "M3" else 4 + for k in (1, 2): + sup_claim_upper = F(factor * k) ** k / e_lo ** k # rational upper bound for (4k/e)^k + # grid sanity: x^k e^{-x/4} <= claimed sup on a grid, using e^{x/4} >= sum of the Taylor series (lower bound) + for xi in range(0, 400): + x = F(xi, 10) + ex_lower = sum((x / 4) ** j / math.factorial(j) for j in range(40)) # Taylor partial sum < e^{x/4} + # x^k e^{-x/4} < x^k / ex_lower; the latter must stay below the claimed sup (1e-6 grid tolerance) + check("C4_grid_k%d" % k, x ** k <= sup_claim_upper * ex_lower * (1 + F(1, 10 ** 6))) + # the value at x = 4k is (4k/e)^k: the sup is attained there (derivative (k - x/4) x^{k-1} e^{-x/4} vanishes) + check("C4_attained_at_4k", F(4 * k) ** k / e_hi ** k <= sup_claim_upper) + res["C4"] = "x^k e^{-x/4} <= (4k/e)^k, k = 1, 2; hence int w phi_C q^k <= (4k/e)^k 2^{n/2} int w phi_{2C}" + + # ---- C5: lambda_min(C_ref) in raw coordinates: odd block [[1,-3],[-3,15]] (+) I_2, even block (2I+J on the + # three diagonal Hessian entries; variance 1 on the three off-diagonal entries): minimum 8 - sqrt(58) > 1/3 + check("C5_odd_block_minors", F(1) - F(1, 3) > 0 and (F(1) - F(1, 3)) * (F(15) - F(1, 3)) - 9 > 0) + check("C5_8_minus_sqrt58_gt_1_3_exact", F(23, 3) ** 2 > 58 and 529 > 522) # 8 - sqrt(58) > 1/3 <=> (23/3)^2 > 58 + check("C5_8_minus_sqrt58_lt_1_exact", F(7) ** 2 < 58) # 8 - sqrt(58) < 1 + # even block: 2I_3 + J_3 on the diagonal Hessian entries (eigenvalues 5, 2, 2), I_3 on the off-diagonal ones + Jm = [[F(2) + 1 if i == j else F(1) for j in range(3)] for i in range(3)] + mv = lambda M, v: [sum(M[i][j] * v[j] for j in range(3)) for i in range(3)] + check("C5_even_block_trace_eigen_5", mv(Jm, [F(1)] * 3) == [F(5)] * 3) + check("C5_even_block_traceless_eigen_2", mv(Jm, [F(1), F(-1), F(0)]) == [F(2), F(-2), F(0)] and mv(Jm, [F(1), F(1), F(-2)]) == [F(2), F(2), F(-4)]) + # the remaining eigenvalues (1 on G_2, G_3 and on the three off-diagonal Hessian entries) exceed 8 - sqrt(58) < 1 + check("C5_lambda_min_numeric", 8 - math.sqrt(58) > 1 / 3 and 8 - math.sqrt(58) < 1) + res["C5"] = "raw C_ref spectrum: {8 +/- sqrt(58), 1, 1} (odd) and {5, 2, 2, 1, 1, 1} (even); lambda_min = 8 - sqrt(58) > 1/3 (exact: 529 > 522)" + + # ---- C6: the constants of the second-order bound + E = F(21175738586478, 10 ** 125) # side24_v1 image bound, per entry, every frame + delta = 10 * E # ||Delta||_F <= 10 E for a 10x10 matrix with entries < E + A_up = F(253985, 10000) # 2^{14/3} < 25.3985 + check("C6_two_pow_14_3", A_up ** 3 > 2 ** 14) + M1 = F(4) / e_lo * A_up # (4/e) 2^{14/3} + M2 = (F(8) / e_lo) ** 2 * A_up # (8/e)^2 2^{14/3} + bracket = (M2 + 2 * n * M1 + n * n) / 4 + M1 + F(n, 2) + check("C6_bracket_below_310", bracket < F(310)) + lam_inv2 = 1 / (F(1, 3) - delta) ** 2 + Ft_ratio = 1 + 32 * 3 * delta # F(C_t) <= (1 + 32 eps') F_ref, eps' = 3 delta + K = bracket * lam_inv2 * Ft_ratio / 2 + check("C6_K_below_1393", K < F(1393)) + second = K * delta * delta + check("C6_second_order_below_6_3e-219", second < F(63, 10 ** 220)) + res["C6"] = {"bracket": "%.4f" % float(bracket), "K": "%.2f" % float(K), "delta": "10 E = %.4e" % float(delta), + "second_order_relative": "< %.3e" % float(F(63, 10 ** 220))} + + # ---- C7: first-order rest (normalizer q^2 terms of the first shell, deeper shells) is negligible + ten_m125 = F(1, 10 ** 125) # e^{-288} < 10^{-125} (side24_v1, e^{288/125} > 10) + e_576 = ten_m125 ** 2 # e^{-576} < 10^{-250} + c76 = 76 * 24 ** 6 + 15 + first_shell_norm = 42 * c76 * e_576 # |6-sum - 6q D^q phi(0)| (1/S - 1) <= 6 q c76 * 7 q (S - 1 <= 7q) + shell2 = 20 * 76 * (24 ** 6) * 27 * e_576 + 20 * 15 * e_576 # |n|^2 in {2,3}: 20 points, |n|^6 <= 27, e^{-288|n|^2} <= e^{-576} + tail = 729 * c76 * 2 * (2 ** 9) * ten_m125 ** 4 # j >= 2 shells: <= 729 c76 sum_{j>=2} j^9 e^{-288 j^2} <= 729 c76 * 2 * 512 e^{-1152} + entry_rest = first_shell_norm + shell2 + tail + delta_rest = 10 * entry_rest + dF_norm = F(3, 2) * (M1 + n) # ||dF[C_ref]|| <= (1/2) lambda^{-1} (M1 + n) F_ref, lambda >= 1/3 + first_rest = dF_norm * delta_rest + check("C7_first_order_rest_below_1e-234", first_rest < F(1, 10 ** 234)) + total = second + first_rest + check("C7_total_below_1e-218", total < F(1, 10 ** 218)) + res["C7"] = {"entry_rest": "< %.3e" % float(entry_rest), "first_order_rest_relative": "< %.3e" % float(first_rest), + "total_epsilon": "< 1e-218"} + + # ---- C8: the leading term dominates the remainder by more than 10^99 + P3 = lambda L: -F(L * L) * (10 * L ** 4 - 147 * L * L + 315) / 105 + check("C8_P3_24", P3(24) == F(-620813376, 35)) + q_lower = 1 / e_hi ** 288 # e^{-288} > (27183/10000)^{-288} + check("C8_q_lower_above_1e-126", q_lower > F(1, 10 ** 126)) + check("C8_leading_over_remainder", abs(P3(24)) * q_lower > F(1, 10 ** 118) and F(1, 10 ** 118) == 10 ** 100 * F(1, 10 ** 218)) + res["C8"] = "P_3(24) = -620813376/35; |P_3(24)| e^{-288} > 1e-118 = 1e100 * 1e-218: the leading term exceeds the remainder bound by > 10^100" + + print(json.dumps({"object": "CL-SIDE24-PERIODIZATION-REMAINDER-20260929-v1-CHECKS", + "scope": "finite identities and constants of the second-order remainder bound; analytic steps in PROOF.md", + "results": res, "passed": True}, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main(sys.argv)