From 3abcc10ed63a626a90957c06b21d18d8ed730587 Mon Sep 17 00:00:00 2001 From: d6g8k5htny-coder Date: Wed, 30 Sep 2026 20:16:34 +0000 Subject: [PATCH 1/2] Add exact closed form of the SIDE24 cone moment D_3 (d = 4) coefficients/side24_d4_closed_form_20260930: D_3 = 50/3 - 76/(3 pi) - (200/(9 pi)) arctan(1/2) = (50 pi + 200 arctan 2 - 228)/(9 pi), obtained by exact integration of the one-dimensional reduction of Math-#199 in exact arithmetic on the Q-span of sqrt(r) pi^(k/2) arctan-atoms (only odd J_k occur, so every term is a Gaussian moment with at most one error function; base integrals and a by-parts recurrence). The same path returns 4/3 and 29/6 - sqrt6 exactly; the 60-digit interval evaluation lies inside the certified enclosure of #199 with 47 common digits. Corollary: c_{4,ref} = Gamma(7/6)(3/2)^(1/3)(50 pi + 200 arctan 2 - 228)/(72 sqrt3 pi^(7/2)). Twelve rules, eleven mutants, workflow replay. Scientific effect NONE; coefficients/side24_v1 unchanged; C8 stays OPEN; no register surface touched. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- .github/workflows/side24-d4-closed-form.yml | 80 ++ .../side24_d4_closed_form_20260930/NOTE.md | 214 +++++ .../RESULTS.json | 237 +++++ .../SOURCE_FILES.json | 70 ++ .../closed_form_d3.py | 840 ++++++++++++++++++ 5 files changed, 1441 insertions(+) create mode 100644 .github/workflows/side24-d4-closed-form.yml create mode 100644 coefficients/side24_d4_closed_form_20260930/NOTE.md create mode 100644 coefficients/side24_d4_closed_form_20260930/RESULTS.json create mode 100644 coefficients/side24_d4_closed_form_20260930/SOURCE_FILES.json create mode 100644 coefficients/side24_d4_closed_form_20260930/closed_form_d3.py diff --git a/.github/workflows/side24-d4-closed-form.yml b/.github/workflows/side24-d4-closed-form.yml new file mode 100644 index 000000000..4d42acacd --- /dev/null +++ b/.github/workflows/side24-d4-closed-form.yml @@ -0,0 +1,80 @@ +name: SIDE24 d4 closed form + +'on': + pull_request: + paths: + - 'coefficients/side24_d4_closed_form_20260930/**' + - '.github/workflows/side24-d4-closed-form.yml' + - 'imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md' + - 'coefficients/side24_v1/PROOF.md' + workflow_dispatch: + +permissions: + contents: read + +jobs: + certify-and-reject-mutants: + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources and pins, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import concurrent.futures, hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('coefficients/side24_d4_closed_form_20260930').resolve() + manifest_doc = json.loads((root / 'SOURCE_FILES.json').read_text()) + manifest = manifest_doc['files'] + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest] + ['SOURCE_FILES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest: + 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']) + for pin in manifest_doc['pins_on_main']: + if not pin.get('workflow_checked'): + continue + p = pathlib.Path(pin['path']) + if p.is_symlink() or not p.is_file(): + raise ValueError('pinned source missing: ' + pin['path']) + data = p.read_bytes() + blob = hashlib.sha1(b'blob %d\0' % len(data) + data).hexdigest() + if blob != pin['git_blob']: + raise ValueError('pinned source drifted: ' + pin['path'] + ' ' + blob) + script = str(root / 'closed_form_d3.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['shift-variance', 'vandermonde', 'erfc-sign', 'jacobian', 'mehta', 'by-parts', 'one-erf', 'jk-init', 'gauss-half', 'boundary-term', 'atom-pi'] + def mutant_rc(args): + flags, m = args + return m, flags, subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=600).returncode + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], + check=True, capture_output=True, timeout=600).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + doc = json.loads(out) + if not (doc['passed'] and len(doc['checks']) == 12 and all(doc['checks'].values())): + raise RuntimeError('certification did not pass under ' + ' '.join(flags)) + if doc['closed_forms']['D_3'] != '50/3 + -76/3 pi^(-1) + -200/9 pi^(-1) arctan(1/2)': + raise RuntimeError('closed form differs from the stated one') + with concurrent.futures.ThreadPoolExecutor(max_workers=4) as pool: + for m, fl, rc in pool.map(mutant_rc, [(flags, m) for m in mutants]): + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected under ' + ' '.join(fl)) + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False, 'exact_identity_checked': True, 'side24_v1': 'unchanged'})) + PY + git diff --exit-code diff --git a/coefficients/side24_d4_closed_form_20260930/NOTE.md b/coefficients/side24_d4_closed_form_20260930/NOTE.md new file mode 100644 index 000000000..cbf35dead --- /dev/null +++ b/coefficients/side24_d4_closed_form_20260930/NOTE.md @@ -0,0 +1,214 @@ +# The SIDE24 cone moment `D_3` in closed form (`d = 4`) + +**Object** `CL-SIDE24-D3-CLOSED-FORM-20260930-v1` · **scientific effect NONE** · declarative record, `executed: false` · +base `main 3e0a91b` · claim: Math-#199 comment 5918624116 · companion: Math-#199 (`coefficients/side24_d4_20260930`, head `4fc6d15`), +whose one-dimensional reduction is the input and whose certified enclosure is the independent check. +`coefficients/side24_v1` is unchanged; catalog entry C8 stays OPEN; no register, GRAPH, STATUS or catalog surface is touched. +Same GitHub account as every lane: zero organizational-independence credit. Claude reads of this record count for nothing. +The author will not merge. + +## 0. Statement + +**Proposition (closed form of `D_3`).** For SIDE24's reference law in `d = 4` (`A = Q + √(2/3) Z I_3`, `Q` the `3×3` GOE of +density `∝ exp(−tr Q²/4)`, `Z` an independent standard normal), the cone moment `D_3 = E[det(A)² 1{A ≺ 0}]` of [LP] (15.1) is + +``` +D_3 = 50/3 − 76/(3π) − (200/(9π)) arctan(1/2) + = (50π + 200 arctan 2 − 228)/(9π) + = 50/3 − 76/(3π) − (100/(9π)) arccos(3/5) + = 5.32318026888989689492319873968726063578438852944092005011… +``` + +**Corollary (the `d = 4` reference coefficient).** With [LP] (15.2) as written out in Math-#199 §4, + +``` +c_{4,ref} = Γ(7/6) (3/2)^{1/3} D_3 / (8√3 π^{5/2}) + = Γ(7/6) (3/2)^{1/3} (50π + 200 arctan 2 − 228) / (72√3 π^{7/2}) + = 0.02332166600295283509452119495285688515310137236324033440… +``` + +and `c_{4,24}` is as in Math-#199: `|c_{4,24}/c_{4,ref} − 1| ≤ 1.5702·10⁻¹⁰⁸`, so `c_{4,24}` carries the same digits. + +This continues `D_1 = 4/3`, `D_2 = 29/6 − √6` (SIDE24 §1) with the first value in which `π` and an arctangent appear. +`D_4` (Math-#200) remains an enclosure; see §6. + +**What is proved here and from what.** The identity is obtained by *exact* integration of the one-dimensional integral to +which Math-#199 reduces `D_3`. That reduction is exact algebra on the ordered-sector integrand of the eigenvalue form of +`D_m` (Math-#199 NOTE §§1–2; the same code, re-run here, and checked at `m = 1, 2` against SIDE24's `4/3` and `29/6 − √6` +through the identical path). Nothing in the chain is approximated, sampled or fitted: the output of the script is an element +of a finite-dimensional `Q`-vector space with basis `√r · π^{k/2} · A` (`r` squarefree, `k ∈ Z`, `A = 1` or an arctan atom), +and the closed form above is that element. The certified enclosure of Math-#199 (an independent method: order-40 Taylor +quadrature with Cauchy remainders) contains the interval evaluation of the closed form, with 47 common digits (rule +`D3_INSIDE_CERTIFIED`). + +## 1. Input: the one-dimensional reduction (Math-#199 NOTE §§1–2) + +In the ordered sector `μ_3 = −a, μ_2 = −a−p, μ_1 = −a−p−q`, after the exact `a`-integral and the substitution +`p = (s − q)/2` (Jacobian `1/2`, region `0 < q < s`), Math-#199 obtains + +``` +D_3 = (1/(32π)) [ √(2π/3) ∫_0^∞ e^{−s²/24} erfc(s/(2√6)) Σ_k e_k(s) J_k(s) ds + ∫_0^∞ e^{−s²/12} Σ_k r_k(s) J_k(s) ds ], +J_k(s) = ∫_0^s q^k e^{−q²/8} dq, +``` + +where `1/(32π) = √(3/6) · 3! · (1/2) / Z_3` (`Z_3 = 48√2 π`, Mehta), `√(2π/3) = ½√(π/α)` with `α = 3/8` is the constant of +`G_0`, `κ = 1/(2√6)` is the erfc slope (`β/(2√α)` with `β = s/4`), and the two exponents are `s²/24 + q²/8` (erfc branch) and +`s²/12 + q²/8` (polynomial branch). The rational polynomials, generated by the code (`RESULTS.json`, `reduction_data`), are + +| `k` | `e_k(s)` (erfc branch) | `r_k(s)` (polynomial branch) | +|---|---|---| +| 1 | `80s²/9 − 2s⁴/9 + s⁶/432 + s⁸/46656` | `80s³/27 − 2s⁵/243 − s⁷/11664` | +| 3 | `−80/9 − 4s²/9 + 5s⁴/432 − 19s⁶/46656` | `−80s/27 − 16s³/243 + 19s⁵/11664` | +| 5 | `2/3 + s²/144 + 11s⁴/5184` | `2s/27 − 11s³/1296` | +| 7 | `−1/48 − s²/576` | `s/144` | + +Only **odd** `k` occur (rule `STRUCTURE`). This matters: for odd `k` the primitive `J_k` contains no error function, + +``` +J_1 = 4 − 4e^{−s²/8}, J_3 = 32 − (32 + 4s²) e^{−s²/8}, J_5 = 512 − (512 + 64s² + 4s⁴) e^{−s²/8}, +J_7 = 12288 − (12288 + 1536s² + 96s⁴ + 4s⁶) e^{−s²/8} +``` + +(from `J_1 = 4(1 − e^{−s²/8})`, `J_{k+2} = −4s^{k+1}e^{−s²/8} + 4(k+1)J_k`), so after expanding `erfc = 1 − erf` every +term of `D_3` is one of the moments + +``` +M_n(λ, 1) = ∫_0^∞ s^n e^{−λs²} ds, M_n(λ, erf(κ·)) = ∫_0^∞ s^n e^{−λs²} erf(κs) ds, +λ ∈ {1/24, 1/6} (erfc branch: 1/24 and 1/24 + 1/8), λ ∈ {1/12, 5/24} (polynomial branch), κ = 1/(2√6), n ≤ 8. +``` + +## 2. Three lemmas + +**L1 (the primitives `J_k`).** Write `J_k(s) = A_k √(2π) erf(s/(2√2)) + B_k + C_k(s) e^{−s²/8}` with rational `A_k, B_k` and a +rational polynomial `C_k`, generated from `J_0 = √(2π) erf(s/(2√2))`, `J_1 = 4(1 − e^{−s²/8})` by the recurrence. The triple is +characterised by `J_k(0) = 0` (`B_k + C_k(0) = 0`), `J_k'(s) = s^k e^{−s²/8}` (`A_k + C_k'(s) − (s/4) C_k(s) = s^k` as polynomials), +and `J_k(∞) = ½ 8^{(k+1)/2} Γ((k+1)/2)`; all three are verified exactly for `k ≤ 7` (rule `JK_EXACT`). For odd `k`, `A_k = 0`. + +**L2 (base integrals).** For `λ > 0`, `κ > 0`: + +``` +M_0(λ, 1) = ½ √(π/λ), M_1(λ, 1) = 1/(2λ), M_0(λ, erf(κ·)) = arctan(κ/√λ) / √(πλ). +``` + +*Proof of the third.* `∂_κ ∫_0^∞ e^{−λs²} erf(κs) ds = (2/√π) ∫_0^∞ s e^{−(λ+κ²)s²} ds = 1/(√π (λ + κ²))`, and the value at +`κ = 0` is `0`, so `M_0(λ, erf(κ·)) = (1/√π) ∫_0^κ dt/(λ + t²) = arctan(κ/√λ)/√(πλ)`. ∎ +(The code also carries `∫_0^∞ e^{−λs²} erf(us) erf(vs) ds = arctan(uv/√(λ(λ+u²+v²)))/√(πλ)`, needed only if an even `k` +occurred; it is not on the path of `D_3`, and a float control checks it, rule `BASE_INTEGRALS_FLOAT`.) + +**L3 (moments by parts).** For `n ≥ 1` and `f ∈ {1, erf(κ·)}`, writing `s^n e^{−λs²} f(s) = s^{n−1} f(s) · s e^{−λs²}` and +integrating by parts, + +``` +M_n(λ, f) = [ (n−1) M_{n−2}(λ, f) + (2κ/√π) M_{n−1}(λ + κ², 1) ]/(2λ) (the second term only for f = erf(κ·)), +``` + +because `d/ds erf(κs) = (2κ/√π) e^{−κ²s²}` and the boundary term `[−s^{n−1} f(s) e^{−λs²}/(2λ)]_0^∞` vanishes for `n ≥ 2` +(`s^{n−1} = 0` at `0`) and for `n = 1, f = erf(κ·)` (`erf(0) = 0`); for `n = 1, f = 1` it equals `1/(2λ)`, which is the base value +`M_1(λ, 1)`. The recurrence terminates at `M_0` and `M_1` of L2. As an internal check, the recurrence at `f = 1` reproduces +`½ Γ((n+1)/2) λ^{−(n+1)/2}` exactly for `n ≤ 12` and every `λ` that occurs (rule `GAUSS_MOMENTS`). + +By L1–L3, `D_3` is a finite `Q`-linear combination of `√r π^{k/2}` and `√r π^{k/2} arctan(θ)` with `θ = κ/√λ` for the two +`λ` of the erfc branch: `θ = κ√24 = 1` (`λ = 1/24`, `arctan 1 = π/4`) and `θ = κ√6 = 1/2` (`λ = 1/6`). Hence +`D_3 ∈ Q + Q·π^{−1} + Q·π^{−1} arctan(1/2)` after the powers of `√π` combine (they do; every surviving term is rational +times `π^0` or `π^{−1}`). + +## 3. The exact computation + +`closed_form_d3.py` implements the `Q`-span of `√r · π^{k/2} · A` as dictionaries `(r, 2k, atom) → Fraction` with exact +surd reduction (`√r√r' = m√r''`, `r''` squarefree). `arctan` arguments are algebraic numbers `c√r`; the arguments `1`, `√3`, +`1/√3` are replaced by `π/4`, `π/3`, `π/6`, an argument above `1` is reflected (`arctan t = π/2 − arctan(1/t)`), and any other +argument becomes an atom `arctan(c√r)` with `0 < c√r ≤ 1`. Products of two atoms never occur (they would raise). +The moments `M_n(λ, f)` are computed by L2–L3 in this arithmetic, `J_k` by L1, and the two branches of §1 are assembled with the +exact prefactor `1/(32π)` and `G_0` constant `√(2π/3)` (both produced from Mehta's `Z_3` and `α = 3/8` in the same +arithmetic). The result, with the two branches separately: + +``` +erfc branch : 50/3 − 13958/(375π) − (200/(9π)) arctan(1/2) +polynomial branch : 1486/(125π) +D_3 : 50/3 − 76/(3π) − (200/(9π)) arctan(1/2) (−13958/375 + 1486/125 = −76/3) +``` + +The equivalent forms of §0 use `arctan(1/2) = π/2 − arctan 2` and `2 arctan(1/2) = arccos(3/5)`. + +The same code path at `m = 1` and `m = 2` (the `m = 2` erfc branch has `κ_2 = √30/20` against `e^{−p²/8}`, whose base +integral produces the atom `arctan(√15/5)`) returns exactly `4/3` and exactly `29/6 − √6`: the `arctan(√15/5)` terms cancel +identically in `D_2`, and no `π` survives (rules `D1_EXACT`, `D2_EXACT`, exact equality of dictionaries). + +## 4. Verification + +Twelve rules, all exact except the two float controls and the two interval containments: + +| rule | content | +|---|---| +| `STRUCTURE` | decoupled exponents (checked inside the reduction), `κ = √6/12`, `λ_erfc = 1/24`, `λ_poly = 1/12`, only odd `k ≤ 7`, the derivation created exactly the atoms `arctan(√15/5)` (from `m = 2`) and `arctan(1/2)` | +| `GAUSS_MOMENTS` | L3 at `f = 1` equals `½Γ((n+1)/2)λ^{−(n+1)/2}` exactly, `n ≤ 12`, seven values of `λ` | +| `JK_EXACT` | L1: `J_k(0) = 0`, `J_k' = s^k e^{−s²/8}`, `J_k(∞) = ½8^{(k+1)/2}Γ((k+1)/2)`, `k ≤ 7`, exactly | +| `D1_EXACT`, `D2_EXACT` | `4/3` and `29/6 − √6` exactly | +| `D3_FORM` | the output equals `50/3 − 76/(3π) − (200/(9π)) arctan(1/2)` exactly (pinned coefficients) | +| `BASE_INTEGRALS_FLOAT`, `MOMENTS_FLOAT` | Simpson quadrature (`math.erf`) of the base integrals and of sampled `M_n` agrees with the exact values to `10⁻⁹`/`10⁻⁸` (controls) | +| `D3_INSIDE_CERTIFIED` | the 60-digit interval evaluation of the closed form (Machin `π`, integer roots, `arctan(1/2)` by argument halving and bracketed alternating series) lies inside Math-#199's certified `D_3` enclosure and has width `< 10⁻⁵⁵` | +| `C4_CLOSED` | the same for `c_{4,ref}` against Math-#199's enclosure (`Γ(7/6)` and `(3/2)^{1/3}` by the #199 toolkit) | +| `LIBRARY_EXACT` | `decimal` `exp`/`sqrt`/negation against exact rational brackets, as in Math-#190 v1.3 and #199 | +| `PINNED` | `π`, `D_3`, `c_{4,ref}` digit prefixes | + +Eleven mutants exit 1 in both interpreter modes: `shift-variance` (`S²/24 → S²/20`), `vandermonde` (factor dropped), +`erfc-sign` (`erfc = 1 + erf`), `jacobian` (`1/2` dropped), `mehta` (`Z_4` for `Z_3`), `by-parts` (`n−1 → n`), `one-erf` +(`arctan(κ/√λ) → arctan(κ/λ)`), `jk-init` (`J_1` halved), `gauss-half` (`M_0` doubled), `boundary-term` (`M_1(λ,1) = 1/λ`), +`atom-pi` (`arctan 1 = π/3`). Each is caught by `D3_FORM` and the two containments, most also by the exact `m = 1, 2` rules or +`GAUSS_MOMENTS`/`JK_EXACT`. Runtime about two seconds. + +The 47 common digits with Math-#199 are the decisive independent check: #199 encloses the same integral by a method that +shares only the exact reduction code with this record, and that code is itself checked at `m = 1, 2` against SIDE24, by the +float orthant quadrature of the original `m`-dimensional integral and by a Monte Carlo of the matrix definition (#199 §5). + +## 5. The coefficient in every `d ≤ 4` + +With `c_{d,ref} = Γ(7/6)(3/2)^{1/3} |S^{d−1}| D_{d−1} / (√3 √π (2π)^d)` (Math-#199 §4, from [LP] (15.2)): + +| `d` | `D_{d−1}` | `c_{d,ref}` closed form | value | +|---|---|---|---| +| 2 | `4/3` | `2Γ(7/6)(3/2)^{1/3}/(3√3 π^{3/2})` | `0.0734069193060342710301359629577…` (SIDE24) | +| 3 | `29/6 − √6` | `Γ(7/6)(3/2)^{1/3}(29/6 − √6)/(2√3 π^{5/2})` | `0.0417759318405983433429366654285…` (SIDE24) | +| 4 | `(50π + 200 arctan 2 − 228)/(9π)` | `Γ(7/6)(3/2)^{1/3}(50π + 200 arctan 2 − 228)/(72√3 π^{7/2})` | `0.0233216660029528350945211949528…` (this record; #199 encloses) | +| 5 | Math-#200 enclosure `14.21876345897735760130646567787…` | none claimed | `0.0132193193800849680760334875146…` (#200 encloses) | + +The torus constants `c_{d,24}` follow from the covariance sandwich of SIDE24 §§3–4 with the constants of #199 (`d = 4`, +`δ = 1.5702·10⁻¹⁰⁸`) and #200 (`d = 5`); a closed form for `c_{4,ref}` does not change `c_{4,24}`'s status (enclosed, not equated). + +## 6. Scope and non-claims + +- The Proposition is an identity, proved by L1–L3 applied to the exact reduction of Math-#199. It consumes [LP] (15.1)–(15.2) and + SIDE24 §1 at their scope (the reference law, `p_G(0)p_V(0)`, `τ² = 6`) and does not review them. +- **No closed form for `D_4` is claimed or expected by this method.** In the `m = 4` reduction (Math-#200 §§1–2) the outer + integral carries `erfc(κT)` against the cumulative integrals `L_a(T) = ∫_0^T e^{−v²/24} q_a(v) dv`, whose integrands contain + `erf(v/(2√2))` (even `k` occur there through `J_k(v)`), so the terms are Gaussian integrals over a two-dimensional wedge with + two error-function factors: four-dimensional Gaussian orthant-type integrals, which are not elementary in general. Math-#200's + enclosure stands as the record for `d = 5`. +- Math-#199 §7 says "no closed form for `D_3` claimed"; this record supplies one. Math-#199 is not edited here. If a nonauthor + lane accepts this record, a one-line pointer in #199 §7 is the natural amendment; it is not made by the author unprompted. +- C8 stays OPEN (the constants `C`, `r_*`, `z_*` and the window coefficients are not touched); `coefficients/side24_v1` is + unchanged; no register, GRAPH, STATUS, PROOF_INDEX, SELECTOR_REGION or catalog surface is touched; `executed: false`. + +## 7. Files, pins, how to run + +`coefficients/side24_d4_closed_form_20260930/{NOTE.md, closed_form_d3.py, RESULTS.json, SOURCE_FILES.json}` and +`.github/workflows/side24-d4-closed-form.yml` (manifest, pins, byte-identical replay in `-B -S` and `-B -O -S`, the eleven +mutants). Pins on `main 3e0a91b`: [LP] `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` blob `dfed3b8d` +((15.1), (15.2)); SIDE24 `coefficients/side24_v1/PROOF.md` blob `44b66f04` (§1). Companion, not on `main`: Math-#199 at +`4fc6d15`, `coefficients/side24_d4_20260930/RESULTS.json` blob `187552f5` (the two enclosures quoted in the script) and +`NOTE.md` blob `20e9acdb` (§§1–2, the reduction). Run: `python3 -B -S closed_form_d3.py` (exit 0, JSON on stdout identical to +`RESULTS.json`); `--mutant NAME` exits 1. + +## 8. Current disposition + +- **Head / owner:** see the PR's disposition block; branch `claude/side24-d3-closed-form-20260930` (base `main 3e0a91b`); + author lane Anthropic / Claude (`session_017Mi3hxjaxV45x6zo6o1ee3`). +- **Claim:** the Proposition and Corollary of §0, proved by exact integration of the Math-#199 reduction; exact `m = 1, 2` + regressions; 47-digit agreement with the independent certified enclosure. No theorem of [LP] or SIDE24 is proved or reviewed. +- **Completed review scopes:** none yet. Requested: nonauthor reads of Slice A (§1: the reduction data, odd `k`, `J_k`; L1), + Slice B (§2 L2–L3: the base integrals and the by-parts recurrence; §3 the arithmetic, atoms, reflection, the cancellations), + Slice C (§§4–6: rules, mutants, the containment, the coefficient table, the `D_4` non-claim). +- **Unresolved finding IDs:** none. +- **Validation:** 12/12 rules in both modes, byte-identical output; 11/11 mutants rejected in both modes; workflow replayed + locally; hosted run pending at opening. +- **Next action:** nonauthor reads; amendments on this branch, recorded in `SOURCE_FILES.json`. Author will not merge. diff --git a/coefficients/side24_d4_closed_form_20260930/RESULTS.json b/coefficients/side24_d4_closed_form_20260930/RESULTS.json new file mode 100644 index 000000000..a44807969 --- /dev/null +++ b/coefficients/side24_d4_closed_form_20260930/RESULTS.json @@ -0,0 +1,237 @@ +{ + "object": "CL-SIDE24-D3-CLOSED-FORM-20260930-v1", + "scientific_effect": "NONE", + "certified": true, + "mutant": null, + "passed": true, + "checks": { + "STRUCTURE": true, + "GAUSS_MOMENTS": true, + "JK_EXACT": true, + "D1_EXACT": true, + "D2_EXACT": true, + "D3_FORM": true, + "BASE_INTEGRALS_FLOAT": true, + "MOMENTS_FLOAT": true, + "D3_INSIDE_CERTIFIED": true, + "C4_CLOSED": true, + "LIBRARY_EXACT": true, + "PINNED": true + }, + "closed_forms": { + "D_1": "4/3", + "D_2": "29/6 + -1 sqrt(6)", + "D_3": "50/3 + -76/3 pi^(-1) + -200/9 pi^(-1) arctan(1/2)", + "D_3_equivalent": "(50 pi + 200 arctan 2 - 228) / (9 pi) = 50/3 - 76/(3 pi) - (100/(9 pi)) arccos(3/5)", + "c_4_ref": "Gamma(7/6) (3/2)^(1/3) (50 pi + 200 arctan 2 - 228) / (72 sqrt3 pi^(7/2))", + "erfc_branch_of_D_3": "50/3 + -13958/375 pi^(-1) + -200/9 pi^(-1) arctan(1/2)", + "polynomial_branch_of_D_3": "1486/125 pi^(-1)" + }, + "interval_evaluation": { + "D_3": [ + "5.32318026888989689492319873968726063578438852944092005011779", + "5.32318026888989689492319873968726063578438852944092005012189" + ], + "c_4_ref": [ + "0.0233216660029528350945211949528568851531013723632403344029687", + "0.0233216660029528350945211949528568851531013723632403344090027" + ], + "arctan(1/2)": [ + "0.463647609000806116214256231461214402028537054286120263810832", + "0.463647609000806116214256231461214402028537054286120263811026" + ], + "pi": [ + "3.14159265358979323846264338327950288419716939937510582097457", + "3.14159265358979323846264338327950288419716939937510582097528" + ], + "Gamma(7/6)": [ + "0.927719333630039200708349482534621018566466519145475576700351", + "0.927719333630039200708349482534621018566466519145475576939062" + ], + "(3/2)^(1/3)": [ + "1.14471424255333186780804221193967700891590692078793107209905", + "1.14471424255333186780804221193967700891590692078793107209906" + ] + }, + "certified_enclosures_math_199": { + "D_3": [ + "5.32318026888989689492319873968726063578438852940845576405060", + "5.32318026888989689492319873968726063578438852947338433618854" + ], + "c_4_ref": [ + "0.0233216660029528350945211949528568851531013723630981034059901", + "0.0233216660029528350945211949528568851531013723633825654059788" + ] + }, + "reduction_data": { + "m=3": { + "alpha": "3/8", + "kappa": "1/12 sqrt(6)", + "lambda_erfc": "1/24", + "lambda_poly": "1/12", + "prefactor": "1/32 pi^(-1)", + "G_0_constant": "1/3 sqrt(6) pi^(1/2)", + "e_k(s) by power, erfc branch": { + "1": [ + "0", + "0", + "80/9", + "0", + "-2/9", + "0", + "1/432", + "0", + "1/46656" + ], + "3": [ + "-80/9", + "0", + "-4/9", + "0", + "5/432", + "0", + "-19/46656" + ], + "5": [ + "2/3", + "0", + "1/144", + "0", + "11/5184" + ], + "7": [ + "-1/48", + "0", + "-1/576" + ] + }, + "r_k(s) by power, polynomial branch": { + "1": [ + "0", + "0", + "0", + "80/27", + "0", + "-2/243", + "0", + "-1/11664" + ], + "3": [ + "0", + "-80/27", + "0", + "-16/243", + "0", + "19/11664" + ], + "5": [ + "0", + "2/27", + "0", + "-11/1296" + ], + "7": [ + "0", + "1/144" + ] + }, + "J_k = A_k sqrt(2 pi) erf(s/(2 sqrt2)) + B_k + C_k(s) e^{-s^2/8}": { + "0": { + "A": "1", + "B": "0", + "C": [] + }, + "1": { + "A": "0", + "B": "4", + "C": [ + "-4" + ] + }, + "2": { + "A": "4", + "B": "0", + "C": [ + "0", + "-4" + ] + }, + "3": { + "A": "0", + "B": "32", + "C": [ + "-32", + "0", + "-4" + ] + }, + "4": { + "A": "48", + "B": "0", + "C": [ + "0", + "-48", + "0", + "-4" + ] + }, + "5": { + "A": "0", + "B": "512", + "C": [ + "-512", + "0", + "-64", + "0", + "-4" + ] + }, + "6": { + "A": "960", + "B": "0", + "C": [ + "0", + "-960", + "0", + "-80", + "0", + "-4" + ] + }, + "7": { + "A": "0", + "B": "12288", + "C": [ + "-12288", + "0", + "-1536", + "0", + "-96", + "0", + "-4" + ] + } + } + }, + "m=2": { + "kappa": "1/20 sqrt(30)", + "lambda_erfc": "1/8", + "lambda_poly": "1/5" + }, + "atoms_created_by_the_derivation": [ + "1", + "arctan(1/5 sqrt(15))", + "arctan(1/2 sqrt(1))" + ], + "note": "arctan(sqrt15/5) arises in the m = 2 erfc branch (kappa = sqrt30/20 against e^{-p^2/8}) and cancels exactly in D_2" + }, + "exact_relations": { + "M_0(lam, 1)": "(1/2) sqrt(pi/lam)", + "M_1(lam, 1)": "1/(2 lam)", + "M_0(lam, erf(u .))": "arctan(u/sqrt lam)/sqrt(pi lam)", + "M_0(lam, erf(u .) erf(v .))": "arctan(u v/sqrt(lam (lam + u^2 + v^2)))/sqrt(pi lam) (present in the code; not on the path of D_3)", + "M_n(lam, f), n >= 1": "[(n-1) M_{n-2}(lam, f) + sum_{u in f} (2u/sqrt pi) M_{n-1}(lam + u^2, f minus u)]/(2 lam)", + "D_3 integral": "(1/(32 pi)) [sqrt(2 pi/3) int e^{-s^2/24} erfc(s/(2 sqrt6)) sum_k e_k J_k + int e^{-s^2/12} sum_k r_k J_k]", + "arguments": "kappa/sqrt(1/24) = 1 (arctan = pi/4), kappa/sqrt(1/6) = 1/2" + } +} diff --git a/coefficients/side24_d4_closed_form_20260930/SOURCE_FILES.json b/coefficients/side24_d4_closed_form_20260930/SOURCE_FILES.json new file mode 100644 index 000000000..5d834f9c6 --- /dev/null +++ b/coefficients/side24_d4_closed_form_20260930/SOURCE_FILES.json @@ -0,0 +1,70 @@ +{ + "schema": 1, + "object": "CL-SIDE24-D3-CLOSED-FORM-20260930-v1", + "scientific_effect": "NONE", + "certified": true, + "review_status": "AUTHOR_SIDE_EXACT_IDENTITY_NONAUTHOR_READS_OPEN", + "disposition": "EXACT_CLOSED_FORM_OF_D3_FROM_THE_MATH199_REDUCTION_NO_REGISTER_CHANGE_SIDE24_V1_UNCHANGED", + "declarative": true, + "executed": false, + "base": "3e0a91b69892b9717564c592e7a966492a81566a", + "claim": "https://github.com/d6g8k5htny-coder/Math-/pull/199#issuecomment-5918624116", + "result": { + "D_3": "50/3 - 76/(3 pi) - (200/(9 pi)) arctan(1/2) = (50 pi + 200 arctan 2 - 228)/(9 pi)", + "c_4_ref": "Gamma(7/6) (3/2)^(1/3) (50 pi + 200 arctan 2 - 228)/(72 sqrt3 pi^(7/2))", + "D_1": "4/3", + "D_2": "29/6 - sqrt6" + }, + "pins_on_main": [ + { + "label": "LP", + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "role": "(15.1) the cone moment; (15.2) the coefficient c_{d,L}", + "workflow_checked": true + }, + { + "label": "S24", + "path": "coefficients/side24_v1/PROOF.md", + "git_blob": "44b66f04f89fcd87383b3603fa69f1feb64cdddd", + "role": "section 1 reference law A = Q + sqrt(2/3) Z I_m, D_1 = 4/3, D_2 = 29/6 - sqrt6 (the m = 1, 2 regressions)", + "workflow_checked": true + } + ], + "companion_not_on_main": [ + { + "pr": "https://github.com/d6g8k5htny-coder/Math-/pull/199", + "commit": "4fc6d15", + "path": "coefficients/side24_d4_20260930/RESULTS.json", + "git_blob": "187552f596576c9dcdecd1deabc0304412d8a1f7", + "role": "the certified enclosures of D_3 and c_{4,ref} quoted in the script (rules D3_INSIDE_CERTIFIED, C4_CLOSED, PINNED)" + }, + { + "pr": "https://github.com/d6g8k5htny-coder/Math-/pull/199", + "commit": "4fc6d15", + "path": "coefficients/side24_d4_20260930/NOTE.md", + "git_blob": "20e9acdba67f36e83a9db640b8759ce03485d3dc", + "role": "sections 1-2, the one-dimensional reduction that is integrated exactly here; section 4, the coefficient formula" + } + ], + "files": [ + { + "path": "NOTE.md", + "bytes": 15525, + "sha256": "b0756af59a92f9c8397614c9b4775959fe20caa7254949a664ee8285dfec0b2c", + "git_blob": "cbf35dead9f20cb8e68c357c62aca6413fb870af" + }, + { + "path": "RESULTS.json", + "bytes": 5092, + "sha256": "bfbe37fde021f47a878a9c565bd9f3790a4891c2b8f397bbcd89a6ac6e234d67", + "git_blob": "a44807969567a2091d909dc2a772bc1a91ec4eaa" + }, + { + "path": "closed_form_d3.py", + "bytes": 33890, + "sha256": "bd471be7d8b9199a3f305b0e1418ccfaa11cb7020b3d7e24412b9bada224eab5", + "git_blob": "a0c9169227c9a0b42c66deaca2b4f2e3168046ab" + } + ] +} diff --git a/coefficients/side24_d4_closed_form_20260930/closed_form_d3.py b/coefficients/side24_d4_closed_form_20260930/closed_form_d3.py new file mode 100644 index 000000000..a0c916922 --- /dev/null +++ b/coefficients/side24_d4_closed_form_20260930/closed_form_d3.py @@ -0,0 +1,840 @@ +"""The SIDE24 cone moment D_3 in closed form: D_3 = 50/3 - 76/(3 pi) - (200/(9 pi)) arctan(1/2) = (50 pi + 200 arctan 2 - 228)/(9 pi). + +Standard library only. Run from anywhere: python -B -S closed_form_d3.py [--mutant NAME] + +Object. Math-#199 (coefficients/side24_d4_20260930) reduces the d = 4 cone moment D_3 = E[det(A)^2 1{A < 0}] of SIDE24's +reference law A = Q + sqrt(2/3) Z I_3 to the one-dimensional integral + + D_3 = (1/(32 pi)) [ sqrt(2 pi/3) int_0^inf e^{-s^2/24} erfc(s/(2 sqrt6)) sum_k e_k(s) J_k(s) ds + + int_0^inf e^{-s^2/12} sum_k r_k(s) J_k(s) ds ], J_k(s) = int_0^s q^k e^{-q^2/8} dq, + +with rational polynomials e_k, r_k produced by exact algebra from the ordered-sector integrand (the same code as #199), and +encloses it by certified quadrature. Here the same integral is evaluated exactly. Only odd k occur, so every J_k is +B_k + C_k(s) e^{-s^2/8} with a rational constant B_k and a rational polynomial C_k (no erf inside J_k), and every term of +D_3 is a moment M_n(lam, f) = int_0^inf s^n e^{-lam s^2} f(s) ds with f = 1 or f = erf(kappa s), kappa = 1/(2 sqrt6), +lam in {1/24, 1/12, 1/6, 5/24} (erfc = 1 - erf). These are elementary: + + M_0(lam, 1) = (1/2) sqrt(pi/lam), M_1(lam, 1) = 1/(2 lam), M_0(lam, erf(kappa .)) = arctan(kappa/sqrt lam)/sqrt(pi lam), + M_n(lam, f) = [ (n-1) M_{n-2}(lam, f) + (2 kappa/sqrt pi) M_{n-1}(lam + kappa^2, 1) ] / (2 lam) (n >= 1, by parts), + +and the arguments that occur are kappa/sqrt lam = 1 (lam = 1/24, arctan = pi/4) and 1/2 (lam = 1/6). The computation is +carried out in exact arithmetic on the Q-span of sqrt(r) pi^(k/2) A (r squarefree, k an integer, A = 1 or an arctan atom), +so the output is an identity, not an approximation. The same code gives D_1 = 4/3 and D_2 = 29/6 - sqrt6 exactly (rules), +and the interval evaluation of the closed form lies inside #199's certified enclosure of D_3 (47 common digits; rule). +Consequently c_{4,ref} = Gamma(7/6) (3/2)^(1/3) (50 pi + 200 arctan 2 - 228) / (72 sqrt3 pi^(7/2)). Scientific effect NONE. +""" +import argparse +import json +import math +import sys +import time +from decimal import Decimal, Context, ROUND_FLOOR, ROUND_CEILING, ROUND_HALF_EVEN, setcontext +from fractions import Fraction as Fr +from functools import lru_cache + +MUTANTS = ("shift-variance", "vandermonde", "erfc-sign", "jacobian", "mehta", "by-parts", "one-erf", "jk-init", + "gauss-half", "boundary-term", "atom-pi") +MUT = None + +PREC = 60 +CF = Context(prec=PREC, rounding=ROUND_FLOOR, Emin=-9999999, Emax=9999999) +CC = Context(prec=PREC, rounding=ROUND_CEILING, Emin=-9999999, Emax=9999999) +CE = Context(prec=PREC, rounding=ROUND_HALF_EVEN, Emin=-9999999, Emax=9999999) +setcontext(Context(prec=2 * PREC + 20, rounding=ROUND_HALF_EVEN, Emin=-9999999, Emax=9999999)) +ZERO, ONE, HALF = Decimal(0), Decimal(1), Decimal("0.5") +ROOT_DIGITS = 70 + +# Math-#199 v1.1 (coefficients/side24_d4_20260930/RESULTS.json at 4fc6d15): the certified enclosures this closed form must meet +CERTIFIED = { + "D_3": ("5.32318026888989689492319873968726063578438852940845576405060", "5.32318026888989689492319873968726063578438852947338433618854"), + "c_4_ref": ("0.0233216660029528350945211949528568851531013723630981034059901", "0.0233216660029528350945211949528568851531013723633825654059788"), +} +PINNED = {"D_3": "5.323180268889896894923198739687260635784388529", + "c_4_ref": "0.023321666002952835094521194952856885153101372363", + "pi": "3.14159265358979323846264338327950288419716939937510"} +CLOSED_FORM = {"1": Fr(50, 3), "1/pi": Fr(-76, 3), "arctan(1/2)/pi": Fr(-200, 9)} + + +# ---------------- interval arithmetic over decimal (the #199 toolkit, unchanged) +def ulp(x): + if x == 0: + return Decimal(1).scaleb(-PREC - 30) + return Decimal(1).scaleb(x.adjusted() - PREC + 1) + + +class Iv: + """Closed interval [lo, hi] of Decimals; every operation encloses the exact result.""" + __slots__ = ("lo", "hi") + + def __init__(self, lo, hi=None): + if hi is None: + hi = lo + if lo > hi: + raise ValueError("empty interval") + self.lo, self.hi = lo, hi + + @staticmethod + def frac(q): + q = Fr(q) + n, d = Decimal(q.numerator), Decimal(q.denominator) + return Iv(CF.divide(n, d), CC.divide(n, d)) + + @staticmethod + def of(x): + return x if isinstance(x, Iv) else Iv.frac(x) + + def __add__(a, b): + b = Iv.of(b) + return Iv(CF.add(a.lo, b.lo), CC.add(a.hi, b.hi)) + __radd__ = __add__ + + def __neg__(a): + return Iv(a.hi.copy_negate(), a.lo.copy_negate()) + + def __sub__(a, b): + b = Iv.of(b) + return Iv(CF.subtract(a.lo, b.hi), CC.subtract(a.hi, b.lo)) + + def __rsub__(a, b): + return Iv.of(b) - a + + def __mul__(a, b): + b = Iv.of(b) + c = [(x, y) for x in (a.lo, a.hi) for y in (b.lo, b.hi)] + return Iv(min(CF.multiply(x, y) for x, y in c), max(CC.multiply(x, y) for x, y in c)) + __rmul__ = __mul__ + + def __truediv__(a, b): + b = Iv.of(b) + if b.lo <= 0 <= b.hi: + raise ZeroDivisionError("interval division by an interval containing 0") + c = [(x, y) for x in (a.lo, a.hi) for y in (b.lo, b.hi)] + return Iv(min(CF.divide(x, y) for x, y in c), max(CC.divide(x, y) for x, y in c)) + + def __rtruediv__(a, b): + return Iv.of(b) / a + + def sq(a): + if a.lo <= 0 <= a.hi: + return Iv(ZERO, max(CC.multiply(a.lo, a.lo), CC.multiply(a.hi, a.hi))) + return a * a + + def exp(a): + lo, hi = CE.exp(a.lo), CE.exp(a.hi) + return Iv(max(ZERO, CF.subtract(lo, CC.multiply(Decimal(2), ulp(lo)))), CC.add(hi, CC.multiply(Decimal(2), ulp(hi)))) + + def sqrt(a): + if a.lo < 0: + raise ValueError("sqrt of an interval with negative part") + lo, hi = CE.sqrt(a.lo), CE.sqrt(a.hi) + return Iv(max(ZERO, CF.subtract(lo, CC.multiply(Decimal(2), ulp(lo)))), CC.add(hi, CC.multiply(Decimal(2), ulp(hi)))) + + def width(a): + return CC.subtract(a.hi, a.lo) + + def contains(a, x): + x = Iv.of(x) + return a.lo <= x.lo and x.hi <= a.hi + + def intersects(a, b): + return a.lo <= b.hi and b.lo <= a.hi + + def pair(a): + return [str(a.lo), str(a.hi)] + + +def hull(a, b): + return Iv(min(a.lo, b.lo), max(a.hi, b.hi)) + + +def ipow(x, n): + r = Iv(ONE) + for _ in range(n): + r = r * x + return r + + +def inroot(N, n): + if N < 2: + return N + x = 1 << ((N.bit_length() + n - 1) // n) + while True: + y = ((n - 1) * x + N // pow(x, n - 1)) // n + if y >= x: + break + x = y + if not (pow(x, n) <= N < pow(x + 1, n)): + raise ValueError("integer root failed") + return x + + +def root_frac(q, n): + q = Fr(q) + if q <= 0: + raise ValueError("root of a nonpositive number") + p, d = q.numerator, q.denominator + scale = 10 ** ROOT_DIGITS + r = inroot(p * d ** (n - 1) * scale ** n, n) + den = d * scale + return Iv(Iv.frac(Fr(r, den)).lo, Iv.frac(Fr(r + 1, den)).hi) + + +def pi_interval(): + def atan_inv(n, terms): + x = Fr(1, n) + partial, sums = Iv(ZERO), [] + for m in range(terms + 2): + t = Iv.frac(x ** (2 * m + 1) / (2 * m + 1)) + partial = partial + t if m % 2 == 0 else partial - t + sums.append(partial) + return hull(sums[-1], sums[-2]) + return atan_inv(5, 44) * 16 - atan_inv(239, 22) * 4 + + +PI = pi_interval() +SQRTPI = PI.sqrt() +SQRT3 = Iv.frac(3).sqrt() +TINY = Decimal(10) ** (-PREC - 8) + + +def gamma_lower_point(x, a): + """gamma(a, x) by the positive series x^a e^-x sum_n x^n/(a (a+1) ... (a+n)); a = 7/6, x a Decimal > 0.""" + X = Iv(x) + t, S, n = Iv.frac(1 / a), Iv(ZERO), 0 + while True: + S = S + t + n += 1 + ratio = X / Iv.frac(a + n) + t = t * ratio + if ratio.hi <= HALF and t.hi < S.lo * TINY: + break + xa = X * root_frac(Fr(x), 6) + return xa * (-X).exp() * (S + Iv(ZERO, CC.multiply(Decimal(2), t.hi))) + + +def gamma_complete(a, X=Decimal(120)): + """Gamma(a) = gamma(a, X) + Gamma(a, X), 1 < a < 2, X^(a-1) e^-X <= Gamma(a, X) <= X^(a-1) e^-X / (1 - (a-1)/X).""" + low = gamma_lower_point(X, a) + up = root_frac(Fr(X), 6) * (-Iv(X)).exp() + return low + Iv(up.lo, (up / (1 - Iv.frac(a - 1) / Iv(X))).hi) + + +GAMMA76 = gamma_complete(Fr(7, 6)) +CBRT32 = root_frac(Fr(12), 3) / 2 # (3/2)^(1/3) + + +def atan_iv(a, N=90): + """arctan(a) for an interval 0 <= a <= 1: halve the argument, then the alternating series bracketed by consecutive + partial sums (for each fixed argument the terms decrease, so the value lies between them).""" + if a.lo < 0 or a.hi > 1: + raise ValueError("atan_iv needs 0 <= a <= 1") + a1 = a / (1 + (1 + a.sq()).sqrt()) + a1sq, p, S, prev = a1.sq(), a1, Iv(ZERO), None + for n in range(N + 1): + t = p / (2 * n + 1) + prev = S + S = S + t if n % 2 == 0 else S - t + p = p * a1sq + return 2 * hull(prev, S) + + +# ---------------- exact arithmetic: surds, and the Q-span of sqrt(r) pi^(k/2) ATOM +def sqf(n): + """n a positive integer -> (k, r) with sqrt(n) = k sqrt(r), r squarefree.""" + k, r, p, m = 1, 1, 2, n + while p * p <= m: + while m % (p * p) == 0: + m //= p * p + k *= p + if m % p == 0: + m //= p + r *= p + p += 1 + return k, r * m + + +def surd_mul(u, v): + """(c1, r1) (c2, r2) with (c, r) = c sqrt r.""" + k, r = sqf(u[1] * v[1]) + return (u[0] * v[0] * k, r) + + +def surd_sqrt(q): + """sqrt of a positive rational as a surd.""" + q = Fr(q) + if q <= 0: + raise ValueError("sqrt of a nonpositive rational") + k, r = sqf(q.numerator * q.denominator) + return (Fr(k, q.denominator), r) + + +def surd_inv(u): + return (1 / (u[0] * u[1]), u[1]) + + +def surd_sq(u): + return u[0] * u[0] * u[1] + + +ATOMS = [None] # index 0 is the number 1; index i > 0 is arctan(c sqrt r) for ATOMS[i] = (c, r), c sqrt r <= 1 + + +def E(c=1, r=1, twok=0, atom=0): + """The element c sqrt(r) pi^(twok/2) ATOMS[atom].""" + return {(r, twok, atom): Fr(c)} if c != 0 else {} + + +def add(u, v): + w = dict(u) + for k, c in v.items(): + w[k] = w.get(k, Fr(0)) + c + return {k: c for k, c in w.items() if c != 0} + + +def scale(u, c): + c = Fr(c) + return {k: v * c for k, v in u.items() if v * c != 0} + + +def mul_surd(u, s): + out = {} + for (r, twok, atom), c in u.items(): + k, r2 = sqf(r * s[1]) + key = (r2, twok, atom) + out[key] = out.get(key, Fr(0)) + c * s[0] * k + return {k: c for k, c in out.items() if c != 0} + + +def mul_pi_half(u, j): + """multiply by pi^(j/2).""" + return {(r, twok + j, atom): c for (r, twok, atom), c in u.items()} + + +def mul(u, v): + out = {} + for (r1, k1, a1), c1 in u.items(): + for (r2, k2, a2), c2 in v.items(): + if a1 and a2: + raise ValueError("product of two arctan atoms is outside the span") + k, r = sqf(r1 * r2) + key = (r, k1 + k2, a1 or a2) + out[key] = out.get(key, Fr(0)) + c1 * c2 * k + return {k: c for k, c in out.items() if c != 0} + + +def inv_monomial(u): + (r, twok, atom), c = next(iter(u.items())) + if len(u) != 1 or atom: + raise ValueError("only monomials without atoms are inverted") + return E(1 / (c * r), r, -twok) + + +def atan_elem(t): + """arctan(c sqrt r) as an element: rational multiples of pi are recognised (arguments 1, sqrt3, 1/sqrt3), an argument + above 1 is reflected (arctan t = pi/2 - arctan(1/t)), anything else becomes an atom with argument in (0, 1].""" + c, r = t + if c == 0: + return {} + if c < 0: + return scale(atan_elem((-c, r)), -1) + if surd_sq(t) > 1: + return add(E(Fr(1, 2), 1, 2), scale(atan_elem(surd_inv(t)), -1)) + if (c, r) == (1, 1): + return E(Fr(1, 4) if MUT != "atom-pi" else Fr(1, 3), 1, 2) + if r == 3 and c == Fr(1, 3): + return E(Fr(1, 6), 1, 2) + for i, a in enumerate(ATOMS): + if a == (c, r): + return E(1, 1, 0, i) + ATOMS.append((c, r)) + return E(1, 1, 0, len(ATOMS) - 1) + + +def iv_eval(u): + """Interval evaluation of an element (60 digits).""" + total = Iv(ZERO) + for (r, twok, atom), c in u.items(): + term = Iv.frac(c) + if r != 1: + term = term * root_frac(Fr(r), 2) + if twok: + pp = ipow(PI, abs(twok) // 2) * (SQRTPI if twok % 2 else Iv(ONE)) + term = term * pp if twok > 0 else term / pp + if atom: + ca, ra = ATOMS[atom] + arg = Iv.frac(ca) * (root_frac(Fr(ra), 2) if ra != 1 else Iv(ONE)) + term = term * atan_iv(arg) + total = total + term + return total + + +def fl_eval(u): + """Float evaluation of an element (controls only).""" + v = 0.0 + for (r, twok, atom), c in u.items(): + t = float(c) * math.sqrt(r) * math.pi ** (twok / 2) + if atom: + ca, ra = ATOMS[atom] + t *= math.atan(float(ca) * math.sqrt(ra)) + v += t + return v + + +def show(u): + parts = [] + for (r, twok, atom) in sorted(u, key=lambda k: (k[2], -k[1], k[0])): + c = u[(r, twok, atom)] + s = str(c) + if r != 1: + s += " sqrt(%d)" % r + if twok: + s += " pi^(%s)" % Fr(twok, 2) + if atom: + ca, ra = ATOMS[atom] + s += " arctan(%s%s)" % (ca, "" if ra == 1 else " sqrt(%d)" % ra) + parts.append(s) + return " + ".join(parts) if parts else "0" + + +# ---------------- the moments M(n, lam, slopes) = int_0^inf s^n e^{-lam s^2} prod_u erf(u s) ds +@lru_cache(maxsize=None) +def M(n, lam, slopes): + lam = Fr(lam) + if n == 0: + inv_sqrt_lam = surd_sqrt(1 / lam) + if not slopes: # (1/2) sqrt(pi/lam) + return mul_pi_half(mul_surd(E(Fr(1, 2) if MUT != "gauss-half" else Fr(1)), inv_sqrt_lam), 1) + if len(slopes) == 1: # arctan(u/sqrt lam)/sqrt(pi lam) + u = slopes[0] + t = surd_mul(u, inv_sqrt_lam) if MUT != "one-erf" else (u[0] / lam, u[1]) + return mul_pi_half(mul_surd(atan_elem(t), inv_sqrt_lam), -1) + if len(slopes) == 2: # arctan(uv/sqrt(lam(lam+u^2+v^2)))/sqrt(pi lam) + u, v = slopes + den = surd_sqrt(lam * (lam + surd_sq(u) + surd_sq(v))) + t = surd_mul(surd_mul(u, v), surd_inv(den)) + return mul_pi_half(mul_surd(atan_elem(t), inv_sqrt_lam), -1) + raise ValueError("at most two erf factors") + if n == 1 and not slopes: + return E(1 / (2 * lam) if MUT != "boundary-term" else 1 / lam) + # by parts: s^n e^{-lam s^2} f = s^{n-1} f . s e^{-lam s^2}; the boundary term vanishes (n >= 2, or f(0) = 0) + out = {} + if n >= 2: + out = add(out, scale(M(n - 2, lam, slopes), n - 1 if MUT != "by-parts" else n)) + for i, u in enumerate(slopes): + rest = slopes[:i] + slopes[i + 1:] + term = M(n - 1, lam + surd_sq(u), rest) # f' contributes (2u/sqrt pi) e^{-u^2 s^2} + out = add(out, mul_pi_half(mul_surd(term, (2 * u[0], u[1])), -1)) + return scale(out, 1 / (2 * lam)) + + +def gauss_moment_closed(n, lam): + """(1/2) Gamma((n+1)/2) lam^{-(n+1)/2} as an element (the direct closed form, used only by rule GAUSS_MOMENTS).""" + lam = Fr(lam) + g = gamma_half(n + 1) + if (n + 1) % 2 == 0: + return scale(mul(g, E(Fr(1) / lam ** ((n + 1) // 2))), Fr(1, 2)) + return scale(mul_surd(mul(g, E(Fr(1) / lam ** (n // 2))), surd_sqrt(1 / lam)), Fr(1, 2)) + + +# ---------------- exact polynomial algebra and the sector reduction (as in #199) +def padd(u, v): + w = dict(u) + for k, c in v.items(): + w[k] = w.get(k, Fr(0)) + c + return {k: c for k, c in w.items() if c != 0} + + +def pmul(u, v): + w = {} + for k1, c1 in u.items(): + for k2, c2 in v.items(): + k = tuple(a + b for a, b in zip(k1, k2)) + w[k] = w.get(k, Fr(0)) + c1 * c2 + return {k: c for k, c in w.items() if c != 0} + + +def pscale(u, c): + return {k: v * c for k, v in u.items() if v * c != 0} + + +def pconst(c, nvars): + return {(0,) * nvars: Fr(c)} if c != 0 else {} + + +def pvar(i, nvars): + e = [0] * nvars + e[i] = 1 + return {tuple(e): Fr(1)} + + +def ppow(u, n, nvars): + r = pconst(1, nvars) + for _ in range(n): + r = pmul(r, u) + return r + + +def psubst(u, images, nvars_out): + out = {} + for k, c in u.items(): + term = pconst(c, nvars_out) + for i, e in enumerate(k): + if e: + term = pmul(term, ppow(images[i], e, nvars_out)) + out = padd(out, term) + return out + + +def univariate(u): + if not u: + return [Fr(0)] + deg = max(k[0] for k in u) + return [u.get((n,), Fr(0)) for n in range(deg + 1)] + + +def reduce_sector(m): + """Ordered sector mu_m = -a, mu_{m-1} = -a - p_1, ...: (prod mu_i^2 prod_{i 0: + acc = padd(acc, pvar(i, nv)) + mus.append(pscale(acc, Fr(-1))) + poly = pconst(1, nv) + for mu in mus: + poly = pmul(poly, pmul(mu, mu)) + if MUT != "vandermonde": + for i in range(m): + for j in range(i + 1, m): + poly = pmul(poly, padd(mus[i], pscale(mus[j], Fr(-1)))) + S, norm2 = {}, {} + for mu in mus: + S = padd(S, mu) + norm2 = padd(norm2, pmul(mu, mu)) + shift = Fr(1, 4 * (m + 3)) if MUT != "shift-variance" or m != 3 else Fr(1, 20) + quad = padd(pscale(norm2, Fr(1, 4)), pscale(pmul(S, S), -shift)) + return poly, quad + + +def a_integrated_terms(m): + """Exact a-integral: erfc branch PE (times G_0) and polynomial branch PR, with exponents expE and rest.""" + poly, quad = reduce_sector(m) + nv = m + alpha = quad.get((2,) + (0,) * (nv - 1), Fr(0)) + beta = {k[1:]: c for k, c in quad.items() if k[0] == 1} + rest = {k[1:]: c for k, c in quad.items() if k[0] == 0} + nvr = nv - 1 + P = [pconst(1, nvr), pscale(beta, Fr(-1, 2) / alpha)] + R = [{}, pconst(Fr(1, 2) / alpha, nvr)] + deg_a = max(k[0] for k in poly) + for n in range(1, deg_a): + P.append(pscale(padd(pscale(P[n - 1], Fr(n)), pscale(pmul(beta, P[n]), Fr(-1))), Fr(1, 2) / alpha)) + R.append(pscale(padd(pscale(R[n - 1], Fr(n)), pscale(pmul(beta, R[n]), Fr(-1))), Fr(1, 2) / alpha)) + PE, PR = {}, {} + for k, c in poly.items(): + n = k[0] + w = {k[1:]: c} + PE = padd(PE, pmul(w, P[n])) + PR = padd(PR, pmul(w, R[n])) + expE = padd(rest, pscale(pmul(beta, beta), Fr(-1, 4) / alpha)) + return alpha, beta, PE, PR, expE, rest + + +def gamma_half(twice): + """Gamma(twice/2) as an element.""" + if twice % 2 == 0: + return E(math.factorial(twice // 2 - 1)) + k = (twice - 1) // 2 + return E(Fr(math.factorial(2 * k), 4 ** k * math.factorial(k)), 1, 1) + + +def mehta_Z(m): + """Z_m = 2^(m/2 + m(m-1)/4) (2 pi)^(m/2) prod_{j<=m} Gamma(1 + j/2) / Gamma(3/2)^m as an element.""" + m_eff = m + 1 if (MUT == "mehta" and m == 3) else m + prod = E(1) + for j in range(1, m_eff + 1): + prod = mul(prod, gamma_half(j + 2)) + pw = Fr(m_eff, 2) + Fr(m_eff * (m_eff - 1), 4) + two_pow = E(2 ** int(pw), 2 if pw.denominator == 2 else 1) + twopi_pow = mul_pi_half(E(2 ** (m_eff // 2), 2 if m_eff % 2 else 1), m_eff) + g = E(1) + for _ in range(m_eff): + g = mul(g, gamma_half(3)) + return mul(mul(mul(two_pow, twopi_pow), prod), inv_monomial(g)) + + +def prefactor(m, jac): + """sqrt(3/(m+3)) m! / Z_m times the Jacobian of the final substitution.""" + return mul_surd(scale(inv_monomial(mehta_Z(m)), math.factorial(m) * jac), surd_sqrt(Fr(3, m + 3))) + + +def jk_exact(kmax): + """J_k(s) = A_k sqrt(2 pi) erf(s/(2 sqrt2)) + B_k + C_k(s) e^{-s^2/8}: (A_k, B_k, C_k by power) from J_0, J_1 and + J_{k+2} = -4 s^{k+1} e^{-s^2/8} + 4(k+1) J_k.""" + J = [(Fr(1), Fr(0), []), (Fr(0), Fr(4), [Fr(-4)])] + if MUT == "jk-init": + J[1] = (Fr(0), Fr(2), [Fr(-2)]) + for k in range(kmax - 1): + A, B, C = J[k] + Cn = [4 * (k + 1) * c for c in C] + [Fr(0)] * max(0, k + 2 - len(C)) + Cn[k + 1] += Fr(-4) + J.append((4 * (k + 1) * A, 4 * (k + 1) * B, Cn)) + return J + + +def jk_identities(JK): + """J_k(0) = 0, J_k'(s) = s^k e^{-s^2/8} (A_k + C_k' - (s/4) C_k = s^k), J_k(inf) = (1/2) 8^{(k+1)/2} Gamma((k+1)/2).""" + ok = True + for k, (A, B, C) in enumerate(JK): + ok &= B + (C[0] if C else 0) == 0 + deriv = {} + for i, c in enumerate(C): + if i: + deriv[i - 1] = deriv.get(i - 1, Fr(0)) + i * c + deriv[i + 1] = deriv.get(i + 1, Fr(0)) - c / 4 + deriv[0] = deriv.get(0, Fr(0)) + A + ok &= {i: c for i, c in deriv.items() if c} == {k: Fr(1)} + at_inf = add(mul_pi_half(E(A, 2), 1), E(B)) + eight = E(8 ** ((k + 1) // 2), 2 if (k + 1) % 2 else 1) + if (k + 1) % 2: + eight = scale(eight, 2) # 8^(1/2) = 2 sqrt2 + ok &= at_inf == scale(mul(eight, gamma_half(k + 1)), Fr(1, 2)) + return ok + + +# ---------------- D_1, D_2, D_3 exactly +def D1_exact(): + """D_1 = (sqrt3/2) (1/(2 sqrt pi)) int_0^inf mu^2 e^{-3 mu^2/16} dmu.""" + return mul_pi_half(mul_surd(scale(M(2, Fr(3, 16), ()), Fr(1, 4)), (Fr(1), 3)), -1) + + +def erfc_moment(n, lam, kappa): + """int_0^inf s^n e^{-lam s^2} erfc(kappa s) ds = M_n(lam, 1) - M_n(lam, erf(kappa .)).""" + sign = -1 if MUT != "erfc-sign" else 1 + return add(M(n, lam, ()), scale(M(n, lam, (kappa,)), sign)) + + +def D2_exact(): + """m = 2: one remaining variable p; erfc branch e^{-p^2/8} erfc(p sqrt30/20), polynomial branch e^{-p^2/5}.""" + alpha, beta, PE, PR, expE, rest = a_integrated_terms(2) + if set(expE) - {(2,)} or set(rest) - {(2,)} or set(beta) - {(1,)}: + raise ValueError("m = 2 structure") + gE, gR, b1 = expE[(2,)], rest[(2,)], beta[(1,)] + kappa = surd_mul((b1 / 2, 1), surd_sqrt(1 / alpha)) + constE = mul_pi_half(mul_surd(E(Fr(1, 2)), surd_sqrt(1 / alpha)), 1) # (1/2) sqrt(pi/alpha) + eb, rb = {}, {} + for n, c in enumerate(univariate(PE)): + eb = add(eb, scale(erfc_moment(n, gE, kappa), c)) + for n, c in enumerate(univariate(PR)): + rb = add(rb, scale(M(n, gR, ()), c)) + return mul(prefactor(2, 1), add(mul(constE, eb), rb)), {"kappa": kappa, "lambda_erfc": gE, "lambda_poly": gR} + + +def D3_exact(): + """m = 3: p = (s - q)/2 (Jacobian 1/2), q over (0, s) through J_k, then the s-moments exactly.""" + alpha, beta, PE, PR, expE, rest = a_integrated_terms(3) + s, q = pvar(0, 2), pvar(1, 2) + images = [pscale(padd(s, pscale(q, Fr(-1))), Fr(1, 2)), q] + PEs, PRs = psubst(PE, images, 2), psubst(PR, images, 2) + eE, eR, bs = psubst(expE, images, 2), psubst(rest, images, 2), psubst(beta, images, 2) + if set(eE) != {(2, 0), (0, 2)} or set(eR) != {(2, 0), (0, 2)} or eE[(0, 2)] != Fr(1, 8) or eR[(0, 2)] != Fr(1, 8) or set(bs) != {(1, 0)}: + raise ValueError("decoupling failed: " + repr((eE, eR, bs))) + gE, gR = eE[(2, 0)], eR[(2, 0)] + kappa = surd_mul((bs[(1, 0)] / 2, 1), surd_sqrt(1 / alpha)) + b = (Fr(1, 4), 2) # 1/(2 sqrt2), the erf slope inside J_even + constE = mul_pi_half(mul_surd(E(Fr(1, 2)), surd_sqrt(1 / alpha)), 1) + + def by_q_power(Pxy): + out = {} + for (i, j), c in Pxy.items(): + out.setdefault(j, {})[(i,)] = c + return out + qE, qR = by_q_power(PEs), by_q_power(PRs) + kmax = max(max(qE), max(qR)) + JK = jk_exact(kmax) + sqrt2pi = mul_pi_half(E(1, 2), 1) + polys = {"e": {k: univariate(v) for k, v in sorted(qE.items())}, "r": {k: univariate(v) for k, v in sorted(qR.items())}} + + def branch(Pq, lam, erfc): + tot = {} + for k, coef_poly in sorted(Pq.items()): + A, B, C = JK[k] + for j, c in enumerate(univariate(coef_poly)): + if c == 0: + continue + term = {} + if A: # A_k sqrt(2 pi) erf(s/(2 sqrt2)) + x = M(j, lam, (b,)) + if erfc: + x = add(x, scale(M(j, lam, (kappa, b)), -1 if MUT != "erfc-sign" else 1)) + term = add(term, scale(mul(sqrt2pi, x), A)) + if B: # the constant B_k + term = add(term, scale(erfc_moment(j, lam, kappa) if erfc else M(j, lam, ()), B)) + for i, ci in enumerate(C): # C_k(s) e^{-s^2/8} + if ci: + term = add(term, scale(erfc_moment(j + i, lam + Fr(1, 8), kappa) if erfc else M(j + i, lam + Fr(1, 8), ()), ci)) + tot = add(tot, scale(term, c)) + return tot + jac = Fr(1, 2) if MUT != "jacobian" else Fr(1) + pref = prefactor(3, jac) + eb = mul(mul(pref, constE), branch(qE, gE, True)) + rb = mul(pref, branch(qR, gR, False)) + info = {"alpha": alpha, "kappa": kappa, "lambda_erfc": gE, "lambda_poly": gR, "kmax": kmax, + "q_powers_erfc": sorted(qE), "q_powers_poly": sorted(qR), "polys": polys, "JK": JK, + "erfc_branch": eb, "poly_branch": rb, "prefactor": pref, "constE": constE} + return add(eb, rb), info + + +# ---------------- float controls (not part of the certificate) +def simpson(f, a, b, n=4000): + h = (b - a) / n + s = f(a) + f(b) + for i in range(1, n): + s += (4 if i % 2 else 2) * f(a + i * h) + return s * h / 3 + + +def float_moment(n, lam, slopes): + lam = float(lam) + us = [float(c) * math.sqrt(r) for c, r in slopes] + T = math.sqrt(140 / lam) + def f(s): + v = s ** n * math.exp(-lam * s * s) + for u in us: + v *= math.erf(u * s) + return v + return simpson(f, 0.0, T, 20000) + + +# ---------------- main +def main(): + global MUT + ap = argparse.ArgumentParser() + ap.add_argument("--mutant", choices=MUTANTS) + args = ap.parse_args() + MUT = args.mutant + t0 = time.time() + checks = {} + + d1 = D1_exact() + d2, info2 = D2_exact() + d3, info3 = D3_exact() + atoms_used = list(ATOMS) # the atoms created by the derivation itself (controls below may add more) + D2_target = add(E(Fr(29, 6)), E(-1, 6)) + D3_target = add(add(E(CLOSED_FORM["1"]), E(CLOSED_FORM["1/pi"], 1, -2)), + mul_pi_half(scale(atan_elem((Fr(1, 2), 1)), CLOSED_FORM["arctan(1/2)/pi"]), -2)) + + # STRUCTURE: the decoupled exponents (checked inside D3_exact), erfc slope kappa = 1/(2 sqrt6), only odd q-powers, arguments 1 and 1/2 + checks["STRUCTURE"] = bool(info3["kappa"] == (Fr(1, 12), 6) and info3["lambda_erfc"] == Fr(1, 24) and info3["lambda_poly"] == Fr(1, 12) + and all(k % 2 == 1 for k in info3["q_powers_erfc"] + info3["q_powers_poly"]) and info3["kmax"] == 7 + and atoms_used[-1] == (Fr(1, 2), 1) and len(atoms_used) == 3) + # GAUSS_MOMENTS: the by-parts recurrence at f = 1 reproduces (1/2) Gamma((n+1)/2) lam^{-(n+1)/2} exactly + lams = (Fr(1, 24), Fr(1, 12), Fr(1, 6), Fr(5, 24), Fr(1, 8), Fr(1, 5), Fr(3, 16)) + checks["GAUSS_MOMENTS"] = bool(all(M(n, lam, ()) == gauss_moment_closed(n, lam) for n in range(13) for lam in lams)) + checks["JK_EXACT"] = bool(jk_identities(info3["JK"])) + checks["D1_EXACT"] = bool(d1 == E(Fr(4, 3))) + checks["D2_EXACT"] = bool(d2 == D2_target) + checks["D3_FORM"] = bool(d3 == D3_target) + # float controls of the base integrals and of sampled moments (Simpson on [0, sqrt(140/lam)]; erf from math) + b1 = [(Fr(1, 24), (Fr(1, 12), 6)), (Fr(1, 6), (Fr(1, 12), 6)), (Fr(1, 8), (Fr(1, 20), 30)), (Fr(1, 7), (Fr(2, 3), 1))] + ok = True + for lam, u in b1: + got = float_moment(0, lam, (u,)) + want = math.atan(float(u[0]) * math.sqrt(u[1]) / math.sqrt(lam)) / math.sqrt(math.pi * lam) + ok &= abs(got - want) < 1e-9 + for lam, u, v in ((Fr(1, 24), (Fr(1, 12), 6), (Fr(1, 4), 2)), (Fr(1, 3), (Fr(1, 2), 1), (Fr(1, 3), 5))): + got = float_moment(0, lam, (u, v)) + uu, vv = float(u[0]) * math.sqrt(u[1]), float(v[0]) * math.sqrt(v[1]) + want = math.atan(uu * vv / math.sqrt(lam * (lam + uu * uu + vv * vv))) / math.sqrt(math.pi * lam) + ok &= abs(got - want) < 1e-9 + checks["BASE_INTEGRALS_FLOAT"] = bool(ok) + ok = True + for n in range(7): + for lam, slopes in ((Fr(1, 24), ((Fr(1, 12), 6),)), (Fr(1, 6), ((Fr(1, 12), 6),)), (Fr(1, 12), ()), (Fr(1, 8), ((Fr(1, 20), 30),)), + (Fr(1, 24), ((Fr(1, 12), 6), (Fr(1, 4), 2)))): + ex, fl = fl_eval(M(n, lam, slopes)), float_moment(n, lam, slopes) + ok &= abs(ex - fl) <= 1e-8 * max(1.0, abs(fl)) + checks["MOMENTS_FLOAT"] = bool(ok) + # interval evaluation of the closed form against #199's certified enclosure + D3_iv = iv_eval(d3) + cert = Iv(Decimal(CERTIFIED["D_3"][0]), Decimal(CERTIFIED["D_3"][1])) + checks["D3_INSIDE_CERTIFIED"] = bool(cert.contains(D3_iv) and D3_iv.width() < Decimal("1e-55")) + c4 = GAMMA76 * CBRT32 * D3_iv / (8 * SQRT3 * PI * PI * SQRTPI) + cert4 = Iv(Decimal(CERTIFIED["c_4_ref"][0]), Decimal(CERTIFIED["c_4_ref"][1])) + checks["C4_CLOSED"] = bool(cert4.contains(c4) and c4.width() < Decimal("1e-55")) + checks["LIBRARY_EXACT"] = bool(library_exact()) + pinned = {"D_3": D3_iv, "c_4_ref": c4, "pi": PI} + checks["PINNED"] = bool(all(str(pinned[k].lo).startswith(p) and str(pinned[k].hi).startswith(p) for k, p in PINNED.items())) + if len(checks) != 12: + raise ValueError("rule count changed") + passed = all(checks.values()) + + def fr(x): + return str(x) + out = { + "object": "CL-SIDE24-D3-CLOSED-FORM-20260930-v1", + "scientific_effect": "NONE", + "certified": True, + "mutant": MUT, + "passed": passed, + "checks": checks, + "closed_forms": { + "D_1": show(d1), + "D_2": show(d2), + "D_3": show(d3), + "D_3_equivalent": "(50 pi + 200 arctan 2 - 228) / (9 pi) = 50/3 - 76/(3 pi) - (100/(9 pi)) arccos(3/5)", + "c_4_ref": "Gamma(7/6) (3/2)^(1/3) (50 pi + 200 arctan 2 - 228) / (72 sqrt3 pi^(7/2))", + "erfc_branch_of_D_3": show(info3["erfc_branch"]), + "polynomial_branch_of_D_3": show(info3["poly_branch"]), + }, + "interval_evaluation": {"D_3": D3_iv.pair(), "c_4_ref": c4.pair(), "arctan(1/2)": atan_iv(Iv.frac(Fr(1, 2))).pair(), + "pi": PI.pair(), "Gamma(7/6)": GAMMA76.pair(), "(3/2)^(1/3)": CBRT32.pair()}, + "certified_enclosures_math_199": {"D_3": list(CERTIFIED["D_3"]), "c_4_ref": list(CERTIFIED["c_4_ref"])}, + "reduction_data": { + "m=3": {"alpha": fr(info3["alpha"]), "kappa": "%s sqrt(%d)" % info3["kappa"], "lambda_erfc": fr(info3["lambda_erfc"]), + "lambda_poly": fr(info3["lambda_poly"]), "prefactor": show(info3["prefactor"]), "G_0_constant": show(info3["constE"]), + "e_k(s) by power, erfc branch": {str(k): [fr(c) for c in v] for k, v in info3["polys"]["e"].items()}, + "r_k(s) by power, polynomial branch": {str(k): [fr(c) for c in v] for k, v in info3["polys"]["r"].items()}, + "J_k = A_k sqrt(2 pi) erf(s/(2 sqrt2)) + B_k + C_k(s) e^{-s^2/8}": { + str(k): {"A": fr(A), "B": fr(B), "C": [fr(c) for c in C]} for k, (A, B, C) in enumerate(info3["JK"])}}, + "m=2": {"kappa": "%s sqrt(%d)" % info2["kappa"], "lambda_erfc": fr(info2["lambda_erfc"]), "lambda_poly": fr(info2["lambda_poly"])}, + "atoms_created_by_the_derivation": ["1"] + ["arctan(%s sqrt(%d))" % a for a in atoms_used[1:]], + "note": "arctan(sqrt15/5) arises in the m = 2 erfc branch (kappa = sqrt30/20 against e^{-p^2/8}) and cancels exactly in D_2", + }, + "exact_relations": { + "M_0(lam, 1)": "(1/2) sqrt(pi/lam)", "M_1(lam, 1)": "1/(2 lam)", + "M_0(lam, erf(u .))": "arctan(u/sqrt lam)/sqrt(pi lam)", + "M_0(lam, erf(u .) erf(v .))": "arctan(u v/sqrt(lam (lam + u^2 + v^2)))/sqrt(pi lam) (present in the code; not on the path of D_3)", + "M_n(lam, f), n >= 1": "[(n-1) M_{n-2}(lam, f) + sum_{u in f} (2u/sqrt pi) M_{n-1}(lam + u^2, f minus u)]/(2 lam)", + "D_3 integral": "(1/(32 pi)) [sqrt(2 pi/3) int e^{-s^2/24} erfc(s/(2 sqrt6)) sum_k e_k J_k + int e^{-s^2/12} sum_k r_k J_k]", + "arguments": "kappa/sqrt(1/24) = 1 (arctan = pi/4), kappa/sqrt(1/6) = 1/2", + }, + } + sys.stdout.write(json.dumps(out, indent=1) + "\n") + sys.stderr.write("seconds %.1f\n" % (time.time() - t0)) + sys.exit(0 if passed else 1) + + +def library_exact(): + ok = True + for q in (Fr(3), Fr(120), Fr(1, 2), Fr(288), Fr(5, 7), Fr(48) - Fr(51035039649098175696, 10 ** 29)): + g = -q / 64 + parts, term, ssum = [], Fr(1), Fr(0) + for k in range(0, 60): + ssum += term + parts.append(ssum) + term = term * g / (k + 1) + lo, hi = min(parts[-1], parts[-2]), max(parts[-1], parts[-2]) + exact = Iv(Iv.frac(lo ** 64).lo, Iv.frac(hi ** 64).hi) + X = Iv.frac(q) + got = (-X).exp() + ok &= got.intersects(exact) and CC.divide(got.width(), got.lo) < Decimal(10) ** (-PREC + 3) + r = root_frac(q, 2) + ok &= X.sqrt().intersects(r) and CC.divide(X.sqrt().width(), r.lo) < Decimal(10) ** (-PREC + 3) + ok &= (-X).lo == X.hi.copy_negate() and (-X).hi == X.lo.copy_negate() + return ok + + +if __name__ == "__main__": + main() From 6276eba02ec20903da6f762e16a84dc5b277a192 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 23:58:43 +0000 Subject: [PATCH 2/2] D_3 closed form v1.1: apply the S3 nonauthor read (F6-F8; mathematics PASS) Grok Bot agent 4's S3 read (Math-#201 comment 5974652541): AMEND, wording and one output label. - F6: the D_4 non-claim drops the rationale that Math-#202 contradicts. - F7: the script emits "certified": passed (RESULTS.json byte-identical); the workflow accepts a mutant only if it exits 1 with JSON passed: false. - F8: Math-#199's enclosure and c_{4,24} transfer labelled author-certified, nonauthor review open. NOTE section 8 points to the PR disposition; section 9 records v1.1. The workflow replays locally with all mutants rejected by rule. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- .github/workflows/side24-d4-closed-form.yml | 15 +++++--- .../side24_d4_closed_form_20260930/NOTE.md | 35 ++++++++++++------- .../SOURCE_FILES.json | 12 +++---- .../closed_form_d3.py | 2 +- 4 files changed, 39 insertions(+), 25 deletions(-) diff --git a/.github/workflows/side24-d4-closed-form.yml b/.github/workflows/side24-d4-closed-form.yml index 4d42acacd..597bcc7a6 100644 --- a/.github/workflows/side24-d4-closed-form.yml +++ b/.github/workflows/side24-d4-closed-form.yml @@ -59,8 +59,13 @@ jobs: mutants = ['shift-variance', 'vandermonde', 'erfc-sign', 'jacobian', 'mehta', 'by-parts', 'one-erf', 'jk-init', 'gauss-half', 'boundary-term', 'atom-pi'] def mutant_rc(args): flags, m = args - return m, flags, subprocess.run([sys.executable, *flags, script, '--mutant', m], - capture_output=True, timeout=600).returncode + r = subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=600) + try: + ok = r.returncode == 1 and json.loads(r.stdout)['passed'] is False + except (ValueError, KeyError, TypeError): + ok = False + return m, flags, ok for flags in (['-B', '-S'], ['-B', '-O', '-S']): out = subprocess.run([sys.executable, *flags, script], check=True, capture_output=True, timeout=600).stdout @@ -72,9 +77,9 @@ jobs: if doc['closed_forms']['D_3'] != '50/3 + -76/3 pi^(-1) + -200/9 pi^(-1) arctan(1/2)': raise RuntimeError('closed form differs from the stated one') with concurrent.futures.ThreadPoolExecutor(max_workers=4) as pool: - for m, fl, rc in pool.map(mutant_rc, [(flags, m) for m in mutants]): - if rc != 1: - raise RuntimeError('mutant ' + m + ' not rejected under ' + ' '.join(fl)) + for m, fl, ok in pool.map(mutant_rc, [(flags, m) for m in mutants]): + if not ok: + raise RuntimeError('mutant ' + m + ' not rejected by its rules under ' + ' '.join(fl)) print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False, 'exact_identity_checked': True, 'side24_v1': 'unchanged'})) PY git diff --exit-code diff --git a/coefficients/side24_d4_closed_form_20260930/NOTE.md b/coefficients/side24_d4_closed_form_20260930/NOTE.md index cbf35dead..8c97ea364 100644 --- a/coefficients/side24_d4_closed_form_20260930/NOTE.md +++ b/coefficients/side24_d4_closed_form_20260930/NOTE.md @@ -2,7 +2,8 @@ **Object** `CL-SIDE24-D3-CLOSED-FORM-20260930-v1` · **scientific effect NONE** · declarative record, `executed: false` · base `main 3e0a91b` · claim: Math-#199 comment 5918624116 · companion: Math-#199 (`coefficients/side24_d4_20260930`, head `4fc6d15`), -whose one-dimensional reduction is the input and whose certified enclosure is the independent check. +whose one-dimensional reduction is the input and whose author-certified enclosure (nonauthor review open) is the independent +check. `coefficients/side24_v1` is unchanged; catalog entry C8 stays OPEN; no register, GRAPH, STATUS or catalog surface is touched. Same GitHub account as every lane: zero organizational-independence credit. Claude reads of this record count for nothing. The author will not merge. @@ -27,17 +28,18 @@ c_{4,ref} = Γ(7/6) (3/2)^{1/3} D_3 / (8√3 π^{5/2}) = 0.02332166600295283509452119495285688515310137236324033440… ``` -and `c_{4,24}` is as in Math-#199: `|c_{4,24}/c_{4,ref} − 1| ≤ 1.5702·10⁻¹⁰⁸`, so `c_{4,24}` carries the same digits. +and `c_{4,24}` is as in Math-#199: `|c_{4,24}/c_{4,ref} − 1| ≤ 1.5702·10⁻¹⁰⁸`, so `c_{4,24}` carries the same digits (Math-#199's +transfer; not re-derived or reviewed here). This continues `D_1 = 4/3`, `D_2 = 29/6 − √6` (SIDE24 §1) with the first value in which `π` and an arctangent appear. -`D_4` (Math-#200) remains an enclosure; see §6. +`D_4` (Math-#200) is enclosed, not put in closed form here; see §6. **What is proved here and from what.** The identity is obtained by *exact* integration of the one-dimensional integral to which Math-#199 reduces `D_3`. That reduction is exact algebra on the ordered-sector integrand of the eigenvalue form of `D_m` (Math-#199 NOTE §§1–2; the same code, re-run here, and checked at `m = 1, 2` against SIDE24's `4/3` and `29/6 − √6` through the identical path). Nothing in the chain is approximated, sampled or fitted: the output of the script is an element of a finite-dimensional `Q`-vector space with basis `√r · π^{k/2} · A` (`r` squarefree, `k ∈ Z`, `A = 1` or an arctan atom), -and the closed form above is that element. The certified enclosure of Math-#199 (an independent method: order-40 Taylor +and the closed form above is that element. The enclosure of Math-#199 (author-certified; its nonauthor review is open) (an independent method: order-40 Taylor quadrature with Cauchy remainders) contains the interval evaluation of the closed form, with 47 common digits (rule `D3_INSIDE_CERTIFIED`). @@ -170,7 +172,7 @@ With `c_{d,ref} = Γ(7/6)(3/2)^{1/3} |S^{d−1}| D_{d−1} / (√3 √π (2π)^d | 2 | `4/3` | `2Γ(7/6)(3/2)^{1/3}/(3√3 π^{3/2})` | `0.0734069193060342710301359629577…` (SIDE24) | | 3 | `29/6 − √6` | `Γ(7/6)(3/2)^{1/3}(29/6 − √6)/(2√3 π^{5/2})` | `0.0417759318405983433429366654285…` (SIDE24) | | 4 | `(50π + 200 arctan 2 − 228)/(9π)` | `Γ(7/6)(3/2)^{1/3}(50π + 200 arctan 2 − 228)/(72√3 π^{7/2})` | `0.0233216660029528350945211949528…` (this record; #199 encloses) | -| 5 | Math-#200 enclosure `14.21876345897735760130646567787…` | none claimed | `0.0132193193800849680760334875146…` (#200 encloses) | +| 5 | Math-#200 enclosure `14.21876345897735760130646567787…` | none claimed here (see Math-#202) | `0.0132193193800849680760334875146…` (#200 encloses) | The torus constants `c_{d,24}` follow from the covariance sandwich of SIDE24 §§3–4 with the constants of #199 (`d = 4`, `δ = 1.5702·10⁻¹⁰⁸`) and #200 (`d = 5`); a closed form for `c_{4,ref}` does not change `c_{4,24}`'s status (enclosed, not equated). @@ -179,11 +181,9 @@ The torus constants `c_{d,24}` follow from the covariance sandwich of SIDE24 § - The Proposition is an identity, proved by L1–L3 applied to the exact reduction of Math-#199. It consumes [LP] (15.1)–(15.2) and SIDE24 §1 at their scope (the reference law, `p_G(0)p_V(0)`, `τ² = 6`) and does not review them. -- **No closed form for `D_4` is claimed or expected by this method.** In the `m = 4` reduction (Math-#200 §§1–2) the outer - integral carries `erfc(κT)` against the cumulative integrals `L_a(T) = ∫_0^T e^{−v²/24} q_a(v) dv`, whose integrands contain - `erf(v/(2√2))` (even `k` occur there through `J_k(v)`), so the terms are Gaussian integrals over a two-dimensional wedge with - two error-function factors: four-dimensional Gaussian orthant-type integrals, which are not elementary in general. Math-#200's - enclosure stands as the record for `d = 5`. +- **No closed form for `D_4` is claimed here.** Math-#200's enclosure is the `d = 5` record at this head. The author's follow-up + Math-#202 (head `4512309`, nonauthor review open) reports that only odd `k` also occur at `m = 4` and claims an exact `D_4`; + this record neither relies on nor reviews that claim. - Math-#199 §7 says "no closed form for `D_3` claimed"; this record supplies one. Math-#199 is not edited here. If a nonauthor lane accepts this record, a one-line pointer in #199 §7 is the natural amendment; it is not made by the author unprompted. - C8 stays OPEN (the constants `C`, `r_*`, `z_*` and the window coefficients are not touched); `coefficients/side24_v1` is @@ -204,11 +204,20 @@ mutants). Pins on `main 3e0a91b`: [LP] `imports/lifetime_parent_20260925/UNIFORM - **Head / owner:** see the PR's disposition block; branch `claude/side24-d3-closed-form-20260930` (base `main 3e0a91b`); author lane Anthropic / Claude (`session_017Mi3hxjaxV45x6zo6o1ee3`). - **Claim:** the Proposition and Corollary of §0, proved by exact integration of the Math-#199 reduction; exact `m = 1, 2` - regressions; 47-digit agreement with the independent certified enclosure. No theorem of [LP] or SIDE24 is proved or reviewed. -- **Completed review scopes:** none yet. Requested: nonauthor reads of Slice A (§1: the reduction data, odd `k`, `J_k`; L1), + regressions; 47-digit agreement with Math-#199's author-certified enclosure (nonauthor review open). No theorem of [LP] or SIDE24 is proved or reviewed. +- **Completed review scopes:** see the PR's disposition block, which is the live record (none at opening). Requested: nonauthor reads of Slice A (§1: the reduction data, odd `k`, `J_k`; L1), Slice B (§2 L2–L3: the base integrals and the by-parts recurrence; §3 the arithmetic, atoms, reflection, the cancellations), Slice C (§§4–6: rules, mutants, the containment, the coefficient table, the `D_4` non-claim). - **Unresolved finding IDs:** none. - **Validation:** 12/12 rules in both modes, byte-identical output; 11/11 mutants rejected in both modes; workflow replayed - locally; hosted run pending at opening. + locally; hosted runs: see the PR's disposition block (pending at opening). - **Next action:** nonauthor reads; amendments on this branch, recorded in `SOURCE_FILES.json`. Author will not merge. + +## 9. Revisions + +- **v1.1 (nonauthor read S3, Grok Bot agent 4, Math-#201 comment 5974652541, on `3abcc10`; mathematics PASS).** Wording and one + output label; `RESULTS.json` is byte-identical. F6: the `D_4` non-claim no longer asserts a rationale that Math-#202 + contradicts (§0, §5, §6). F7: the script emits `"certified": passed` instead of a hard-coded `true` (unchanged on a passing + run; a mutant run now reports `false`), and the workflow accepts a mutant only if it exits 1 with JSON `passed: false`. F8: + Math-#199's enclosure and its `c_{4,24}` transfer are labelled author-certified with nonauthor review open (header, §0, §8). + §8's review and hosted-run lines point to the PR's disposition block. diff --git a/coefficients/side24_d4_closed_form_20260930/SOURCE_FILES.json b/coefficients/side24_d4_closed_form_20260930/SOURCE_FILES.json index 5d834f9c6..3f282b58c 100644 --- a/coefficients/side24_d4_closed_form_20260930/SOURCE_FILES.json +++ b/coefficients/side24_d4_closed_form_20260930/SOURCE_FILES.json @@ -50,9 +50,9 @@ "files": [ { "path": "NOTE.md", - "bytes": 15525, - "sha256": "b0756af59a92f9c8397614c9b4775959fe20caa7254949a664ee8285dfec0b2c", - "git_blob": "cbf35dead9f20cb8e68c357c62aca6413fb870af" + "bytes": 16289, + "sha256": "1b98443e4a9a297fa5b9c3a8c7549dd6ea713bdc5039a92f2b35fbd783253d13", + "git_blob": "8c97ea3642930646395566d09d0499d0ca090d35" }, { "path": "RESULTS.json", @@ -62,9 +62,9 @@ }, { "path": "closed_form_d3.py", - "bytes": 33890, - "sha256": "bd471be7d8b9199a3f305b0e1418ccfaa11cb7020b3d7e24412b9bada224eab5", - "git_blob": "a0c9169227c9a0b42c66deaca2b4f2e3168046ab" + "bytes": 33892, + "sha256": "dff95710019b4ec8656473565b16982f7ad367c561a1de610637462af1205f4a", + "git_blob": "5e7e4e59bb5de239e0c7a1b6bdb632f8300745dc" } ] } diff --git a/coefficients/side24_d4_closed_form_20260930/closed_form_d3.py b/coefficients/side24_d4_closed_form_20260930/closed_form_d3.py index a0c916922..5e7e4e59b 100644 --- a/coefficients/side24_d4_closed_form_20260930/closed_form_d3.py +++ b/coefficients/side24_d4_closed_form_20260930/closed_form_d3.py @@ -775,7 +775,7 @@ def fr(x): out = { "object": "CL-SIDE24-D3-CLOSED-FORM-20260930-v1", "scientific_effect": "NONE", - "certified": True, + "certified": passed, "mutant": MUT, "passed": passed, "checks": checks,