diff --git a/.github/workflows/elder-third-order.yml b/.github/workflows/elder-third-order.yml new file mode 100644 index 000000000..98928ee2f --- /dev/null +++ b/.github/workflows/elder-third-order.yml @@ -0,0 +1,158 @@ +name: Elder third-order exact controls + +'on': + pull_request: + paths: + - 'frontiers/elder_third_order_20261001/**' + - '.github/workflows/elder-third-order.yml' + # bound merged sources (consumed in SOURCES.json) and the pinned unmerged dependencies + - 'frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md' + - 'imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md' + - 'imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md' + - 'reviews/d1_section9_borel_repair_20260925/REPAIR.md' + - 'reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md' + - 'frontiers/c7_zero_gap_limit_20260929/PROOF.md' + - 'frontiers/c7_total_bounded_20260929/PROOF.md' + - 'frontiers/remainder_vanishing_20260930/PROOF.md' + - 'frontiers/remainder_rate_20260930/PROOF.md' + - 'frontiers/cusp_second_order_20261001/PROOF.md' + - 'frontiers/candidate_third_order_20261001/PROOF.md' + - 'frontiers/far_elder_rate_20260930/PROOF.md' + workflow_dispatch: + +permissions: + contents: read + pull-requests: read + +jobs: + exact-controls: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + GH_TOKEN: ${{ github.token }} + GH_REPOSITORY: ${{ github.repository }} + run: | + set -euo pipefail + python -B -S - <<'PY' + import base64, hashlib, json, os, pathlib, subprocess, sys, urllib.parse, urllib.request + root = pathlib.Path('frontiers/elder_third_order_20261001').resolve() + manifest = json.loads((root / 'SOURCES.json').read_text()) + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest['files']] + ['SOURCES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest['files']: + path = root / entry['path'] + if path.is_symlink(): + raise ValueError('symlink: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('packet file identity mismatch: ' + entry['path']) + def same(data, entry): + framed = b'blob ' + str(len(data)).encode() + b'\0' + data + return len(data) == entry['bytes'] and hashlib.sha256(data).hexdigest() == entry['sha256'] and hashlib.sha1(framed).hexdigest() == entry['git_blob'] + def tree_entry(path): + # the checked-out commit's tree entry for path: (mode, type, blob) or None; symlinks have mode 120000 + out = subprocess.run(['git', 'ls-tree', '-z', 'HEAD', '--', path], check=True, capture_output=True).stdout + if not out: + return None + meta, name = out.rstrip(b'\0').split(b'\t', 1) + if name.decode() != path: + raise ValueError('unexpected tree entry for ' + path) + mode, kind, sha = meta.decode().split() + return mode, kind, sha + def tree_bytes(entry): + # a source read from the checkout must be a regular file whose tree blob is the recorded one + te = tree_entry(entry['path']) + if te is None: + return None + mode, kind, sha = te + if mode != '100644' or kind != 'blob' or sha != entry['git_blob']: + raise ValueError('tree entry is not the recorded regular-file blob (mode/type/blob ' + ' '.join(te) + '): ' + entry['path']) + path = pathlib.Path(entry['path']) + if path.is_symlink() or not path.is_file(): + raise ValueError('checkout path is not a regular file: ' + entry['path']) + return path.read_bytes() + for entry in manifest['consumed'] + manifest['cited_only']: + data = tree_bytes(entry) + if data is None or not same(data, entry): + raise ValueError('merged source drifted or absent: ' + entry['path']) + # unmerged sources are bound to their recorded commit, path and blob through the repository API: the head must + # resolve, the path in that head's tree must be a file with the recorded blob id and size, and the bytes must have + # the recorded sha256; a consumed dependency that has landed is instead read from the tree and must be identical + # to the pinned version (else this packet needs rebinding) + api = 'https://api.github.com/repos/' + os.environ['GH_REPOSITORY'] + def get_json(url): + req = urllib.request.Request(url, headers={'Authorization': 'Bearer ' + os.environ['GH_TOKEN'], + 'Accept': 'application/vnd.github+json'}) + with urllib.request.urlopen(req, timeout=60) as resp: + return json.load(resp) + def bound(entry): + commit = get_json(api + '/commits/' + entry['head']) + if commit.get('sha') != entry['head']: + raise ValueError('recorded head does not resolve: ' + entry['head']) + node = get_json(api + '/contents/' + urllib.parse.quote(entry['path']) + '?ref=' + entry['head']) + if (node.get('type') != 'file' or node.get('path') != entry['path'] or node.get('sha') != entry['git_blob'] + or node.get('size') != entry['bytes']): + raise ValueError('recorded head/path does not map to the recorded blob: ' + entry['path']) + blob = get_json(api + '/git/blobs/' + entry['git_blob']) + if blob.get('encoding') != 'base64': + raise ValueError('unexpected blob encoding for ' + entry['path']) + return base64.b64decode(blob['content']) + def current(entry): + # drift gate (Copilot review on #220): the recorded head keeps resolving after a dependency PR advances, so + # also resolve the dependency PR now. Open: the file at its current head must be the pinned blob. Merged: + # the file at its merge commit must be the pinned blob. Closed unmerged: rebinding is required. + pr = get_json(api + '/pulls/' + entry['pr'].split('#', 1)[1]) + if pr.get('merged'): + ref = pr.get('merge_commit_sha') + elif pr.get('state') == 'open': + ref = pr['head']['sha'] + else: + raise ValueError('dependency ' + entry['pr'] + ' closed without merge: rebind required') + node = get_json(api + '/contents/' + urllib.parse.quote(entry['path']) + '?ref=' + ref) + if node.get('type') != 'file' or node.get('sha') != entry['git_blob'] or node.get('size') != entry['bytes']: + raise ValueError('dependency ' + entry['pr'] + ' advanced: ' + entry['path'] + ' at ' + ref + + ' is not the pinned blob (rebind required)') + return ref + for kind in ('consumed_unmerged', 'cited_unmerged'): + for entry in manifest.get(kind, []): + # a landed consumed dependency must be the recorded regular-file blob in this tree (symlinks and any + # other mode are rejected by tree_bytes); otherwise the source is bound through the API + landed = tree_bytes(entry) if kind == 'consumed_unmerged' else None + if landed is not None: + data, where = landed, 'tree' + else: + if os.path.lexists(entry['path']) and kind == 'consumed_unmerged': + raise ValueError('path present in the checkout but not as a tracked blob: ' + entry['path']) + data, where = bound(entry), 'head/path/blob api' + if not same(data, entry): + raise ValueError(kind + ' source differs from its pinned blob (rebind required): ' + entry['path'] + ' via ' + where) + now = current(entry) if kind == 'consumed_unmerged' else None + print(json.dumps({kind + '_bound': entry['path'], 'git_blob': entry['git_blob'], 'head': entry['head'], + 'via': where, 'current_ref_checked': now})) + script = str(root / 'e3_check.py') + expected = (root / 'RESULTS.json').read_bytes() + 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)) + for m in manifest['mutants']: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], capture_output=True, timeout=600).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + rc = subprocess.run([sys.executable, *flags, script, '--mutant', 'M9'], capture_output=True, timeout=600).returncode + if rc != 2: + raise RuntimeError('unknown mutant label not rejected with exit 2') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/frontiers/elder_third_order_20261001/PROOF.md b/frontiers/elder_third_order_20261001/PROOF.md new file mode 100644 index 000000000..c8767ddec --- /dev/null +++ b/frontiers/elder_third_order_20261001/PROOF.md @@ -0,0 +1,861 @@ +# The elder density to third order up to its far part, and the three-term law with rate `ℓ^{4/11}` given Math- #187 (merged) + +Object: CL-ELDER-THIRD-ORDER-20261001-v1.1 (supersedes v1 on the same branch). +Author: Anthropic Claude (claude.ai session `session_01NMeKEismAyeqgdB4sy2NJU`), 1 October 2026. + +**v1.1 changes.** +- Lemma B′, and with it #207 Lemma CU.5 and the exponent `β`, is replaced by two new lemmas (§3): + - **Lemma H.** The rescaled Hessian `H̃ = Λ_r^{−1}H_MΛ_r^{−1}`, with `Λ_r = diag(r, 1, …, 1)`, is a uniformly + nondegenerate Gaussian under the pins for all `r ≤ r_0^*`. + - **Lemma S′.** `E_Q[(W_r/r²)e] ≤ Cℓ^{2/3}r^{−2}(κ + r)P^N` for `r ≤ r_0^*` and `k ≤ r`. + + Together they are the near-regime spectral refinement that #198 Remark 1 describes. +- The intermediate separations `[ρ_c, r_0^*]` now contribute `O(ℓ^{2/5})`: #198 (W.1) below `ℓ^{2/15}`, Lemma S′ above. + So (E3.0) is an expansion with only the far elder density at the fixed radius `r_0^*` left unexpanded. +- Consequently (E3.3) has the rate `O(ℓ^{4/11})` and uses #187 at the single separation `r_0^*`. v1's `ε`-argument + (`r₁ ↓ 0`) is gone, and so is v1 Remark 2's need for a quantified `C(ρ)`. Corollary E3′(3) gets the same rate. +- (E3.1), (E3.2) and Lemmas CU.1′, S, Q, G, CE and O′ are unchanged, except that Lemma CE's radius no longer involves + #207 Lemma CU.5. (CU.5 still appears in #218's dependency list, but only nominally: #218's Step F1 re-proves the + nondegeneracy of the free jets on `(0, r_0^*]`.) +- Controls: X1 is the new ledger. X8 (Lemma S′'s linear algebra) and X9 (Lemma H's exact form (H.1) on exactly pinned + polynomial fields) are new, with mutants M6–M8. +- The nonauthor reviews of v1 on #220 (OpenAI / Codex, delegated; Slices A, B and C, all PASS_TECHNICAL at their stated + scope) requested two amendments: + - **OA-220-B-01**, applied: Lemma G (b) now assumes `E[H(E)] < ∞`, and Step E6 records why it holds there. + - **OA-220-C-01**, superseded: it repaired v1 Remark 2's shrinking cut-off `r₁ = ℓ^{1/(3(p+β))}`, which could fall + below the cusp band. v1.1 has no shrinking cut-off: the near/far cut is the fixed `r_0^*`, and Remark 2 is replaced. +- #191 and #198 have been merged with the blobs consumed here, so they are now listed as merged inputs. #207's head moved + to `782211f`, a merge of `main`; its PROOF blob `f6df5a73` is unchanged. + +**Status update of 1 October 2026, 15:30 UTC (v1.1; no mathematical change).** Made after the nonauthor successor +Slice C review (OpenAI / Codex, delegated; review 5380878588, PASS_TECHNICAL for Lemmas H and S′ and the §§3–4 +assembly), which released its scope and invited this update. It needs a bounded delta check. +- Math- #187 was merged on 1 October 2026 at 13:34 UTC (merge commit `c2f1270`), with the blob `07260114` that v1.1 + pins. It is now listed with the merged inputs, and the statements that used it are worded accordingly: (E3.3) and + Corollary E3′(3) use #187's Theorem F, a merged input, at the single separation `r_0^*`. Nothing else changes. +- Lemma S′'s barrier step now states its range and sign explicitly: `r ≤ r_0^* ≤ r_0^{[R]} ≤ 1` (#191 line 27, [R] + line 55) and `−H̃ > 0`. This answers xAI's question in review 5379839929 (reply 5932919884). +- Control X8 adds a negative witness: at `r = 2` the inequality `λ_min(−H_M) ≥ r²λ_min(−H̃)` fails (xAI's example), so + the range `r ≤ 1` is necessary. + +**v1.1 review record.** Before submission of v1.1, a clean-context same-family referee read the v1 → v1.1 delta +against all eight sources at their declared blobs (`REFEREE_2.md` in the project archive). Its verdict was ACCEPT WITH +MINOR FIXES, with no major finding. +- *What it verified independently.* + - (H.1), symbolically by Peano kernels (sympy), and on non-polynomial test functions. + - Lemma H's covariance, numerically. The direct form of `H̃` and the segment form (H.1) agree to `7·10⁻¹¹` for the + Gaussian kernel (two representations sharing one covariance code), and they reproduce the author's 60-digit + `mpmath` exploration, which uses the raw pins. The segment form was also evaluated on small tori (`L = 2, 3, 6` in + `d = 2`, `L = 3` in `d = 3`) in several frames. + - The `ε²` mechanism of Lemma S′, by Monte Carlo under the exact pinned law of `H̃`. + - The §4 ledger and every comparison claim, in exact rationals. + - All controls and mutants. +- *Fixes applied.* + - **MINOR-1.** (F1) is stated for every `r ≤ r_0^*`, as the own-jet form of #198 (3.1), with the reason. + - **Nits.** The pin rows `U_r` and the target `v_r` are cited from [P] (3.1)–(3.3). The continuity and invertibility + arguments of Lemma H (a) are made explicit. The rescaling matrix is renamed `Λ_r`, to avoid a clash with [R] §4's + `D_r`. `n′` is defined in Lemma S′, and Lemma H (b) cites the argument of #218 (1.2), not its statement. The + identification of #187's far density with #198's (2.1), the content of the first equivalence, and Remark 1's + attribution are all corrected or stated. X8 now asserts the attained case. The exploration paragraph records the + small-torus constants. + +**v1 review record.** Before submission of v1, a clean-context same-family referee read the whole note against its +sources (`REFEREE_1.md` in the project archive). Its verdict was ACCEPT WITH MINOR FIXES, with no major finding. Its +four minor findings and nine nits were applied: +- the radius `r_Q` is defined, and Step E2 states the conditions on `r` alone; +- (F3) and (F5) are derived from #218 Step F1 instead of being attributed; +- Remark 3 now describes #216's Monte Carlo correctly: its elder-pair row estimates `ν_eld` itself; +- the title no longer states the conditional (E3.3) as proved; +- the nits: the derivation of `λ₂`, notation, dependency citations and Remarks 2, 4 and 6. + +The referee also tested Lemma Q's decision by a two-dimensional union–find maximin on 48 exactly pinned fields, all three +cases, margins down to `0.02`: 48 of 48 agree (floating point; exploration). + +Disposition: AUTHOR-SIDE PROOF CANDIDATE; NONAUTHOR REVIEW REQUIRED. Scientific effect: NONE — no register, graph, +STATUS, PROOF_INDEX, prize or Boolean change; no numerical constant is certified. Same GitHub account as every lane; +zero organizational independence. + +**Dependencies (consumed, now merged).** Math- #191 and #198 were merged into `main` on 1 October 2026 (merge commits +`9556547` and `124c37d`), with the same blobs that v1 consumed. Math- #187 was merged on 1 October 2026 (merge commit +`c2f1270`), with the blob that v1.1 consumes. They are now merged inputs: +- Math- #191 (`frontiers/remainder_vanishing_20260930/PROOF.md`, blob `441152df`): Lemma E Steps 1–4, §2 (2.1), the + admissible radius `r_0^*`. +- Math- #198 (`frontiers/remainder_rate_20260930/PROOF.md`, blob `abfb98ae`): (3.1) and the sign window of §3, Lemma + B's barrier (1.2) and §1's elder-density identity, Lemma W's (W.1), the far integral (2.1), Lemma F′. +- For (E3.3) and Corollary E3′(3) only: Math- #187 (`frontiers/far_elder_rate_20260930/PROOF.md`, blob `07260114`), + Theorem F at the single separation `ρ = r_0^*`. (v1.1 rebound it on 1 October from blob `37dcf6ef`, after #187's + status-only repair; Theorem F and its proof are unchanged.) + +**Dependencies (unmerged, consumed).** This note cannot be integrated before the following, and must be rebound if any +of them changes: +- Math- #207 (`frontiers/cusp_second_order_20261001/PROOF.md`, v1.1 blob `f6df5a73`): §0 (the cusp objects), the proof + of Theorem CU.1, Theorem CU.2, the structure of Proposition CU.3 (re-proved here with explicit margins), §6 ((6.1), + (CU.2)). +- Math- #218 (`frontiers/candidate_third_order_20261001/PROOF.md`, blob `70ca57ef`): Lemma D (also applied here to the + rescaled Hessian of Lemma H), (1.2) and its proof, Lemma F (Steps F1, F3, (F.2)), Lemma C (Steps C1, C2 and C3), + Lemma O, Theorem T and §4 (the fold region and the exponent ledger). + +**Merged inputs:** [R], [P] with [E1]/[E2]/[REC] ([P] §2's linear independence of derivative functionals also enters +Lemma H directly), [C7-K] ((K2) and §4), and [Z] (Z13)–(Z14) with [P] §10 (the change of variables behind the +near/far identity); [182] and further parts of [Z] enter through #198 and #191. + +## 0. Statement + +Setting and notation are those of #218 §0, which are those of [R], #191, #198 and #207: +- fixed `d ≥ 2`, `m = d − 1`, `L > 0`, the [P] field on `X = R^d/(LZ^d)`; +- near pins `M = −ru/2`, `S = ru/2` at heights `b`, `b − kr³`, the pinned law `Q = Q_{r,b,k}`, the pin density + `π_r(v_r)`, `P = 1 + |b| + k`, the scaled endpoint Hessians `K_M`, `K_S`, and `W_r/r² = F_d(K_M)F_{d−1}(K_S)`; +- the elder mark `e = 1{d_f(M) = f(S)}`, with `d_f(M) = sup{min_t f(γ(t)) : γ(0) = M, f(γ(1)) > f(M)}` ([P] §8; Borel by + [E2] §9); +- the kernels `A_r = 12π_r(v_r)E_Q[W_r/r²]`, `A_r^{eld} = 12π_r(v_r)E_Q[(W_r/r²)e]` and `A_0 = 12π_0(v_0)z_0`. + +For every `r_0 ∈ (0, r_0^*]`, the canonical marked Kac–Rice version of the elder density is + + ν_eld(ℓ) = ∫_0^{r_0}∫_R∫_{S^{d−1}} r^{−2}A_r^{eld}(b, ℓ/r³, u) dσ db dr + ν_eld^{far,r_0}(ℓ). + +This combines #198 §1's identity on separations `[ρ, r_0)` (the identity behind (B.2)), the far integral #198 (2.1), +and the change of variables of [P] §10 ([Z] (Z13)–(Z14)); #207 §0 states it at `r_0 = r_0^*`. Also +`cℓ^{−1/3} = ∫_0^∞∫∫ r^{−2}A_0(b, ℓ/r³, u)`. The candidate and rejected densities are `ν_cand` and +`ρ_rej = ν_cand − ν_eld` (#198 §0). + +**Cusp objects (#207 §§0, 4, 6).** Jets at `0` under the contact law at the zero-gap target `v_0(b, 0)`: `f₄`, `γ`, +`A`, `Δ = det A` and `Y = (f₄/12)Δ − γᵀadj(A)γ/4`; `E_0[· | b]` is the expectation under that law. For `κ > 0`, + + w_κ^{eld}(A, Y) := (36κ²(det A)² − Y²) 1{A < 0, |Y| < 2κ|det A|}, + loss_κ(A, Y) := 36κ²(det A)²1{A < 0} − w_κ^{eld}(A, Y) = [Y²1{|Y| < 2κ|Δ|} + 36κ²Δ²1{|Y| ≥ 2κ|Δ|}] 1{A < 0}, (0.1) + +`𝒜^{eld}(b, κ, u) = 12π_0(u; v_0(b, 0))E_0[w_κ^{eld} | b]` and `𝒜^{con}(b, κ, u) = 12π_0(u; v_0(b, 0))E_0[36κ²Δ²1{A < 0} | b]`, +so that `𝒜^{eld} − 𝒜^{con} = −12π_0E_0[loss_κ | b] ≤ 0`. The second-order coefficient is + + c₁ = ∫_{S^{d−1}}∫_R∫_0^∞ (𝒜^{eld} − 𝒜^{con})(b, s^{−4}, u) ds db dσ(u) < 0 (0.2) + +(#207 §6: the `s`-integral is (6.1), and (0.2) is (CU.2)). The third-order coefficient `c₂` is #218 (0.1), the +Hadamard finite part of `(1/3)∫∫∫A₂k^{−4/3}`, where `A₂(b, k, u)` is the fold coefficient of #218 Lemma F, with +`A₂(b, 0, u) = −12π_0E_0[Y²1{A < 0} | b]` ((F.2) there). `𝒜^{cand}` is #218 §0's candidate cusp kernel (weight +`(36κ²Δ² − Y²)1{A < 0, |Y| < 6κ|Δ|}`), and `I^{cand}` and `B_{d,L}` are as in #218 §0. + +**Theorem E3 (the elder density to third order).** For every `d ≥ 2` and `L > 0`, as `ℓ ↓ 0`, + + ν_eld(ℓ) = c ℓ^{−1/3} + c₁ ℓ^{1/4} + c₂ ℓ^{1/3} + ν_eld^{far,r_0^*}(ℓ) + O(ℓ^{4/11}), 0 ≤ ν_eld^{far,r_0^*}(ℓ) ≤ C ℓ^{1/3}. (E3.0) + +Consequently + + ν_eld(ℓ) = c ℓ^{−1/3} + c₁ ℓ^{1/4} + O(ℓ^{1/3}); (E3.1) + ν_eld(ℓ) ≥ c ℓ^{−1/3} + c₁ ℓ^{1/4} + c₂ ℓ^{1/3} − C ℓ^{4/11}; (E3.2) + +and, by Math- #187's Theorem F (merged) at the separation `ρ = r_0^*` (`ν_eld^{far,r_0^*}(ℓ) ≤ Cℓ^{2/3}`), + + ν_eld(ℓ) = c ℓ^{−1/3} + c₁ ℓ^{1/4} + c₂ ℓ^{1/3} + O(ℓ^{4/11}). (E3.3) + +More precisely, (E3.0) reduces the third-order law to the far elder density at the one fixed separation `r_0^*`: +- for `0 < θ ≤ 4/11`, `ν_eld(ℓ) − cℓ^{−1/3} − c₁ℓ^{1/4} − c₂ℓ^{1/3} = O(ℓ^θ)` if and only if `ν_eld^{far,r_0^*}(ℓ) = O(ℓ^θ)` + (for `θ ≤ 1/3` both sides hold by (E3.1) and #198 Lemma F′, so the content is `1/3 < θ ≤ 4/11`); +- the three-term law with remainder `o(ℓ^{1/3})` holds if and only if `ν_eld^{far,r_0^*}(ℓ) = o(ℓ^{1/3})`. + +**Corollary E3′ (the rejected density).** With Theorem T of #218, + + ρ_rej(ℓ) = B_{d,L} + (I^{cand} − c₁) ℓ^{1/4} − ν_eld^{far,r_0^*}(ℓ) + O(ℓ^{4/11}). (E3′.0) + +In particular: +1. `ρ_rej(ℓ) = B_{d,L} + (I^{cand} − c₁)ℓ^{1/4} + O(ℓ^{1/3})` — a rate for #207's (CU′.2); +2. `ρ_rej(ℓ) ≤ B_{d,L} + (I^{cand} − c₁)ℓ^{1/4} + Cℓ^{4/11}`; +3. under #187's Theorem F at `ρ = r_0^*`, `ρ_rej(ℓ) = B_{d,L} + (I^{cand} − c₁)ℓ^{1/4} + O(ℓ^{4/11})`: the `ℓ^{1/3}` + terms of the candidate and elder densities are equal, so the rejected density has none. + +(E3.1) is a rate for #207's (CU.1), which claimed no rate for its `o(ℓ^{1/4})`. (E3.3) identifies the third coefficient +of the elder law with the `c₂` that Math- #216 defines and computes (`0.22152441` in `d = 2`, `0.16123405` in `d = 3` +for the Gaussian kernel; numerical approximations, not certified), with the rate `ℓ^{4/11}` of #218's Theorem T. + +**How it works.** The decomposition is that of Theorem T (#218 §4), with the elder kernel in place of the candidate +kernel. +- *Fold scale `r ≍ ℓ^{1/3}`.* The elder deficit `A_r − A_r^{eld}` is at most `Cr³/k` ([C7-K] (K2)), which contributes + `O(ρ_f⁵/ℓ)`, the same order as the boundary layer of #218 Lemma F. So the fold region gives `c₂ℓ^{1/3}` exactly as + for the candidate density. +- *Cusp scale `r ≍ ℓ^{1/4}`.* Lemma CE gives the elder cusp kernel with the candidate rate, `O(r(1 + κ)²)`. Its new + input is Lemma Q, a quantitative form of #207's Proposition CU.3: the elder decision is correct as soon as the rescaled + ridge is within `(3/2)κ||φ| − 1/3|` of the model ridge in `C⁰` and within `κ/4` in `C²`. Both distances are + `O(𝒩r(1 + |γ|/λ)²)`, where `λ` is the transverse concavity and `𝒩` bounds the `C⁵` norm. A wrong decision therefore needs `φ` in a window of width + `O(𝒩r(1 + |γ|/λ)²/κ)` or a small `λ`, and the weight `36κ²Δ²` pays for both: `Δ² ≤ λ²‖A‖^{2m−2}` cancels the `1/λ²`. +- *Overlap.* Lemma O′: `𝒜^{cand} − 𝒜^{eld} = O(1/κ)`, so the elder cusp loss tends to `A₂(b, 0)` at rate `1/κ`, as the + candidate loss does (#218 Lemma O). The overlap cancellation of #218 §4 goes through unchanged. +- *Intermediate separations `ρ_c ≤ r ≤ r_0^*`.* Split at `ℓ^{2/15}`. + - Below the split, #198's unmarked bound (W.1) suffices. + - Above it, Lemma S′ applies. #198's barrier puts an eigenvalue of `−H_M` below `(ℓK²/c_L)^{1/3}`. The pins make the + axial curvature `∂_u²f(M)` of order `r²`, so the right object is the rescaled Hessian `H̃ = Λ_r^{−1}H_MΛ_r^{−1}`, and + the barrier puts `λ_min(−H̃)` below `Cℓ^{1/3}r^{−2}`. + - Lemma H shows that `H̃` is a uniformly nondegenerate Gaussian under the pins. So #218's Lemma D charges that event + twice: once in `|det H̃|` and once in probability. The result is `E_Q[(W_r/r²)e] ≤ Cℓ^{2/3}r^{−2}(κ + r)P^N`. + - Both halves integrate to `O(ℓ^{2/5})`. +- *Far separations `r ≥ r_0^*`.* `ν_eld^{far,r_0^*}` stays as it is in (E3.0). + - #198 Lemma F′ bounds it by `Cℓ^{1/3}`, which gives (E3.1). + - #187 bounds it by `C(r_0^*)ℓ^{2/3}`, which gives (E3.3) with the rate `ℓ^{4/11}`. + + Only the one fixed separation `r_0^*` is involved, so no limit in a cut-off and no dependence of #187's constant on + `ρ` are needed. + +**What is not claimed.** +- (E3.3) and Corollary E3′(3) use #187 (merged on 1 October 2026 as an author-side packet) at the single separation + `r_0^*`. (E3.0)–(E3.2), (E3′.0) and Corollary E3′(1)–(2) do not use it. +- No sharpness of the exponent `4/11`. It is the least exponent of #218's ledger, attained by `ρ_f⁵/ℓ` and `ℓ²ρ_f^{−6}`. + The intermediate separations contribute only `O(ℓ^{2/5})`. +- No certified numerical value of `c`, `c₁`, `c₂`, `I^{cand}` or `B_{d,L}`. +- No uniformity in `d` or `L`; no finite-radius band; no statement about the adjacent-pair density, which #216 also + measures. +- Nothing beyond the existential scope of [R], [Z], [C7-K], #191, #198, #207, #218 and (for (E3.3)) #187. + +## 1. The elder decision, quantitatively + +This section is deterministic. Fix `f ∈ C⁵(X)` and `𝒩 ≥ max(1, ‖f‖_{C⁵})`, where `‖f‖_{C^q}` is the supremum over `X` +of the operator norms of the derivatives of order `≤ q`. Let `0 < r ≤ r_Q := min{1/10, r_L}`, where `r_L` is the +positive root of `6r + 10r² = L/8`; let `κ > 0`, and let `M = −ru/2`, `S = ru/2` be +critical points with `f(M) = b`, `f(S) = b − κr⁴`. In the frame `(u, Θ)` put `Φ(X, Ξ) := rXu + r²ΘΞ`, +`𝔉 := r^{−4}(f∘Φ − b)`, and let `(f₄, γ, A)` be the jets of `f` at `0` and `𝔓` the cusp polynomial (#207 (0.2)) built +from them: + + 𝔓(X, Ξ) = 2κ(X + ½)²(X − 1) + (f₄/24)(X² − ¼)² + ½(X² − ¼)γ·Ξ + ½ΞᵀAΞ. + +When `A < 0`, `Ξ*(X) := −½(X² − ¼)A^{−1}γ` and `g(X) := 𝔓(X, Ξ*(X)) = κ[2(X + ½)²(X − 1) + 3φ(X² − ¼)²]` with +`φ := (f₄ − 3γᵀA^{−1}γ)/(72κ)` (#207 Theorem CU.2 (a)). + +**Lemma CU.1′ (weighted Taylor bounds).** There is `C₁ = C₁(d)` such that on `{|X| ≤ 3, r|Ξ| ≤ 1}` + + |𝔉 − 𝔓|, |∂_X(𝔉 − 𝔓)| ≤ C₁𝒩r(1 + |Ξ|)², |∂_Ξ(𝔉 − 𝔓)|, |∂_X²(𝔉 − 𝔓)|, |∂_X∂_Ξ(𝔉 − 𝔓)| ≤ C₁𝒩r(1 + |Ξ|), ‖∂_Ξ²(𝔉 − 𝔓)‖ ≤ C₁𝒩r. (1.1) + +*Proof.* Follow the proof of #207 Theorem CU.1, keeping track of `Ξ`. There are three sources of `𝔉 − 𝔓`. +- *Pin corrections.* The pinned jets differ from the values that produce `𝔓` by `O(𝒩r⁵)` (`ϑ₀ − b`), `O(𝒩r⁴)` (`ϑ₁`), + `O(𝒩r³)` (`ϑ₂`), `O(𝒩r²)` (`ϑ₃`), `O(𝒩r⁴)` (`ψ₀`) and `O(𝒩r²)` (`ψ₁`); the constants do not depend on `κ`, which enters + only through the exact pins. After rescaling they contribute `O(𝒩r)(1 + |X|³) + O(𝒩r)|X||Ξ| + O(𝒩r²)|Ξ|`, and their + derivatives obey (1.1). +- *Dropped monomials.* These are the Taylor monomials `x^iy^j` with weighted degree `i + 2|j| ≥ 5` and total degree + `i + |j| ≤ 4`: `(i, |j|) ∈ {(3,1), (1,2), (2,2), (0,3), (1,3), (0,4)}`, with coefficients bounded by `C𝒩`. Each becomes + `r^aX^iΞ^j` with `a = i + 2|j| − 4 ≥ 1`. On `r|Ξ| ≤ 1` (and `r ≤ 1`), `r^a|Ξ|^s ≤ r|Ξ|^{s−a+1}` for `s ≥ a − 1`, and `≤ r` otherwise. + Here `|j| − a + 1 = 5 − i − |j| ≤ 2`. A derivative in `Ξ` lowers `s` by one. Two derivatives in `X` need `i ≥ 2`, + and then `5 − i − |j| ≤ 1`. One derivative in `X` keeps the bound `(1 + |Ξ|)²`, through `∂_X(rXΞ²) = rΞ²`. +- *Remainder.* `|∂^αρ₅(x, y)| ≤ C𝒩(|x| + |y|)^{5−|α|}` for `|α| ≤ 2`. At `(rX, r²Ξ)` with `|X| ≤ 3` and `r|Ξ| ≤ 1`, + `|x| + |y| ≤ 4r`. So `|∂_X^p∂_Ξ^q[r^{−4}ρ₅(rX, r²Ξ)]| = r^{p+2q−4}|∂_x^p∂_y^qρ₅| ≤ C𝒩4⁵r^{1+q}`. ∎ (The `∂_X` bound in (1.1) is not used +below.) + +Checker X5 verifies the mechanism exactly on pinned polynomial fields in `d = 2, 3`: every monomial `r^aX^iΞ^j` of +`𝔉 − 𝔓` has `a ≥ 1` and `|j| ≤ a + 1`. + +**Lemma S (Schur complements).** Let `D, D′ ∈ Sym(m)` with `D ≤ −λI` and `D′ ≤ −(λ/2)I`, and let `a, a′ ∈ R` and +`b, b′ ∈ R^m`. Put `s := a − bᵀD^{−1}b` and `s′ := a′ − b′ᵀD′^{−1}b′`. Then + + |s′ − s| ≤ |a′ − a| + (2/λ)|b′ − b|(|b| + |b′|) + (2/λ²)|b|²‖D′ − D‖. (1.2) + +*Proof.* `b′ᵀD′^{−1}b′ − bᵀD^{−1}b = (b′ − b)ᵀD′^{−1}(b′ + b) + bᵀD′^{−1}(D − D′)D^{−1}b`, with `‖D′^{−1}‖ ≤ 2/λ` and +`‖D^{−1}‖ ≤ 1/λ`. ∎ + +**Lemma Q (the elder decision with explicit margins).** Suppose `A ≤ −λI` with `λ > 0`, and put + + Γ := |γ|/λ, ε* := 80C₁𝒩r(1 + Γ)², R := 5(1 + Γ) + 3((κ + 1)/λ)^{1/2}. + +Assume +- (Q1) `𝒩(3r + r²R) ≤ λ/2` and `6r + 2r²R ≤ L/4`; +- (Q2) `5r(1 + Γ) ≤ 1` and `8C₁𝒩r(1 + 5Γ) ≤ λ`; +- (Q3) `ε* ≤ κ/4`; +- (Q4) `|φ| ≤ 1` and `||φ| − 1/3| > 2ε*/(3κ)`. + +Then + + e(f) = 1{d_f(M) = f(S)} = 1{|φ| < 1/3}. (1.3) + +*Proof.* Put `M₁ := (35/8)Γ`, so that `|Ξ*(X)| ≤ ½·(35/4)|A^{−1}γ| ≤ M₁` for `X ∈ [−3, 2]`. + +*Step Q1 (the window).* Let `𝒲 := [−3, 2] × {|Ξ| ≤ R}`. +- `Φ` is linear and injective. `Φ(𝒲)` has diameter at most `5r + 2r²R < L/4` by (Q1), so `Φ` embeds a neighbourhood of + `𝒲` in the torus. In particular it maps the interior and boundary of every subregion of `𝒲` onto the interior and + boundary of its image. +- On `𝒲`, `∂_Ξ²𝔉(X, Ξ) = D_Θ²f(Φ(X, Ξ)) ≤ A + ‖D³f‖(3r + r²R)I ≤ −(λ/2)I` by (Q1), as `‖D³f‖ ≤ 𝒩`. + +*Step Q2 (the ridge and its distance from the model's).* Fix `X ∈ [−3, 2]`. The ball `{|Ξ − Ξ*(X)| ≤ 1}` lies in +`{|Ξ| ≤ 5(1 + Γ)}`, where `r|Ξ| ≤ 1` by (Q2); and it lies in `𝒲`. +- *The maximizer.* Since `∂_Ξ𝔓(X, Ξ*) = 0`, (1.1) gives `|∂_Ξ𝔉(X, Ξ*)| ≤ C₁𝒩r(1 + M₁) ≤ λ/8` by (Q2). So on the sphere + `|Ξ − Ξ*| = 1`, `𝔉(X, Ξ) ≤ 𝔉(X, Ξ*) + λ/8 − λ/4 < 𝔉(X, Ξ*)`. Hence the unique maximizer `Ξ_𝔉(X)` of the strictly + concave `𝔉(X, ·)` over `{|Ξ| ≤ R}` lies in the open unit ball around `Ξ*`. There `∂_Ξ𝔉 = 0`, and strong concavity gives + `|Ξ_𝔉 − Ξ*| ≤ (2/λ)|∂_Ξ(𝔉 − 𝔓)(X, Ξ*)| ≤ 1/4`. +- *The ridge function.* `g_𝔉(X) := 𝔉(X, Ξ_𝔉(X))` is `C²` by the implicit function theorem. Its second derivative is the + Schur complement of `∂_Ξ²𝔉` in `Hess 𝔉` at `(X, Ξ_𝔉)`. The same holds for `g` with `(𝔓, Ξ*)` (#207 Proposition CU.3, + Step 1). +- *`C⁰` distance.* `g − |𝔉 − 𝔓|(X, Ξ*) ≤ 𝔉(X, Ξ*) ≤ g_𝔉(X) ≤ 𝔓(X, Ξ_𝔉) + |𝔉 − 𝔓|(X, Ξ_𝔉) ≤ g + |𝔉 − 𝔓|(X, Ξ_𝔉)`. + Hence `ε₀ := sup_{[−3,2]}|g_𝔉 − g| ≤ C₁𝒩r(5/4 + M₁)² ≤ ε*`. +- *`C²` distance.* Apply (1.2) with `(a, b, D) = (∂_X²𝔓, Xγ, A)` at `(X, Ξ*)` and `(a′, b′, D′)` the blocks of `Hess 𝔉` + at `(X, Ξ_𝔉)`. + - `∂_X²𝔓` depends on `Ξ` only through `γ·Ξ`, so `|a′ − a| ≤ C₁𝒩r(5/4 + M₁) + |γ||Ξ_𝔉 − Ξ*| ≤ C₁𝒩r[(5/4 + M₁) + 2Γ(1 + M₁)]`. + - `|b′ − b| ≤ C₁𝒩r(5/4 + M₁) ≤ 5λ/32` by (Q2), `‖D′ − D‖ ≤ C₁𝒩r`, and `|b| ≤ 3|γ|`. + - So `ε₂ := sup_{[−3,2]}|g_𝔉″ − g″| ≤ C₁𝒩r[(5/4 + M₁)(21/16 + 12Γ) + 2Γ(1 + M₁) + 18Γ²] + = C₁𝒩r[105/64 + (2911/128)Γ + (317/4)Γ²] ≤ ε*`. + + (Checker X6 verifies (1.2) and both polynomial bounds exactly.) + +*Step Q3 (reduction to the ridge).* This is #207 Proposition CU.3, Steps 2–3, with `𝒲` as above. +- For every `t`, each nonempty `X`-fiber of `𝒲 ∩ {𝔉 > t}` is convex and contains `Ξ_𝔉(X)`, and it is nonempty iff + `g_𝔉(X) > t`. So the path components of `𝒲 ∩ {𝔉 > t}` are the parts over the components of + `{X ∈ [−3, 2] : g_𝔉(X) > t}`, and the supremum of `𝔉` over such a part is the supremum of `g_𝔉` over that interval. +- On `|Ξ| = R`, `|Ξ − Ξ_𝔉(X)| ≥ R − M₁ − 1/4 ≥ 3((κ + 1)/λ)^{1/2}`, so by strong concavity + `𝔉(X, Ξ) ≤ g_𝔉(X) − (9/4)(κ + 1)`. (1.4) + +*Step Q4 (exact values at the pins).* `M = Φ(−½, 0)` and `S = Φ(½, 0)` are critical points of `f`. So `(±½, 0)` are +critical points of `𝔉`, `Ξ_𝔉(±½) = 0`, `g_𝔉(−½) = 0`, `g_𝔉(½) = −κ` and `g_𝔉′(±½) = 0`. The same holds for `g`. +Therefore `h := g_𝔉 − g` satisfies `|h| ≤ ε₀` and `|h(X)| ≤ (ε₂/2)(X ∓ ½)²` on `[−3, 2]`. + +*Step Q5 (the margins of the model ridge).* With `X₃ := −1/(2φ)`, from #207 (2.1) and Theorem CU.2 (d): +- (M1) `g + κ = κ(X − ½)²[2(X + 1) + 3φ(X + ½)²]` and `g = κ(X + ½)²[2(X − 1) + 3φ(X − ½)²]`; +- (M2) `g + κ ≥ κ(X − ½)²` on `[−½, X_R]` when `|φ| < 1/3`, where `X_R := 2` for `φ ≥ −1/4` and `X_R := X₃ = 1/(2|φ|) ∈ (3/2, 2)` + for `−1/3 < φ < −1/4`. For `φ ≥ 0` the bracket is `≥ 2(X + 1) ≥ 1`; for `φ < 0` it is `1 + (X + ½)(2 − 3|φ|(X + ½)) ≥ 1` + as long as `X + ½ ≤ 2/(3|φ|)`, which holds up to `X₃ = 1/(2|φ|)` when `|φ| ≤ 1/3`; +- (M3) `g ≤ −κ(X + ½)²` on `[−3/2, ½]` when `φ ≤ 1/3`. The bracket is `≤ 2(X − 1) + (X − ½)²`, which is convex and equals + `−1` at both ends; +- (M4) `g(X₃) + κ = κ(φ + 1)³(3φ − 1)/(16φ³)` and `g(X₃) = κ(φ − 1)³(3φ + 1)/(16φ³)`. Hence: + - for `1/3 ≤ φ ≤ 1`, `g(X₃) + κ − (3/2)κ(φ − 1/3) = κ(3φ − 1)[(φ + 1)³ − 8φ³]/(16φ³) + = κ(3φ − 1)(1 − φ)(7φ² + 4φ + 1)/(16φ³) ≥ 0`; + - for `−1 ≤ φ ≤ −1/3`, the same identity in `ψ = −φ` gives `−g(X₃) ≥ (3/2)κ(|φ| − 1/3)`; + - for `−1/3 ≤ φ < 0`, with `ψ = −φ`, `g(X₃) = κ(1 + ψ)³(1 − 3ψ)/(16ψ³)` and + `g(X₃) − 12κ(1/3 − ψ) = κ(1 − 3ψ)[(1 + ψ)³ − 64ψ³]/(16ψ³) = κ(1 − 3ψ)²(21ψ² + 6ψ + 1)/(16ψ³) ≥ 0`; +- (M5) `g(2) = κ(25/2 + (675/16)φ)`, `g(−3/2) = κ(−5 + 12φ)` and `g(−3) = κ(−50 + (3675/16)φ)`. So `g(2) ≥ (125/64)κ` for + `φ ≥ −1/4`; `g(2) ≤ −(25/16)κ` and `g(−3/2) ≤ −9κ` for `φ ≤ −1/3`; `g(−3/2) + κ = −12κ(1/3 − φ)`; and + `g(−3) ≥ (425/16)κ` for `φ ≥ 1/3`; +- (M6) `g′ = 6κ(X² − ¼)(1 + 2φX)`. For `1/3 < φ ≤ 1`, `g` decreases on `[−3, X₃]` and increases on `[X₃, −½]`. For + `−1 ≤ φ < −1/3`, `g` increases on `[½, X₃]` and decreases on `[X₃, 2]`. + +(Checkers X2–X3 verify (M1)–(M5) exactly.) + +*Step Q6 (the decision).* By (Q3)–(Q4), `ε₂ ≤ ε* ≤ κ/4` and `ε₀ ≤ ε* < (3/2)κ||φ| − 1/3|`. +- *Case E, `|φ| < 1/3`.* + - *Path.* On `[−½, X_R]`, (M2) and Step Q4 give `g_𝔉 + κ ≥ (κ − ε₂/2)(X − ½)² ≥ 0`. At `X_R`, `g_𝔉(X_R) > 0`: for + `φ ≥ −1/4`, `g(2) ≥ (125/64)κ > κ/4 ≥ ε₀`; otherwise `g(X₃) ≥ 12κ(1/3 − |φ|) > ε₀` by (M4). So the ridge curve + `X ↦ Φ(X, Ξ_𝔉(X))`, `X ∈ [−½, X_R]`, runs from `M` through `S` to a point above `b`, and along it `f ≥ f(S)`. Hence + `d_f(M) ≥ f(S)`. + - *Trap.* Let `𝒟 := (−3/2, ½) × {|Ξ| < R}` and `𝒟_phys := Φ(𝒟)`. + - At `X = −3/2`: `𝔉 ≤ g_𝔉(−3/2) ≤ −κ − 12κ(1/3 − φ) + ε₀ < −κ`, since `ε₀ < 12κ(1/3 − φ)` (for `φ ≤ 0` the margin is + `≥ 4κ`). + - At `X = ½`: `𝔉 ≤ g_𝔉(½) = −κ`, with equality only at `Ξ = 0`, i.e. at `S`. + - On `[−3/2, ½]`, (M3) and Step Q4 give `g_𝔉 ≤ −(κ − ε₂/2)(X + ½)² ≤ 0`. So at `|Ξ| = R`, (1.4) gives + `𝔉 ≤ −(9/4)(κ + 1) < −κ`. + + So `f ≤ f(S)` on `∂𝒟_phys`. The path component `C` of `{f > f(S)}` containing `M` does not meet `∂𝒟_phys`, hence + `C ⊂ 𝒟_phys`. By Step Q3 its supremum is `b + r⁴ sup g_𝔉` over an interval in `(−3/2, ½)`, which is `≤ b`. So every + path from `M` to a point above `b` leaves `C`, and `d_f(M) ≤ f(S)`. Thus `e = 1`. +- *Case R⁺, `1/3 < φ ≤ 1`.* By (M6) and (M4), `min_{[−3,−½]} g = g(X₃) ≥ −κ + (3/2)κ(φ − 1/3)`, so + `min_{[−3,−½]} g_𝔉 > −κ`. Also `g_𝔉(−3) ≥ (425/16)κ − κ/4 > 0` by (M5). So the ridge curve from `M` to `X = −3` ends + above `b` and stays above `f(S)`: `d_f(M) > f(S)` and `e = 0`. +- *Case R⁻, `−1 ≤ φ < −1/3`.* Put `t* := −(5/4)κ` and `𝒟′ := (−3/2, 2) × {|Ξ| < R}`. + - `g_𝔉 ≤ 0` on `[−3/2, 2]`. On `[−3/2, ½]` this is (M3) with Step Q4. On `[½, 2]`, (M6) and (M4) give + `g ≤ g(X₃) ≤ −(3/2)κ(|φ| − 1/3) < −ε₀`. + - On `∂𝒟′`: `g_𝔉(−3/2) ≤ −9κ + κ/4 < t*` and `g_𝔉(2) ≤ −(25/16)κ + κ/4 < t*` by (M5); at `|Ξ| = R`, (1.4) gives + `𝔉 ≤ −(9/4)(κ + 1) < t*`. + + So the component `C′` of `{f > b + r⁴t*}` containing `M` lies in `Φ(𝒟′)`, and its supremum is at most `b`. Every path + from `M` to a point above `b` leaves `C′`, so `d_f(M) ≤ b + r⁴t* < f(S)` (or `d_f(M) = −∞`), and `e = 0`. ∎ + +Only window information is used, as in #207: every conclusion is an explicit path inside `Φ(𝒲)` or a trap whose boundary +lies inside it. No type condition is used either: Lemma Q does not need `M`, `S` to be typed. + +## 2. The elder cusp kernel with a rate + +**Notation for this section.** Let `0 < r ≤ r₂`, `κ > 0` and `k = κr ≤ 1`, and let `f = F_r` under `Q`. +- `𝒩_r := 1 + k + ‖F_r‖_{C⁹}`. +- `J′` is the vector of free jets of `f` at `0` of order `≤ 9` (#218 Step F1); `J″ := J′ ∖ {f₄}` and + `J‴ := J″ ∖ {A}`, where `A := D_Θ²f(0)`. +- `Δ := det A`, `λ := λ_min(−A)` on `{A < 0}`, `γ := ∇_Θ∂_u²f(0)` and `B := ∂_uD_Θ²f(0)`. All of these lie in `J′`. +- `Y_r := (f₄/12)Δ + 3k tr(adj(A)B) − γᵀadj(A)γ/4`. This is #191's `Y`, built from `F_r`'s own jets. +- `Y′ := Y_r − 3k tr(adj(A)B)` and `φ_r := (f₄ − 3γᵀA^{−1}γ)/(72κ)`, so that `Y′ = 6κΔφ_r`. +- `w_κ(A, Y) := (36κ²(det A)² − Y²)₊1{A < 0}`. + +**Facts used.** +- (F1) `det K_M = −6kΔ + rY_r + R_M` and `det K_S = 6kΔ + rY_r + R_S`, with `|R_i| ≤ Cr²(1 + k)𝒩_r^{N₁}`. This is the + own-jet form of #198 (3.1): `F_r`'s own transverse Hessian `A` replaces `A_0`, and `𝒩_r` replaces #191's `T`. It holds + pathwise for every `0 < r ≤ r_0^*` and `k > 0`, not only in this section's range. Indeed, #191 Steps 1–3 are pathwise + Taylor expansions of the pinned function `F_r` about its own jets at `0`, with remainders polynomial in `‖F_r‖_{C⁷}` and + `k` for every `r ≤ 1`; the coupling enters only once, through `‖A − A_0‖ ≤ r²T` in Step 2, and that step disappears + when `A` is used (#218 Step F1 records this). Also `r_0^* ≤ r_0^{[R]} ≤ 1` ([R] §2). +- (F2) `|r^{−2}F_d(K_M)F_{d−1}(K_S) − w_κ(A, Y_r)| ≤ Cr(1 + κ)𝒩_r^N`. This is #218 (C.2) with `(A, 𝒩_r)` in place of + `(A_0, T)`. Its case analysis (Step C1) uses only (F1) and `‖A_i − A‖ ≤ (r/2)‖F_r‖_{C³} ≤ r𝒩_r`. +- (F3) Given `J″`, `f₄` is Gaussian under `Q`, with variance in `[c, C]` and mean `μ`, `|μ| ≤ C(P + |J″|)`. Indeed, + under `Q` the vector `J′` is Gaussian; `Cov_Q(J′)` is uniformly invertible on `(0, r_0^*]` (#218 Step F1); and + `E_QJ′ = Cov(J′, U_r)Σ_r^{−1}v_r`, so `|E_QJ′| ≤ C|v_r| ≤ CP` by [R] (R2)–(R3). `Var_Q(f₄ | J″)` is a Schur complement + in `Cov_Q(J′)`, hence at least `λ_min(Cov_Q J′) ≥ c` and at most `Var_Q(f₄) ≤ C`. The conditional mean is + `E_Qf₄ + Cov_Q(f₄, J″)Cov_Q(J″)^{−1}(J″ − E_QJ″)`, with coefficients bounded by the same uniform invertibility. (#207 + Lemma CU.5 proves the density bound for small `r`, given its own vector of free jets of order `≤ 8`; the argument here + covers all of `(0, r_0^*]`.) So the conditional density is at most a constant `C₀`, and since the Gaussian factor + absorbs polynomial weights, for every `J″`-measurable interval `I` and `p ≥ 0` + + E_Q[(1 + |f₄|)^p 1{f₄ ∈ I} | J″] ≤ C_p (P + |J″|)^p |I|. (2.1) +- (F4) #218 (1.2) with `J₀ = J′`: `E_Q[𝒩_r^p | J′] ≤ C_p(P + |J′|)^p`. +- (F5) Given `J‴`, `A` is Gaussian under `Q`, with covariance between `cI` and `CI` (a Schur complement in `Cov_Q(J′)`, + as in (F3)) and mean `μ_A`, `|μ_A| ≤ C(P + |J‴|)`. So #218 Lemma D applies conditionally: + + E_Q[(1 + ‖A‖)^n 1{|λ_max(A)| < ε} | J‴] ≤ C (P + |J‴|)^{n′} ε, n′ = n + m(m − 1)/2. (2.2) +- (F6) #218 Step F3: under `Q`, `J′ ~ N(μ_r, Γ_r)`, and under the contact law at `v_0(b, k)`, `J′ ~ N(μ_0, Γ_0)`, with + `|μ_r − μ_0| ≤ Cr²P`, `‖Γ_r − Γ_0‖ ≤ Cr²` and `Γ_r, Γ_0 ≥ cI`. +- (F7) The parity factorization ([P] §15; #218 Step C3). Under the contact law at `v_0(b, k)`, the even free jets + (among them `A` and `f₄`) are independent of the odd ones (among them `γ`). The law of the even jets does not depend on + `k`. The odd jets are `N(12kw, Σ_o)`, with `w` and `Σ_o` independent of `k`. Finally + `π_0(v_0(b, k)) = p_e(b, 0, 0)p_o(0, 12k, 0)`, where `p_o` is a centred Gaussian density. + +**Lemma G (two Gaussian comparisons).** Fix `n`, `p` and `0 < c_G ≤ C_G`. +- (a) Let `J ~ N(μ, Γ)` and `J̃ ~ N(μ̃, Γ̃)` on `R^n`, with `c_GI ≤ Γ, Γ̃ ≤ C_GI`, and let `G` be Borel with + `|G(j)| ≤ H(1 + |j|)^p`. Then + `|E G(J̃) − E G(J)| ≤ CH(1 + |μ| + |μ̃|)^{p+2}(|μ̃ − μ| + ‖Γ̃ − Γ‖)`. +- (b) Let `E` and `O` be independent, with `O ~ N(s, Σ)` on `R^{n_o}`, `c_GI ≤ Σ ≤ C_GI` and `|s| ≤ s₀`. Let + `G(e, −o) = G(e, o)` and `|G(e, o)| ≤ H(e)(1 + |o|)^p`, and assume `E[H(E)] < ∞`. Then + `|E G(E, O) − E G(E, O₀)| ≤ C|s|²E[H(E)]`, where `O₀ ~ N(0, Σ)` is independent of `E` and `C` depends also on `s₀`. + (v1.1, after the nonauthor Slice B review's OA-220-B-01: without `E[H(E)] < ∞` both expectations can be infinite, + e.g. `G(e, o) = H(e) = e` with `E` nonintegrable; the integrability is also what justifies differentiating under + the integral below.) + +*Proof.* +- (a) Interpolate `(μ_t, Γ_t)` linearly; then `c_GI ≤ Γ_t ≤ C_GI`. The Gaussian density satisfies + `∂_t log p_t(j) = (j − μ_t)ᵀΓ_t^{−1}δμ + ½(j − μ_t)ᵀΓ_t^{−1}δΓΓ_t^{−1}(j − μ_t) − ½tr(Γ_t^{−1}δΓ)`, so + `|∂_tp_t| ≤ C(|δμ| + ‖δΓ‖)(1 + |j − μ_t|²)p_t`. Integrate `|G||∂_tp_t|` over `j` and `t ∈ [0, 1]`. +- (b) `h(s) := E G(E, O_s)` is smooth, and even in `s`: substitute `o ↦ −o` and use `G(e, −o) = G(e, o)` and the + evenness of the centred density. So `∇h(0) = 0`, and `|h(s) − h(0)| ≤ ½|s|²sup_{|t|≤s₀}‖∇²h(t)‖`. Differentiating the + density twice gives `‖∇²h(t)‖ ≤ CE[H(E)]` for `|t| ≤ s₀`. ∎ + +(b) differentiates the Gaussian density, not `G`: no regularity of `G` is needed, which matters because `loss_κ` jumps at +`|Y| = 2κ|Δ|`. + +**Lemma CE (the elder cusp kernel with a rate).** There are `r₂ > 0` and `C, c, N` such that for `0 < r ≤ r₂`, +`b ∈ R`, `u ∈ S^{d−1}` and `κ > 0` with `κr ≤ 1`, + + |r^{−2}(A_r^{eld} − A_0)(b, κr, u) − (𝒜^{eld} − 𝒜^{con})(b, κ, u)| ≤ C r (1 + κ)² (1 + |b|)^N e^{−cb²}. (CE.1) + +This is #218's (C.1) for the elder kernel, with the same rate. + +*Proof.* Take `r₂ := min(r_0^*, 1/2, r_Q)`. (v1 also required `r₂ ≤` the radius of #207 Lemma CU.5, for Lemma B′; v1.1 +does not use Lemma CU.5.) + +*Step E1 (pathwise comparison).* Put `G(J′) := w_κ(A, Y_r)1{|φ_r| < 1/3}`. Since +`r^{−2}F_dF_{d−1}e − G = (r^{−2}F_dF_{d−1} − w_κ)e + w_κ(e − 1{|φ_r| < 1/3})`, (F2) bounds the first term by +`Cr(1 + κ)𝒩_r^N`. Consider the second term on `{w_κ > 0}`. +- If the pair is not typed, `F_dF_{d−1} = 0`, and (F2) gives `w_κ ≤ Cr(1 + κ)𝒩_r^N`. +- If it is typed and Lemma Q's hypotheses (Q1)–(Q4) hold for `f = F_r` with `𝒩 = 𝒩_r`, then + `e = 1{|φ_r| < 1/3}` by (1.3), and the term vanishes. + +Let `𝔅` be the event that (Q1)–(Q4) fail. Then + + |r^{−2}F_d(K_M)F_{d−1}(K_S)e − G(J′)| ≤ 2Cr(1 + κ)𝒩_r^N + w_κ(A, Y_r)1_𝔅. (2.3) + +*Step E2 (the wrong decisions have small weight).* `E_Q[w_κ(A, Y_r)1_𝔅] ≤ Cr(1 + κ)²P^N`. +- *The bad event.* The conditions of Lemma Q on `r` alone hold because `r ≤ r₂ ≤ r_Q`: `r ≤ 1/10` and + `6r + 10r² ≤ L/8`. The others are monotone in `𝒩` and `λ`. With `R ≤ 5(1 + Γ) + 3((κ + 1)/λ)^{1/2}`, they reduce as + follows (write `𝒩` for `𝒩_r`). + - (Q1), first part: it holds if `3𝒩r`, `5𝒩r²(1 + Γ)` and `3𝒩r²((κ + 1)/λ)^{1/2}` are each `≤ λ/6`; this follows + from `λ ≥ 18𝒩r`, `λ ≥ 60𝒩r²`, `λ² ≥ 60𝒩r²|γ|` and `λ^{3/2} ≥ 18𝒩r²(κ + 1)^{1/2}`. The last follows from + `λ ≥ 18^{2/3}2^{1/3}𝒩r`, as `r(κ + 1) ≤ 2`. + - (Q1), second part: given `6r + 10r² ≤ L/8`, it holds if `10r²|γ|/λ ≤ L/16` and `6r²((κ + 1)/λ)^{1/2} ≤ L/16`, which + follow from `λ ≥ 160r²|γ|/L` and `λ ≥ (96/L)²r⁴(κ + 1)`. + - (Q2): `5r(1 + Γ) ≤ 1` holds if `λ ≥ 10r|γ|`; `8C₁𝒩r(1 + 5Γ) ≤ λ` holds if `λ ≥ 16C₁𝒩r` and `λ² ≥ 80C₁𝒩r|γ|`. + - (Q3): `ε* ≤ κ/4` holds if `κ ≥ 1280C₁𝒩r` and `λ² ≥ 1280C₁𝒩r|γ|²/κ`, by `(1 + Γ)² ≤ 2(1 + Γ²)`. + + Since `κr ≤ 1 ≤ 𝒩` gives `r²|γ| ≤ r|γ| ≤ |γ|(𝒩r/κ)^{1/2}`, and `r⁴(κ + 1) ≤ 2r`, all of these hold whenever + `κ ≥ C₂𝒩_r r` and `λ ≥ λ₂(𝒩_r)`, where `C₂ = C₂(d, L)` and + + λ₂(𝒩) := C₂[𝒩r + (𝒩r|γ|)^{1/2} + |γ|(𝒩r/κ)^{1/2}]. + + So `𝔅 ⊂ 𝔅_λ ∪ 𝔅_κ ∪ 𝔅_4 ∪ 𝔅_5`, with `𝔅_λ := {λ < λ₂(𝒩_r)}`, `𝔅_κ := {κ < C₂𝒩_r r}`, + `𝔅_4 := {||φ_r| − 1/3| ≤ 2ε*/(3κ)}` and `𝔅_5 := {|φ_r| > 1}`. +- *The common reduction.* `w_κ(A, Y_r) ≤ 36κ²Δ²1{A < 0, |Y_r| < 6κ|Δ|}`. `Y_r` is affine in `f₄` with slope `Δ/12` + and `J″`-measurable intercept. So `{|Y_r| < 6κ|Δ|}` is `{f₄ ∈ I_typ}` for a `J″`-measurable interval `I_typ` of length `144κ`. + The thresholds of `𝔅_λ`, `𝔅_κ` and `𝔅_4` depend on `𝒩_r`. On `{𝒩_r ∈ [2^j, 2^{j+1})}`, replace `𝒩_r` by `2^{j+1}`, + bound `1{𝒩_r ≥ 2^j}` by (F4), then integrate `f₄` by (2.1). This gives, for each `j`, a factor + `C_p2^{−jp}(P + |J″|)^p`. The sum over `j` converges for `p` large. +- *`𝔅_λ`.* Integrating `f₄` over `I_typ` gives a factor `min(1, 144C₀κ)`. On `{λ < λ₂}`, `Δ² ≤ λ₂²‖A‖^{2m−2}`, and (2.2), + applied given `J‴` (`λ₂` depends on `|γ|`, which lies in `J‴`), gives a factor `λ₂`. So the contribution is at most + `Cκ²min(1, κ)Σ_j2^{−jp}E[λ₂(2^{j+1})³(P + |J‴|)^{N}]` (`N` a generic exponent). The three terms of `λ₂³` contribute + `κ²min(1, κ)(r³ + r^{3/2} + (r/κ)^{3/2})P^N ≤ Cr(1 + κ)²P^N`, using `κr ≤ 1` and `r ≤ 1`. +- *`𝔅_κ`.* `P(𝒩_r > κ/(C₂r) | J′) ≤ min(1, C_3(r/κ)³(P + |J′|)³)`, so the contribution is at most + `Cκ²min(1, κ)min(1, (r/κ)³)P^N ≤ Cr³P^N`. +- *`𝔅_4`.* This is `f₄` in two `J″`-measurable intervals of total length `192ε*`, with + `ε* = 80C₁𝒩_r r(1 + Γ)²`. With `Δ²(1 + Γ)² ≤ 2Δ² + 2|γ|²‖A‖^{2m−2}` (as `Δ² ≤ λ²‖A‖^{2m−2}`), the contribution is + `≤ Crκ²P^N`. +- *`𝔅_5` (on `{w_κ > 0}`).* `|Y_r| < 6κ|Δ| < |Y′|`, so `6κ|Δ| − |Y_r| < τ := 3k|tr(adj(A)B)|`, and + `w_κ ≤ 12κ|Δ|τ`. Also `|Y′|` lies in `(6κ|Δ|, 6κ|Δ| + τ)`, which puts `f₄` in two intervals of total length + `24τ/|Δ|`. The contribution is `≤ 288C₀κE[τ²(P + |J″|)^p] ≤ Cκ³r²P^N ≤ Cκ²rP^N`. + +*Step E3 (removing the `k`-term).* `G₀(J′) := w_κ^{eld}(A, Y′)` equals `w_κ(A, Y′)1{|φ_r| < 1/3}`, because +`|φ_r| < 1/3 ⟺ |Y′| < 2κ|Δ|`. `w_κ` is Lipschitz in `Y` with constant `12κ|Δ|` (#218 Step C2; checker T3 there). Hence +`|G − G₀| ≤ 12κ|Δ|·3k|tr(adj(A)B)| ≤ Cκ²r‖A‖^{N}|B|`, and `E_Q|G − G₀| ≤ Cκ²rP^N`. + +*Step E4 (from `Q` to the contact law at `v_0(b, k)`).* `|G₀| ≤ 36κ²|J′|^{2m}`. By (F6) and Lemma G (a), +`|E_Q[G₀] − E_{v_0(b,k)}[G₀]| ≤ Cκ²r²P^N`. + +*Step E5 (densities).* By [R] (R5) as used in #218 Step C3, `|π_r(v_r) − π_0(v_0(b, k))| ≤ Cr²P²e^{−c(b²+k²)}`. Also +`E_Q[r^{−2}F_dF_{d−1}e] ≤ C(1 + κ)²P^N` by the sign window. Hence, by Steps E1–E4, + + r^{−2}A_r^{eld}(b, κr, u) = 12π_0(v_0(b, k))E_{v_0(b,k)}[w_κ^{eld}(A, Y)] + O(r(1 + κ)²P^Ne^{−c(b²+k²)}). + +`r^{−2}A_0(b, κr, u) = 12π_0(v_0(b, k))E_{v_0(b,k)}[36κ²Δ²1{A < 0}]` exactly (#218 Step C3). Subtracting, + + r^{−2}(A_r^{eld} − A_0)(b, κr, u) = −12π_0(v_0(b, k))E_{v_0(b,k)}[loss_κ(A, Y)] + O(r(1 + κ)²P^Ne^{−c(b²+k²)}). (2.4) + +*Step E6 (the target `v_0(b, k) → v_0(b, 0)`).* `loss_κ` depends on the even jets `(A, f₄)` and on the odd jet `γ` +only through `γᵀadj(A)γ`, so it is even in the odd jets. Also `0 ≤ loss_κ ≤ 9Y²`: on `{|Y| ≥ 2κ|Δ|}`, +`36κ²Δ² ≤ 9Y²`. So Lemma G (b) applies with `E = (A, f₄)`, `O` the odd jets and +`H(A, f₄) = C(1 + |f₄|)²(1 + ‖A‖)^{2m}` (the odd-jet factor of `Y²` is absorbed in `(1 + |o|)^p`, `p = 4`), and +`E[H] ≤ C(1 + |b|)^N` under the contact law. By (F7) and Lemma G (b) with `s = 12kw` (`|s| ≤ 12|w|`, as `k ≤ 1`), +`|E_{v_0(b,k)}[loss_κ] − E_{v_0(b,0)}[loss_κ]| ≤ Ck²(1 + |b|)^N`, with no growth in `κ`. And +`p_o(0, 12k, 0) = p_o(0, 0, 0)(1 + O(k²))`. So the right side of (2.4) is +`(𝒜^{eld} − 𝒜^{con})(b, κ, u) + O(k²(1 + |b|)^Ne^{−cb²}) + O(r(1 + κ)²P^Ne^{−c(b²+k²)})`. Since `k² = κ²r² ≤ r(1 + κ)²` +and `P^Ne^{−ck²} ≤ C(1 + |b|)^N`, this is (CE.1). ∎ + +(The coupling `(F_r, F_0)` is not used in this proof. Every pathwise statement concerns `F_r` alone, and the passage to +the contact law is Lemma G (a) applied to the free-jet laws.) + +## 3. The overlap and the intermediate separations + +**Lemma O′ (elder overlap).** For `κ ≥ 1`, + + 0 ≤ (𝒜^{cand} − 𝒜^{eld})(b, κ, u) ≤ C κ^{−1} (1 + |b|)^N e^{−cb²}. (O′.1) + +Consequently, with #218 Lemma O, `|(𝒜^{eld} − 𝒜^{con})(b, κ, u) − A₂(b, 0, u)| ≤ Cκ^{−1}(1 + |b|)^Ne^{−cb²}`. + +*Proof.* `𝒜^{cand} − 𝒜^{eld} = 12π_0E_0[(36κ²Δ² − Y²)1{A < 0, 2κ|Δ| ≤ |Y| < 6κ|Δ|} | b]`. On this event +`36κ²Δ² ≤ 9Y²` and `|Δ| ≤ |Y|/(2κ)`. So the difference is at most `108π_0E_0[Y²1{|Δ| ≤ |Y|/(2κ)} | b]`, and the dyadic +argument of #218 Lemma O (Lemma D for `det A`, with the Gaussian tails of `Y` given `A`) bounds this by +`Cκ^{−1}(1 + |b|)^Ne^{−cb²}`. ∎ + +The next two lemmas replace v1's Lemma B′. They hold for every separation `0 < r ≤ r_0^*`, not only for `r ≤ r₂`. Their +only inputs from §2 are `𝒩_r := 1 + k + ‖F_r‖_{C⁹}`, `Δ = det A` and (F1), the own-jet form of #198 (3.1), which holds +for every `r ≤ r_0^*` (see (F1)). + +**Lemma H (the rescaled Hessian at `M`).** Let `0 < r ≤ r_0^*`, `b ∈ R` and `0 < k ≤ r` (so `κ = k/r ≤ 1`), and let +`f = F_r` under `Q`. In the frame `(u, Θ)` put `Λ_r := diag(r, 1, …, 1)`, `H_M := D²f(M)` and +`H̃ := Λ_r^{−1}H_MΛ_r^{−1}`, so that + + H̃_uu = r^{−2}∂_u²f(M), H̃_uΘ = r^{−1}∂_u∇_Θf(M), H̃_ΘΘ = D_Θ²f(M), det H_M = r² det H̃. + +(`Λ_r` is not [R] §4's `D_r = diag(√r, I)`, which defines `K_M = D_r^{−1}H_MD_r^{−1}`; the two are related by +`H̃ = diag(r^{−1/2}, I) K_M diag(r^{−1/2}, I)`.) + +There are `c > 0` and `C, C_p < ∞`, depending only on `d`, `L` (and `p`), such that: +- (a) under `Q`, `H̃` is a Gaussian random element of `Sym(d)` with `cI ≤ Cov_Q(H̃) ≤ CI` and `|E_QH̃| ≤ CP`, so #218 + Lemma D applies to `G = H̃` with `|μ| ≤ CP`; +- (b) `E_Q[𝒩_r^p | H̃] ≤ C_p(P + |H̃|)^p` for every `p ≥ 1`. + +*Proof.* *The exact form.* Put `g(t) := f(M + tu)` and `h(t) := ∇_Θf(M + tu)` for `0 ≤ t ≤ r`. Taylor's formula with +integral remainder gives, for every `C⁴` function, + + r²g″(0)/6 = [g(r) − g(0) − rg′(0)] − (r/3)[g′(r) − g′(0)] + (1/6)∫_0^r t(r − t)² g⁗(t) dt, + rh′(0) = [h(r) − h(0)] − ∫_0^r (r − t) h″(t) dt. + +Under `Q` the pins give `g(0) = b`, `g(r) = b − kr³`, `g′(0) = g′(r) = 0` and `h(0) = h(r) = 0`. So the bracketed pin +combinations equal `−kr³` and `0`, and with `t = rs` + + H̃ = m_κ + 𝒢_r(f), m_κ := −6κ e_u e_uᵀ, + 𝒢_r(f) := ( ∫_0^1 s(1 − s)² ∂_u⁴f(M + rsu) ds ; −∫_0^1 (1 − s) ∂_u²∇_Θf(M + rsu) ds ; D_Θ²f(M) ), (H.1) + +listing the `uu`, `uΘ` and `ΘΘ` blocks. `𝒢_r` is a linear map on `C⁴` functions with `|𝒢_r(g)| ≤ C‖g‖_{C⁴}`. It is +defined also at `r = 0`, where `𝒢_0(g) = (∂_u⁴g(0)/12, −∂_u²∇_Θg(0)/2, D_Θ²g(0))`; for the cusp jets this is +`(f₄/12, −γ/2, A)`. Control X9 checks (H.1) exactly on pinned polynomial fields. + +*(a).* Under `Q`, `f` is the Gaussian field `F` conditioned on its pin rows ([R] (R2)–(R3)). Let `U_r = T_rO_r` be the +rescaled pin rows of [P] (3.1) (`U0`–`U3` and `V_{j0}`, `V_{j1}`), with target +`v_r = (b − kr³/2, −kr², 0, 12k, 0, …, 0)` ([P] (3.3)); as `r → 0` they converge to the six pinned jets +`(F, ∂_uF, ∂_u²F, ∂_u³F, ∇_ΘF, ∂_u∇_ΘF)` at `0`. Then `Cov_Q(H̃) = Cov(𝒢_r(F) | U_r)`, the Schur complement of `U_r` in +the Gram matrix `Γ_r` of `(𝒢_r(F), U_r)`. +- *Continuity.* Every entry of `(𝒢_r(F), U_r)` is an integral of some `∂^αF(M + rsu)`, `|α| ≤ 4`, against a fixed finite + measure on `s ∈ [0, 1]` (a density or an endpoint mass), independent of `r`; by Taylor's formula this holds for the + difference rows of [P] (3.1) too. So each entry of `Γ_r` has the form + `∫∫ ±∂^{α+β}K_L(r(s − s′)u) μ_i(ds) μ_j(ds′)`, with `K_L` the smooth covariance of `F`. This is continuous on the + compact set `[0, r_0^*] × {frames}`, including at `r = 0`. +- *`r > 0`.* The map from `(D²F(M), O_r)` to `(𝒢_r(F), U_r)` is block-triangular with invertible diagonal blocks: + `𝒢_r(F) = Λ_r^{−1}D²F(M)Λ_r^{−1} − (a linear function of the pins)` by the two identities above, read for an + arbitrary `C⁴` function, and `U_r = T_rO_r` with `|det T_r| = 12r^{−(d+3)}` ([P] (3.2)). So `(𝒢_r(F), U_r)` is an + invertible linear image of `(D²F(M), F(M), F(S), ∇F(M), ∇F(S))`. These are distinct derivative evaluation + functionals at the two distinct sites `M ≠ S` (`r ≤ r_0^* < L`), linearly independent by [P] §2: "Any finite list of + distinct derivative evaluation functionals at distinct sites is linearly independent." +- *`r = 0`.* `(𝒢_0(F), U_0)` is an invertible image of `∂_u⁴F(0)`, `∂_u²∇_ΘF(0)` and `D_Θ²F(0)` together with the six + pinned jets. These are distinct jets at one point in the frame `(u, Θ)`, independent by [P] §2: "At one site in a + rotated frame the same assertion also follows …". + +So `Γ_r` is invertible at every point of the compact set, hence `Γ_r ≥ cI` uniformly. Therefore +`Cov_Q(H̃) ≥ λ_min(Γ_r)I ≥ cI` (the inverse of the Schur complement is a block of `Γ_r^{−1}`), and +`Cov_Q(H̃) ≤ Cov(𝒢_r(F)) ≤ CI`. + +For the mean, `E_QH̃ = m_κ + Cov(𝒢_r(F), U_r)Cov(U_r)^{−1}v_r`, with `|v_r| ≤ |b| + 14k`. The regression coefficient is +bounded by the same uniform invertibility, and `|m_κ| = 6κ ≤ 6`. So `|E_QH̃| ≤ CP`; this is the computation of (F3) +with `𝒢_r` in place of `J′`. + +*(b).* Conditioning `Q` on `H̃` is conditioning `F` on `(𝒢_r(F), U_r) = (H̃ − m_κ, v_r)`, whose Gram matrix `Γ_r` is +uniformly invertible by (a). +- The conditional mean of `F` is the regression on these values. Its `C⁹` norm is `≤ C(P + |H̃|)`, since `Γ_r^{−1}` is + bounded, the covariances of `F(·)` with `𝒢_r(F)` and `U_r` have bounded `C⁹` norms, and `|m_κ| ≤ 6`. +- The conditional covariance is at most `Cov F`, so by Anderson's inequality the conditional moments of the centred + part's `C⁹` norm are at most those of `F`. + +This is the argument (not the statement) of #218 (1.2), applied to the conditioning vector `(𝒢_r(F), U_r)`; no +coupling is needed, because `𝒩_r` involves `F_r` only. (Jensen's inequality can replace Anderson's: write the centred +field as `g + h` with `h` centred and independent of `g`; then `E‖g‖^p ≤ E‖g + h‖^p`.) Since +`𝒩_r = 1 + k + ‖F_r‖_{C⁹}` and `k ≤ P`, (b) follows. ∎ + +**Lemma S′ (the elder weight through the rescaled Hessian).** For `0 < r ≤ r_0^*`, `b ∈ R` and `0 < k ≤ r`, with `ℓ = kr³` and +`κ = k/r ≤ 1`, + + E_Q[(W_r/r²) e] ≤ C ℓ^{2/3} r^{−2} (κ + r) P^N. (S′.1) + +*Proof.* +- *The barrier, rescaled.* Fix a realisation in `{W_r > 0} ∩ {e = 1}`. Then `H_M < 0`, so `H̃ < 0`. + - #198 (1.2) gives `λ_min(−H_M) ≤ (ℓK²/c_L)^{1/3}`, where `K = 1 + ‖D²f‖_∞ + ‖D³f‖_∞ ≤ C_K𝒩_r`. + - Since `−H_M = Λ_r(−H̃)Λ_r` and `|Λ_rv| ≥ r|v|` (`r ≤ 1`), `vᵀ(−H_M)v ≥ r²λ_min(−H̃)|v|²`. So + `λ_min(−H_M) ≥ r²λ_min(−H̃)` (control X8). Both conditions are used: `r ≤ r_0^* ≤ r_0^{[R]} ≤ 1` (#191 line 27 + defines `r_0^*` as a minimum that includes `r_0^{[R]}`, and [R] line 55 chooses `r_0 ≤ 1`; `L/(4√2)` is only a + further cap), and `−H̃ > 0` on this event. For `r > 1`, or for an indefinite `H̃`, the inequality can fail (X8's + negative witness at `r = 2`). + + Hence + + 0 < λ_min(−H̃) ≤ ε(𝒩_r), ε(t) := C₃ ℓ^{1/3} r^{−2} t^{2/3}, C₃ := (C_K²/c_L)^{1/3}. (S′.2) + +- *The weight.* By [R] §4's dictionary, `|det K_M| = |det H_M|/r = r|det H̃| ≤ rλ_min(−H̃)‖H̃‖^{d−1}`. The pair is + typed, so the two determinants have opposite signs, and the sign window (#198 §3) applied to (F1) gives + `|det K_S| ≤ 12k|Δ| + 2max_i|R_i| ≤ Cr(κ + r)𝒩_r^{N₂}`, using `|Δ| ≤ 𝒩_r^m` and `1 + k ≤ 𝒩_r`. Since + `{H̃ < 0, λ_min(−H̃) ≤ ε} ⊂ {|λ_max(H̃)| ≤ ε}`, everywhere + + (W_r/r²) e ≤ C r²(κ + r) ε(𝒩_r) ‖H̃‖^{d−1} 𝒩_r^{N₂} 1{|λ_max(H̃)| ≤ ε(𝒩_r)}. + +- *Dyadic layers in `𝒩_r`.* On `{𝒩_r ∈ [2^j, 2^{j+1})}`, `ε(𝒩_r) ≤ ε_j := ε(2^{j+1})`. Condition on `H̃`, and bound + `P_Q(𝒩_r ≥ 2^j | H̃) ≤ C_p2^{−jp}(P + |H̃|)^p` by Lemma H (b). Then + + E_Q[(W_r/r²) e] ≤ C r²(κ + r) Σ_{j≥0} 2^{(j+1)N₂ − jp} ε_j E_Q[‖H̃‖^{d−1}(P + |H̃|)^p 1{|λ_max(H̃)| < 2ε_j}]. + + By Lemma H (a), #218 Lemma D (first bound, for `d × d` matrices, with `n = d − 1 + p` and `n′ := n + d(d − 1)/2`) + bounds the expectation by `CP^{p+n′}ε_j`. So the `j`-th term is at most `C2^{j(N₂ + 4/3 − p)}P^Nℓ^{2/3}r^{−4}`. Take `p = N₂ + 2`; the series + converges and gives (S′.1). ∎ + +**How (S′.1) compares with #198 (B.1).** (B.1) is `E_Q[(W_r/r²)e] ≤ Cℓ^{1/3}r^{−1}(k + r)P^N`. The ratio of (S′.1) to +(B.1) is `ℓ^{1/3}r^{−2}(k + r²)/(k + r)`. With `k = ℓr^{−3} ≤ r`, this is `≍ ℓ^{4/3}r^{−6}` for `r ≤ ℓ^{1/5}` and +`≍ ℓ^{1/3}r^{−1}` for `r ≥ ℓ^{1/5}`, so (S′.1) is the sharper bound once `r ≫ ℓ^{2/9}`, in particular on all of +`[ℓ^{2/15}, r_0^*]`. +- The gain is the second factor `ε`. The barrier puts `H̃` within `ε` of the singular set, and Lemma H makes that event + cost `ε` in probability (Lemma D). +- The size `ε ≍ ℓ^{1/3}r^{−2}` reflects the pins: they make `∂_u²f(M)` of order `r²`. The `uu`-entry of `H̃` tends to + `f₄/12 − 6κ` as `r → 0`. + +Lemma H is the lower bound on the conditional variance of the axial curvature under the pins, with `f₄` in the +limiting rows, that #198 Remark 1 asks for. Lemma S′ is the resulting refinement of #198 Lemma B, by the spectral +mechanism of #187 §3. At a fixed separation, (S′.1) is `O(ℓ^{2/3})`, the order of #187's Theorem F. + +## 4. Proof of Theorem E3 and of Corollary E3′ + +*Setup.* As in #218 §4, put `ρ_f := ℓ^{1/4 + 1/44}` and `ρ_c := ℓ^{1/4 − 1/36} = ℓ^{2/9}`, with `s_f := ρ_fℓ^{−1/4} = ℓ^{1/44}` +and `s_c := ρ_cℓ^{−1/4} = ℓ^{−1/36}`; also put `a := ℓ^{2/15}`. Let `r₂` be as in Lemma CE, and take `ℓ` so small that +`ρ_c ≤ r₂`, `a < r_0^*` and `ℓρ_f^{−3} ≤ 1`. Then `ρ_f < ρ_c < a`, since `3/11 > 2/9 > 2/15`. By the near/far identity +at `r_0 = r_0^*` (§0), + + ν_eld(ℓ) − cℓ^{−1/3} = F^{eld} + K^{eld} + I^{eld} − J₄ + ν_eld^{far,r_0^*}(ℓ), + +with all integrands at `(b, ℓ/r³, u)`, inner integrals `db dσ(u)`, and +- `F^{eld} := ∫_0^{ρ_f}∫∫ r^{−2}(A_r^{eld} − A_0)`; +- `K^{eld} := ∫_{ρ_f}^{ρ_c}∫∫ r^{−2}(A_r^{eld} − A_0)`; +- `I^{eld} := ∫_{ρ_c}^{r_0^*}∫∫ r^{−2}A_r^{eld} ≥ 0`; +- `J₄ := ∫_{ρ_c}^∞∫∫ r^{−2}A_0 ≥ 0`. + +*`F^{eld}`: the fold region.* Write `A_r^{eld} = A_r − A_r^{rej}`, `A_r^{rej} := 12π_r(v_r)E_Q[(W_r/r²)(1 − e)]`. +- The candidate part `∫_0^{ρ_f}∫∫r^{−2}(A_r − A_0)` is #218's `F`: + `c₂ℓ^{1/3} + ρ_f∫∫A₂(b, 0, u) + O(ρ_f² + ρ_f⁵/ℓ + ℓρ_f^{−2})` (#218 §4, from Lemma F). +- For `r ≤ ρ_f < ℓ^{1/4}`, `k = ℓ/r³ > r`, and `r ≤ r₂ ≤ r_0^* ≤ r_0^{[K]}`. So [C7-K] (K2), with `1 − e ≤ 1_{G_r^c}` ([C7-K] §4) and (R5), gives + `0 ≤ r^{−2}A_r^{rej} ≤ Cr^{−2}(r³/k)P^Ne^{−c(b²+k²)} ≤ C(r⁴/ℓ)(1 + |b|)^Ne^{−cb²}`. Integrated, this is `O(ρ_f⁵/ℓ)`. + +So `F^{eld} = c₂ℓ^{1/3} + ρ_f∫∫A₂(b, 0, u) + O(ρ_f² + ρ_f⁵/ℓ + ℓρ_f^{−2})`. + +*`K^{eld}`: the cusp region.* Here `k ≤ ℓρ_f^{−3} ≤ 1` and `r ≤ ρ_c ≤ r₂`. +- By (CE.1) with `κ = ℓ/r⁴`, the error is `∫_{ρ_f}^{ρ_c}Cr(1 + ℓr^{−4})²dr ≤ C(ρ_c² + ℓρ_f^{−2} + ℓ²ρ_f^{−6})`. +- With `r = sℓ^{1/4}`, the main term is `ℓ^{1/4}∫∫∫_{s_f}^{s_c}(𝒜^{eld} − 𝒜^{con})(b, s^{−4}, u) ds db dσ`. +- *Upper tail.* `0 ≤ 𝒜^{con} − 𝒜^{eld} ≤ 𝒜^{con} ≤ Cs^{−8}(1 + |b|)^Ne^{−cb²}`, so the part over `s > s_c` is `O(s_c^{−7})`. +- *Lower end.* By Lemma O′ and #218 Lemma O, `∫_0^{s_f}(𝒜^{eld} − 𝒜^{con})(b, s^{−4}, u) ds = s_fA₂(b, 0, u) + O(s_f⁵)`, since `s ≤ s_f < 1` means `κ = s^{−4} ≥ 1`. +- With (0.2), + `K^{eld} = c₁ℓ^{1/4} − ρ_f∫∫A₂(b, 0, u) + O(ℓ^{1/4}s_f⁵ + ℓ^{1/4}s_c^{−7} + ρ_c² + ℓρ_f^{−2} + ℓ²ρ_f^{−6})`. + +*The overlap cancels.* The terms `±ρ_f∫∫A₂(b, 0, u)` cancel, and `ℓ^{1/4}s_f⁵ = ρ_f⁵/ℓ`, `ℓ^{1/4}s_c^{−7} = ℓ²ρ_c^{−7}`. The +error terms are those of #218 §4: by #218's ledger (checker T1 there; X1 here), every exponent is `≥ 4/11`. So + + F^{eld} + K^{eld} = c₁ℓ^{1/4} + c₂ℓ^{1/3} + O(ℓ^{4/11}). (4.1) + +*`J₄`.* `A_0 ≤ k²H` gives `0 ≤ J₄ ≤ Cℓ²ρ_c^{−7} = Cℓ^{4/9}`. + +*`I^{eld}`: intermediate separations.* On `[ρ_c, r_0^*]`, `k = ℓ/r³ ≤ ℓρ_c^{−3} = ℓ^{1/3} ≤ 1`. Split at `a = ℓ^{2/15}`. +- *On `[ρ_c, a]`.* `e ≤ 1`, #198 (W.1) and (R5) give + `0 ≤ r^{−2}A_r^{eld} ≤ r^{−2}A_r ≤ Cr^{−2}(k² + r⁴)P^Ne^{−c(b²+k²)} ≤ C(κ² + r²)(1 + |b|)^Ne^{−cb²}`, with + `κ = ℓr^{−4}`. This integrates to at most `C(ℓ²ρ_c^{−7} + a³) = C(ℓ^{4/9} + ℓ^{2/5})`. +- *On `[a, r_0^*]`.* Here `κ = ℓr^{−4} ≤ ℓ^{7/15} ≤ 1`, i.e. `k ≤ r`. Lemma S′ with (R5) gives + `0 ≤ r^{−2}A_r^{eld} ≤ Cℓ^{2/3}r^{−4}(κ + r)(1 + |b|)^Ne^{−cb²} = Cℓ^{2/3}(ℓr^{−8} + r^{−3})(1 + |b|)^Ne^{−cb²}`. This + integrates to at most `C(ℓ^{5/3}a^{−7} + ℓ^{2/3}a^{−2}) = C(ℓ^{11/15} + ℓ^{2/5})`. + +So `0 ≤ I^{eld} ≤ Cℓ^{2/5}`. The split point balances `a³` against `ℓ^{2/3}a^{−2}` (control X1). + +*Conclusion.* By (4.1), `0 ≤ I^{eld} ≤ Cℓ^{2/5}` and `0 ≤ J₄ ≤ Cℓ^{4/9}`, and since `4/11 < 2/5 < 4/9`, + + ν_eld(ℓ) − cℓ^{−1/3} − c₁ℓ^{1/4} − c₂ℓ^{1/3} − ν_eld^{far,r_0^*}(ℓ) = O(ℓ^{4/11}). + +This is (E3.0). The bound `0 ≤ ν_eld^{far,r_0^*}(ℓ) ≤ Cℓ^{1/3}` there is #198 Lemma F′ at `r_0 = r_0^*` +(`r_0^* ≤ L/(4√2) < L/2`). +- (E3.1): `ν_eld^{far,r_0^*} = O(ℓ^{1/3})` absorbs `c₂ℓ^{1/3}` and the `O(ℓ^{4/11})`. +- (E3.2): `ν_eld^{far,r_0^*} ≥ 0`. +- (E3.3): #187's Theorem F at `ρ = r_0^*` (`∈ (0, L/2]`) gives `ν_eld^{far,r_0^*}(ℓ) ≤ C(r_0^*)ℓ^{2/3} ≤ Cℓ^{4/11}` for + `0 < ℓ ≤ 1`. #187's far density (its (0.1)) at `ρ = r_0^*` is the same integral as #198's (2.1) at `r_0 = r_0^*`: the + same domain `{dist(0, y) ≥ r_0^*}`, the same `O_y`, `v_{b,ℓ}`, `p_y`, `Q_{y,b,ℓ}` and `W`, and the same Borel mark of + [P] §8. +- The two equivalences: by (E3.0) the difference of the two sides is `O(ℓ^{4/11})`, which is `O(ℓ^θ)` for `θ ≤ 4/11` + and `o(ℓ^{1/3})`. ∎ + +*Proof of Corollary E3′.* `ρ_rej = ν_cand − ν_eld`. Subtracting (E3.0) from #218's (T.1), +`ν_cand(ℓ) = cℓ^{−1/3} + B_{d,L} + I^{cand}ℓ^{1/4} + c₂ℓ^{1/3} + O(ℓ^{4/11})`, gives (E3′.0): the `cℓ^{−1/3}` and +`c₂ℓ^{1/3}` terms cancel. Then (1) follows from `ν_eld^{far,r_0^*} ≤ Cℓ^{1/3}`, (2) from `ν_eld^{far,r_0^*} ≥ 0`, and (3) +from #187's Theorem F at `ρ = r_0^*`. ∎ + +## 5. Remarks + +1. **Why the elder law has the candidate's `c₂`.** The elder rule enters the expansion at three places. + - At the fold scale the rejected mass is `O(r³/k)` ([C7-K] (K2)). That is the order of the boundary layer, below + `ℓ^{1/3}` after integration. + - At the cusp scale the elder rule is the window `|φ| < 1/3` (#207). It changes the `ℓ^{1/4}` coefficient from + `I^{cand}` to `c₁`, and changes nothing at order `ℓ^{1/3}`: by Lemma O′ the elder and candidate cusp losses have the + same limit `A₂(b, 0)` as `κ → ∞`, which is what the finite part `c₂` subtracts. + - At intermediate separations, elder pairs need a soft maximum. On `[ℓ^{2/15}, r_0^*]` Lemma S′ bounds the elder + weight by `ℓ^{2/3}r^{−2}(κ + r)`; below `ℓ^{2/15}` the unmarked bound (W.1) suffices. Together these separations + carry only `O(ℓ^{2/5})`. + - At far separations #187 (merged) gives `O(ℓ^{2/3})`; (E3.0) keeps that part separate, so it does not use #187. + + So `c₂` is a fold-scale quantity, as #216 argued formally. (E3.0) makes this a theorem up to the far part, and (E3.3) + completes it with #187. +2. **The far part is the only remaining input.** (E3.0) reduces the elder third-order law to the far elder density at + the fixed separation `r_0^*`. + - v1 needed an `ε`-argument in a cut-off `r₁ ↓ 0`, and a rate would have needed #187's constant quantified as + `C(ρ) ≤ Cρ^{−p}`. Lemma S′ removes both: below `r_0^*` the elder mass is controlled directly. + - Any bound `ν_eld^{far,r_0^*}(ℓ) = O(ℓ^θ)` gives the three-term law with remainder `O(ℓ^{min(θ, 4/11)})`. #187's + Theorem F gives `θ = 2/3`. + - #188 (unmerged; cited only, not consumed) proposes `ν_eld^{far,ρ}(ℓ) = O(ℓ^N)` for every `N` and every + `ρ ∈ (0, L/4]`, which would serve equally (`r_0^* ≤ L/(4√2)`). + - Lemma S′ also sharpens #198 (B.2). For `ℓ^{1/4} ≤ ρ ≤ r_0^*`, the elder density from separations in `[ρ, r_0^*)` + is `≤ C(ℓ^{2/3}ρ^{−2} + ℓ^{5/3}ρ^{−7})`, against #198's `Cℓ^{1/3}(ρ^{−1} + ℓρ^{−5})`; the new bound is smaller + when `ρ ≫ ℓ^{2/9}`. +3. **The SIDE24 values and the Monte Carlo (exploration, not certified).** For the Gaussian kernel in `d = 3`, #207 §8 + and #216 give `c = 0.0417759`, `c₁ = −0.2118484` and `c₂ = 0.1612340`. So under (E3.3) + `ν_{3,24}(ℓ) ≈ cℓ^{−1/3}(1 − 5.0711ℓ^{7/12} + 3.8595ℓ^{2/3})` up to a relative `O(ℓ^{23/33})`; the Gaussian-kernel values agree with + the `L = 24` torus up to a relative `O(e^{−L²/8})`. The elder-pair row of #216 v1.2 §3 is an exploratory estimate of + `ν_eld` itself: the exact elder rule by union–find on the full periodized field, `d = 2` at `L = 64` and `d = 3` at + `L = 16`. On `[10⁻⁴, 10⁻²]` it gives data/law `1.006 ± 0.004` (`χ² = 7.0/11`) in `d = 2` and `1.008 ± 0.010` + (`χ² = 5.0/11`) in `d = 3` for the three-term law, and rejects the two-term law (`χ² = 714/11` and `175/11`). Its + adjacent-pair row, which #218 Remark 3 concerns, is not covered here. +4. **Lemma Q is field-independent.** It is a deterministic statement about `C⁵` functions with two pinned critical + points: the elder window `|φ| < 1/3` of #207 is stable, with explicit margins, as long as + `𝒩r(1 + |γ|/λ)² ≪ κ||φ| − 1/3|` and `λ ≫ 𝒩r + (𝒩r|γ|)^{1/2}`, with the window inside the torus ((Q1)–(Q4)). #207's + Proposition CU.3 is its qualitative case. Only §§2–4 use the law of the [P] field. +5. **For the manuscript.** Once #207, #218 and this note are reviewed (#187, #191 and #198 are merged), the abstract can state + `ν_{3,24}(ℓ) = c_{3,24}ℓ^{−1/3} + c₁ℓ^{1/4} + O(ℓ^{1/3})` with `c₁ < 0` the explicit integral (CU.2). With #187 it can + state the three-term law with remainder `O(ℓ^{4/11})`. Until then V3 edit E10 is the safe statement. +6. **Consistency.** + - (E3.0) implies (E3.1), which implies #207's (CU.1) and #198's (0.1). + - Corollary E3′(1) implies #207's (CU′.2). + - Corollary E3′(1), with `I^{cand} − c₁ = (1 − 3^{1/4}/2)|c₁| > 0` (#207 (CU′.2)), shows that the rejected density + approaches `B_{d,L}` from above, by the rejected cusp mass, now with a rate. Corollary E3′(2) bounds the approach + from above to order `ℓ^{4/11}`. By (E3′.0), the only other `ρ_rej`-correction above order `ℓ^{4/11}` is + `−ν_eld^{far,r_0^*}`. + - (S′.1) at a fixed separation is `O(ℓ^{2/3})`, the order of #187's far bound. Accordingly (E3.0) holds with + `r_0^*` replaced by any fixed `r_0 ∈ (0, r_0^*]`: by Lemma S′ the elder mass from separations in `[r_0, r_0^*)` is + `O(ℓ^{2/3})`. + +## 6. Sources (exact identities in `SOURCES.json`) + +| Tag | Path | Role | +|---|---|---| +| [R] | `frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md` (blob `247b3ecf`) | (R2)–(R5): pin covariance, regression, moments, pin densities; §4 scaled Hessians — consumed | +| [P] | `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` (blob `dfed3b8d`) | §2 finite-jet rank (also for Lemma H), §8 maximin and elder mark, §§9–10 as [E2] (the near/far identity), §15 parity factorization and (15.2) — consumed | +| [E1] | `imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md` (blob `213594d6`) | reading rule | +| [E2] | `reviews/d1_section9_borel_repair_20260925/REPAIR.md` (blob `fe9b9ce4`) | §9 replacement | +| [REC] | `reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md` (blob `75da2597`) | reading rule | +| [C7-K] | `frontiers/c7_total_bounded_20260929/PROOF.md` (blob `28748b08`) | (K2); §4 `1 − e ≤ 1_{G_r^c}` — consumed | +| [Z] | `frontiers/c7_zero_gap_limit_20260929/PROOF.md` (blob `5b6328ea`) | (Z13)–(Z14): the change of variables in the near/far identity — consumed | +| #191 | `frontiers/remainder_vanishing_20260930/PROOF.md` (merged 1 October 2026 at `9556547`; blob `441152df`) | Lemma E Steps 1–4, §2 (2.1), `r_0^*` — consumed | +| #198 | `frontiers/remainder_rate_20260930/PROOF.md` (merged 1 October 2026 at `124c37d`; blob `abfb98ae`) | (3.1), §3 sign window, Lemma B's barrier (1.2) and §1 identity, Lemma W (W.1), (2.1), Lemma F′ — consumed | +| #207 | `frontiers/cusp_second_order_20261001/PROOF.md` (unmerged; v1.1 blob `f6df5a73`) | §0, proof of CU.1, CU.2, structure of CU.3, §6 ((6.1), (CU.2)) — **consumed, unmerged** | +| #218 | `frontiers/candidate_third_order_20261001/PROOF.md` (unmerged; blob `70ca57ef`) | Lemma D (also for `H̃`), (1.2) and its proof, Lemma F (F1, F3, (F.2)), Lemma C (C1, C2, C3), Lemma O, Theorem T, §4 — **consumed, unmerged** | +| #187 | `frontiers/far_elder_rate_20260930/PROOF.md` (merged 1 Oct at `c2f1270`; blob `07260114`, rebound from `37dcf6ef` after a status-only repair) | Theorem F at `ρ = r_0^*` — **consumed, for (E3.3) and Corollary E3′(3) only** | +| #216 | `frontiers/third_order_coefficient_20261001/` (unmerged) | numerical `c₂`, the Monte Carlo — cited only | +| #188 | `frontiers/far_elder_flat_ridge_20260930/PROOF.md` (unmerged) | Theorem G, an alternative far bound (Remark 2) — cited only | + +## 7. Exact controls (`e3_check.py`; stdlib; exact rationals; byte-identical under `-O`) + +- **X1** the exponent ledger of §4. + - #218's ledger: least exponent `4/11`, attained exactly by `ρ_f⁵/ℓ` and `ℓ²ρ_f^{−6}`. + - The intermediate terms: `ℓ²ρ_c^{−7}` and `a³` on `[ρ_c, a]`; `ℓ^{5/3}a^{−7}` and `ℓ^{2/3}a^{−2}` on `[a, r_0^*]`. All + have exponents `> 4/11`, the least being `2/5`. + - The facts used: `ρ_f < ρ_c < a`; `k ≤ ℓ^{1/3}` on `[ρ_c, r_0^*]`; `κ ≤ ℓ^{7/15} ≤ 1` on `[a, r_0^*]`; and that + `a = ℓ^{2/15}` balances `a³` against `ℓ^{2/3}a^{−2}`. +- **X2** the ridge identities (M1) and the closed forms (M4)–(M5), as exact polynomial identities in `Q[X, φ]`, with + `g(X₃)` checked on a grid of rational `φ`. +- **X3** the margins: + - (M4) through the factorizations `(φ + 1)³ − 8φ³ = (1 − φ)(7φ² + 4φ + 1)` and `(1 + ψ)³ − 64ψ³ = (1 − 3ψ)(21ψ² + 6ψ + 1)`; + - (M2)–(M3) on dense rational grids of `(φ, X)`; + - the sharpness of `3/2` (equality at `φ = 1`). +- **X4** the one-dimensional decision under perturbation. For random rational `φ` and polynomial perturbations + `h = (X² − ¼)²q(X)`, scaled so that rigorous coefficient bounds give `sup|h″| ≤ κ/4` and + `sup|h| < (3/2)κ||φ| − 1/3|`, the path and trap inequalities of Step Q6 hold exactly on a fine rational grid in every + case. +- **X5** Lemma CU.1′'s mechanism. On exactly pinned polynomial fields of degree 6–7 in `d = 2, 3` with `k = κr`, every + monomial `r^aX^iΞ^j` of `𝔉 − 𝔓` has `a ≥ 1` and `|j| ≤ a + 1`, and the bound is attained (`rXΞ²`). +- **X6** Lemma S on random rational instances and on near-extremal ones; and the two polynomial bounds of Step Q2, + `(5/4 + 35Γ/8)² ≤ 80(1 + Γ)²` and `105/64 + (2911/128)Γ + (317/4)Γ² ≤ 80(1 + Γ)²`. +- **X7** the pointwise facts of §§2–3: `0 ≤ loss_κ ≤ 9Y²`; the equivalence `|φ| < 1/3 ⟺ |Y′| < 2κ|Δ|`; the Lemma O′ + domination; and Step E2's `𝔅_5` bound `w_κ ≤ 12κ|Δ|τ` when `|Y_r| < 6κ|Δ| < |Y′|`. +- **X8** Lemma S′'s linear algebra, on 121 instances in `d = 2, 3, 4`. Each has `−H̃ = O diag(λ) Oᵀ`, with `O` a rational + orthogonal matrix (Cayley transform) and rational `λ`, and `H_M = Λ_rH̃Λ_r`. The checks: + - `det H_M = r² det H̃`; + - `−H_M − r²λ_min(−H̃)I` is positive semidefinite, by all principal minors, so `λ_min(−H_M) ≥ r²λ_min(−H̃)`; at the + instance `H̃ = −I`, `r = 1/2` the matrix is singular, so the bound is attained; + - `|det H̃| ≤ λ_min(−H̃)‖H̃‖^{d−1}`; + - a negative witness (status update of 1 October): at `r = 2` and `−H̃ = diag(1, 2)`, `−H_M − r²λ_min(−H̃)I = + diag(0, −2)` is not positive semidefinite, so the range `r ≤ 1` is necessary. +- **X9** Lemma H's exact form (H.1). The fields are exactly pinned polynomial fields (`d = 2`: degree 6 and 7; `d = 3`: + degree 6; `k = κr`), at the separations `r ∈ {1/3, 2/7, 1/2, 1}`. The checks: + - the pins themselves; + - `r^{−2}∂_u²f(M) = −6κ + ∫_0^1 s(1 − s)²∂_u⁴f(M + rsu) ds`; + - `r^{−1}∂_u∂_θf(M) = −∫_0^1 (1 − s)∂_u²∂_θf(M + rsu) ds`; + - as polynomials in `r`, the values at `r = 0`: `−6κ + f₄/12`, `−γ/2` and `A`. +- **Mutants.** Each exits 1: + - M1 `ρ_c = ℓ^{1/4 − 1/120}`; + - M2 margin constant `8/5` in place of `3/2`; + - M3 elder threshold `0.36` in place of `1/3` in X4; + - M4 the claim `|j| ≤ a` in X5; + - M5 coefficient `1/λ` in place of `2/λ` in (1.2); + - M6 the factor `1` in place of `r²` in X8 (`λ_min(−H_M) ≥ λ_min(−H̃)`); + - M7 the kernel `s²(1 − s)` in place of `s(1 − s)²` in (H.1) (the same mass `1/12`, hence the same `r = 0` value); + - M8 the split at `ℓ^{1/5}` in place of `ℓ^{2/15}` (then `ℓ^{2/3}a^{−2} = ℓ^{4/15}`, below `4/11`). + + An unknown label exits 2. + +**What the controls do not test.** Lemma CU.1′ for non-polynomial fields; the probability estimates of Lemma CE (Steps +E2–E6); Lemma G; Lemma O′, Lemma H's covariance bounds and Lemma S′ as statements about random fields; and the assembly +of §4. These are proved in prose only. + +**Exploration (floating point; archive only, not a control).** +- *The Gaussian kernel on `R^d`, the large-`L` regime.* `Cov(H̃ | pins)` for `e^{−|z|²/2}` (`d = 2, 3`; 60-digit + `mpmath`) has smallest eigenvalue `0.1667` at `r = 0.001`. It decreases smoothly to `0.1360` at `r = 1`, `0.0714` at + `r = 2` and `0.0239` at `r = 3`, and the largest eigenvalue is `2` throughout. + - In `d = 2` the conditional covariance at `r → 0` is diagonal, with eigenvalues `24/144 = 1/6`, `2/4 = 1/2` and `2`: + `Var(f₄ | pins) = 105 − 81 = 24`, `Var(γ | pins) = 3 − 1 = 2` and `Var(A | pins) = 3 − 1 = 2`, for the entries + `f₄/12`, `−γ/2` and `A` of `H̃`. + - The decrease at large `r` is the scaling `H̃_uu = r^{−2}∂_u²f(M)`: once the pin at `S` stops constraining + `∂_u²f(M)`, the variance of `H̃_uu` is about `2r^{−4}` (`0.0247` at `r = 3`). +- *Small tori.* The referee's independent probe (REFEREE_2, R2) found the bound positive and smooth at `r = 0` on tori + with `L = 2, 3, 6` in `d = 2` and `L = 3` in `d = 3`, over several frames, for `r` up to `1.5·min(1, L/(4√2))`. The + constant depends on `L` and the frame and can be tiny: `λ_min ≈ 4·10⁻⁵` at `d = 2`, `L = 2`, `u = e₁`, + `r ≈ 0.354`. Lemma H claims no uniformity in `L`. + +## 8. Review slices + +- **A** §1: Lemma CU.1′, Lemma S and Lemma Q. Points to check: + - the window and its embedding; + - the ridge and the `C⁰`/`C²` distances; + - the reduction to the ridge; + - the margins (M1)–(M6); + - the three cases of Step Q6. +- **B** §2: Lemma G and Lemma CE. Points to check: + - (F1)–(F7) against #198, #207 and #218; + - the pathwise comparison (2.3); + - the four bad events of Step E2 and their dyadic `𝒩_r`-bookkeeping; + - the Gaussian comparisons of Steps E4 and E6. +- **C** §§3–4: Lemma O′; Lemma H (the exact form (H.1), the uniform nondegeneracy at `r = 0` and `r > 0`, the + conditional moments); Lemma S′ (the rescaled barrier, the sign window, the dyadic use of Lemma D); the decomposition + at `r_0^*`, the fold-region elder deficit, the split at `ℓ^{2/15}`; and Corollary E3′. diff --git a/frontiers/elder_third_order_20261001/README.md b/frontiers/elder_third_order_20261001/README.md new file mode 100644 index 000000000..dfd2623ad --- /dev/null +++ b/frontiers/elder_third_order_20261001/README.md @@ -0,0 +1,118 @@ +# The elder density to third order (CL-ELDER-THIRD-ORDER-20261001-v1.1) + +Author-side proof candidate. Anthropic Claude, 1 October 2026. Scientific effect NONE. Nonauthor review required. + +**Statement (Theorem E3).** For every `d ≥ 2` and `L > 0`, as `ℓ ↓ 0`, + + ν_eld(ℓ) = c ℓ^{−1/3} + c₁ ℓ^{1/4} + c₂ ℓ^{1/3} + ν_eld^{far,r_0^*}(ℓ) + O(ℓ^{4/11}), 0 ≤ ν_eld^{far,r_0^*}(ℓ) ≤ C ℓ^{1/3}. (E3.0) + +Hence: + + ν_eld(ℓ) = c ℓ^{−1/3} + c₁ ℓ^{1/4} + O(ℓ^{1/3}); (E3.1) + ν_eld(ℓ) ≥ c ℓ^{−1/3} + c₁ ℓ^{1/4} + c₂ ℓ^{1/3} − C ℓ^{4/11}; (E3.2) + +and, by Math- #187's Theorem F (merged on 1 October 2026) at the one separation `ρ = r_0^*` (the far elder density +there is `O(ℓ^{2/3})`), + + ν_eld(ℓ) = c ℓ^{−1/3} + c₁ ℓ^{1/4} + c₂ ℓ^{1/3} + O(ℓ^{4/11}). (E3.3) + +- (E3.0) reduces the elder third-order law exactly to the far elder density at the fixed separation `r_0^*`. The law + holds with remainder `O(ℓ^θ)`, `θ ≤ 4/11`, if and only if that far density is `O(ℓ^θ)`. +- `c₁ < 0` is #207's cusp coefficient (CU.2). +- `c₂` is #218's (0.1): the fold-scale Hadamard finite part that Math- #216 defines and computes (`0.16123405` in `d = 3` + for the Gaussian kernel; a numerical approximation, not certified). +- (E3.1) is a rate for #207's (CU.1), which claimed none. + +**Corollary E3′ (the rejected density).** With Theorem T (#218), +`ρ_rej = B_{d,L} + (I^{cand} − c₁)ℓ^{1/4} − ν_eld^{far,r_0^*}(ℓ) + O(ℓ^{4/11})`. In particular: +- `ρ_rej = B_{d,L} + (I^{cand} − c₁)ℓ^{1/4} + O(ℓ^{1/3})`, a rate for #207's (CU′.2); +- `ρ_rej ≤ B_{d,L} + (I^{cand} − c₁)ℓ^{1/4} + Cℓ^{4/11}`; +- under #187, `ρ_rej = B_{d,L} + (I^{cand} − c₁)ℓ^{1/4} + O(ℓ^{4/11})`. The candidate and elder densities have the same + `ℓ^{1/3}` coefficient, so the rejected density has no `ℓ^{1/3}` term. + +**What changed in v1.1.** v1 bounded the intermediate separations by an `ε`-argument (`Cℓ^{1/3}r₁^β`, then `r₁ ↓ 0`). +So its (E3.3) had no rate, and it needed #187 at every small separation. v1.1 replaces v1's Lemma B′ with Lemmas H and +S′. The intermediate separations then contribute `O(ℓ^{2/5})`, and only the far part at the fixed radius `r_0^*` is +left. #207's Lemma CU.5 is no longer consumed. + +**The new lemmas.** +- **Lemma Q (the elder decision with explicit margins).** This is #207's Proposition CU.3 made quantitative. The elder + decision is `1{|φ| < 1/3}` whenever the rescaled ridge is within `(3/2)κ||φ| − 1/3|` of the model ridge in `C⁰` and + within `κ/4` in `C²`. Both distances are `O(𝒩r(1 + |γ|/λ)²)`, by Lemma CU.1′ (`Ξ`-weighted Taylor bounds) and Lemma S + (a Schur-complement perturbation bound). The margin constant `3/2` is sharp, with equality at `φ = 1`. +- **Lemma CE (the elder cusp kernel with a rate).** + `|r^{−2}(A_r^{eld} − A_0)(b, κr) − (𝒜^{eld} − 𝒜^{con})(b, κ)| ≤ Cr(1 + κ)²(…)`. This is the candidate rate of #218 + Lemma C. Wrong decisions cost little because the weight `36κ²Δ²` vanishes to second order in the transverse concavity + `λ`. The passages to the contact law and to the zero-gap target use Gaussian comparisons (Lemma G), which need no + regularity of the jumping elder loss. +- **Lemma O′ (elder overlap).** `𝒜^{cand} − 𝒜^{eld} = O(1/κ)`, so the elder cusp loss tends to `A₂(b, 0)` like the + candidate loss. +- **Lemma H (the rescaled Hessian at `M`; new in v1.1).** `H̃ = D_r^{−1}D²f(M)D_r^{−1}`, with `D_r = diag(r, 1, …, 1)`, + equals `−6κe_ue_uᵀ` plus explicit segment integrals of `∂_u⁴f` and `∂_u²∇_Θf` (the exact form (H.1)). It is a + Gaussian with covariance between `cI` and `CI` uniformly in `r ≤ r_0^*`, by [P] §2's linear independence at `r > 0` + and at `r = 0`. This is the conditional variance bound for the axial curvature under the pins that #198 Remark 1 + asks for. +- **Lemma S′ (new in v1.1).** `E_Q[(W_r/r²)e] ≤ Cℓ^{2/3}r^{−2}(κ + r)P^N` for `r ≤ r_0^*` and `k ≤ r`. + - #198's barrier puts `λ_min(−H̃)` below `Cℓ^{1/3}r^{−2}`. + - Lemma D for `H̃` charges that event twice: once in `|det H̃|` and once in probability. + +**The assembly.** It uses #218 §4's decomposition and ledger with the elder kernel, so the least exponent is again `4/11`. +- The fold-region elder deficit is `O(ρ_f⁵/ℓ)`, by [C7-K] (K2). +- The intermediate separations `[ρ_c, r_0^*]` contribute `O(ℓ^{2/5})`: #198 (W.1) below `ℓ^{2/15}`, Lemma S′ above. +- The far part `ν_eld^{far,r_0^*}` is kept in (E3.0). #198 Lemma F′ bounds it by `Cℓ^{1/3}`, and #187 by `Cℓ^{2/3}`. + +**Numerical illustration (exploration).** The elder-pair row of Math- #216 v1.2's full-field Monte Carlo uses the exact +elder rule, by union–find. It fits the three-term law with data/law `1.006 ± 0.004` in `d = 2` and `1.008 ± 0.010` in +`d = 3`, and rejects the two-term law. + +**Not claimed:** +- (E3.3) and Corollary E3′(3) without #187; +- sharpness of `4/11`; +- certified constants; +- uniformity in `d` or `L`; +- anything about the adjacent-pair density. + +**Dependencies.** +- *Consumed, unmerged:* Math- #207 and #218. This packet must be rebound if either changes. +- *Consumed, merged:* Math- #191 and #198 (merged on 1 October 2026 with the blobs consumed here); #187 (merged on + 1 October 2026 at `c2f1270` with the blob consumed here), for (E3.3) and Corollary E3′(3) only, at `ρ = r_0^*`; [R], + [P] (with [E1], [E2], [REC]), [C7-K] and [Z]. +- *Cited:* #216, #188. + +**Files.** +- `PROOF.md`. +- `e3_check.py`: standard library, exact rationals. Its output is `RESULTS.json`, byte-identical under `-O` and on + CPython 3.10–3.14; the run takes about 11 s. The controls are: + - **X1** the exponent ledger, with the intermediate split at `ℓ^{2/15}`; + - **X2** the ridge identities; + - **X3** the margins and the sharpness of `3/2`; + - **X4** the one-dimensional decision under perturbation, in all three cases; + - **X5** the weighted Taylor structure on exactly pinned polynomial fields in `d = 2, 3`; + - **X6** Lemma S and the `C⁰`/`C²` polynomial bounds; + - **X7** the pointwise facts of Lemmas CE and O′; + - **X8** Lemma S′'s linear algebra (`det H_M = r² det H̃`; `λ_min(−H_M) ≥ r²λ_min(−H̃)` by principal minors; a negative witness at `r = 2`); + - **X9** Lemma H's exact form (H.1) on exactly pinned polynomial fields, and its `r = 0` values. + + Mutants M1–M8 exit 1, and an unknown label exits 2. +- `SOURCES.json`: the exact identities of all sources. + +**Review record.** +- v1, same-family: a clean-context referee read the whole note against its sources. Verdict: ACCEPT WITH MINOR FIXES, + with no major finding; its four minor findings and nine nits are applied. A delta check of the revision by the same + referee: ACCEPT. Its two-dimensional union–find test of Lemma Q's decision agreed in 48 of 48 exactly pinned fields + (floating point; exploration). +- v1, nonauthor (on #220, at head `6da0715`): + - OpenAI / Codex (delegated) reviewed Slices A, B and C, each PASS_TECHNICAL at its stated scope. It requested two + amendments. OA-220-B-01 (the integrability hypothesis of Lemma G (b)) is applied. OA-220-C-01 (v1 Remark 2's + shrinking cut-off) is superseded, because v1.1 has no shrinking cut-off. + - xAI checked the ridge identities of Lemma Q with sympy. +- v1.1, same-family: a clean-context referee read the v1 → v1.1 delta against all eight sources. Verdict: ACCEPT WITH + MINOR FIXES, with no major finding; one minor finding and eleven nits, all applied. Its delta check of the fixes: + ACCEPT. + +Same account, zero organizational independence. + +**Review slices** (PROOF §8): +- **A** §1: Lemma CU.1′, Lemma S and Lemma Q; +- **B** §2: Lemma G and Lemma CE; +- **C** §§3–4: Lemmas O′, H and S′, and the assembly. diff --git a/frontiers/elder_third_order_20261001/RESULTS.json b/frontiers/elder_third_order_20261001/RESULTS.json new file mode 100644 index 000000000..4f1b390b1 --- /dev/null +++ b/frontiers/elder_third_order_20261001/RESULTS.json @@ -0,0 +1,215 @@ +{ + "checks": { + "X1_exponent_ledger": { + "core": { + "l rho_f^-2": "5/11", + "l^2 rho_c^-7": "4/9", + "l^2 rho_f^-6": "4/11", + "rho_c^2": "4/9", + "rho_f^2": "6/11", + "rho_f^5/l": "4/11" + }, + "intermediate": { + "[a,r0*]: l^(2/3) a^-2": "2/5", + "[a,r0*]: l^(5/3) a^-7": "11/15", + "[rho_c,a]: a^3": "2/5", + "[rho_c,a]: l^2 rho_c^-7": "4/9" + }, + "least": "4/11", + "passed": true, + "split_exponent": "2/15" + }, + "X2_ridge_identities": { + "X3_closed_forms_at_rational_phi": 400, + "factorizations": true, + "g_at_points": { + "-3": [ + "-50", + "3675/16" + ], + "-3/2": [ + "-5", + "12" + ], + "2": [ + "25/2", + "675/16" + ] + }, + "passed": true + }, + "X3_margins": { + "margin_constant": "3/2", + "min_ratio_over_grid": "3/2", + "passed": true, + "sharp_at_phi_1": true + }, + "X4_decision_1d": { + "cases": { + "E": 117, + "R+": 123, + "R-": 123 + }, + "grid_points": 501, + "passed": true, + "threshold": "1/3" + }, + "X5_weighted_taylor": { + "fields": [ + { + "d": 2, + "degree": 6, + "kappa": "161/100", + "min_slack": 0, + "monomials": 26 + }, + { + "d": 2, + "degree": 6, + "kappa": "117/50", + "min_slack": 0, + "monomials": 25 + }, + { + "d": 2, + "degree": 6, + "kappa": "157/100", + "min_slack": 0, + "monomials": 25 + }, + { + "d": 2, + "degree": 7, + "kappa": "42/25", + "min_slack": 0, + "monomials": 37 + }, + { + "d": 2, + "degree": 7, + "kappa": "17/25", + "min_slack": 0, + "monomials": 37 + }, + { + "d": 2, + "degree": 7, + "kappa": "51/50", + "min_slack": 0, + "monomials": 37 + }, + { + "d": 3, + "degree": 6, + "kappa": "213/100", + "min_slack": 0, + "monomials": 78 + }, + { + "d": 3, + "degree": 6, + "kappa": "13/100", + "min_slack": 0, + "monomials": 79 + }, + { + "d": 3, + "degree": 6, + "kappa": "29/100", + "min_slack": 0, + "monomials": 72 + } + ], + "passed": true + }, + "X6_lemma_S": { + "Q2_C0_poly": [ + "25/16", + "175/16", + "1225/64" + ], + "Q2_C2_poly": [ + "105/64", + "2911/128", + "317/4" + ], + "coefficient": "2", + "passed": true, + "random_instances": 900 + }, + "X7_pointwise": { + "passed": true, + "trials": 5000 + }, + "X8_lemma_S_prime_algebra": { + "extremal_singular": true, + "instances": 121, + "loewner_factor": "r^2", + "passed": true, + "range_witness_r2_fails": true + }, + "X9_lemma_H_exact_form": { + "fields": [ + { + "d": 2, + "degree": 6, + "kappa": "11/100", + "separations": 4 + }, + { + "d": 2, + "degree": 6, + "kappa": "237/100", + "separations": 4 + }, + { + "d": 2, + "degree": 6, + "kappa": "169/100", + "separations": 4 + }, + { + "d": 2, + "degree": 7, + "kappa": "52/25", + "separations": 4 + }, + { + "d": 2, + "degree": 7, + "kappa": "23/20", + "separations": 4 + }, + { + "d": 2, + "degree": 7, + "kappa": "69/25", + "separations": 4 + }, + { + "d": 3, + "degree": 6, + "kappa": "57/100", + "separations": 4 + }, + { + "d": 3, + "degree": 6, + "kappa": "29/10", + "separations": 4 + }, + { + "d": 3, + "degree": 6, + "kappa": "151/100", + "separations": 4 + } + ], + "passed": true + } + }, + "mutant": null, + "object": "CL-ELDER-THIRD-ORDER-20261001-v1.1 controls", + "passed": true, + "scientific_effect": "NONE" +} diff --git a/frontiers/elder_third_order_20261001/SOURCES.json b/frontiers/elder_third_order_20261001/SOURCES.json new file mode 100644 index 000000000..80ab6b490 --- /dev/null +++ b/frontiers/elder_third_order_20261001/SOURCES.json @@ -0,0 +1,229 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "object": "CL-ELDER-THIRD-ORDER-20261001-v1.1", + "supersedes": "CL-ELDER-THIRD-ORDER-20261001-v1 (head 6da0715, PROOF blob f84b69eb)", + "status_update": "2026-10-01 15:30 UTC, after the nonauthor successor Slice C review 5380878588 (PASS_TECHNICAL, scope released): #187 merged (c2f1270) and listed as a merged input; Lemma S-prime states its range r <= r_0^* <= r_0^{[R]} <= 1 and the sign -Ht > 0 explicitly; control X8 adds a negative witness at r = 2; no mathematical change. Previous PROOF blob 736a35de at head e481d23.", + "kind": "author-side proof candidate: the elder lifetime density to third order in every d >= 2 up to its far part: nu_eld = c l^(-1/3) + c1 l^(1/4) + c2 l^(1/3) + nu_eld^{far,r_0^*}(l) + O(l^(4/11)) with 0 <= nu_eld^{far,r_0^*} <= C l^(1/3) (E3.0); hence nu_eld = c l^(-1/3) + c1 l^(1/4) + O(l^(1/3)) (a rate for (CU.1) of Math- #207), the lower bound nu_eld >= c l^(-1/3) + c1 l^(1/4) + c2 l^(1/3) - C l^(4/11), and, conditional on Math- #187 Theorem F at rho = r_0^*, nu_eld = c l^(-1/3) + c1 l^(1/4) + c2 l^(1/3) + O(l^(4/11)) with c2 the coefficient of Math- #216/#218; new Lemmas H and S-prime (the rescaled Hessian under the pins; E_Q[(W_r/r^2)e] <= C l^(2/3) r^(-2)(kappa + r)P^N); Corollary for the rejected density", + "author": "Anthropic Claude", + "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", + "read_at": { + "branch_base": "f9ebba17f5cc590232b2fb2cd37b04b996abc143" + }, + "consumed": [ + { + "path": "frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md", + "bytes": 17734, + "sha256": "380b7d0abdb0fe2de5a6564565af9560d3f1b1ce22fd5538927db0c52f4f3a4a", + "git_blob": "247b3ecf80bfbe896948d5d489b2d5842a81c481", + "tag": "R", + "use": "(R2)-(R5): pin covariance, regression, moments, pin densities; section 4 scaled Hessians" + }, + { + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "bytes": 40261, + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "tag": "P", + "use": "section 2 linear independence of distinct derivative functionals (also Lemma H, at two sites and at one site in a rotated frame); section 3 pin rows (3.1)-(3.3) (Lemma H); section 8 maximin and elder mark; sections 9-10 as [E2] (the near/far identity); section 15 parity factorization and (15.2)" + }, + { + "path": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", + "bytes": 1782, + "sha256": "bad7ef609c4ad8c41ad6af562c1b6807921e19a9d556ed793ad1a0db6e202028", + "git_blob": "213594d6ca6a86fb938110f4d166d9ce275a02d0", + "tag": "E1", + "use": "reading rule" + }, + { + "path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", + "bytes": 9062, + "sha256": "845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f", + "git_blob": "fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a", + "tag": "E2", + "use": "section 9 replacement" + }, + { + "path": "reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md", + "bytes": 23312, + "sha256": "451b9d7ffee072a73fc904cab891b6693e3f233808b89df10cce1b57036b65da", + "git_blob": "75da2597971510f843f8d90c743950cb8c177342", + "tag": "REC", + "use": "reading rule" + }, + { + "path": "frontiers/c7_total_bounded_20260929/PROOF.md", + "bytes": 14982, + "sha256": "16c0efe372c1b1f26460aaa109287fed78e6fbd2dd00a0530998db296278dd01", + "git_blob": "28748b086ec6761ef467dc67cba475fbdf8b7455", + "tag": "C7-K", + "use": "(K2): the fold-region elder deficit; section 4: 1 - e <= 1_{G_r^c}" + }, + { + "path": "frontiers/c7_zero_gap_limit_20260929/PROOF.md", + "bytes": 17592, + "sha256": "f0e563c45c41333f2bb6e5bf5cb98f0d3b592e2abf2af1c1b098c21ad77cb777", + "git_blob": "5b6328ea3d6afcbeb731698b3834e536f72d1bcb", + "tag": "Z", + "use": "(Z13)-(Z14): the change of variables in the near/far identity" + }, + { + "path": "frontiers/remainder_vanishing_20260930/PROOF.md", + "bytes": 25353, + "sha256": "0cb5b949261476f10e539677e2744e3288752474393af25ba787e67b1350f32a", + "git_blob": "441152dfc1d8d00cb268cebdb0394212a5bfacdb", + "tag": "191", + "use": "Math- #191 (merged 2026-10-01, merge commit 9556547; the blob v1 consumed): Lemma E Steps 1-4 (expansions), section 2 (2.1), r_0^*" + }, + { + "path": "frontiers/remainder_rate_20260930/PROOF.md", + "bytes": 33131, + "sha256": "0b690df6ac40707ca06783f5641d8b480277c716df75b1031d84ee53a0575f72", + "git_blob": "abfb98ae41d66a86d3cb094162db6547d0f29e7e", + "tag": "198", + "use": "Math- #198 (merged 2026-10-01, merge commit 124c37d; the blob v1 consumed): (3.1) and the sign window of section 3 (own-jet form (F1)); Lemma B barrier (1.2) and the section 1 elder-density identity; Lemma W (W.1); the far integral (2.1); Lemma F-prime" + }, + { + "path": "frontiers/far_elder_rate_20260930/PROOF.md", + "bytes": 16493, + "sha256": "ed908ed97348ed708c6fd06e5c09f6290ab0e8c47e6384b7bdded321452f523b", + "git_blob": "072601145601a1021037a2e91bf8826c1c971ecc", + "tag": "187", + "use": "Math- #187 (merged 2026-10-01 13:34 UTC, merge commit c2f1270; the blob v1.1 consumed since its rebind): Theorem F at the single separation rho = r_0^* (far elder density O(l^(2/3))), for (E3.3) and Corollary E3-prime(3) only" + } + ], + "consumed_unmerged": [ + { + "path": "frontiers/cusp_second_order_20261001/PROOF.md", + "bytes": 52605, + "sha256": "cffc1b83ac364da58bd650c3c301ea1babd38e19af54f74010bdc120edce38a8", + "git_blob": "f6df5a7356a54771b0052e42a864a140709903ad", + "tag": "207", + "use": "section 0 cusp objects; proof of Theorem CU.1; Theorem CU.2; structure of Proposition CU.3 (re-proved quantitatively); section 6 (6.1), (CU.2)", + "head": "b12ff464b3534b6899a90cc250c585b1caf5dfec", + "pr": "Math- #207" + }, + { + "path": "frontiers/candidate_third_order_20261001/PROOF.md", + "bytes": 37220, + "sha256": "6c1279164499d4fe2fbeee244b40dafa2159758d20f04826cd67d7602ea97fe4", + "git_blob": "70ca57ef05199e75417d7d57928c1e1c93bf944e", + "tag": "218", + "use": "Lemma D (also applied to the rescaled Hessian of Lemma H); the argument of (1.2); Lemma F Steps F1, F3, (F.2); Lemma C Steps C1, C2, C3; Lemma O; Theorem T (T.1); section 4 fold region and exponent ledger", + "head": "0cf048d18eb28a4ba37eba89c238a2910d4ca915", + "pr": "Math- #218" + } + ], + "cited_only": [], + "cited_unmerged": [ + { + "path": "frontiers/third_order_coefficient_20261001/NOTE.md", + "bytes": 24186, + "sha256": "ae15c0ee173b9d01d258536a11780cc4b128c57811d1fb5db9db391ffc759ee5", + "git_blob": "aa078a9cbfc3aa859c089596892e34a8293831eb", + "tag": "216", + "use": "numerical values of c2; the elder-pair Monte Carlo row (Remark 3, exploration)", + "head": "04c08e1534122f210be888742fcd7a568e45b097", + "pr": "Math- #216" + }, + { + "path": "frontiers/far_elder_flat_ridge_20260930/PROOF.md", + "bytes": 22806, + "sha256": "957f9c5e6557a558b2c055fa2a1f11ba301581995b8958658fad2edf47136f57", + "git_blob": "50cfbf4fcb9a3526f979eaedf885d42824a3c3a3", + "tag": "188", + "use": "Theorem G, an alternative far elder bound O(l^N) for rho in (0, L/4] (Remark 2)", + "head": "85f0586a468c2b2f73af0e340d251e33a52caade", + "pr": "Math- #188" + } + ], + "cited_external": [ + { + "tag": "Haynsworth", + "reference": "E. V. Haynsworth, inertia additivity of the Schur complement (1968)", + "use": "through #218 Lemma C, Step C1 (fact (F2))" + }, + { + "tag": "Anderson", + "reference": "T. W. Anderson, The integral of a symmetric unimodal function over a symmetric convex set and some probability inequalities, Proc. Amer. Math. Soc. 6 (1955) 170-176", + "use": "Lemma H (b), as in the argument of #218 (1.2)" + }, + { + "tag": "Weyl", + "reference": "Weyl integration formula on symmetric matrices", + "use": "through #218 Lemma D (fact (F5))" + } + ], + "mutants": [ + "M1", + "M2", + "M3", + "M4", + "M5", + "M6", + "M7", + "M8" + ], + "replayed": [ + "e3_check.py" + ], + "referee": { + "kind": "clean-context same-family referee (Anthropic Claude subagent), before submission of v1, with a delta check of the revision", + "verdict": "ACCEPT WITH MINOR FIXES (no major finding; four minor findings and nine nits, all applied); delta check of the revision: ACCEPT", + "report": "project archive V2_2/frontiers_elder_third_order_20261001/REFEREE_1.md", + "report_sha256": "0af4192a773d12dd14f38bdf53a731053728b2a055c90e9dfbc2a5101c824c36", + "report_bytes": 36560, + "exploration": "the referee tested Lemma Q by a 2D union-find maximin on 48 exactly pinned fields (floating point): 48 of 48 agree", + "independence": "same provider and GitHub account as the author; zero organizational independence" + }, + "referee_v1_1": { + "kind": "clean-context same-family referee (Anthropic Claude subagent) of the v1 -> v1.1 delta against all eight sources at their declared blobs, with a delta check of the fixes", + "verdict": "ACCEPT WITH MINOR FIXES (no major finding; one minor finding and eleven nits, all applied); delta check of the fixes: ACCEPT", + "report": "project archive V2_2/frontiers_elder_third_order_20261001/REFEREE_2.md", + "report_sha256": "9d93d25f17e494e84956af2578b115ddee7d9f4c1f258da2dcf33d0be0453b03", + "report_bytes": 26106, + "independent_checks": "(H.1) by Peano kernels (sympy); Lemma H covariance numerically: the direct and segment forms of H-tilde agree to 7e-11 for the Gaussian kernel (two representations sharing one covariance code) and reproduce the author mpmath exploration (raw pins); the segment form also on tori L = 2, 3, 6 (d = 2) and L = 3 (d = 3) (floating point); the eps^2 mechanism of Lemma S-prime by Monte Carlo; the section 4 ledger in exact rationals; all controls and mutants", + "independence": "same provider and GitHub account as the author; zero organizational independence" + }, + "nonauthor_reviews_of_v1_1": { + "on": "Math- #220 at head e481d23 (PROOF blob 736a35de; sections 1-4 byte-identical to b229143 / 5dec8985)", + "reviews": [ + "OpenAI / Codex (delegated, agent /root/review_density_proof_gaps): successor Slice C, Lemmas H and S-prime and the sections 3-4 assembly, PASS_TECHNICAL, no blocking defect (review 5380878588); OA-220-B-01 resolved, OA-220-C-01 superseded", + "OpenAI / Codex: v1 -> v1.1 delta of slices A/B verified, A/B conclusions preserved (comment 5932298017)" + ] + }, + "nonauthor_reviews_of_v1": { + "on": "Math- #220 at head 6da0715 (PROOF blob f84b69eb)", + "reviews": [ + "OpenAI / Codex (delegated, agent /root/review_density_proof_gaps): Slice A PASS_TECHNICAL (review 5379101929); Slice B PASS_TECHNICAL with amendment OA-220-B-01 (review 5379015767); Slice C PASS_TECHNICAL with amendment OA-220-C-01 (review 5379186710)", + "xAI: sympy check of the Lemma Q ridge identities (review 5379144440)" + ], + "amendments": { + "OA-220-B-01": "applied in v1.1: Lemma G (b) assumes E[H(E)] < infinity; Step E6 records why it holds", + "OA-220-C-01": "superseded in v1.1: v1 Remark 2 shrinking cut-off removed; the near/far cut is the fixed r_0^*" + } + }, + "delivered_under": "explicit owner instructions of Dylan Roy in claude.ai session session_01NMeKEismAyeqgdB4sy2NJU, given after OWNER_STOP (2026-09-27): 2026-09-30 \"Continue to Work on closing as many mathematical items as possible while working with and supporting the other models in the GitHub. Also advance the mathematics in every place that's justified based on what we currently know\", followed by \"Continue\"; standing: \"Any request or permissions are preapproved in advance by me Dylan Roy\", pull requests only, never self-merge, no register/GRAPH/STATUS/lemma_closed/prize/premise edits, OWNER_STOP.md untouched. OWNER_STOP.md addresses Cursor agents and is untouched; nothing is merged by its author.", + "files": [ + { + "path": "PROOF.md", + "bytes": 70544, + "sha256": "74b5f031ba5be6f50b5e543636136df1d9b5fad0fcd2c8210320cfef02f80e37" + }, + { + "path": "README.md", + "bytes": 7913, + "sha256": "4010d885a8fdff55601f067e5504c9736edb40f4f34bef3b402ca8ce01020722" + }, + { + "path": "e3_check.py", + "bytes": 31425, + "sha256": "ffedf4dc3ea5e64a27f8cd77531c1e1524ac76bda5addddaab181f213c0650cc" + }, + { + "path": "RESULTS.json", + "bytes": 3533, + "sha256": "3390d0fc2fd74138fb34b6d5447c7d56191ffc4257fe9ba3985786d1ab661fb1" + } + ] +} diff --git a/frontiers/elder_third_order_20261001/e3_check.py b/frontiers/elder_third_order_20261001/e3_check.py new file mode 100644 index 000000000..b5f04a87f --- /dev/null +++ b/frontiers/elder_third_order_20261001/e3_check.py @@ -0,0 +1,705 @@ +#!/usr/bin/env python3 +"""Exact controls for CL-ELDER-THIRD-ORDER-20261001-v1.1 (frontiers/elder_third_order_20261001/PROOF.md). +Standard library only, exact rationals. Run: python3 -B -S e3_check.py (and with -O; output byte-identical). +Mutants: --mutant M1|...|M8 must exit 1; an unknown label exits 2. + + X1 the exponent ledger of section 4 (rho_f = l^(1/4+1/44), rho_c = l^(1/4-1/36), a = l^(2/15)): least exponent 4/11, + attained exactly by rho_f^5/l and l^2 rho_f^-6; the intermediate terms l^2 rho_c^-7 and a^3 (on [rho_c, a], from + #198 (W.1)) and l^(5/3) a^-7 and l^(2/3) a^-2 (on [a, r0*], from Lemma S'), all above 4/11, least 2/5; the order + rho_f < rho_c < a; k <= l^(1/3) on [rho_c, r0*]; kappa <= l^(7/15) <= 1 on [a, r0*]; a balances a^3 and + l^(2/3) a^-2 + X2 the ridge identities (M1), (M5) of Lemma Q as polynomial identities in Q[X, phi], and the closed forms (M4) of + g(X3) at 401 rational phi (each side times 16 phi^3 is a polynomial of degree <= 8 in phi, so this is an identity) + X3 the margins (M2)-(M4): the factorizations (phi+1)^3 - 8 phi^3 = (1-phi)(7phi^2+4phi+1) and + (1+psi)^3 - 64 psi^3 = (1-3psi)(21psi^2+6psi+1); the margin inequalities on dense rational grids; sharpness of 3/2 + X4 the one-dimensional decision of Step Q6 under perturbations h = s (X^2-1/4)^2 q(X), scaled by rigorous coefficient + bounds to sup|h''| <= kappa/4 and sup|h| < (3/2) kappa ||phi| - 1/3|: the path and trap inequalities of each case + hold exactly on a rational grid of [-3, 2] + X5 Lemma CU.1' mechanism: on exactly pinned polynomial fields (d = 2: degree 6, 7; d = 3: degree 6) with k = kappa r, + every monomial r^a X^i Xi^j of (rescaled field) - (cusp polynomial) has a >= 1 and |j| <= a + 1, attained + X6 Lemma S (Schur complements) on random rational instances and an extremal one (rigorous rational lower bounds for + the square roots on the right side); the two polynomial bounds of Step Q2, coefficientwise + X7 pointwise facts: 0 <= loss <= 9 Y^2 and loss = 36 k^2 D^2 - w_eld; the Lemma O' domination; the B_5 bound + w <= 12 kappa |D| tau when |Y_r| < 6 kappa |D| < |Y'| and |Y_r - Y'| <= tau + X8 Lemma S' linear algebra: for -Ht = O diag(lam) O^T (rational orthogonal O by the Cayley transform, d = 2, 3, 4) + and H_M = Lam_r Ht Lam_r, Lam_r = diag(r, 1, ..., 1): det H_M = r^2 det Ht, and -H_M - r^2 lam_min(-Ht) I is positive + semidefinite (all principal minors >= 0), so lam_min(-H_M) >= r^2 lam_min(-Ht), with a singular (attained) case at + Ht = -I, r = 1/2; |det Ht| <= lam_min ||Ht||^(d-1); and a negative witness at r = 2 (-Ht = diag(1, 2)), where the + r^2 bound fails, so the range r <= r_0^* <= 1 is necessary + X9 Lemma H's exact form (H.1) on exactly pinned polynomial fields (d = 2: degree 6, 7; d = 3: degree 6; k = kappa r) + at several rational r: r^-2 f_uu(M) = -6 kappa + int_0^1 s (1-s)^2 f_uuuu(M + r s u) ds and + r^-1 f_u,theta(M) = -int_0^1 (1-s) f_uu,theta(M + r s u) ds; and, as polynomials in r, the r = 0 values + -6 kappa + f4/12, -gamma/2 and A +""" +import argparse +import json +import random +import sys +from fractions import Fraction as Fr +from math import factorial, isqrt + +MUTANT = None + + +# ----------------------------------------------------------------------------------------------- X1 exponents +def x1(): + q = Fr(1, 4) + ef, ec = q + Fr(1, 44), q - Fr(1, 36) + if MUTANT == 'M1': + ec = q - Fr(1, 120) + ea = Fr(1, 5) if MUTANT == 'M8' else Fr(2, 15) # the split point a = l^ea of I^eld + core = {'rho_f^2': 2 * ef, 'rho_f^5/l': 5 * ef - 1, 'l rho_f^-2': 1 - 2 * ef, 'l^2 rho_f^-6': 2 - 6 * ef, + 'rho_c^2': 2 * ec, 'l^2 rho_c^-7': 2 - 7 * ec} + # I^eld on [rho_c, a]: int (kappa^2 + r^2) dr, kappa = l r^-4 -> l^2 rho_c^-7 / 7 + a^3 / 3 + # I^eld on [a, r0*]: int l^(2/3) (l r^-8 + r^-3) dr -> l^(5/3) a^-7 / 7 + l^(2/3) a^-2 / 2 + inter = {'[rho_c,a]: l^2 rho_c^-7': 2 - 7 * ec, '[rho_c,a]: a^3': 3 * ea, + '[a,r0*]: l^(5/3) a^-7': Fr(5, 3) - 7 * ea, '[a,r0*]: l^(2/3) a^-2': Fr(2, 3) - 2 * ea} + allt = dict(core) + allt.update(inter) + least = min(allt.values()) + ok = least == Fr(4, 11) and sorted(k for k, v in allt.items() if v == least) == ['l^2 rho_f^-6', 'rho_f^5/l'] + ok &= all(v > Fr(4, 11) for v in inter.values()) and min(inter.values()) == Fr(2, 5) + ok &= ef > ec > ea > 0 # rho_f < rho_c < a for l < 1 + ok &= 1 - 3 * ec == Fr(1, 3) # k = l r^-3 <= l^(1/3) on [rho_c, r0*] + ok &= 1 - 4 * ea == Fr(7, 15) and ea <= q # kappa = l r^-4 <= l^(7/15) <= 1 on [a, r0*] + ok &= 3 * ea == Fr(2, 3) - 2 * ea # a balances a^3 against l^(2/3) a^-2 + ok &= ef > q > ec and 1 - 3 * ef >= 0 and Fr(4, 11) > Fr(1, 3) and Fr(2, 5) < Fr(4, 9) + return {'core': {k: str(v) for k, v in sorted(core.items())}, + 'intermediate': {k: str(v) for k, v in sorted(inter.items())}, 'split_exponent': str(ea), + 'least': str(least), 'passed': bool(ok)} + + +# ----------------------------------------------------------------------------------------------- polynomials in (X, phi) +def padd2(a, b): + o = dict(a) + for k, v in b.items(): + o[k] = o.get(k, 0) + v + return {k: v for k, v in o.items() if v != 0} + + +def pmul2(a, b): + o = {} + for (i, j), u in a.items(): + for (k, l), v in b.items(): + o[(i + k, j + l)] = o.get((i + k, j + l), 0) + u * v + return {k: v for k, v in o.items() if v != 0} + + +def psc2(a, c): + return {k: c * v for k, v in a.items() if c * v != 0} + + +def cst(c): + return {(0, 0): Fr(c)} if c != 0 else {} + + +XX = {(1, 0): Fr(1)} +PH = {(0, 1): Fr(1)} + + +def pw2(a, n): + o = cst(1) + for _ in range(n): + o = pmul2(o, a) + return o + + +def ev2(a, x, ph): + return sum(v * x ** i * ph ** j for (i, j), v in a.items()) + + +def dX(a): + return {(i - 1, j): i * v for (i, j), v in a.items() if i > 0} + + +XP, XM = padd2(XX, cst(Fr(1, 2))), padd2(XX, cst(Fr(-1, 2))) +G = padd2(psc2(pmul2(pw2(XP, 2), padd2(XX, cst(-1))), 2), psc2(pmul2(PH, pw2(pmul2(XP, XM), 2)), 3)) # g / kappa + + +def g_val(x, ph): + return ev2(G, x, ph) + + +def x2(): + ok = True + r1 = pmul2(pw2(XM, 2), padd2(psc2(padd2(XX, cst(1)), 2), psc2(pmul2(PH, pw2(XP, 2)), 3))) + ok &= padd2(G, cst(1)) == r1 + r2 = pmul2(pw2(XP, 2), padd2(psc2(padd2(XX, cst(-1)), 2), psc2(pmul2(PH, pw2(XM, 2)), 3))) + ok &= G == r2 + ok &= dX(G) == psc2(pmul2(pmul2(XP, XM), padd2(cst(1), psc2(pmul2(PH, XX), 2))), 6) + vals = {} + for xv, a0, a1 in ((Fr(2), Fr(25, 2), Fr(675, 16)), (Fr(-3, 2), Fr(-5), Fr(12)), (Fr(-3), Fr(-50), Fr(3675, 16))): + lin = {(0, j): v for (i, j), v in {(i, j): v * xv ** i for (i, j), v in G.items()}.items()} + coeff = {} + for (i, j), v in G.items(): + coeff[j] = coeff.get(j, 0) + v * xv ** i + ok &= coeff.get(0, 0) == a0 and coeff.get(1, 0) == a1 and all(j in (0, 1) for j in coeff if coeff[j] != 0) + vals[str(xv)] = [str(a0), str(a1)] + n_ok = 0 + for n in range(-200, 201): + ph = Fr(n, 200) + if ph == 0: + continue + x3 = -1 / (2 * ph) + a = 16 * ph ** 3 * (g_val(x3, ph) + 1) == (ph + 1) ** 3 * (3 * ph - 1) + b = 16 * ph ** 3 * g_val(x3, ph) == (ph - 1) ** 3 * (3 * ph + 1) + ok &= a and b + n_ok += a and b + return {'factorizations': True if ok else False, 'g_at_points': vals, 'X3_closed_forms_at_rational_phi': n_ok, + 'passed': bool(ok and n_ok == 400)} + + +# ----------------------------------------------------------------------------------------------- X3 margins +def poly1(coeffs): + return {i: Fr(c) for i, c in enumerate(coeffs) if c != 0} + + +def pmul1(a, b): + o = {} + for i, u in a.items(): + for j, v in b.items(): + o[i + j] = o.get(i + j, 0) + u * v + return {k: v for k, v in o.items() if v != 0} + + +def padd1(a, b): + o = dict(a) + for k, v in b.items(): + o[k] = o.get(k, 0) + v + return {k: v for k, v in o.items() if v != 0} + + +def x3(): + ok = True + c = Fr(8, 5) if MUTANT == 'M2' else Fr(3, 2) + one_plus = poly1([1, 1]) + lhs = padd1(pmul1(pmul1(one_plus, one_plus), one_plus), poly1([0, 0, 0, -8])) + ok &= lhs == pmul1(poly1([1, -1]), poly1([1, 4, 7])) + lhs2 = padd1(pmul1(pmul1(one_plus, one_plus), one_plus), poly1([0, 0, 0, -64])) + ok &= lhs2 == pmul1(poly1([1, -3]), poly1([1, 6, 21])) + ok &= 4 * 4 - 4 * 7 < 0 and 6 * 6 - 4 * 21 < 0 # 7x^2+4x+1 and 21x^2+6x+1 have no real roots + worst = None + for n in range(0, 2001): + ph = Fr(1, 3) + Fr(2, 3) * Fr(n, 2000) # R+ margin, and (with psi = |phi|) the R- margin + v = (ph + 1) ** 3 * (3 * ph - 1) / (16 * ph ** 3) + ok &= v >= c * (ph - Fr(1, 3)) + if n: + ratio = v / (ph - Fr(1, 3)) + worst = ratio if worst is None else min(worst, ratio) + ok &= g_val(-1 / (2 * ph), ph) + 1 == v + ok &= -g_val(1 / (2 * ph), -ph) == v # phi -> -phi: |g(X3)| on the R- side + sharp = (Fr(2) ** 3 * 2 / 16) == Fr(3, 2) * Fr(2, 3) # equality at phi = 1 + for n in range(0, 1001): + ps = Fr(1, 4) + Fr(1, 12) * Fr(n, 1000) # local maximum X3 in (3/2, 2] for -1/3 <= phi < -1/4 + ok &= (ps + 1) ** 3 * (1 - 3 * ps) / (16 * ps ** 3) >= 12 * (Fr(1, 3) - ps) + for n in range(-100, 101): # (M2) on [-1/2, X_R], |phi| <= 1/3 + ph = Fr(n, 300) + xr = Fr(2) if ph >= Fr(-1, 4) else -1 / (2 * ph) + for t in range(0, 301): + x = Fr(-1, 2) + (xr + Fr(1, 2)) * Fr(t, 300) + ok &= 2 * (x + 1) + 3 * ph * (x + Fr(1, 2)) ** 2 >= 1 + for n in range(-300, 101): # (M3) on [-3/2, 1/2], phi <= 1/3 + ph = Fr(n, 300) + for t in range(0, 201): + x = Fr(-3, 2) + 2 * Fr(t, 200) + ok &= 2 * (x - 1) + 3 * ph * (x - Fr(1, 2)) ** 2 <= -1 + # (M5) thresholds + ok &= Fr(25, 2) + Fr(675, 16) * Fr(-1, 4) == Fr(125, 64) and Fr(25, 2) + Fr(675, 16) * Fr(-1, 3) == Fr(-25, 16) + ok &= Fr(-5) + 12 * Fr(-1, 3) == -9 and Fr(-50) + Fr(3675, 16) * Fr(1, 3) == Fr(425, 16) + return {'margin_constant': str(c), 'min_ratio_over_grid': str(worst), 'sharp_at_phi_1': bool(sharp), + 'passed': bool(ok and sharp)} + + +# ----------------------------------------------------------------------------------------------- X4 decision in 1D +def sup_bound(coeffs): # rigorous bound of sup_{[-3,2]} |sum c_i X^i| + return sum(abs(c) * Fr(3) ** i for i, c in enumerate(coeffs)) + + +def pmulc(p, q): + o = [Fr(0)] * (len(p) + len(q) - 1) + for i, a in enumerate(p): + for j, b in enumerate(q): + o[i + j] += a * b + return o + + +def deriv(p): + return [i * p[i] for i in range(1, len(p))] or [Fr(0)] + + +def evalc(p, x): + return sum(c * x ** i for i, c in enumerate(p)) + + +def x4(rng): + thr = Fr(9, 25) if MUTANT == 'M3' else Fr(1, 3) + base = pmulc([Fr(-1, 4), Fr(0), Fr(1)], [Fr(-1, 4), Fr(0), Fr(1)]) # (X^2 - 1/4)^2 + grid = [Fr(-3) + Fr(5) * Fr(t, 500) for t in range(501)] + ok = True + counts = {'E': 0, 'R+': 0, 'R-': 0} + phis = [Fr(n, 60) for n in range(-60, 61) if abs(abs(Fr(n, 60)) - Fr(1, 3)) > 0] + [Fr(7, 20), Fr(-7, 20)] + for ph in phis: + for trial in range(3): + kap = Fr(rng.randint(1, 400), 100) + q = [Fr(rng.randint(-50, 50), 25) for _ in range(3)] + h0 = pmulc(base, q) + m0 = sup_bound(h0) + m2 = sup_bound(deriv(deriv(h0))) + margin = Fr(3, 2) * kap * abs(abs(ph) - Fr(1, 3)) + if m0 == 0 or m2 == 0: + continue + s = min(kap / 4 / m2, margin / m0 * Fr(99, 100)) + s *= rng.choice((1, -1)) * Fr(rng.randint(50, 100), 100) + h = [s * c for c in h0] + gk = lambda x: kap * g_val(x, ph) + evalc(h, x) + if abs(ph) < thr: # case E + counts['E'] += 1 + xr = Fr(2) if ph >= Fr(-1, 4) else -1 / (2 * ph) + ok &= all(gk(x) + kap >= 0 for x in grid if Fr(-1, 2) <= x <= xr) + ok &= gk(xr) > 0 and gk(Fr(-3, 2)) < -kap + ok &= all(gk(x) <= 0 for x in grid if Fr(-3, 2) <= x <= Fr(1, 2)) + elif ph > 0: # case R+ + counts['R+'] += 1 + ok &= all(gk(x) > -kap for x in grid if x <= Fr(-1, 2)) and gk(Fr(-3)) > 0 + else: # case R- + counts['R-'] += 1 + ok &= all(gk(x) <= 0 for x in grid if Fr(-3, 2) <= x <= 2) + ok &= gk(Fr(-3, 2)) < -Fr(5, 4) * kap and gk(Fr(2)) < -Fr(5, 4) * kap + return {'threshold': str(thr), 'cases': counts, 'grid_points': len(grid), 'passed': bool(ok)} + + +# ----------------------------------------------------------------------------------------------- X5 pinned polynomials +def padd(p, q): + out = list(p) + [Fr(0)] * max(0, len(q) - len(p)) + for i, c in enumerate(q): + out[i] += c + return out + + +def pmul(p, q): + out = [Fr(0)] * (len(p) + len(q) - 1) + for i, a in enumerate(p): + if a: + for j, b in enumerate(q): + out[i + j] += a * b + return out + + +def pscale(p, c): + return [c * x for x in p] + + +def rpow(n): + return [Fr(0)] * n + [Fr(1)] + + +def axis_odd_sum(c, D, h, shift, skip): + out = [Fr(0)] + for i in range(1, D + 2, 2): + key = c.get(i + shift) + if key is None or i + shift == skip: + continue + out = padd(out, pmul(pscale(rpow(i - 1), h ** (i - 1) / factorial(i)), key)) + return out + + +def axis_even_sum(c, D, h, skip): + out = [Fr(0)] + for i in range(0, D + 2, 2): + key = c.get(i) + if key is None or i == skip: + continue + out = padd(out, pmul(pscale(rpow(i), h ** i / factorial(i)), key)) + return out + + +def pinned_field(free, b, kpoly, D, m): + """free Taylor coefficients (f = sum c_a x^i y^j / (i! j!)); returns all coefficients as polynomials in r, the + pinned ones solved exactly from the pin rows of [R] section 2 with gap parameter k = kpoly(r)""" + c = {key: [val] for key, val in free.items()} + h = Fr(1, 2) + z = (0,) * m + ax = {i: c[(i,) + z] for i in range(D + 1) if (i,) + z in c} + ax[2] = pscale(axis_odd_sum(ax, D, h, 1, 2), Fr(-1)) + rest = [Fr(0)] + for j in range(5, D + 1, 2): + if j in ax: + rest = padd(rest, pmul(pscale(rpow(j - 3), Fr(12 * (j - 1)) * h ** (j - 1) / factorial(j)), ax[j])) + ax[3] = padd(pscale(kpoly, Fr(12)), pscale(rest, Fr(-1))) + ax[1] = padd(pscale(pmul(rpow(2), kpoly), Fr(-1)), pscale(axis_odd_sum(ax, D, h, 0, 1), Fr(-1))) + ax[0] = padd(padd([b], pscale(pmul(rpow(3), kpoly), Fr(-1, 2))), pscale(axis_even_sum(ax, D, h, 0), Fr(-1))) + for i in range(4): + c[(i,) + z] = ax[i] + for l in range(m): + e = tuple(1 if t == l else 0 for t in range(m)) + tr = {i: c[(i,) + e] for i in range(D) if (i,) + e in c} + c[(0,) + e] = pscale(axis_even_sum(tr, D, h, 0), Fr(-1)) + c[(1,) + e] = pscale(axis_odd_sum(tr, D, h, 0, 1), Fr(-1)) + return c + + +def multi_indices(d, D): + out = [] + + def rec(prefix, left, slots): + if slots == 0: + out.append(tuple(prefix)) + return + for v in range(left + 1): + rec(prefix + [v], left - v, slots - 1) + rec([], D, d) + return out + + +def x5(rng): + ok = True + rows = [] + for d, D in ((2, 6), (2, 7), (3, 6)): + m = d - 1 + unit = lambda l: tuple(1 if t == l else 0 for t in range(m)) + pinned = {(i,) + (0,) * m for i in range(4)} + for l in range(m): + pinned |= {(0,) + unit(l), (1,) + unit(l)} + for trial in range(3): + kap = Fr(rng.randint(1, 300), 100) + b = Fr(rng.randint(-300, 300), 97) + free = {a: Fr(rng.randint(-26, 26), 13) for a in multi_indices(d, D) if a not in pinned} + c = pinned_field(free, b, [Fr(0), kap], D, m) + F = {} + for a, poly in c.items(): + i, j = a[0], a[1:] + s = i + 2 * sum(j) - 4 + den = factorial(i) + for t in j: + den *= factorial(t) + for p, v in enumerate(poly): + if v: + F.setdefault(a, {}) + F[a][p + s] = F[a].get(p + s, 0) + v / den + z = (0,) * (m + 1) + F.setdefault(z, {}) + F[z][-4] = F[z].get(-4, 0) - b + P = {} + + def addp(a, v): + P[a] = P.get(a, 0) + v + f4 = free[(4,) + (0,) * m] + addp((3,) + (0,) * m, 2 * kap) + addp((1,) + (0,) * m, -3 * kap / 2) + addp(z, -kap / 2) + addp((4,) + (0,) * m, f4 / 24) + addp((2,) + (0,) * m, -f4 / 48) + addp(z, f4 / 384) + for l in range(m): + gl = free[(2,) + unit(l)] + addp((2,) + unit(l), gl / 2) + addp((0,) + unit(l), -gl / 8) + for l in range(m): + for q in range(l, m): + e = tuple(unit(l)[t] + unit(q)[t] for t in range(m)) + A = free[(0,) + e] + addp((0,) + e, A / 2 if l == q else A) + gap_min = None + nmono = 0 + for a in set(F) | set(P): + lp = dict(F.get(a, {})) + lp[0] = lp.get(0, 0) - P.get(a, 0) + for p, v in lp.items(): + if v == 0: + continue + nmono += 1 + j = sum(a[1:]) + lim = p if MUTANT == 'M4' else p + 1 + ok &= p >= 1 and j <= lim + gap = p + 1 - j + gap_min = gap if gap_min is None else min(gap_min, gap) + ok &= gap_min == 0 + rows.append({'d': d, 'degree': D, 'kappa': str(kap), 'monomials': nmono, 'min_slack': gap_min}) + return {'fields': rows, 'passed': bool(ok)} + + +# ----------------------------------------------------------------------------------------------- X6 Lemma S +def sqrt_lower(x): # rational lower bound of sqrt(x), x >= 0 rational + if x <= 0: + return Fr(0) + p, q = x.numerator, x.denominator + if isqrt(p) ** 2 == p and isqrt(q) ** 2 == q: # exact for rational squares + return Fr(isqrt(p), isqrt(q)) + scale = 10 ** 12 + return Fr(isqrt(int(x * scale * scale)), scale) + + +def matinv(M): + n = len(M) + A = [list(row) + [Fr(int(i == j)) for j in range(n)] for i, row in enumerate(M)] + for col in range(n): + piv = next(r for r in range(col, n) if A[r][col] != 0) + A[col], A[piv] = A[piv], A[col] + pv = A[col][col] + A[col] = [v / pv for v in A[col]] + for r in range(n): + if r != col and A[r][col] != 0: + f = A[r][col] + A[r] = [a - f * b for a, b in zip(A[r], A[col])] + return [row[n:] for row in A] + + +def quad(b, M, c): + return sum(b[i] * M[i][j] * c[j] for i in range(len(b)) for j in range(len(c))) + + +def neg_def(rng, m, lam): # D = -lam I - S^T S (so D <= -lam I) + S = [[Fr(rng.randint(-20, 20), 10) for _ in range(m)] for _ in range(m)] + return [[-lam * (i == j) - sum(S[t][i] * S[t][j] for t in range(m)) for j in range(m)] for i in range(m)] + + +def lemma_s_ok(a, b, D, a2, b2, D2, lam, coef): + s1 = a - quad(b, matinv(D), b) + s2 = a2 - quad(b2, matinv(D2), b2) + m = len(b) + nb = sqrt_lower(sum(x * x for x in b)) + nb2 = sqrt_lower(sum(x * x for x in b2)) + ndb = sqrt_lower(sum((x - y) ** 2 for x, y in zip(b, b2))) + E = [[D2[i][j] - D[i][j] for j in range(m)] for i in range(m)] + nE = sqrt_lower(sum(E[i][j] ** 2 for i in range(m) for j in range(m)) / m) # Frobenius/sqrt(m) <= operator norm + rhs = abs(a2 - a) + coef / lam * ndb * (nb + nb2) + Fr(2) / lam ** 2 * (nb * nb) * nE + return abs(s2 - s1) <= rhs + + +def x6(rng): + coef = Fr(1) if MUTANT == 'M5' else Fr(2) + ok = True + n = 0 + for m in (1, 2, 3): + for _ in range(300): + lam = Fr(rng.randint(1, 300), 100) + D = neg_def(rng, m, lam) + D2 = neg_def(rng, m, lam / 2) + b = [Fr(rng.randint(-60, 60), 20) for _ in range(m)] + b2 = [x + Fr(rng.randint(-30, 30), 40) for x in b] + a = Fr(rng.randint(-60, 60), 20) + a2 = a + Fr(rng.randint(-20, 20), 40) + ok &= lemma_s_ok(a, b, D, a2, b2, D2, lam, coef) + n += 1 + # extremal instance: m = 1, D = -lam, D' = -lam/2, a = a', b = 0, b' = delta: |s' - s| = 2 delta^2/lam + lam, dl = Fr(3, 2), Fr(1, 3) + ok &= lemma_s_ok(Fr(0), [Fr(0)], [[-lam]], Fr(0), [dl], [[-lam / 2]], lam, coef) + # Step Q2 polynomial bounds, coefficientwise in Gamma >= 0 + c0 = Fr(5, 4) * Fr(21, 16) + c1 = Fr(5, 4) * 12 + Fr(35, 8) * Fr(21, 16) + 2 + c2 = Fr(35, 8) * 12 + Fr(35, 4) + 18 + poly_ok = (c0, c1, c2) == (Fr(105, 64), Fr(2911, 128), Fr(317, 4)) and c0 <= 80 and c1 <= 160 and c2 <= 80 + sq = (Fr(25, 16), 2 * Fr(5, 4) * Fr(35, 8), Fr(35, 8) ** 2) # (5/4 + 35G/8)^2 + poly_ok &= sq[0] <= 80 and sq[1] <= 160 and sq[2] <= 80 + return {'random_instances': n, 'coefficient': str(coef), 'Q2_C2_poly': [str(c0), str(c1), str(c2)], + 'Q2_C0_poly': [str(x) for x in sq], 'passed': bool(ok and poly_ok)} + + +# ----------------------------------------------------------------------------------------------- X7 pointwise +def x7(rng): + ok = True + for _ in range(5000): + kap = Fr(rng.randint(1, 400), 100) + D = Fr(rng.randint(-300, 300), 100) or Fr(1, 7) + Y = Fr(rng.randint(-900, 900), 50) + weld = (36 * kap * kap * D * D - Y * Y) if abs(Y) < 2 * kap * abs(D) else Fr(0) + loss = Y * Y if abs(Y) < 2 * kap * abs(D) else 36 * kap * kap * D * D + ok &= 0 <= loss <= 9 * Y * Y and loss == 36 * kap * kap * D * D - weld + rej = (36 * kap * kap * D * D - Y * Y) if 2 * kap * abs(D) <= abs(Y) < 6 * kap * abs(D) else Fr(0) + ok &= rej <= (9 * Y * Y if abs(D) <= abs(Y) / (2 * kap) else 0) + phi = Y / (6 * kap * D) + ok &= (abs(phi) < Fr(1, 3)) == (abs(Y) < 2 * kap * abs(D)) + tau = Fr(rng.randint(0, 200), 100) + yr = Y + Fr(rng.randint(-100, 100), 100) * tau + if abs(yr) < 6 * kap * abs(D) < abs(Y): + ok &= 36 * kap * kap * D * D - yr * yr <= 12 * kap * abs(D) * tau + return {'trials': 5000, 'passed': bool(ok)} + + +# ----------------------------------------------------------------------------------------------- X8 Lemma S' linear algebra +def det(M): # exact determinant (fraction Gaussian elimination) + n = len(M) + A = [list(row) for row in M] + out = Fr(1) + for col in range(n): + piv = next((r for r in range(col, n) if A[r][col] != 0), None) + if piv is None: + return Fr(0) + if piv != col: + A[col], A[piv] = A[piv], A[col] + out = -out + pv = A[col][col] + out *= pv + for r in range(col + 1, n): + if A[r][col] != 0: + f = A[r][col] / pv + A[r] = [x - f * y for x, y in zip(A[r], A[col])] + return out + + +def psd_by_minors(M): # positive semidefinite iff all principal minors >= 0 + n = len(M) + for mask in range(1, 1 << n): + idx = [i for i in range(n) if mask >> i & 1] + if det([[M[i][j] for j in idx] for i in idx]) < 0: + return False + return True + + +def matmul(A, B): + return [[sum(A[i][t] * B[t][j] for t in range(len(B))) for j in range(len(B[0]))] for i in range(len(A))] + + +def transpose(A): + return [list(row) for row in zip(*A)] + + +def cayley(K): # (I - K)(I + K)^-1 is orthogonal for skew-symmetric K + n = len(K) + ipk = [[Fr(int(i == j)) + K[i][j] for j in range(n)] for i in range(n)] + imk = [[Fr(int(i == j)) - K[i][j] for j in range(n)] for i in range(n)] + return matmul(imk, matinv(ipk)) + + +def x8(rng): + ok = True + insts = [] + for d in (2, 3, 4): + for _ in range(40): + K = [[Fr(0)] * d for _ in range(d)] + for i in range(d): + for j in range(i + 1, d): + v = Fr(rng.randint(-9, 9), rng.randint(1, 5)) + K[i][j], K[j][i] = v, -v + lam = [Fr(rng.randint(1, 60), rng.randint(1, 12)) for _ in range(d)] + insts.append((cayley(K), lam, Fr(rng.randint(1, 20), 20))) + eye3 = [[Fr(int(i == j)) for j in range(3)] for i in range(3)] + insts.append((eye3, [Fr(1)] * 3, Fr(1, 2))) # Ht = -I, r = 1/2: equality in the uu-direction + fac_label = '1' if MUTANT == 'M6' else 'r^2' + extremal_singular = False + for idx, (O, lam, r) in enumerate(insts): + d = len(lam) + OtO = matmul(transpose(O), O) + ok &= all(OtO[i][j] == int(i == j) for i in range(d) for j in range(d)) + neg_ht = matmul(matmul(O, [[lam[i] if i == j else Fr(0) for j in range(d)] for i in range(d)]), transpose(O)) + ht = [[-v for v in row] for row in neg_ht] + dr = [[(r if i == 0 else Fr(1)) if i == j else Fr(0) for j in range(d)] for i in range(d)] + hm = matmul(matmul(dr, ht), dr) + ok &= det(hm) == r * r * det(ht) + fac = Fr(1) if MUTANT == 'M6' else r * r + lmin, lmax = min(lam), max(lam) + gap = [[-hm[i][j] - (fac * lmin if i == j else 0) for j in range(d)] for i in range(d)] + ok &= psd_by_minors(gap) + if idx == len(insts) - 1: # the extremal instance: the bound is attained + extremal_singular = det(gap) == 0 + ok &= extremal_singular + prod = Fr(1) + for v in lam: + prod *= v + ok &= abs(det(ht)) == prod and prod <= lmin * lmax ** (d - 1) + # negative witness (xAI review 5379839929): for r > 1 the r^2 factor fails, so Lemma S' uses r <= r_0^* <= 1 + w_neg = [[Fr(1), Fr(0)], [Fr(0), Fr(2)]] # -Ht = diag(1, 2), lam_min(-Ht) = 1 + rr = Fr(2) + w_hm = [[rr * rr * w_neg[0][0], Fr(0)], [Fr(0), w_neg[1][1]]] # -H_M = Lam (-Ht) Lam = diag(4, 2) + witness_fails = not psd_by_minors([[w_hm[i][j] - (rr * rr if i == j else 0) for j in range(2)] for i in range(2)]) + ok &= witness_fails + return {'instances': len(insts), 'loewner_factor': fac_label, 'extremal_singular': bool(extremal_singular), + 'range_witness_r2_fails': bool(witness_fails), + 'passed': bool(ok)} + + +# ----------------------------------------------------------------------------------------------- X9 Lemma H (H.1) +def pval(poly, r): + return sum(c * r ** i for i, c in enumerate(poly)) + + +def x9(rng): + ok = True + rows = [] + w4 = [Fr(0), Fr(0), Fr(1), Fr(-1)] if MUTANT == 'M7' else [Fr(0), Fr(1), Fr(-2), Fr(1)] # s(1-s)^2 + w2 = [Fr(1), Fr(-1)] # 1 - s + for d, D in ((2, 6), (2, 7), (3, 6)): + m = d - 1 + unit = lambda l: tuple(1 if t == l else 0 for t in range(m)) + z = (0,) * m + pinned = {(i,) + z for i in range(4)} + for l in range(m): + pinned |= {(0,) + unit(l), (1,) + unit(l)} + for trial in range(3): + kap = Fr(rng.randint(1, 300), 100) + b = Fr(rng.randint(-300, 300), 97) + free = {a: Fr(rng.randint(-26, 26), 13) for a in multi_indices(d, D) if a not in pinned} + c = pinned_field(free, b, [Fr(0), kap], D, m) + + def axis(p, beta, rr): # d_x^p d_y^beta f(x, 0) as {power of x: coefficient} + out = {} + for a, poly in c.items(): + if a[1:] == beta and a[0] >= p: + n = a[0] - p + out[n] = out.get(n, 0) + pval(poly, rr) / factorial(n) + return out + + def at(px, x): + return sum(v * x ** n for n, v in px.items()) + + def seg(px, w, rr): # int_0^1 w(s) P(rr (s - 1/2)) ds, exactly + tot, powx = [Fr(0)], [Fr(1)] + for n in range(max(px) + 1 if px else 1): + if n in px: + tot = padd(tot, pscale(powx, px[n])) + powx = pmul(powx, [-rr / 2, rr]) + return sum(v / (i + 1) for i, v in enumerate(pmul(tot, w))) + + for rr in (Fr(1, 3), Fr(2, 7), Fr(1, 2), Fr(1)): + xm, xs = -rr / 2, rr / 2 + f0, f1 = axis(0, z, rr), axis(1, z, rr) + ok &= at(f0, xm) == b and at(f0, xs) == b - kap * rr ** 4 and at(f1, xm) == 0 and at(f1, xs) == 0 + for l in range(m): + fy = axis(0, unit(l), rr) + ok &= at(fy, xm) == 0 and at(fy, xs) == 0 + ok &= at(axis(2, z, rr), xm) / rr ** 2 == -6 * kap + seg(axis(4, z, rr), w4, rr) + for l in range(m): + ok &= at(axis(1, unit(l), rr), xm) / rr == -seg(axis(2, unit(l), rr), w2, rr) + + def axis_poly(p, beta): # d_x^p d_y^beta f(M), M = -r/2, as a polynomial in r + out = [Fr(0)] + for a, poly in c.items(): + if a[1:] == beta and a[0] >= p: + n = a[0] - p + out = padd(out, pmul(poly, pscale(rpow(n), Fr(-1, 2) ** n / factorial(n)))) + return out + + huu = axis_poly(2, z) + ok &= huu[0] == 0 and huu[1] == 0 and huu[2] == -6 * kap + free[(4,) + z] / 12 + for l in range(m): + hut = axis_poly(1, unit(l)) + ok &= hut[0] == 0 and hut[1] == -free[(2,) + unit(l)] / 2 + for q2 in range(l, m): + e = tuple(unit(l)[t] + unit(q2)[t] for t in range(m)) + ok &= axis_poly(0, e)[0] == free[(0,) + e] + rows.append({'d': d, 'degree': D, 'kappa': str(kap), 'separations': 4}) + return {'fields': rows, 'passed': bool(ok)} + + +def main(): + global MUTANT + ap = argparse.ArgumentParser() + ap.add_argument('--mutant', default=None) + args = ap.parse_args() + if args.mutant is not None and args.mutant not in ('M1', 'M2', 'M3', 'M4', 'M5', 'M6', 'M7', 'M8'): + sys.stderr.write('unknown mutant label\n') + return 2 + MUTANT = args.mutant + rng = random.Random(20261001) + out = {'object': 'CL-ELDER-THIRD-ORDER-20261001-v1.1 controls', 'scientific_effect': 'NONE', 'mutant': MUTANT, + 'checks': {'X1_exponent_ledger': x1(), 'X2_ridge_identities': x2(), 'X3_margins': x3(), + 'X4_decision_1d': x4(rng), 'X5_weighted_taylor': x5(rng), 'X6_lemma_S': x6(rng), + 'X7_pointwise': x7(rng), 'X8_lemma_S_prime_algebra': x8(rng), + 'X9_lemma_H_exact_form': x9(rng)}} + out['passed'] = all(v['passed'] for v in out['checks'].values()) + sys.stdout.write(json.dumps(out, indent=1, sort_keys=True) + '\n') + return 0 if out['passed'] else 1 + + +if __name__ == '__main__': + sys.exit(main())