From 60e56ef27e7f2374d6b0ca663e9c0dc88a175293 Mon Sep 17 00:00:00 2001 From: d6g8k5htny-coder Date: Wed, 30 Sep 2026 20:37:34 +0000 Subject: [PATCH 1/4] Add exact closed form of the SIDE24 cone moment D_4 (d = 5) coefficients/side24_d5_closed_form_20260930: D_4 = 6695/54 - (405/32) sqrt6 - (1/pi)[(1375/72) sqrt21 + (6695/27) arctan sqrt(3/7) + (405/16) sqrt6 arctan(1/sqrt14)], obtained by exact integration of the reduction of Math-#200 with the exact arithmetic of Math-#201 extended by one cumulative layer: only odd J_k occur, the cumulative integrals are incomplete Gaussian moments (polynomials, e^{-mu T^2} and erf(sqrt(mu) T) terms), and the outer moments carry at most two error functions (elementary base integrals and a by-parts recurrence). The same path returns 4/3, 29/6 - sqrt6, the D_3 closed form and Mehta's Z_4 = 1536 pi exactly; the 60-digit evaluation sits at the centre of #200's certified enclosure (43 common digits). Corollary: c_{5,ref} = Gamma(7/6)(3/2)^(1/3) D_4/(12 sqrt3 pi^(7/2)); all c_{d,ref}, d <= 5, are now in closed form. Sixteen rules, fourteen 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-d5-closed-form.yml | 80 ++ .../side24_d5_closed_form_20260930/NOTE.md | 207 ++++ .../RESULTS.json | 981 +++++++++++++++ .../SOURCE_FILES.json | 77 ++ .../closed_form_d4.py | 1061 +++++++++++++++++ 5 files changed, 2406 insertions(+) create mode 100644 .github/workflows/side24-d5-closed-form.yml create mode 100644 coefficients/side24_d5_closed_form_20260930/NOTE.md create mode 100644 coefficients/side24_d5_closed_form_20260930/RESULTS.json create mode 100644 coefficients/side24_d5_closed_form_20260930/SOURCE_FILES.json create mode 100644 coefficients/side24_d5_closed_form_20260930/closed_form_d4.py diff --git a/.github/workflows/side24-d5-closed-form.yml b/.github/workflows/side24-d5-closed-form.yml new file mode 100644 index 000000000..4e8b6d0ad --- /dev/null +++ b/.github/workflows/side24-d5-closed-form.yml @@ -0,0 +1,80 @@ +name: SIDE24 d5 closed form + +'on': + pull_request: + paths: + - 'coefficients/side24_d5_closed_form_20260930/**' + - '.github/workflows/side24-d5-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_d5_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_d4.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['shift-variance', 'vandermonde', 'erfc-sign', 'jacobian', 'mehta', 'by-parts', 'one-erf', 'two-erf', 'jk-init', 'gauss-half', 'boundary-term', 'atom-pi', 'cumulative-init', 'cumulative-recurrence'] + 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']) == 16 and all(doc['checks'].values())): + raise RuntimeError('certification did not pass under ' + ' '.join(flags)) + if doc['closed_forms']['D_4'] != '6695/54 + -405/32 sqrt(6) + -1375/72 sqrt(21) pi^(-1) + -405/16 sqrt(6) pi^(-1) arctan(1/4 sqrt(14)) + -6695/27 pi^(-1) arctan(1/7 sqrt(21)) + 405/16 sqrt(6) pi^(-1) arctan(1/7 sqrt(14))' or doc['closed_forms']['Z_4'] != '1536 pi^(1)': + 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_d5_closed_form_20260930/NOTE.md b/coefficients/side24_d5_closed_form_20260930/NOTE.md new file mode 100644 index 000000000..821be30ae --- /dev/null +++ b/coefficients/side24_d5_closed_form_20260930/NOTE.md @@ -0,0 +1,207 @@ +# The SIDE24 cone moment `D_4` in closed form (`d = 5`) + +**Object** `CL-SIDE24-D4-CLOSED-FORM-20260930-v1` · **scientific effect NONE** · declarative record, `executed: false` · +base `main 3e0a91b` · claim: Math-#200 comment 5918942608 · companions: Math-#200 (`coefficients/side24_d5_20260930`, head +`33d50de`), whose reduction is the input and whose certified enclosure is the independent check, and Math-#201 +(`coefficients/side24_d4_closed_form_20260930`), whose exact arithmetic and lemmas are extended here by one cumulative layer. +`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_4`).** For SIDE24's reference law in `d = 5` (`A = Q + √(2/3) Z I_4`, `Q` the `4×4` GOE of +density `∝ exp(−tr Q²/4)`, `Z` an independent standard normal), the cone moment `D_4 = E[det(A)² 1{A ≺ 0}]` of [LP] (15.1) is + +``` +D_4 = 6695/54 − (405/32)√6 − (1/π) [ (1375/72)√21 + (6695/27) arctan√(3/7) + (405/16)√6 arctan(1/√14) ] + = 14.21876345897735760130646567787407831734060231608202158418… +``` + +(`arctan√(3/7) = arctan(√21/7)`, `arctan(1/√14) = arctan(√14/14)`). The exact arithmetic returns the two last atoms as +`arctan(√14/4)` and `arctan(√14/7)` with coefficients `∓(405/16)√6/π`; they combine by the subtraction formula, +`(√14/4 − √14/7)/(1 + 14/28) = √14/14`, both angles lying in `(0, π/2)` with a positive difference below `π/2` (rule +`SIMPLIFIED_FORM` evaluates both forms in interval arithmetic). + +**Corollary (the `d = 5` reference coefficient).** With [LP] (15.2) as written out in Math-#200 §4 (`|S⁴| = 8π²/3`), + +``` +c_{5,ref} = Γ(7/6) (3/2)^{1/3} D_4 / (12√3 π^{7/2}) = 0.01321931938008496807603348751464139652105289012569990545… +``` + +and `c_{5,24}` is as in Math-#200: `|c_{5,24}/c_{5,ref} − 1| ≤ 1.8554·10⁻¹⁰⁷`. + +With SIDE24 §1 (`D_1 = 4/3`, `D_2 = 29/6 − √6`) and Math-#201 (`D_3 = (50π + 200 arctan 2 − 228)/(9π)`), the reference +coefficients `c_{d,ref}` of [LP] (15.2) are now in closed form for every `d ≤ 5` (§5). `D_5` (`d = 6`) is not claimed (§6). + +**What is proved here and from what.** The identity is obtained by exact integration of the integral to which Math-#200 +reduces `D_4` (that reduction is exact algebra on the ordered-sector integrand, re-run here by the same code, and checked at +`m = 1, 2, 3` against `4/3`, `29/6 − √6` and Math-#201's `D_3` through the identical path). The computation lives in the +finite-dimensional `Q`-vector space with basis `√r · π^{k/2} · A` (`r` squarefree, `k ∈ Z`, `A = 1` or an arctan atom), so its +output is an identity. Math-#200's certified enclosure of `D_4` (an independent method: order-40 Taylor quadrature with Cauchy +remainders and certified cumulative integrals) contains the interval evaluation of the closed form, which lies at its centre +(`1.94·10⁻⁴²` from either endpoint of a `3.9·10⁻⁴²`-wide enclosure; 43 common digits; rule `D4_INSIDE_CERTIFIED`). Mehta's +`Z_4 = 1536π` is reproduced **exactly** by the same triangle machinery (rule `MEHTA_Z4_EXACT`). + +## 1. Input: the reduction of Math-#200 (its NOTE §§1–2) + +With `t_j = p_1 + … + p_j`, `T = Σ t_j`, the exact `a`-integral (`α = 3m/(4(m+3)) = 3/7`, `β = 3T/(2(m+3)) = 3T/14`), the +coordinates `p_1 = (T − 2p_2 − p_3)/3`, `v = 2p_2 + p_3` (Jacobian `1/6`, region `0 < p_3 < v < T`), and the decoupled +exponents `T²/48 + v²/24 + p_3²/8` (erfc branch) and `T²/21 + v²/24 + p_3²/8` (polynomial branch), Math-#200 writes + +``` +D_4 = pref [ c_E ∫_0^∞ e^{−T²/48} erfc(κT) Σ_a T^a L_a^E(T) dT + ∫_0^∞ e^{−T²/21} Σ_a T^a L_a^R(T) dT ], +L_a(T) = ∫_0^T e^{−v²/24} q_a(v) dv, q_a(v) = Σ_k e_{a,k}(v) J_k(v), J_k(v) = ∫_0^v p_3^k e^{−p_3²/8} dp_3, +``` + +`pref = √(3/7)·4!·(1/6)/Z_4 = √21/(2688π)` (`Z_4 = 1536π`), `c_E = ½√(π/α) = √21√π/6`, `κ = β/(2√α)/T = √21/28` +(`κ² = 3/112`; note `1/48 + κ² = 1/21`, the polynomial branch's exponent). The rational polynomials `e_{a,k}(v)` (erfc branch: +122 monomials, `T`-powers `0–9, 11`, `v`-degree `≤ 11`; polynomial branch: 95 monomials, `T`-powers `0–8, 10`) are listed in +`RESULTS.json` (`reduction_data`). In both branches the `p_3`-powers are `k ∈ {1, 3, 5, 7, 9}` — **only odd `k`** (rule +`STRUCTURE`), exactly as in the `d = 4` case of Math-#201. Hence `J_k = B_k + C_k(v) e^{−v²/8}` with rational `B_k` and +rational polynomials `C_k` (no error function inside `J_k`), and + +``` +L_a(T) = Σ_{k,j} e_{a,k,j} [ B_k G_j(1/24, T) + Σ_i C_{k,i} G_{j+i}(1/6, T) ], G_n(μ, T) = ∫_0^T v^n e^{−μv²} dv. +``` + +## 2. Four lemmas + +**L1 (the primitives `J_k`).** As Math-#201 L1: `J_k(0) = 0`, `J_k' = s^k e^{−s²/8}`, `J_k(∞) = ½8^{(k+1)/2}Γ((k+1)/2)`, verified +exactly for `k ≤ 9` (rule `JK_EXACT`); for odd `k`, `A_k = 0`. + +**L2 (incomplete Gaussian moments).** For `μ > 0`, `T ≥ 0`: + +``` +G_0(μ, T) = ½√(π/μ) erf(√μ T), G_1(μ, T) = (1 − e^{−μT²})/(2μ), G_n = [ (n−1) G_{n−2} − T^{n−1} e^{−μT²} ]/(2μ) (n ≥ 2), +``` + +by parts on `[0, T]` (`v^{n−1} · v e^{−μv²}`; the boundary term is `−T^{n−1}e^{−μT²}/(2μ)` at `T` and `0` at `0`). So every +`G_n(μ, ·)` is a polynomial in `T`, plus a polynomial times `e^{−μT²}`, plus (even `n`) a multiple of `erf(√μ T)`. The script +represents such "T-functions" exactly and verifies `G_n(μ, 0) = 0` and `∂_T G_n = T^n e^{−μT²}` in that space for `n ≤ 20`, +`μ ∈ {1/24, 1/6}` (rule `CUMULATIVE_EXACT`); the two identities characterise `G_n`. + +**L3 (base integrals).** For `λ, u, v > 0`: + +``` +M_0(λ, 1) = ½√(π/λ), M_1(λ, 1) = 1/(2λ), M_0(λ, erf(u·)) = arctan(u/√λ)/√(πλ), +M_0(λ, erf(u·) erf(v·)) = arctan( uv / √(λ(λ + u² + v²)) ) / √(πλ). +``` + +*Proof of the last.* Differentiate in `v`: the left side gives `(2/√π) ∫_0^∞ s e^{−(λ+v²)s²} erf(us) ds`, which by parts is +`(2/√π) · u/(2(λ+v²)√(λ+v²+u²))` (Math-#201 L3 at `n = 1`), i.e. `u/(√π (λ+v²) √(λ+u²+v²))`. On the right, with +`g(v) = uv/√(λ(λ+u²+v²))`: `g' = u(λ+u²)/(√λ (λ+u²+v²)^{3/2})` and `1 + g² = (λ+u²)(λ+v²)/(λ(λ+u²+v²))`, so +`(arctan g)' = u√λ/((λ+v²)√(λ+u²+v²))`, and dividing by `√(πλ)` gives the same expression. Both sides vanish at `v = 0`. ∎ +(The single-erf case is Math-#201 L2; rule `BASE_INTEGRALS_FLOAT` checks all four at the parameters that occur.) + +**L4 (moments by parts).** For `n ≥ 1` and `f` a product of at most two error functions (or `1`), + +``` +M_n(λ, f) = [ (n−1) M_{n−2}(λ, f) + Σ_{u∈f} (2u/√π) M_{n−1}(λ + u², f∖{u}) ]/(2λ), +``` + +with vanishing boundary terms (`n ≥ 2`, or `f(0) = 0`); the case `n = 1, f = 1` is the base value `1/(2λ)`. At `f = 1` the +recurrence reproduces `½Γ((n+1)/2)λ^{−(n+1)/2}` exactly for `n ≤ 20` and the thirteen values of `λ` that occur (rule +`GAUSS_MOMENTS`). + +By L1–L4 every term of `D_4` is an outer moment of one of three kinds: a polynomial part (`λ = g`, no extra factor), an +`e^{−μT²}` part (`λ = g + μ`), or an `erf(√μ T)` part (slope `√μ`), each multiplied on the erfc branch by `erfc(κT) = 1 − erf(κT)`, +so the two-error-function moments of L3–L4 occur exactly for the products `erf(√μ T) erfc(κT)`. + +## 3. The exact computation + +`closed_form_d4.py` extends Math-#201's arithmetic (dictionaries `(r, 2k, atom) → Fraction` with exact surd reduction, +`arctan` arguments `1, √3, 1/√3` folded into `π`, arguments above `1` reflected, all other algebraic arguments kept as atoms +with argument in `(0, 1]`) by the T-function layer of L2. The two branches of §1 are assembled with the exact `pref` and `c_E` +(from Mehta's `Z_4` and `α = 3/7` in the same arithmetic): + +``` +erfc branch : 6695/54 − (6066622595/603979776)√6 − (46299277168087/1415577600000)√21/π + − (6695/27) arctan(√21/7)/π − (6066622595/301989888)√6 [arctan(√14/4) − arctan(√14/7)]/π +polynomial branch : − (1577496445/603979776)√6 + (19265677168087/1415577600000)√21/π + − (1577496445/301989888)√6 [arctan(√14/4) − arctan(√14/7)]/π +D_4 : 6695/54 − (405/32)√6 − (1375/72)√21/π − (6695/27) arctan(√21/7)/π − (405/16)√6 [arctan(√14/4) − arctan(√14/7)]/π +``` + +(`603979776 = 2²⁶·9`; the large rational coefficients of the two branches cancel to `405/32`, `1375/72`, `405/16`.) The atoms +created along the way are `arctan(√15/5)` (from `m = 2`, and again from the two-erf base at `λ = 1/48`, `μ = 1/24`), +`arctan(1/2)` (`m = 3`), `arctan(√14/4)`, `arctan(√21/7)`, `arctan(√14/7)` and `arctan(1/√7)` (`κ/√λ` at `λ = 3/16`); the last +and `arctan(√15/5)` cancel identically in `D_4`. Mehta's `Z_4` through the same triangle machinery (§1 of Math-#200: +`4!√π(1/6) ∫e^{−T²/48}∫_0^T e^{−v²/24}∫_0^v V e^{−p_3²/8}`, `V` the Vandermonde) returns exactly `1536π`; `m = 1, 2, 3` return +exactly `4/3`, `29/6 − √6` and Math-#201's `D_3`. + +## 4. Verification + +Sixteen rules; all exact except the two float controls and the three interval containments: + +| rule | content | +|---|---| +| `STRUCTURE` | `α = 3/7`, `κ = √21/28`, `λ_erfc = 1/48`, `λ_poly = 1/21 = λ_erfc + κ²`, `p_3`-powers `{1,3,5,7,9}` in both branches, the atoms created | +| `GAUSS_MOMENTS` | L4 at `f = 1` equals `½Γ((n+1)/2)λ^{−(n+1)/2}` exactly, `n ≤ 20`, thirteen `λ` | +| `JK_EXACT` | L1 for `k ≤ 9`, exactly | +| `CUMULATIVE_EXACT` | L2: `G_n(μ, 0) = 0` and `∂_T G_n = T^n e^{−μT²}` in the T-function space, `n ≤ 20`, `μ ∈ {1/24, 1/6}` | +| `D1_EXACT`, `D2_EXACT`, `D3_EXACT` | `4/3`, `29/6 − √6`, `50/3 − 76/(3π) − (200/(9π)) arctan(1/2)` exactly | +| `MEHTA_Z4_EXACT` | `Z_4 = 1536π` exactly, and equal to the closed-form Mehta element | +| `D4_FORM` | the output equals the stated closed form exactly (pinned coefficients in the raw basis) | +| `BASE_INTEGRALS_FLOAT`, `MOMENTS_FLOAT` | Simpson quadrature (`math.erf`) of the base integrals (five single-erf, three two-erf parameter sets) and of sampled `M_n` agrees to `10⁻⁹`/`10⁻⁸` (controls) | +| `D4_INSIDE_CERTIFIED` | the 60-digit interval evaluation of the closed form lies inside Math-#200's certified `D_4` enclosure, width `< 10⁻⁵⁵` | +| `SIMPLIFIED_FORM` | the form with `arctan(1/√14)` intersects the raw form's interval and lies inside the enclosure | +| `C5_CLOSED` | the same for `c_{5,ref}` against Math-#200's enclosure | +| `LIBRARY_EXACT`, `PINNED` | as Math-#201 | + +Fourteen mutants exit 1 in both interpreter modes: `shift-variance` (`S²/24` for `S²/28` at `m = 4`), `vandermonde` (rejected +by the structural check: without the Vandermonde factor even `p_3`-powers appear), +`erfc-sign`, `jacobian` (`1/6 → 1/2`), `mehta` (`Z_5` for `Z_4`), `by-parts`, `one-erf`, `two-erf` (`λ + u²` for +`λ + u² + v²` in L3), `jk-init`, `gauss-half`, `boundary-term`, `atom-pi`, `cumulative-init` (`G_1` sign), `cumulative-recurrence` +(`n−1 → n` in L2). Runtime about two seconds. + +## 5. The coefficient in every `d ≤ 5` + +With `c_{d,ref} = Γ(7/6)(3/2)^{1/3} |S^{d−1}| D_{d−1} / (√3 √π (2π)^d)` ([LP] (15.2); Math-#199 §4, Math-#200 §4): + +| `d` | `D_{d−1}` | `c_{d,ref}` | 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…` (Math-#201; #199 encloses) | +| 5 | Proposition above | `Γ(7/6)(3/2)^{1/3} D_4/(12√3 π^{7/2})` | `0.0132193193800849680760334875146…` (this record; #200 encloses) | + +The torus constants `c_{d,24}` remain enclosed through the SIDE24 §§3–4 sandwich with the constants of Math-#199 and #200. + +## 6. Scope and non-claims + +- The Proposition is an identity, proved by L1–L4 applied to the exact reduction of Math-#200. It consumes [LP] (15.1)–(15.2) and + SIDE24 §1 at their scope and does not review them. +- **No closed form for `D_5` (`d = 6`) is claimed or expected by this method.** The `m = 5` reduction needs a second cumulative + layer: the first produces `erf(√μ v)` terms (L2), and a cumulative integral of `e^{−μ'v²} · polynomial · erf(√μ v)` is not + elementary in its upper limit (it is an Owen-`T`-type function), so the outer integrand would carry a non-elementary factor; + equivalently, the terms are Gaussian integrals over a three-dimensional wedge with an `erfc` and an `erf` factor, five-dimensional + orthant-type integrals, which are not elementary in general. +- Math-#200 §7 says "no closed form for `D_4`"; this record supplies one. Math-#200 is not edited here. +- C8 stays OPEN; `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_d5_closed_form_20260930/{NOTE.md, closed_form_d4.py, RESULTS.json, SOURCE_FILES.json}` and +`.github/workflows/side24-d5-closed-form.yml` (manifest, pins, byte-identical replay in `-B -S` and `-B -O -S`, the stated +closed-form string, the fourteen mutants). Pins on `main 3e0a91b`: [LP] `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` +blob `dfed3b8d`; SIDE24 `coefficients/side24_v1/PROOF.md` blob `44b66f04`. Companions, not on `main`: Math-#200 at `33d50de` +(`coefficients/side24_d5_20260930/RESULTS.json` blob `b67c00f4`, the two enclosures quoted in the script; `NOTE.md` blob +`ab3fe17d`, the reduction); Math-#201 at `3abcc10` (`closed_form_d3.py` blob `a0c91692`, the arithmetic and L1, L3–L4, reused +verbatim). Run: `python3 -B -S closed_form_d4.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-d4-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-#200 reduction; exact `m = 1, 2, 3` + and `Z_4` regressions; the closed form at the centre of 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`, the constants; + L1), Slice B (§2 L2–L4 and §3: the T-function layer, the two-erf base integral, the by-parts recurrences, the atoms and + cancellations, the `Z_4` identity), Slice C (§§4–6: rules, mutants, containment, the coefficient table, the `D_5` non-claim). +- **Unresolved finding IDs:** none. +- **Validation:** 16/16 rules in both modes, byte-identical output; 14/14 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_d5_closed_form_20260930/RESULTS.json b/coefficients/side24_d5_closed_form_20260930/RESULTS.json new file mode 100644 index 000000000..52ce9b572 --- /dev/null +++ b/coefficients/side24_d5_closed_form_20260930/RESULTS.json @@ -0,0 +1,981 @@ +{ + "object": "CL-SIDE24-D4-CLOSED-FORM-20260930-v1", + "scientific_effect": "NONE", + "certified": true, + "mutant": null, + "passed": true, + "checks": { + "STRUCTURE": true, + "GAUSS_MOMENTS": true, + "JK_EXACT": true, + "CUMULATIVE_EXACT": true, + "D1_EXACT": true, + "D2_EXACT": true, + "D3_EXACT": true, + "MEHTA_Z4_EXACT": true, + "D4_FORM": true, + "BASE_INTEGRALS_FLOAT": true, + "MOMENTS_FLOAT": true, + "D4_INSIDE_CERTIFIED": true, + "SIMPLIFIED_FORM": true, + "C5_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)", + "Z_4": "1536 pi^(1)", + "D_4": "6695/54 + -405/32 sqrt(6) + -1375/72 sqrt(21) pi^(-1) + -405/16 sqrt(6) pi^(-1) arctan(1/4 sqrt(14)) + -6695/27 pi^(-1) arctan(1/7 sqrt(21)) + 405/16 sqrt(6) pi^(-1) arctan(1/7 sqrt(14))", + "D_4_simplified": "6695/54 - (405/32) sqrt6 - (1/pi) [ (1375/72) sqrt21 + (6695/27) arctan(sqrt21/7) + (405/16) sqrt6 arctan(sqrt14/14) ] (arctan(sqrt14/4) - arctan(sqrt14/7) = arctan(1/sqrt14))", + "c_5_ref": "Gamma(7/6) (3/2)^(1/3) D_4 / (12 sqrt3 pi^(7/2))", + "erfc_branch_of_D_4": "6695/54 + -6066622595/603979776 sqrt(6) + -46299277168087/1415577600000 sqrt(21) pi^(-1) + -6066622595/301989888 sqrt(6) pi^(-1) arctan(1/4 sqrt(14)) + -6695/27 pi^(-1) arctan(1/7 sqrt(21)) + 6066622595/301989888 sqrt(6) pi^(-1) arctan(1/7 sqrt(14))", + "polynomial_branch_of_D_4": "-1577496445/603979776 sqrt(6) + 19265677168087/1415577600000 sqrt(21) pi^(-1) + -1577496445/301989888 sqrt(6) pi^(-1) arctan(1/4 sqrt(14)) + 1577496445/301989888 sqrt(6) pi^(-1) arctan(1/7 sqrt(14))" + }, + "interval_evaluation": { + "D_4": [ + "14.2187634589773576013064656778740783173406023160820215841833", + "14.2187634589773576013064656778740783173406023160820215842323" + ], + "D_4_simplified": [ + "14.2187634589773576013064656778740783173406023160820215841883", + "14.2187634589773576013064656778740783173406023160820215842281" + ], + "c_5_ref": [ + "0.0132193193800849680760334875146413965210528901256999054505140", + "0.0132193193800849680760334875146413965210528901256999054539727" + ], + "arctan(sqrt21/7)": [ + "0.579639740363704299923291897011207918621441782280263529351672", + "0.579639740363704299923291897011207918621441782280263529351866" + ], + "arctan(sqrt14/14)": [ + "0.261157410903024311262049412927851638004440468771565909792296", + "0.261157410903024311262049412927851638004440468771565909792486" + ], + "arctan(sqrt14/4)": [ + "0.752040089192335679842958294184691084003367627670504438870380", + "0.752040089192335679842958294184691084003367627670504438870582" + ], + "arctan(sqrt14/7)": [ + "0.490882678289311368580908881256839445998927158898938529077984", + "0.490882678289311368580908881256839445998927158898938529078176" + ], + "pi": [ + "3.14159265358979323846264338327950288419716939937510582097457", + "3.14159265358979323846264338327950288419716939937510582097528" + ], + "Gamma(7/6)": [ + "0.927719333630039200708349482534621018566466519145475576700351", + "0.927719333630039200708349482534621018566466519145475576939062" + ], + "(3/2)^(1/3)": [ + "1.14471424255333186780804221193967700891590692078793107209905", + "1.14471424255333186780804221193967700891590692078793107209906" + ] + }, + "certified_enclosures_math_200": { + "D_4": [ + "14.2187634589773576013064656778740783173406003782976930345926", + "14.2187634589773576013064656778740783173406042538663501338228" + ], + "c_5_ref": [ + "0.0132193193800849680760334875146413965210528883241234179643777", + "0.0132193193800849680760334875146413965210528919272763929401087" + ] + }, + "reduction_data": { + "m=4": { + "alpha": "3/7", + "beta": "3/14 T", + "kappa": "1/28 sqrt(21)", + "kappa^2": "3/112", + "lambda_erfc": "1/48", + "lambda_poly": "1/21", + "prefactor": "1/2688 sqrt(21) pi^(-1)", + "G_0_constant": "1/6 sqrt(21) pi^(1/2)", + "p3_powers": [ + 1, + 3, + 5, + 7, + 9 + ], + "T_powers_erfc": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 11 + ], + "T_powers_poly": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 10 + ], + "e_{a,k}(v) by power, erfc branch": { + "0": { + "1": [ + "0", + "0", + "0", + "0", + "0", + "-84035/186624", + "0", + "1715/186624", + "0", + "-49/746496", + "0", + "-7/30233088" + ], + "3": [ + "0", + "0", + "0", + "420175/93312", + "0", + "-12005/186624", + "0", + "49/186624", + "0", + "49/7558272" + ], + "5": [ + "0", + "-84035/20736", + "0", + "-12005/62208", + "0", + "343/124416", + "0", + "-35/559872" + ], + "7": [ + "0", + "1715/6912", + "0", + "49/20736", + "0", + "7/31104" + ], + "9": [ + "0", + "-49/9216", + "0", + "-7/41472" + ] + }, + "1": { + "1": [ + "0", + "0", + "0", + "0", + "-84035/62208", + "0", + "1715/62208", + "0", + "-539/2239488", + "0", + "7/6718464" + ], + "3": [ + "0", + "0", + "-84035/31104", + "0", + "8575/62208", + "0", + "-833/1119744", + "0", + "-7/419904" + ], + "5": [ + "84035/20736", + "0", + "1715/20736", + "0", + "-245/31104", + "0", + "49/1119744" + ], + "7": [ + "-1715/6912", + "0", + "49/13824", + "0", + "7/31104" + ], + "9": [ + "49/9216", + "0", + "-7/27648" + ] + }, + "2": { + "1": [ + "0", + "0", + "0", + "0", + "0", + "1715/373248", + "0", + "-343/1492992", + "0", + "49/8957952", + "0", + "-1/80621568" + ], + "3": [ + "0", + "0", + "0", + "-8575/186624", + "0", + "2401/1492992", + "0", + "-49/2239488", + "0", + "7/20155392" + ], + "5": [ + "0", + "1715/41472", + "0", + "2401/497664", + "0", + "-343/1492992", + "0", + "-5/1492992" + ], + "7": [ + "0", + "-343/55296", + "0", + "-49/248832", + "0", + "1/82944" + ], + "9": [ + "0", + "49/110592", + "0", + "-1/110592" + ] + }, + "3": { + "1": [ + "0", + "0", + "84035/46656", + "0", + "-8575/373248", + "0", + "-49/1492992", + "0", + "161/80621568", + "0", + "-1/17915904" + ], + "3": [ + "-84035/46656", + "0", + "-8575/186624", + "0", + "-245/1492992", + "0", + "-679/40310784", + "0", + "1/1119744" + ], + "5": [ + "8575/124416", + "0", + "-49/497664", + "0", + "301/2239488", + "0", + "-7/2985984" + ], + "7": [ + "49/165888", + "0", + "-49/497664", + "0", + "-1/82944" + ], + "9": [ + "-7/331776", + "0", + "1/73728" + ] + }, + "4": { + "1": [ + "0", + "0", + "0", + "0", + "0", + "2891/17915904", + "0", + "-581/107495424", + "0", + "-1/15925248" + ], + "3": [ + "0", + "0", + "0", + "-14455/8957952", + "0", + "4067/107495424", + "0", + "1/3981312" + ], + "5": [ + "0", + "2891/1990656", + "0", + "4067/35831808", + "0", + "7/2654208" + ], + "7": [ + "0", + "-581/3981312", + "0", + "1/442368" + ], + "9": [ + "0", + "-1/196608" + ] + }, + "5": { + "1": [ + "0", + "0", + "-1715/93312", + "0", + "2107/5971968", + "0", + "35/35831808", + "0", + "13/429981696" + ], + "3": [ + "1715/93312", + "0", + "2107/2985984", + "0", + "175/35831808", + "0", + "-245/214990848" + ], + "5": [ + "-2107/1990656", + "0", + "35/11943936", + "0", + "7/1492992" + ], + "7": [ + "-35/3981312", + "0", + "-11/2654208" + ], + "9": [ + "1/1769472" + ] + }, + "6": { + "1": [ + "0", + "0", + "0", + "0", + "0", + "-805/644972544", + "0", + "23/286654464" + ], + "3": [ + "0", + "0", + "0", + "4025/322486272", + "0", + "-161/286654464" + ], + "5": [ + "0", + "-805/71663616", + "0", + "-161/95551488" + ], + "7": [ + "0", + "23/10616832" + ] + }, + "7": { + "1": [ + "0", + "0", + "245/4478976", + "0", + "-637/214990848", + "0", + "1/31850496" + ], + "3": [ + "-245/4478976", + "0", + "-637/107495424", + "0", + "5/31850496" + ], + "5": [ + "637/71663616", + "0", + "1/10616832" + ], + "7": [ + "-1/3538944" + ] + }, + "8": { + "1": [ + "0", + "0", + "0", + "0", + "0", + "-43/6879707136" + ], + "3": [ + "0", + "0", + "0", + "215/3439853568" + ], + "5": [ + "0", + "-43/764411904" + ] + }, + "9": { + "1": [ + "0", + "0", + "175/483729408", + "0", + "-11/2293235712" + ], + "3": [ + "-175/483729408", + "0", + "-11/1146617856" + ], + "5": [ + "11/764411904" + ] + }, + "11": { + "1": [ + "0", + "0", + "1/5159780352" + ], + "3": [ + "-1/5159780352" + ] + } + }, + "e_{a,k}(v) by power, polynomial branch": { + "0": { + "1": [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "343/629856", + "0", + "-49/5038848" + ], + "3": [ + "0", + "0", + "0", + "0", + "0", + "0", + "-6517/629856", + "0", + "49/314928" + ], + "5": [ + "0", + "0", + "0", + "0", + "3773/69984", + "0", + "-343/839808" + ], + "7": [ + "0", + "0", + "-343/7776", + "0", + "-49/23328" + ], + "9": [ + "0", + "0", + "49/20736" + ] + }, + "1": { + "1": [ + "0", + "0", + "0", + "0", + "0", + "-84035/746496", + "0", + "20923/6718464", + "0", + "-833/26873856", + "0", + "7/120932352" + ], + "3": [ + "0", + "0", + "0", + "420175/373248", + "0", + "-146461/6718464", + "0", + "833/6718464", + "0", + "-49/30233088" + ], + "5": [ + "0", + "-84035/82944", + "0", + "-146461/2239488", + "0", + "5831/4478976", + "0", + "35/2239488" + ], + "7": [ + "0", + "20923/248832", + "0", + "833/746496", + "0", + "-7/124416" + ], + "9": [ + "0", + "-833/331776", + "0", + "7/165888" + ] + }, + "2": { + "1": [ + "0", + "0", + "0", + "0", + "-84035/248832", + "0", + "9947/2239488", + "0", + "-539/80621568", + "0", + "7/26873856" + ], + "3": [ + "0", + "0", + "-84035/124416", + "0", + "49735/2239488", + "0", + "-833/40310784", + "0", + "-7/1679616" + ], + "5": [ + "84035/82944", + "0", + "9947/746496", + "0", + "-245/1119744", + "0", + "49/4478976" + ], + "7": [ + "-9947/248832", + "0", + "49/497664", + "0", + "7/124416" + ], + "9": [ + "49/331776", + "0", + "-7/110592" + ] + }, + "3": { + "1": [ + "0", + "0", + "0", + "0", + "0", + "-446243/161243136", + "0", + "2597/80621568", + "0", + "7/23887872" + ], + "3": [ + "0", + "0", + "0", + "2231215/80621568", + "0", + "-18179/80621568", + "0", + "-7/5971968" + ], + "5": [ + "0", + "-446243/17915904", + "0", + "-18179/26873856", + "0", + "-49/3981312" + ], + "7": [ + "0", + "2597/2985984", + "0", + "-7/663552" + ], + "9": [ + "0", + "7/294912" + ] + }, + "4": { + "1": [ + "0", + "0", + "84035/186624", + "0", + "-413315/53747712", + "0", + "-49/26873856", + "0", + "-91/644972544" + ], + "3": [ + "-84035/186624", + "0", + "-413315/26873856", + "0", + "-245/26873856", + "0", + "1715/322486272" + ], + "5": [ + "413315/17915904", + "0", + "-49/8957952", + "0", + "-49/2239488" + ], + "7": [ + "49/2985984", + "0", + "77/3981312" + ], + "9": [ + "-7/2654208" + ] + }, + "5": { + "1": [ + "0", + "0", + "0", + "0", + "0", + "6811/1289945088", + "0", + "-161/429981696" + ], + "3": [ + "0", + "0", + "0", + "-34055/644972544", + "0", + "1127/429981696" + ], + "5": [ + "0", + "6811/143327232", + "0", + "1127/143327232" + ], + "7": [ + "0", + "-161/15925248" + ] + }, + "6": { + "1": [ + "0", + "0", + "95011/40310784", + "0", + "17297/1289945088", + "0", + "-7/47775744" + ], + "3": [ + "-95011/40310784", + "0", + "17297/644972544", + "0", + "-35/47775744" + ], + "5": [ + "-17297/429981696", + "0", + "-7/15925248" + ], + "7": [ + "7/5308416" + ] + }, + "7": { + "1": [ + "0", + "0", + "0", + "0", + "0", + "301/10319560704" + ], + "3": [ + "0", + "0", + "0", + "-1505/5159780352" + ], + "5": [ + "0", + "301/1146617856" + ] + }, + "8": { + "1": [ + "0", + "0", + "-539/322486272", + "0", + "77/3439853568" + ], + "3": [ + "539/322486272", + "0", + "77/1719926784" + ], + "5": [ + "-77/1146617856" + ] + }, + "10": { + "1": [ + "0", + "0", + "-7/7739670528" + ], + "3": [ + "7/7739670528" + ] + } + }, + "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" + ] + }, + "8": { + "A": "26880", + "B": "0", + "C": [ + "0", + "-26880", + "0", + "-2240", + "0", + "-112", + "0", + "-4" + ] + }, + "9": { + "A": "0", + "B": "393216", + "C": [ + "-393216", + "0", + "-49152", + "0", + "-3072", + "0", + "-128", + "0", + "-4" + ] + } + } + }, + "m=3": { + "kappa": "1/12 sqrt(6)", + "lambda_erfc": "1/24", + "lambda_poly": "1/12" + }, + "m=2": { + "kappa": "1/20 sqrt(30)", + "lambda_erfc": "1/8", + "lambda_poly": "1/5" + }, + "atoms_created_by_the_derivations": [ + "1", + "arctan(1/5 sqrt(15))", + "arctan(1/2 sqrt(1))", + "arctan(1/4 sqrt(14))", + "arctan(1/7 sqrt(21))", + "arctan(1/7 sqrt(14))", + "arctan(1/7 sqrt(7))" + ], + "note": "arctan(sqrt15/5) (m = 2) and arctan(1/sqrt7) (m = 4, from lam = 3/16) arise in intermediate terms and cancel" + }, + "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)", + "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)", + "G_n(mu, T)": "G_0 = (1/2) sqrt(pi/mu) erf(sqrt(mu) T); G_1 = (1 - e^{-mu T^2})/(2 mu); G_n = [(n-1) G_{n-2} - T^{n-1} e^{-mu T^2}]/(2 mu)", + "D_4 integral": "sqrt21/(2688 pi) [ (sqrt21 sqrt(pi)/6) int e^{-T^2/48} erfc(sqrt21 T/28) sum_a T^a L_a^E + int e^{-T^2/21} sum_a T^a L_a^R ]", + "L_a": "int_0^T e^{-v^2/24} sum_k e_{a,k}(v) J_k(v) dv, k odd, J_k = B_k + C_k e^{-v^2/8}: incomplete Gaussian moments with mu = 1/24, 1/6", + "Z_4": "4! sqrt(pi) (1/6) int e^{-T^2/48} int_0^T e^{-v^2/24} int_0^v V e^{-p3^2/8} = 1536 pi (exact, rule MEHTA_Z4_EXACT)" + } +} diff --git a/coefficients/side24_d5_closed_form_20260930/SOURCE_FILES.json b/coefficients/side24_d5_closed_form_20260930/SOURCE_FILES.json new file mode 100644 index 000000000..c1dfa21fa --- /dev/null +++ b/coefficients/side24_d5_closed_form_20260930/SOURCE_FILES.json @@ -0,0 +1,77 @@ +{ + "schema": 1, + "object": "CL-SIDE24-D4-CLOSED-FORM-20260930-v1", + "scientific_effect": "NONE", + "certified": true, + "review_status": "AUTHOR_SIDE_EXACT_IDENTITY_NONAUTHOR_READS_OPEN", + "disposition": "EXACT_CLOSED_FORM_OF_D4_FROM_THE_MATH200_REDUCTION_NO_REGISTER_CHANGE_SIDE24_V1_UNCHANGED", + "declarative": true, + "executed": false, + "base": "3e0a91b69892b9717564c592e7a966492a81566a", + "claim": "https://github.com/d6g8k5htny-coder/Math-/pull/200#issuecomment-5918942608", + "result": { + "D_4": "6695/54 - (405/32) sqrt6 - (1/pi) [ (1375/72) sqrt21 + (6695/27) arctan(sqrt(3/7)) + (405/16) sqrt6 arctan(1/sqrt14) ]", + "c_5_ref": "Gamma(7/6) (3/2)^(1/3) D_4 / (12 sqrt3 pi^(7/2))", + "Z_4": "1536 pi (exact, same machinery)", + "D_1, D_2, D_3": "4/3, 29/6 - sqrt6, 50/3 - 76/(3 pi) - (200/(9 pi)) arctan(1/2) (exact, same code path)" + }, + "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/200", + "commit": "33d50de", + "path": "coefficients/side24_d5_20260930/RESULTS.json", + "git_blob": "b67c00f45d053b51c2ec15ce8d53c8a34e49a006", + "role": "the certified enclosures of D_4 and c_{5,ref} quoted in the script (rules D4_INSIDE_CERTIFIED, SIMPLIFIED_FORM, C5_CLOSED, PINNED)" + }, + { + "pr": "https://github.com/d6g8k5htny-coder/Math-/pull/200", + "commit": "33d50de", + "path": "coefficients/side24_d5_20260930/NOTE.md", + "git_blob": "ab3fe17d8fbed0b417a4844ff9490e2eefcb5134", + "role": "sections 1-2, the reduction that is integrated exactly here; section 4, the coefficient formula and |S^4|" + }, + { + "pr": "https://github.com/d6g8k5htny-coder/Math-/pull/201", + "commit": "3abcc10", + "path": "coefficients/side24_d4_closed_form_20260930/closed_form_d3.py", + "git_blob": "a0c9169227c9a0b42c66deaca2b4f2e3168046ab", + "role": "the exact arithmetic, the moments M_n and the m = 1, 2, 3 pipelines, reused verbatim; the D_3 closed form is rule D3_EXACT" + } + ], + "files": [ + { + "path": "NOTE.md", + "bytes": 15468, + "sha256": "6d1c9cd3b2a6132b473947e4d517ab5337078e256cd46514a091c85d3da0cde6", + "git_blob": "821be30aeafb7e48c8bc927575fb9950e0f4d784" + }, + { + "path": "RESULTS.json", + "bytes": 16765, + "sha256": "b878c1d3534a1ce72f01bb461a06b8777888bc0a5fdd9413fc1a4f8a565a2bb3", + "git_blob": "52ce9b5726b8ea92c429ea1193b1812869afe701" + }, + { + "path": "closed_form_d4.py", + "bytes": 44943, + "sha256": "54e348113f67225725b7e2b4399bd39578c51c531967c8f35f8124475d68030b", + "git_blob": "83ff92db2d38156b06a85821c07adcabe0343378" + } + ] +} diff --git a/coefficients/side24_d5_closed_form_20260930/closed_form_d4.py b/coefficients/side24_d5_closed_form_20260930/closed_form_d4.py new file mode 100644 index 000000000..83ff92db2 --- /dev/null +++ b/coefficients/side24_d5_closed_form_20260930/closed_form_d4.py @@ -0,0 +1,1061 @@ +"""The SIDE24 cone moment D_4 in closed form: + D_4 = 6695/54 - (405/32) sqrt6 - (1/pi) [ (1375/72) sqrt21 + (6695/27) arctan(sqrt(3/7)) + (405/16) sqrt6 arctan(1/sqrt14) ]. + +Standard library only. Run from anywhere: python -B -S closed_form_d4.py [--mutant NAME] + +Object. Math-#200 (coefficients/side24_d5_20260930) reduces the d = 5 cone moment D_4 = E[det(A)^2 1{A < 0}] of SIDE24's +reference law A = Q + sqrt(2/3) Z I_4 to + + D_4 = pref [ c_E int_0^inf e^{-T^2/48} erfc(kappa T) sum_a T^a L_a^E(T) dT + int_0^inf e^{-T^2/21} sum_a T^a L_a^R(T) dT ], + L_a(T) = int_0^T e^{-v^2/24} q_a(v) dv, q_a(v) = sum_k e_{a,k}(v) J_k(v), J_k(v) = int_0^v p^k e^{-p^2/8} dp, + +pref = sqrt(3/7) 4! (1/6)/Z_4 = sqrt21/(2688 pi), c_E = (1/2) sqrt(pi/alpha) = sqrt21 sqrt(pi)/6 (alpha = 3/7), kappa = sqrt21/28, +with rational polynomials e_{a,k} from the ordered-sector algebra (the same code as #200), and encloses it by certified +quadrature. Here the same integral is evaluated exactly. Only odd k occur, so J_k = B_k + C_k(v) e^{-v^2/8}; the cumulative +integrals are then incomplete Gaussian moments G_n(mu, T) = int_0^T v^n e^{-mu v^2} dv with mu in {1/24, 1/6}, which are +polynomials, polynomials times e^{-mu T^2}, and (n even) multiples of erf(sqrt(mu) T); the outer integrand therefore carries +at most two error functions, erfc(kappa T) and erf(sqrt(mu) T), and every term is a moment M_n(lam, f) = int_0^inf +T^n e^{-lam T^2} f(T) dT with f in {1, erf(u .), erf(u .) erf(v .)}. These are elementary: + + 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), + M_n(lam, f) = [ (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) (n >= 1), + +and 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. The same code returns D_1 = 4/3, D_2 = 29/6 - sqrt6, the D_3 closed +form of Math-#201 and Mehta's Z_4 = 1536 pi exactly (rules), and the interval evaluation of the closed form lies inside +#200's certified enclosure of D_4 (43 common digits; rule). Consequently +c_{5,ref} = Gamma(7/6) (3/2)^(1/3) D_4 / (12 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", "two-erf", "jk-init", + "gauss-half", "boundary-term", "atom-pi", "cumulative-init", "cumulative-recurrence") +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-#200 (coefficients/side24_d5_20260930/RESULTS.json at 33d50de): the certified enclosures this closed form must meet +CERTIFIED = { + "D_4": ("14.2187634589773576013064656778740783173406003782976930345926", "14.2187634589773576013064656778740783173406042538663501338228"), + "c_5_ref": ("0.0132193193800849680760334875146413965210528883241234179643777", "0.0132193193800849680760334875146413965210528919272763929401087"), +} +PINNED = {"D_4": "14.21876345897735760130646567787407831734060", + "c_5_ref": "0.0132193193800849680760334875146413965210528", + "pi": "3.14159265358979323846264338327950288419716939937510"} +# D_4 in the raw output basis (the two atoms arctan(sqrt14/4) and arctan(sqrt14/7) combine to arctan(1/sqrt14), section 3) +CLOSED_FORM_D4 = {"1": Fr(6695, 54), "sqrt6": Fr(-405, 32), "sqrt21/pi": Fr(-1375, 72), "arctan(sqrt21/7)/pi": Fr(-6695, 27), + "sqrt6 arctan(sqrt14/4)/pi": Fr(-405, 16), "sqrt6 arctan(sqrt14/7)/pi": Fr(405, 16)} +CLOSED_FORM_D3 = {"1": Fr(50, 3), "1/pi": Fr(-76, 3), "arctan(1/2)/pi": Fr(-200, 9)} # Math-#201 + + +# ---------------- 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))) if MUT != "two-erf" else surd_sqrt(lam * (lam + surd_sq(u))) + 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 != 4 else Fr(1, 24) + 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 + + + +# ---------------- one cumulative layer: T-functions and the incomplete Gaussian moments G_n(mu, T) +# A T-function is {(kind, mu): {n: element}}: kind 'c' a polynomial in T, 'e' a polynomial times e^{-mu T^2}, +# 'f' a polynomial times erf(sqrt(mu) T); the coefficients are elements of the exact arithmetic above. +def tf_norm(A): + return {k: {n: c for n, c in v.items() if c} for k, v in A.items() if any(v.values())} + + +def tf_add(A, B): + out = {k: dict(v) for k, v in A.items()} + for key, poly in B.items(): + d = out.setdefault(key, {}) + for n, c in poly.items(): + d[n] = add(d.get(n, {}), c) + return tf_norm(out) + + +def tf_scale(A, c): + return tf_norm({k: {n: scale(e, c) for n, e in v.items()} for k, v in A.items()}) + + +_G_CACHE = {} + + +def G(n, mu): + """int_0^T v^n e^{-mu v^2} dv: G_0 = (1/2) sqrt(pi/mu) erf(sqrt(mu) T), G_1 = (1 - e^{-mu T^2})/(2 mu), + G_n = [(n-1) G_{n-2} - T^{n-1} e^{-mu T^2}]/(2 mu) (by parts).""" + mu = Fr(mu) + key = (n, mu) + if key in _G_CACHE: + return _G_CACHE[key] + if n == 0: + val = {("f", mu): {0: mul_pi_half(mul_surd(E(Fr(1, 2)), surd_sqrt(1 / mu)), 1)}} + elif n == 1: + val = {("c", Fr(0)): {0: E(1 / (2 * mu))}, ("e", mu): {0: E(-1 / (2 * mu) if MUT != "cumulative-init" else 1 / (2 * mu))}} + else: + val = tf_add(tf_scale(G(n - 2, mu), Fr(n - 1) if MUT != "cumulative-recurrence" else Fr(n)), {("e", mu): {n - 1: E(-1)}}) + val = tf_scale(val, 1 / (2 * mu)) + _G_CACHE[key] = val + return val + + +def tf_derivative(A): + """d/dT of a T-function: (p e^{-mu T^2})' = (p' - 2 mu T p) e^{-mu T^2}; (p erf(sqrt mu T))' = p' erf + p (2 sqrt(mu)/sqrt pi) e^{-mu T^2}.""" + out = {} + for (kind, mu), poly in A.items(): + dp = {} + for n, c in poly.items(): + if n: + dp[n - 1] = add(dp.get(n - 1, {}), scale(c, n)) + if kind == "c": + out = tf_add(out, {("c", Fr(0)): dp}) + elif kind == "e": + shifted = {n + 1: scale(c, -2 * mu) for n, c in poly.items()} + out = tf_add(out, {("e", mu): dp}) + out = tf_add(out, {("e", mu): shifted}) + else: + pref = mul_pi_half(mul_surd(E(2), surd_sqrt(mu)), -1) # 2 sqrt(mu)/sqrt(pi) + out = tf_add(out, {("f", mu): dp}) + out = tf_add(out, {("e", mu): {n: mul(c, pref) for n, c in poly.items()}}) + return tf_norm(out) + + +def tf_at_zero(A): + """Value at T = 0 (erf(0) = 0).""" + val = {} + for (kind, mu), poly in A.items(): + if kind != "f" and 0 in poly: + val = add(val, poly[0]) + return val + + +def g_identities(nmax, mus): + """G_n(mu, 0) = 0 and G_n' = T^n e^{-mu T^2}, exactly, for n <= nmax.""" + ok = True + for mu in mus: + for n in range(nmax + 1): + ok &= tf_at_zero(G(n, mu)) == {} + ok &= tf_derivative(G(n, mu)) == tf_norm({("e", Fr(mu)): {n: E(1)}}) + return ok + + +def outer_moment(n, g, kind, mu, erfc, kappa): + """int_0^inf T^n e^{-g T^2} [erfc(kappa T)] {1, e^{-mu T^2}, erf(sqrt(mu) T)} dT as an element.""" + if kind == "c": + lam, slopes = g, () + elif kind == "e": + lam, slopes = g + mu, () + else: + lam, slopes = g, (surd_sqrt(mu),) + val = M(n, lam, slopes) + if erfc: + val = add(val, scale(M(n, lam, tuple(sorted(slopes + (kappa,)))), -1 if MUT != "erfc-sign" else 1)) + return val + + +def organize_tvp(P): + """Polynomial dict in (T, v, p3) -> {a: {k: [coefficients in v by power]}} (a = T power, k = p3 power).""" + out = {} + for (i, j, k), c in P.items(): + out.setdefault(i, {}).setdefault(k, {})[j] = c + return {a: {k: [d.get(j, Fr(0)) for j in range(max(d) + 1)] for k, d in ks.items()} for a, ks in out.items()} + + +def integrate_branch(inner, g, erfc, kappa, JK): + """sum_a int_0^inf T^a e^{-g T^2} [erfc(kappa T)] L_a(T) dT with L_a(T) = int_0^T e^{-v^2/24} sum_k e_{a,k}(v) J_k(v) dv.""" + total = {} + for a, ks in inner.items(): + La = {} + for k, ek in ks.items(): + A, B, C = JK[k] + if A: + raise ValueError("an even p3-power occurred; J_k would carry an error function") + for j, c in enumerate(ek): + if c == 0: + continue + part = tf_scale(G(j, Fr(1, 24)), B) if B else {} + for i, ci in enumerate(C): + if ci: + part = tf_add(part, tf_scale(G(j + i, Fr(1, 6)), ci)) + La = tf_add(La, tf_scale(part, c)) + for (kind, mu), poly in La.items(): + for n, coef in poly.items(): + total = add(total, mul(coef, outer_moment(n + a, g, kind, mu, erfc, kappa))) + return total + + +def m4_reduction(): + """The m = 4 reduction of Math-#200: p_1 = (T - 2p_2 - p_3)/3, then p_2 = (v - p_3)/2 (Jacobian 1/6); returns the two + branches organised as {a: {k: e_{a,k}(v)}} with their constants.""" + m = 4 + alpha, beta, PE, PR, expE, rest = a_integrated_terms(m) + T, p2, p3 = pvar(0, 3), pvar(1, 3), pvar(2, 3) + p1 = pscale(padd(T, padd(pscale(p2, Fr(-2)), pscale(p3, Fr(-1)))), Fr(1, 3)) + img1 = [p1, p2, p3] + PE1, PR1 = psubst(PE, img1, 3), psubst(PR, img1, 3) + eE1, eR1, b1 = psubst(expE, img1, 3), psubst(rest, img1, 3), psubst(beta, img1, 3) + T2, v, q = pvar(0, 3), pvar(1, 3), pvar(2, 3) + img2 = [T2, pscale(padd(v, pscale(q, Fr(-1))), Fr(1, 2)), q] + PE2, PR2 = psubst(PE1, img2, 3), psubst(PR1, img2, 3) + eE2, eR2, b2 = psubst(eE1, img2, 3), psubst(eR1, img2, 3), psubst(b1, img2, 3) + diag = {(2, 0, 0), (0, 2, 0), (0, 0, 2)} + for e in (eE2, eR2): + if set(e) != diag or e[(0, 2, 0)] != Fr(1, 24) or e[(0, 0, 2)] != Fr(1, 8): + raise ValueError("m = 4 decoupling failed: " + repr(e)) + if set(b2) != {(1, 0, 0)}: + raise ValueError("beta is not a multiple of T: " + repr(b2)) + gE, gR = eE2[(2, 0, 0)], eR2[(2, 0, 0)] + kappa = surd_mul((b2[(1, 0, 0)] / 2, 1), surd_sqrt(1 / alpha)) + constE = mul_pi_half(mul_surd(E(Fr(1, 2)), surd_sqrt(1 / alpha)), 1) + jac = Fr(1, 6) if MUT != "jacobian" else Fr(1, 2) + pref = prefactor(4, jac) + innerE, innerR = organize_tvp(PE2), organize_tvp(PR2) + kmax = max(max(max(ks) for ks in innerE.values()), max(max(ks) for ks in innerR.values())) + return {"alpha": alpha, "kappa": kappa, "gE": gE, "gR": gR, "constE": constE, "pref": pref, "innerE": innerE, "innerR": innerR, + "kmax": kmax, "JK": jk_exact(kmax), "beta_T": b2[(1, 0, 0)]} + + +def D4_exact(): + r = m4_reduction() + eb = mul(mul(r["pref"], r["constE"]), integrate_branch(r["innerE"], r["gE"], True, r["kappa"], r["JK"])) + rb = mul(r["pref"], integrate_branch(r["innerR"], r["gR"], False, r["kappa"], r["JK"])) + r["erfc_branch"], r["poly_branch"] = eb, rb + return add(eb, rb), r + + +def Z4_exact(): + """Mehta's Z_4 through the same machinery: Z_4 = 4! sqrt(pi) (1/6) int dT e^{-T^2/48} int_0^T dv e^{-v^2/24} int_0^v dp_3 + V e^{-p_3^2/8}, V the Vandermonde p_1 p_2 p_3 (p_1+p_2)(p_2+p_3)(p_1+p_2+p_3), p_1 = (T - v)/3, p_2 = (v - p_3)/2.""" + T, v, q = pvar(0, 3), pvar(1, 3), pvar(2, 3) + p1 = pscale(padd(T, pscale(v, Fr(-1))), Fr(1, 3)) + p2 = pscale(padd(v, pscale(q, Fr(-1))), Fr(1, 2)) + V = pconst(1, 3) + for f in (p1, p2, q, padd(p1, p2), padd(p2, q), padd(padd(p1, p2), q)): + V = pmul(V, f) + inner = organize_tvp(V) + kmax = max(max(ks) for ks in inner.values()) + jac = Fr(1, 6) if MUT != "jacobian" else Fr(1, 2) + const = mul_pi_half(E(24 * jac), 1) + return mul(const, integrate_branch(inner, Fr(1, 48), False, None, jk_exact(kmax))) + + +# ---------------- 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() + z4 = Z4_exact() + d4, info4 = D4_exact() + atoms_used = list(ATOMS) # the atoms created by the derivations (controls below may add more) + + def target(spec, keys): + out = {} + for name, c in spec.items(): + out = add(out, scale(keys[name], c)) + return out + a_half, a14_4, a14_7, a21_7 = (atan_elem(t) for t in ((Fr(1, 2), 1), (Fr(1, 4), 14), (Fr(1, 7), 14), (Fr(1, 7), 21))) + keys3 = {"1": E(1), "1/pi": E(1, 1, -2), "arctan(1/2)/pi": mul_pi_half(a_half, -2)} + keys4 = {"1": E(1), "sqrt6": E(1, 6), "sqrt21/pi": E(1, 21, -2), "arctan(sqrt21/7)/pi": mul_pi_half(a21_7, -2), + "sqrt6 arctan(sqrt14/4)/pi": mul_pi_half(mul_surd(a14_4, (Fr(1), 6)), -2), + "sqrt6 arctan(sqrt14/7)/pi": mul_pi_half(mul_surd(a14_7, (Fr(1), 6)), -2)} + D3_target, D4_target = target(CLOSED_FORM_D3, keys3), target(CLOSED_FORM_D4, keys4) + + kE = sorted({k for ks in info4["innerE"].values() for k in ks}) + kR = sorted({k for ks in info4["innerR"].values() for k in ks}) + checks["STRUCTURE"] = bool(info4["alpha"] == Fr(3, 7) and info4["kappa"] == (Fr(1, 28), 21) and info4["gE"] == Fr(1, 48) + and info4["gR"] == Fr(1, 21) and info4["gE"] + surd_sq(info4["kappa"]) == info4["gR"] + and kE == kR == [1, 3, 5, 7, 9] and info4["kmax"] == 9 + and atoms_used[1:] == [(Fr(1, 5), 15), (Fr(1, 2), 1), (Fr(1, 4), 14), (Fr(1, 7), 21), (Fr(1, 7), 14), (Fr(1, 7), 7)]) + lams = (Fr(1, 48), Fr(1, 21), Fr(1, 16), Fr(3, 16), Fr(5, 56), Fr(3, 14), 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(21) for lam in lams)) + checks["JK_EXACT"] = bool(jk_identities(info4["JK"])) + checks["CUMULATIVE_EXACT"] = bool(g_identities(20, (Fr(1, 24), Fr(1, 6)))) + checks["D1_EXACT"] = bool(d1 == E(Fr(4, 3))) + checks["D2_EXACT"] = bool(d2 == add(E(Fr(29, 6)), E(-1, 6))) + checks["D3_EXACT"] = bool(d3 == D3_target) + checks["MEHTA_Z4_EXACT"] = bool(z4 == E(1536, 1, 2) and z4 == mehta_Z(4)) + checks["D4_FORM"] = bool(d4 == D4_target) + # float controls (Simpson on [0, sqrt(140/lam)], erf from math): the base integrals at the parameters that occur, and sampled moments + kap, s24, s6 = info4["kappa"], surd_sqrt(Fr(1, 24)), surd_sqrt(Fr(1, 6)) + ok = True + for lam, u in ((Fr(1, 48), kap), (Fr(3, 16), kap), (Fr(1, 21), s24), (Fr(1, 21), s6), (Fr(1, 6), (Fr(1, 12), 6))): + 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, 48), kap, s24), (Fr(1, 48), kap, s6), (Fr(1, 16), kap, s6)): + 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, 48), (kap,)), (Fr(1, 48), tuple(sorted((kap, s24)))), (Fr(1, 48), tuple(sorted((kap, s6)))), + (Fr(1, 21), (s24,)), (Fr(1, 21), ()), (Fr(3, 16), (kap,))): + 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 #200's certified enclosure; the simplified form with arctan(1/sqrt14) + D4_iv = iv_eval(d4) + a_simpl = atan_iv(root_frac(Fr(14), 2) / 14) + D4_simpl = (Iv.frac(Fr(6695, 54)) - Iv.frac(Fr(405, 32)) * root_frac(Fr(6), 2) + - (Iv.frac(Fr(1375, 72)) * root_frac(Fr(21), 2) + Iv.frac(Fr(6695, 27)) * atan_iv(root_frac(Fr(21), 2) / 7) + + Iv.frac(Fr(405, 16)) * root_frac(Fr(6), 2) * a_simpl) / PI) + cert = Iv(Decimal(CERTIFIED["D_4"][0]), Decimal(CERTIFIED["D_4"][1])) + checks["D4_INSIDE_CERTIFIED"] = bool(cert.contains(D4_iv) and D4_iv.width() < Decimal("1e-55")) + checks["SIMPLIFIED_FORM"] = bool(D4_simpl.intersects(D4_iv) and cert.contains(D4_simpl) and D4_simpl.width() < Decimal("1e-55")) + c5 = GAMMA76 * CBRT32 * D4_iv / (12 * SQRT3 * PI * PI * PI * SQRTPI) + cert5 = Iv(Decimal(CERTIFIED["c_5_ref"][0]), Decimal(CERTIFIED["c_5_ref"][1])) + checks["C5_CLOSED"] = bool(cert5.contains(c5) and c5.width() < Decimal("1e-55")) + checks["LIBRARY_EXACT"] = bool(library_exact()) + pinned = {"D_4": D4_iv, "c_5_ref": c5, "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) != 16: + raise ValueError("rule count changed") + passed = all(checks.values()) + + def fr(x): + return str(x) + def inner_json(inner): + return {str(a): {str(k): [fr(c) for c in ek] for k, ek in sorted(ks.items())} for a, ks in sorted(inner.items())} + out = { + "object": "CL-SIDE24-D4-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), + "Z_4": show(z4), + "D_4": show(d4), + "D_4_simplified": "6695/54 - (405/32) sqrt6 - (1/pi) [ (1375/72) sqrt21 + (6695/27) arctan(sqrt21/7) + (405/16) sqrt6 arctan(sqrt14/14) ]" + " (arctan(sqrt14/4) - arctan(sqrt14/7) = arctan(1/sqrt14))", + "c_5_ref": "Gamma(7/6) (3/2)^(1/3) D_4 / (12 sqrt3 pi^(7/2))", + "erfc_branch_of_D_4": show(info4["erfc_branch"]), + "polynomial_branch_of_D_4": show(info4["poly_branch"]), + }, + "interval_evaluation": {"D_4": D4_iv.pair(), "D_4_simplified": D4_simpl.pair(), "c_5_ref": c5.pair(), + "arctan(sqrt21/7)": atan_iv(root_frac(Fr(21), 2) / 7).pair(), "arctan(sqrt14/14)": a_simpl.pair(), + "arctan(sqrt14/4)": atan_iv(root_frac(Fr(14), 2) / 4).pair(), "arctan(sqrt14/7)": atan_iv(root_frac(Fr(14), 2) / 7).pair(), + "pi": PI.pair(), "Gamma(7/6)": GAMMA76.pair(), "(3/2)^(1/3)": CBRT32.pair()}, + "certified_enclosures_math_200": {"D_4": list(CERTIFIED["D_4"]), "c_5_ref": list(CERTIFIED["c_5_ref"])}, + "reduction_data": { + "m=4": {"alpha": fr(info4["alpha"]), "beta": "%s T" % fr(info4["beta_T"]), "kappa": "%s sqrt(%d)" % info4["kappa"], + "kappa^2": fr(surd_sq(info4["kappa"])), "lambda_erfc": fr(info4["gE"]), "lambda_poly": fr(info4["gR"]), + "prefactor": show(info4["pref"]), "G_0_constant": show(info4["constE"]), + "p3_powers": kE, "T_powers_erfc": sorted(info4["innerE"]), "T_powers_poly": sorted(info4["innerR"]), + "e_{a,k}(v) by power, erfc branch": inner_json(info4["innerE"]), + "e_{a,k}(v) by power, polynomial branch": inner_json(info4["innerR"]), + "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(info4["JK"])}}, + "m=3": {"kappa": "%s sqrt(%d)" % info3["kappa"], "lambda_erfc": fr(info3["lambda_erfc"]), "lambda_poly": fr(info3["lambda_poly"])}, + "m=2": {"kappa": "%s sqrt(%d)" % info2["kappa"], "lambda_erfc": fr(info2["lambda_erfc"]), "lambda_poly": fr(info2["lambda_poly"])}, + "atoms_created_by_the_derivations": ["1"] + ["arctan(%s sqrt(%d))" % a for a in atoms_used[1:]], + "note": "arctan(sqrt15/5) (m = 2) and arctan(1/sqrt7) (m = 4, from lam = 3/16) arise in intermediate terms and cancel", + }, + "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)", + "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)", + "G_n(mu, T)": "G_0 = (1/2) sqrt(pi/mu) erf(sqrt(mu) T); G_1 = (1 - e^{-mu T^2})/(2 mu); G_n = [(n-1) G_{n-2} - T^{n-1} e^{-mu T^2}]/(2 mu)", + "D_4 integral": "sqrt21/(2688 pi) [ (sqrt21 sqrt(pi)/6) int e^{-T^2/48} erfc(sqrt21 T/28) sum_a T^a L_a^E + int e^{-T^2/21} sum_a T^a L_a^R ]", + "L_a": "int_0^T e^{-v^2/24} sum_k e_{a,k}(v) J_k(v) dv, k odd, J_k = B_k + C_k e^{-v^2/8}: incomplete Gaussian moments with mu = 1/24, 1/6", + "Z_4": "4! sqrt(pi) (1/6) int e^{-T^2/48} int_0^T e^{-v^2/24} int_0^v V e^{-p3^2/8} = 1536 pi (exact, rule MEHTA_Z4_EXACT)", + }, + } + 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 451230951ddeff48b8e8397acc85846c222ddaf9 Mon Sep 17 00:00:00 2001 From: d6g8k5htny-coder Date: Wed, 30 Sep 2026 20:47:48 +0000 Subject: [PATCH 2/4] D_4 closed form v1.1: point the mehta mutant at Z_4; record the Codex review The mehta mutant altered Z_3 (left over from the D_3 script) and was rejected only through D3_EXACT; it now replaces Z_4 by Z_5 in the m = 4 prefactor and is rejected by MEHTA_Z4_EXACT, D4_FORM and the containments (Codex thread 4149168080). NOTE section 9 records the review, including the workflow finding that is not taken (reasons on the thread). No certified value changed. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- coefficients/side24_d5_closed_form_20260930/NOTE.md | 11 +++++++++++ .../side24_d5_closed_form_20260930/SOURCE_FILES.json | 12 ++++++------ .../side24_d5_closed_form_20260930/closed_form_d4.py | 2 +- 3 files changed, 18 insertions(+), 7 deletions(-) diff --git a/coefficients/side24_d5_closed_form_20260930/NOTE.md b/coefficients/side24_d5_closed_form_20260930/NOTE.md index 821be30ae..dfefe2912 100644 --- a/coefficients/side24_d5_closed_form_20260930/NOTE.md +++ b/coefficients/side24_d5_closed_form_20260930/NOTE.md @@ -205,3 +205,14 @@ verbatim). Run: `python3 -B -S closed_form_d4.py` (exit 0, JSON on stdout identi - **Validation:** 16/16 rules in both modes, byte-identical output; 14/14 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. + +## 9. Revisions + +- **v1.1 (Codex review 5371784947 on `60e56ef`).** (i) Thread 4149168080 (P2), taken: the `mehta` mutant altered `Z_3` (a + leftover of the Math-#201 script) and was rejected only through `D3_EXACT`; it now replaces `Z_4` by `Z_5` in the `m = 4` + prefactor and is rejected by `MEHTA_Z4_EXACT`, `D4_FORM` and the containments. (ii) Thread 4149168070 (P1, the replay + workflow and the 2026-09-27 owner stop), not taken; the reasons are on the thread: the per-packet replay workflow is the + repository's standing convention (88 workflow files on `main 3e0a91b`, about thirty of them added by every lane since + 2026-09-27), the owner's later directives quoted in `AGENTS.md` and the owner workflow of 2026-09-30 govern this record, and + the workflow is path-scoped to this packet and its pins. The owner can direct its removal at any time; the record is + runnable locally in two seconds without it. No certified value changed. diff --git a/coefficients/side24_d5_closed_form_20260930/SOURCE_FILES.json b/coefficients/side24_d5_closed_form_20260930/SOURCE_FILES.json index c1dfa21fa..d3010d5b0 100644 --- a/coefficients/side24_d5_closed_form_20260930/SOURCE_FILES.json +++ b/coefficients/side24_d5_closed_form_20260930/SOURCE_FILES.json @@ -57,9 +57,9 @@ "files": [ { "path": "NOTE.md", - "bytes": 15468, - "sha256": "6d1c9cd3b2a6132b473947e4d517ab5337078e256cd46514a091c85d3da0cde6", - "git_blob": "821be30aeafb7e48c8bc927575fb9950e0f4d784" + "bytes": 16415, + "sha256": "e0f98d57bcfde70b7aef91ebc98fc3b04d526d5d2867a783eb278e1a8bed3798", + "git_blob": "dfefe291223fbc2f6f2611fdca2928baa4d00bcb" }, { "path": "RESULTS.json", @@ -69,9 +69,9 @@ }, { "path": "closed_form_d4.py", - "bytes": 44943, - "sha256": "54e348113f67225725b7e2b4399bd39578c51c531967c8f35f8124475d68030b", - "git_blob": "83ff92db2d38156b06a85821c07adcabe0343378" + "bytes": 45019, + "sha256": "a967be2300baac88129ee575f3adfe62715d59c60b3d7641c30c729f3b25a589", + "git_blob": "e087f4c0007ae2473d28230771588da57f794aab" } ] } diff --git a/coefficients/side24_d5_closed_form_20260930/closed_form_d4.py b/coefficients/side24_d5_closed_form_20260930/closed_form_d4.py index 83ff92db2..e087f4c00 100644 --- a/coefficients/side24_d5_closed_form_20260930/closed_form_d4.py +++ b/coefficients/side24_d5_closed_form_20260930/closed_form_d4.py @@ -558,7 +558,7 @@ def gamma_half(twice): 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 + m_eff = m + 1 if (MUT == "mehta" and m == 4) else m # Z_5 for Z_4 (v1.1: was m == 3, Codex 4149168080) prod = E(1) for j in range(1, m_eff + 1): prod = mul(prod, gamma_half(j + 2)) From db3d38946cfe5928ead02e6eb847ff9a5d6b01ca Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 23:38:28 +0000 Subject: [PATCH 3/4] D_4 closed form v1.2: apply the S4 nonauthor read (F1-F7, wording, carriers, pins) Grok Bot agent 13's S4 read (Math-#202 comment 5974483504): AMEND, no BLOCK. - F1: the Proposition is conditional on the unmerged Math-#200 reduction. - F2: the c_{d,ref} closed forms for d <= 5 are conditional on #199/#200/#201 and on SIDE24 at its stated scope. - F3: on main, SIDE24 encloses c_{d,24} only for d = 2, 3. - F4: what "certified" means in RESULTS.json / SOURCE_FILES.json. - F5: Math-#200 companion pin moves to aa1d51e (NOTE.md blob bb931d46). - F6: displayed D_4 digits end ...0215842... (true digits ...0215842092..., re-derived here with 90-digit Decimal arithmetic). - F7: NOTE section 8 synced with the PR disposition. No script or RESULTS.json byte changed; workflow replay passes locally. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- .../side24_d5_closed_form_20260930/NOTE.md | 61 ++++++++++++------- .../SOURCE_FILES.json | 12 ++-- 2 files changed, 46 insertions(+), 27 deletions(-) diff --git a/coefficients/side24_d5_closed_form_20260930/NOTE.md b/coefficients/side24_d5_closed_form_20260930/NOTE.md index dfefe2912..8f3597e9f 100644 --- a/coefficients/side24_d5_closed_form_20260930/NOTE.md +++ b/coefficients/side24_d5_closed_form_20260930/NOTE.md @@ -15,7 +15,7 @@ density `∝ exp(−tr Q²/4)`, `Z` an independent standard normal), the cone mo ``` D_4 = 6695/54 − (405/32)√6 − (1/π) [ (1375/72)√21 + (6695/27) arctan√(3/7) + (405/16)√6 arctan(1/√14) ] - = 14.21876345897735760130646567787407831734060231608202158418… + = 14.2187634589773576013064656778740783173406023160820215842… ``` (`arctan√(3/7) = arctan(√21/7)`, `arctan(1/√14) = arctan(√14/14)`). The exact arithmetic returns the two last atoms as @@ -29,13 +29,14 @@ D_4 = 6695/54 − (405/32)√6 − (1/π) [ (1375/72)√21 + (6695/27) arctan√ c_{5,ref} = Γ(7/6) (3/2)^{1/3} D_4 / (12√3 π^{7/2}) = 0.01321931938008496807603348751464139652105289012569990545… ``` -and `c_{5,24}` is as in Math-#200: `|c_{5,24}/c_{5,ref} − 1| ≤ 1.8554·10⁻¹⁰⁷`. +and `c_{5,24}` is enclosed in Math-#200 (unmerged): `|c_{5,24}/c_{5,ref} − 1| ≤ 1.8554·10⁻¹⁰⁷`. -With SIDE24 §1 (`D_1 = 4/3`, `D_2 = 29/6 − √6`) and Math-#201 (`D_3 = (50π + 200 arctan 2 − 228)/(9π)`), the reference -coefficients `c_{d,ref}` of [LP] (15.2) are now in closed form for every `d ≤ 5` (§5). `D_5` (`d = 6`) is not claimed (§6). +With SIDE24 §1 (`D_1 = 4/3`, `D_2 = 29/6 − √6`; author-side, nonauthor review open) and Math-#201 (`D_3`, unmerged), the +reference coefficients `c_{d,ref}` of [LP] (15.2) have closed forms for every `d ≤ 5` (§5), conditional on Math-#199/#200/#201 +and on SIDE24 at its stated scope. `D_5` (`d = 6`) is not claimed (§6). **What is proved here and from what.** The identity is obtained by exact integration of the integral to which Math-#200 -reduces `D_4` (that reduction is exact algebra on the ordered-sector integrand, re-run here by the same code, and checked at +reduces `D_4` (unmerged; the Proposition is conditional on that reduction; the reduction is exact algebra on the ordered-sector integrand, re-run here by the same code, and checked at `m = 1, 2, 3` against `4/3`, `29/6 − √6` and Math-#201's `D_3` through the identical path). The computation lives in the finite-dimensional `Q`-vector space with basis `√r · π^{k/2} · A` (`r` squarefree, `k ∈ Z`, `A = 1` or an arctan atom), so its output is an identity. Math-#200's certified enclosure of `D_4` (an independent method: order-40 Taylor quadrature with Cauchy @@ -155,9 +156,16 @@ by the structural check: without the Vandermonde factor even `p_3`-powers appear `λ + u² + v²` in L3), `jk-init`, `gauss-half`, `boundary-term`, `atom-pi`, `cumulative-init` (`G_1` sign), `cumulative-recurrence` (`n−1 → n` in L2). Runtime about two seconds. +`certified` in `RESULTS.json` / `SOURCE_FILES.json` means exact arithmetic of the identity plus interval containment against +Math-#200's author-side enclosure (unmerged, quoted in the script, not byte-checked against #200); it is not a review or +acceptance. + ## 5. The coefficient in every `d ≤ 5` -With `c_{d,ref} = Γ(7/6)(3/2)^{1/3} |S^{d−1}| D_{d−1} / (√3 √π (2π)^d)` ([LP] (15.2); Math-#199 §4, Math-#200 §4): +With `c_{d,ref} = Γ(7/6)(3/2)^{1/3} |S^{d−1}| D_{d−1} / (√3 √π (2π)^d)` ([LP] (15.2); Math-#199 §4, Math-#200 §4), the table +below gives closed forms for every `d ≤ 5`, conditional on Math-#199/#200/#201 and on SIDE24 at its stated scope. SIDE24 (1) on +`main` states the formula for `d = 2, 3` only; for `d = 4, 5` it is cited from the unmerged Math-#199 §4 and #200 §4. SIDE24 +itself is author-side with nonauthor review open. | `d` | `D_{d−1}` | `c_{d,ref}` | value | |---|---|---|---| @@ -166,12 +174,14 @@ With `c_{d,ref} = Γ(7/6)(3/2)^{1/3} |S^{d−1}| D_{d−1} / (√3 √π (2π)^d | 4 | `(50π + 200 arctan 2 − 228)/(9π)` | `Γ(7/6)(3/2)^{1/3}(50π + 200 arctan 2 − 228)/(72√3 π^{7/2})` | `0.0233216660029528350945211949528…` (Math-#201; #199 encloses) | | 5 | Proposition above | `Γ(7/6)(3/2)^{1/3} D_4/(12√3 π^{7/2})` | `0.0132193193800849680760334875146…` (this record; #200 encloses) | -The torus constants `c_{d,24}` remain enclosed through the SIDE24 §§3–4 sandwich with the constants of Math-#199 and #200. +On main, SIDE24 §§3–4 encloses `c_{d,24}` only for `d = 2, 3`. The `d = 4, 5` enclosures are in the unmerged companions Math-#199 +and Math-#200 (nonauthor reads open), not on main. ## 6. Scope and non-claims -- The Proposition is an identity, proved by L1–L4 applied to the exact reduction of Math-#200. It consumes [LP] (15.1)–(15.2) and - SIDE24 §1 at their scope and does not review them. +- The Proposition is an identity, proved by L1–L4 applied to the reduction of Math-#200 (§§1–2 of its NOTE). That reduction is + unmerged and awaits nonauthor review, so the Proposition is conditional on it. It consumes [LP] (15.1)–(15.2) and SIDE24 §1 at + their scope and does not review them. - **No closed form for `D_5` (`d = 6`) is claimed or expected by this method.** The `m = 5` reduction needs a second cumulative layer: the first produces `erf(√μ v)` terms (L2), and a cumulative integral of `e^{−μ'v²} · polynomial · erf(√μ v)` is not elementary in its upper limit (it is an Owen-`T`-type function), so the outer integrand would carry a non-elementary factor; @@ -186,25 +196,26 @@ The torus constants `c_{d,24}` remain enclosed through the SIDE24 §§3–4 sand `coefficients/side24_d5_closed_form_20260930/{NOTE.md, closed_form_d4.py, RESULTS.json, SOURCE_FILES.json}` and `.github/workflows/side24-d5-closed-form.yml` (manifest, pins, byte-identical replay in `-B -S` and `-B -O -S`, the stated closed-form string, the fourteen mutants). Pins on `main 3e0a91b`: [LP] `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` -blob `dfed3b8d`; SIDE24 `coefficients/side24_v1/PROOF.md` blob `44b66f04`. Companions, not on `main`: Math-#200 at `33d50de` +blob `dfed3b8d`; SIDE24 `coefficients/side24_v1/PROOF.md` blob `44b66f04`. Companions, not on `main`: Math-#200 at `aa1d51e` (`coefficients/side24_d5_20260930/RESULTS.json` blob `b67c00f4`, the two enclosures quoted in the script; `NOTE.md` blob -`ab3fe17d`, the reduction); Math-#201 at `3abcc10` (`closed_form_d3.py` blob `a0c91692`, the arithmetic and L1, L3–L4, reused +`bb931d46`, the reduction); Math-#201 at `3abcc10` (`closed_form_d3.py` blob `a0c91692`, the arithmetic and L1, L3–L4, reused verbatim). Run: `python3 -B -S closed_form_d4.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-d4-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-#200 reduction; exact `m = 1, 2, 3` - and `Z_4` regressions; the closed form at the centre of 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`, the constants; - L1), Slice B (§2 L2–L4 and §3: the T-function layer, the two-erf base integral, the by-parts recurrences, the atoms and - cancellations, the `Z_4` identity), Slice C (§§4–6: rules, mutants, containment, the coefficient table, the `D_5` non-claim). -- **Unresolved finding IDs:** none. -- **Validation:** 16/16 rules in both modes, byte-identical output; 14/14 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. +- **Claim:** the Proposition and Corollary of §0, proved by exact integration of the Math-#200 reduction (unmerged; the + Proposition is conditional on it); exact `m = 1, 2, 3` and `Z_4` regressions; the closed form at the centre of Math-#200's + author-side certified enclosure. No theorem of [LP] or SIDE24 is proved or reviewed. +- **Completed review scopes:** Codex code review 5371784947 at `60e56ef` (two findings: one taken, one declined with reasons). + Nonauthor read S4 by Grok Bot agent 13 (Grok Bot support agent; non-Claude, nonauthor lane) at `4512309`, Slices A–C: AMEND, + no BLOCK, no numerical disagreement (an independent route reproduces `D_4` to `1.5·10⁻¹⁵`); F1–F7 applied in v1.2. +- **Unresolved finding IDs:** 4149168070 (P1, the replay workflow vs the 2026-09-27 owner stop; declined with reasons; the + disposition is ledger task B on main#229, left to a non-Claude lane). +- **Validation:** 16/16 rules in `-B -S` and `-B -O -S`, byte-identical output; 14/14 mutants rejected in both modes; the + workflow replayed locally; hosted runs on each head. +- **Next action:** a readback of F1–F7; amendments on this branch, recorded in `SOURCE_FILES.json`. Author will not merge. ## 9. Revisions @@ -216,3 +227,11 @@ verbatim). Run: `python3 -B -S closed_form_d4.py` (exit 0, JSON on stdout identi 2026-09-27), the owner's later directives quoted in `AGENTS.md` and the owner workflow of 2026-09-30 govern this record, and the workflow is path-scoped to this packet and its pins. The owner can direct its removal at any time; the record is runnable locally in two seconds without it. No certified value changed. +- **v1.2 (nonauthor read S4, Grok Bot agent 13, Math-#202 comment 5974483504, on `4512309`).** Wording, carriers and pins + only; no certified value, script or `RESULTS.json` byte changed. F1: the Proposition is conditional on the unmerged Math-#200 + reduction (§0, §6). F2: the `c_{d,ref}` closed forms for `d ≤ 5` are conditional on Math-#199/#200/#201 and on SIDE24 at its + stated scope (§0, §5 lead-in, PR title). F3: on `main`, SIDE24 §§3–4 encloses `c_{d,24}` only for `d = 2, 3`; the `d = 4, 5` + enclosures are in the unmerged Math-#199/#200 (§0, §5). F4: what `certified` means (§4). F5: the Math-#200 companion pin moves + to `aa1d51e` (`NOTE.md` blob `bb931d46`; `RESULTS.json` blob unchanged, `b67c00f4`). F6: the displayed digits of `D_4` end + `…0215842…` (the true digits are `…0215842092…`; the old trailing `18` lay beyond the certified prefix). F7: §8 synced with + the PR's disposition block. diff --git a/coefficients/side24_d5_closed_form_20260930/SOURCE_FILES.json b/coefficients/side24_d5_closed_form_20260930/SOURCE_FILES.json index d3010d5b0..1a759c931 100644 --- a/coefficients/side24_d5_closed_form_20260930/SOURCE_FILES.json +++ b/coefficients/side24_d5_closed_form_20260930/SOURCE_FILES.json @@ -34,16 +34,16 @@ "companion_not_on_main": [ { "pr": "https://github.com/d6g8k5htny-coder/Math-/pull/200", - "commit": "33d50de", + "commit": "aa1d51e", "path": "coefficients/side24_d5_20260930/RESULTS.json", "git_blob": "b67c00f45d053b51c2ec15ce8d53c8a34e49a006", "role": "the certified enclosures of D_4 and c_{5,ref} quoted in the script (rules D4_INSIDE_CERTIFIED, SIMPLIFIED_FORM, C5_CLOSED, PINNED)" }, { "pr": "https://github.com/d6g8k5htny-coder/Math-/pull/200", - "commit": "33d50de", + "commit": "aa1d51e", "path": "coefficients/side24_d5_20260930/NOTE.md", - "git_blob": "ab3fe17d8fbed0b417a4844ff9490e2eefcb5134", + "git_blob": "bb931d46c49dc37cc3870606fc7d862f2368318b", "role": "sections 1-2, the reduction that is integrated exactly here; section 4, the coefficient formula and |S^4|" }, { @@ -57,9 +57,9 @@ "files": [ { "path": "NOTE.md", - "bytes": 16415, - "sha256": "e0f98d57bcfde70b7aef91ebc98fc3b04d526d5d2867a783eb278e1a8bed3798", - "git_blob": "dfefe291223fbc2f6f2611fdca2928baa4d00bcb" + "bytes": 18477, + "sha256": "b502e3f890e36c3a0f477bd98a09cc1985bc8b8c5f97b1e4cec0e50659d966f7", + "git_blob": "8f3597e9f167f9ccac73ebfd92ca3299db743088" }, { "path": "RESULTS.json", From 73dfabbaeb8a1b79af769e8a0a769b5b44e6b9b4 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 4 Oct 2026 00:05:44 +0000 Subject: [PATCH 4/4] D_4 closed form v1.3: S4 readback R1 (header pin) and companion pins Grok Bot agent 13's S4 readback (Math-#202 comment 5974757288): F1-F7 resolved; R1, the NOTE header still pinned Math-#200 at 33d50de. Header and section 7 now pin Math-#200 at 74b1310 (S2 v1.2; RESULTS.json blob b67c00f4 unchanged) and Math-#201 at 6276eba (S3 v1.1; closed_form_d3.py changes only "certified": passed in the output dict). Optional N1, N2 applied. No script or RESULTS.json byte changed. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- .../side24_d5_closed_form_20260930/NOTE.md | 17 ++++++++++++----- .../SOURCE_FILES.json | 16 ++++++++-------- 2 files changed, 20 insertions(+), 13 deletions(-) diff --git a/coefficients/side24_d5_closed_form_20260930/NOTE.md b/coefficients/side24_d5_closed_form_20260930/NOTE.md index 8f3597e9f..42cb76725 100644 --- a/coefficients/side24_d5_closed_form_20260930/NOTE.md +++ b/coefficients/side24_d5_closed_form_20260930/NOTE.md @@ -2,7 +2,7 @@ **Object** `CL-SIDE24-D4-CLOSED-FORM-20260930-v1` · **scientific effect NONE** · declarative record, `executed: false` · base `main 3e0a91b` · claim: Math-#200 comment 5918942608 · companions: Math-#200 (`coefficients/side24_d5_20260930`, head -`33d50de`), whose reduction is the input and whose certified enclosure is the independent check, and Math-#201 +`74b1310`), whose reduction is the input and whose author-side certified enclosure is the independent check, and Math-#201 (`coefficients/side24_d4_closed_form_20260930`), whose exact arithmetic and lemmas are extended here by one cumulative layer. `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. @@ -39,7 +39,7 @@ and on SIDE24 at its stated scope. `D_5` (`d = 6`) is not claimed (§6). reduces `D_4` (unmerged; the Proposition is conditional on that reduction; the reduction is exact algebra on the ordered-sector integrand, re-run here by the same code, and checked at `m = 1, 2, 3` against `4/3`, `29/6 − √6` and Math-#201's `D_3` through the identical path). The computation lives in the finite-dimensional `Q`-vector space with basis `√r · π^{k/2} · A` (`r` squarefree, `k ∈ Z`, `A = 1` or an arctan atom), so its -output is an identity. Math-#200's certified enclosure of `D_4` (an independent method: order-40 Taylor quadrature with Cauchy +output is an identity. Math-#200's author-side certified enclosure of `D_4` (an independent method: order-40 Taylor quadrature with Cauchy remainders and certified cumulative integrals) contains the interval evaluation of the closed form, which lies at its centre (`1.94·10⁻⁴²` from either endpoint of a `3.9·10⁻⁴²`-wide enclosure; 43 common digits; rule `D4_INSIDE_CERTIFIED`). Mehta's `Z_4 = 1536π` is reproduced **exactly** by the same triangle machinery (rule `MEHTA_Z4_EXACT`). @@ -196,9 +196,9 @@ and Math-#200 (nonauthor reads open), not on main. `coefficients/side24_d5_closed_form_20260930/{NOTE.md, closed_form_d4.py, RESULTS.json, SOURCE_FILES.json}` and `.github/workflows/side24-d5-closed-form.yml` (manifest, pins, byte-identical replay in `-B -S` and `-B -O -S`, the stated closed-form string, the fourteen mutants). Pins on `main 3e0a91b`: [LP] `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` -blob `dfed3b8d`; SIDE24 `coefficients/side24_v1/PROOF.md` blob `44b66f04`. Companions, not on `main`: Math-#200 at `aa1d51e` +blob `dfed3b8d`; SIDE24 `coefficients/side24_v1/PROOF.md` blob `44b66f04`. Companions, not on `main`: Math-#200 at `74b1310` (`coefficients/side24_d5_20260930/RESULTS.json` blob `b67c00f4`, the two enclosures quoted in the script; `NOTE.md` blob -`bb931d46`, the reduction); Math-#201 at `3abcc10` (`closed_form_d3.py` blob `a0c91692`, the arithmetic and L1, L3–L4, reused +`7d12f050`, the reduction); Math-#201 at `6276eba` (`closed_form_d3.py` blob `5e7e4e59`, the arithmetic and L1, L3–L4, reused verbatim). Run: `python3 -B -S closed_form_d4.py` (exit 0, JSON on stdout identical to `RESULTS.json`); `--mutant NAME` exits 1. ## 8. Current disposition @@ -210,7 +210,7 @@ verbatim). Run: `python3 -B -S closed_form_d4.py` (exit 0, JSON on stdout identi author-side certified enclosure. No theorem of [LP] or SIDE24 is proved or reviewed. - **Completed review scopes:** Codex code review 5371784947 at `60e56ef` (two findings: one taken, one declined with reasons). Nonauthor read S4 by Grok Bot agent 13 (Grok Bot support agent; non-Claude, nonauthor lane) at `4512309`, Slices A–C: AMEND, - no BLOCK, no numerical disagreement (an independent route reproduces `D_4` to `1.5·10⁻¹⁵`); F1–F7 applied in v1.2. + no BLOCK, no numerical disagreement (an independent route reproduces `D_4` to `1.5·10⁻¹⁵`, relative, float evidence); F1–F7 applied in v1.2. - **Unresolved finding IDs:** 4149168070 (P1, the replay workflow vs the 2026-09-27 owner stop; declined with reasons; the disposition is ledger task B on main#229, left to a non-Claude lane). - **Validation:** 16/16 rules in `-B -S` and `-B -O -S`, byte-identical output; 14/14 mutants rejected in both modes; the @@ -235,3 +235,10 @@ verbatim). Run: `python3 -B -S closed_form_d4.py` (exit 0, JSON on stdout identi to `aa1d51e` (`NOTE.md` blob `bb931d46`; `RESULTS.json` blob unchanged, `b67c00f4`). F6: the displayed digits of `D_4` end `…0215842…` (the true digits are `…0215842092…`; the old trailing `18` lay beyond the certified prefix). F7: §8 synced with the PR's disposition block. +- **v1.3 (S4 readback, Math-#202 comment 5974757288, on `db3d389`; header pin and companions only).** R1: the NOTE header + still pinned Math-#200 at `33d50de`; it now names `74b1310`. The companion pins follow the companions' own nonauthor + amendments: Math-#200 moves to `74b1310` (S2's v1.2; `NOTE.md` blob `7d12f050`, `RESULTS.json` blob unchanged, + `b67c00f4`, so the quoted enclosures are unchanged), and Math-#201 moves to `6276eba` (S3's v1.1; `closed_form_d3.py` + blob `5e7e4e59`, whose only change is `"certified": passed` in the output dict, so every reused function is identical). + N1, N2: "author-side certified enclosure" in the header and §0, and "relative, float evidence" in §8. No script or + `RESULTS.json` byte changed. diff --git a/coefficients/side24_d5_closed_form_20260930/SOURCE_FILES.json b/coefficients/side24_d5_closed_form_20260930/SOURCE_FILES.json index 1a759c931..b9eba588a 100644 --- a/coefficients/side24_d5_closed_form_20260930/SOURCE_FILES.json +++ b/coefficients/side24_d5_closed_form_20260930/SOURCE_FILES.json @@ -34,32 +34,32 @@ "companion_not_on_main": [ { "pr": "https://github.com/d6g8k5htny-coder/Math-/pull/200", - "commit": "aa1d51e", + "commit": "74b1310", "path": "coefficients/side24_d5_20260930/RESULTS.json", "git_blob": "b67c00f45d053b51c2ec15ce8d53c8a34e49a006", "role": "the certified enclosures of D_4 and c_{5,ref} quoted in the script (rules D4_INSIDE_CERTIFIED, SIMPLIFIED_FORM, C5_CLOSED, PINNED)" }, { "pr": "https://github.com/d6g8k5htny-coder/Math-/pull/200", - "commit": "aa1d51e", + "commit": "74b1310", "path": "coefficients/side24_d5_20260930/NOTE.md", - "git_blob": "bb931d46c49dc37cc3870606fc7d862f2368318b", + "git_blob": "7d12f0502d2e557e1c04e101827a554b53ce3def", "role": "sections 1-2, the reduction that is integrated exactly here; section 4, the coefficient formula and |S^4|" }, { "pr": "https://github.com/d6g8k5htny-coder/Math-/pull/201", - "commit": "3abcc10", + "commit": "6276eba", "path": "coefficients/side24_d4_closed_form_20260930/closed_form_d3.py", - "git_blob": "a0c9169227c9a0b42c66deaca2b4f2e3168046ab", + "git_blob": "5e7e4e59bb5de239e0c7a1b6bdb632f8300745dc", "role": "the exact arithmetic, the moments M_n and the m = 1, 2, 3 pipelines, reused verbatim; the D_3 closed form is rule D3_EXACT" } ], "files": [ { "path": "NOTE.md", - "bytes": 18477, - "sha256": "b502e3f890e36c3a0f477bd98a09cc1985bc8b8c5f97b1e4cec0e50659d966f7", - "git_blob": "8f3597e9f167f9ccac73ebfd92ca3299db743088" + "bytes": 19273, + "sha256": "8a12017a9cedafb303779b06e221773f14963615e250a5f10a647436aea05198", + "git_blob": "42cb7672595b39c9afb635c0f9c1720dc1cdc28b" }, { "path": "RESULTS.json",