From 15cf419ff97b08ce0aedf901ee684ac1f0980971 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 1 Oct 2026 15:04:29 +0000 Subject: [PATCH 1/2] Third-order lifetime laws with remainder l^(3/7): candidate and elder densities (Theorems T+ and E3+) Author-side proof candidate; scientific effect NONE; nonauthor review required. Improves the O(l^(4/11)) remainders of Math- #218 (Theorem T) and #220 (Theorem E3) to O(l^(3/7)) in every d >= 2: - Lemma L: (c^2 - y^2)_+ is locally Lipschitz with constant |y| + |y'|, free of c = 6 kappa |det A|; used in #218 Step C2 and #220 Step E3, it removes the factor (1 + kappa)^2 (Lemma C+: error r(1 + kappa)). - A refined bound on the elder decision's edge window B_4: |f4| >= 6 kappa or lambda <= |gamma|^2/(2 kappa), so O(r kappa) instead of O(r kappa^2) (Lemma CE+: error r(1 + kappa) + kappa^2 r^(3/2) + kappa^3 r^2). - Proposition W+: the typed window costs its conditional probability, E_Q[W_r/r^2] <= C r^2 (kappa + r)^2 (kappa + r log(2/r)) P^N for k <= r; the intermediate elder mass is O(l^(4/9) log(1/l)), and the equal-height kernel is O(r^3 log(2/r)) near the diagonal. With rho_f = l^(2/7), rho_c = l^(2/9), a = l^(1/9) the least exponent is 3/7. With merged #187: nu_eld = c l^(-1/3) + c1 l^(1/4) + c2 l^(1/3) + O(l^(3/7)) and rho_rej = B + (I^cand - c1) l^(1/4) + O(l^(3/7)). Consumes unmerged #207, #218, #220 at pinned blobs; merged #187, #191, #198. Clean-context same-family referee: ACCEPT WITH MINOR FIXES (no major), all findings applied; delta check accepted after one README correction. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .github/workflows/third-order-rate.yml | 159 ++++++ frontiers/third_order_rate_20261001/PROOF.md | 471 ++++++++++++++++++ frontiers/third_order_rate_20261001/README.md | 85 ++++ .../third_order_rate_20261001/RESULTS.json | 84 ++++ .../third_order_rate_20261001/SOURCES.json | 233 +++++++++ .../third_order_rate_20261001/r37_check.py | 347 +++++++++++++ 6 files changed, 1379 insertions(+) create mode 100644 .github/workflows/third-order-rate.yml create mode 100644 frontiers/third_order_rate_20261001/PROOF.md create mode 100644 frontiers/third_order_rate_20261001/README.md create mode 100644 frontiers/third_order_rate_20261001/RESULTS.json create mode 100644 frontiers/third_order_rate_20261001/SOURCES.json create mode 100644 frontiers/third_order_rate_20261001/r37_check.py diff --git a/.github/workflows/third-order-rate.yml b/.github/workflows/third-order-rate.yml new file mode 100644 index 000000000..333fcf109 --- /dev/null +++ b/.github/workflows/third-order-rate.yml @@ -0,0 +1,159 @@ +name: Third-order rate 3/7 exact controls + +'on': + pull_request: + paths: + - 'frontiers/third_order_rate_20261001/**' + - '.github/workflows/third-order-rate.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/far_elder_rate_20260930/PROOF.md' + - 'frontiers/cusp_second_order_20261001/PROOF.md' + - 'frontiers/candidate_third_order_20261001/PROOF.md' + - 'frontiers/elder_third_order_20261001/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/third_order_rate_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 (as on #220, after Copilot's review there): 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 / 'r37_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/third_order_rate_20261001/PROOF.md b/frontiers/third_order_rate_20261001/PROOF.md new file mode 100644 index 000000000..4f6dbf252 --- /dev/null +++ b/frontiers/third_order_rate_20261001/PROOF.md @@ -0,0 +1,471 @@ +# The third-order lifetime laws with remainder `ℓ^{3/7}`: candidate and elder densities in every `d ≥ 2` + +Object: CL-THIRD-ORDER-RATE-20261001-v1. +Author: Anthropic Claude (claude.ai session `session_01NMeKEismAyeqgdB4sy2NJU`), 1 October 2026. +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. + +**What is new.** Math- #218 (Theorem T) and Math- #220 (Theorem E3) expand the candidate and elder lifetime densities +to third order with remainder `O(ℓ^{4/11})`. This note improves both remainders to `O(ℓ^{3/7})`. It adds three +ingredients. +- **Lemma L** (§1). The cusp weight `y ↦ (c² − y²)₊` is locally Lipschitz with constant `|y| + |y′|`, which does not + depend on `c`. The inequality itself is the one #218 Step C3 already uses, since `(c² − y²)₊ = c² − min(y², c²)`. + What is new is using it in #218 Step C2 and #220 Step E3, which used the global constant `2c = 12κ|det A|` instead. + That is where the factor `(1 + κ)²` of #218 (C.1) comes from, as #218's closing remark of §3 records; the remark + proposed a parity argument to remove it, and Lemma L makes parity unnecessary. +- **A refined margin estimate** (§3, Step E2⁺). In #220, the elder decision's edge window `𝔅_4` is charged `O(rκ²)`. + At large `κ`, the edge `|φ| ≈ 1/3` needs `|f₄ − 3γᵀA^{−1}γ| ≍ κ`. So either `|f₄| ≥ 6κ`, or the transverse + concavity is `λ ≤ |γ|²/(2κ)`, an event of conditional probability `O(1/κ)` by #218 Lemma D. Each alternative saves + a factor `κ`, so the charge drops from `O(rκ²)` to `O(rκ)`. +- **Proposition W⁺** (§4). Near pairs at small gap need the typed window `|Y| ≲ κ|det A| + r`. Since `Y` is affine + in `f₄` with slope `det A/12`, this window has conditional probability `O(κ + r/|det A|)`. Hence + `E_Q[W_r/r²] ≤ Cr²(κ + r)²(κ + r log(2/r))P^N` for `k ≤ r`. This is better than #198 (W.1) by the factor + `κ + r log(2/r)`, and it controls the elder density at intermediate separations to `O(ℓ^{4/9}log(1/ℓ))`. + +**Dependencies (consumed, unmerged).** 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`, blob `f6df5a73`, head `782211f`): §0 cusp objects, + (0.2)/(CU.2) (the coefficient `c₁`), §7 (through #218). +- Math- #218 (`frontiers/candidate_third_order_20261001/PROOF.md`, blob `70ca57ef`, head `0cf048d`): Lemma D (1.1), + (1.2), Lemma F (F.1)–(F.2), Lemma C and its proof (Steps C1–C3, (C.2)), Lemma O (O.1), (0.1) (`c₂`), and §4 (the + decomposition `F + K + J₂ + … + J₅` and the bounds on `F`, `J₂`–`J₅`). +- Math- #220 (`frontiers/elder_third_order_20261001/PROOF.md`, blob `736a35de`, head `e481d23`): §0 (the near/far + identity, `𝒜^{eld}`, `c₁`), Lemma Q, §2 (notation, facts (F1)–(F7), (2.1)–(2.2), Lemma G, Lemma CE and its proof, + Steps E1–E6), Lemma O′ (O′.1), Lemma H (through Lemma S′), Lemma S′ (S′.1), and §4 (the decomposition + `F^{eld} + K^{eld} + I^{eld} − J₄` and the bound on `F^{eld}`). + +**Merged inputs.** [R] with (R2)–(R5); [P] with [E1], [E2] and [REC] (§2 finite-jet rank, §15 parity); [Z]; [C7-K] +(K2); Math- #191 (`441152df`: Lemma E Steps 1–3, for (F1) at `k = 0`; §2, `r_0^*` and the `k = 0` identity); Math- #198 +(`abfb98ae`: (3.1), the sign window and (3.2) of §3, Lemma W with its `k = 0` clause, (W.1), the `k = 0` identity in +the proof of (W.4), Lemma F′); Math- #187 (`07260114`, merged on 1 October 2026 at `c2f1270`: Theorem F at the single +separation `ρ = r_0^*`). **Cited only:** Math- #216 and #223 (values of `c₂`), #211 (blob `ed0d3fa8`; the +equal-height mass and a heuristic quoted in Remark 3), #188. + +## 0. Statement + +Setting and notation are those of #218 §0 and #220 §0: +- 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`, `κ = k/r`; +- the scaled endpoint Hessians `K_M`, `K_S`, `W_r/r² = F_d(K_M)F_{d−1}(K_S)`, and the elder mark `e`; +- 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`; +- the free jets `J′ ⊃ J″ ⊃ J‴` of `f = F_r` at `0` (#220 §2), with `f₄`, `γ`, `A`, `Δ = det A`, `λ = λ_min(−A)`, + `B = ∂_uD_Θ²f(0)`, `Y_r = (f₄/12)Δ + 3k tr(adj(A)B) − γᵀadj(A)γ/4`, `Y′ = Y_r − 3k tr(adj(A)B)`, `φ_r = Y′/(6κΔ)`, + and `𝒩_r = 1 + k + ‖F_r‖_{C⁹}`; +- the cusp kernels `𝒜^{cand}`, `𝒜^{eld}`, `𝒜^{con}`, the weight `w_κ(A, Y) := (36κ²(det A)² − Y²)₊1{A < 0}`, and the + coefficients `c = c_{d,L}`, `B_{d,L}`, `I^{cand}` (#218 §0), `c₁` (#220 (0.2)) and `c₂` (#218 (0.1)); +- `r₂ := min(r_0^*, 1/2, r_Q)` (#220 Lemma CE). + +**Theorem T⁺ (the candidate density, remainder `ℓ^{3/7}`).** For every `d ≥ 2` and `L > 0`, as `ℓ ↓ 0`, + + ν_cand(ℓ) = c ℓ^{−1/3} + B_{d,L} + I^{cand} ℓ^{1/4} + c₂ ℓ^{1/3} + O(ℓ^{3/7}). (T⁺.1) + +**Theorem E3⁺ (the elder density, remainder `ℓ^{3/7}`).** For every `d ≥ 2` and `L > 0`, as `ℓ ↓ 0`, + + ν_eld(ℓ) = c ℓ^{−1/3} + c₁ ℓ^{1/4} + c₂ ℓ^{1/3} + ν_eld^{far,r_0^*}(ℓ) + O(ℓ^{3/7}), (E3⁺.0) + +and, by Math- #187's Theorem F at `ρ = r_0^*` (`ν_eld^{far,r_0^*}(ℓ) ≤ Cℓ^{2/3}`), + + ν_eld(ℓ) = c ℓ^{−1/3} + c₁ ℓ^{1/4} + c₂ ℓ^{1/3} + O(ℓ^{3/7}). (E3⁺.1) + +The elder density from the intermediate separations `[ℓ^{2/9}, r_0^*]` is `O(ℓ^{4/9}log(1/ℓ))`. (E3⁺.0) does not use +#187: it isolates the far part, so that for `0 < θ ≤ 3/7`, `ν_eld − cℓ^{−1/3} − c₁ℓ^{1/4} − c₂ℓ^{1/3} = O(ℓ^θ)` if and +only if `ν_eld^{far,r_0^*} = O(ℓ^θ)`. With #187 both sides hold at `θ = 3/7`. + +**Corollary R⁺ (the rejected density).** `ρ_rej = ν_cand − ν_eld` satisfies + + ρ_rej(ℓ) = B_{d,L} + (I^{cand} − c₁) ℓ^{1/4} − ν_eld^{far,r_0^*}(ℓ) + O(ℓ^{3/7}) = B_{d,L} + (I^{cand} − c₁) ℓ^{1/4} + O(ℓ^{3/7}). (R⁺.1) + +**Proposition W⁺ (the typed window).** For `0 < r ≤ r_0^*`, `b ∈ R`, `u ∈ S^{d−1}` and `0 ≤ k ≤ r` (so `κ ≤ 1`), + + E_Q[W_r/r²] ≤ C r² (κ + r)² (κ + r log(2/r)) P^N, (W⁺.1) + r^{−2}A_r(b, k, u) ≤ C (κ + r)² (κ + r log(2/r)) (1 + |b|)^N e^{−cb²}. (W⁺.2) + +At `k = 0` this gives `r^{d−1}Ψ_0(b, ru) ≤ Cr³log(2/r)(1 + |b|)^Ne^{−cb²}` for the equal-height kernel `Ψ_0` of [Z] +(Z2), and + + ∫_{0 < dist(0, y) < ρ} ∫_R Ψ_0(b, y) db dy ≤ C ρ⁴ log(2/ρ), 0 < ρ ≤ r_0^*, (W⁺.3) + +which sharpens #198 (W.4) (`Cρ³`). + +**How it works.** The decompositions are those of #218 §4 and #220 §4, with new split points: + + ρ_f := ℓ^{2/7}, ρ_c := ℓ^{2/9}, a := ℓ^{1/9} (#218 and #220: ρ_f = ℓ^{3/11}, a = ℓ^{2/15}). + +- *Cusp region `[ρ_f, ρ_c]`.* Lemma C⁺ (§2) and Lemma CE⁺ (§3) give the cusp kernels with errors + `Cr(1 + κ)` and `C(r(1 + κ) + κ²r^{3/2} + κ³r²)`. #218 and #220 have `Cr(1 + κ)²`; its `rκ²` integrates to + `ℓ²ρ_f^{−6}`, which is what forced `ρ_f = ℓ^{3/11}`. +- *Fold region `[0, ρ_f]`.* Unchanged: Lemma F's boundary layer and the rejected fold mass contribute `O(ρ_f⁵/ℓ)`, + and the finite part `O(ℓρ_f^{−2})`. +- *Intermediate separations `[ρ_c, r_0^*]`.* Proposition W⁺ on `[ρ_c, a]`, Lemma S′ on `[a, r_0^*]`. +- *The ledger.* At `ρ_f = ℓ^{2/7}` the four error terms `ρ_f⁵/ℓ`, `ℓρ_f^{−2}`, `ℓ²ρ_f^{−11/2}` and `ℓ³ρ_f^{−9}` are + exactly `ℓ^{3/7}`; every other term is `O(ℓ^{4/9}log(1/ℓ))` (§5; control R1). + +**What is not claimed.** +- No sharpness of `3/7`. The formal next term is of order `ℓ^{1/2}` (#218 §0); Remark 1 explains why this method stops + at `3/7`. +- 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. +- (E3⁺.1) and the second form of (R⁺.1) use #187 (merged) at the single separation `r_0^*`; (T⁺.1), (E3⁺.0), the first + form of (R⁺.1) and Proposition W⁺ do not. +- Nothing beyond the existential scope of [R], [Z], [C7-K], #187, #191, #198, #207, #218 and #220. + +## 1. A `κ`-free local Lipschitz bound + +**Lemma L.** For `c ≥ 0` and `y, y′ ∈ R`, + + |(c² − y²)₊ − (c² − y′²)₊| ≤ |y − y′| (|y| + |y′|). (L.1) + +Consequently, for every symmetric `A` and `κ > 0`, `|w_κ(A, Y) − w_κ(A, Y′)| ≤ |Y − Y′|(|Y| + |Y′|)`. + +*Proof.* By symmetry assume `|y| ≤ |y′|`. +- If `|y′| ≤ c`, the left side is `|y² − y′²| = |y − y′||y + y′| ≤ |y − y′|(|y| + |y′|)`. +- If `|y| ≤ c < |y′|`, the left side is `c² − y² ≤ y′² − y² = (|y′| − |y|)(|y′| + |y|) ≤ |y′ − y|(|y| + |y′|)`. +- If `c < |y|`, both terms vanish. + +For `w_κ` take `c = 6κ|det A|` on `{A < 0}`; off `{A < 0}` both weights vanish, so the left side is `0`. ∎ + +(L.1) is sharp: equality holds whenever `|y|, |y′| ≤ c` and `yy′ ≥ 0`. Since `(c² − y²)₊ = c² − min(y², c²)`, (L.1) is +the inequality `|min(y², c²) − min(y′², c²)| ≤ (|y| + |y′|)|y − y′|` that #218 Step C3 uses. The global Lipschitz +constant `2c` also holds, but `|y| + |y′|` has moments independent of `κ`, whereas `2c = 12κ|Δ|` grows with `κ` +(control R2). + +## 2. The candidate cusp kernel with rate `r(1 + κ)` + +**Lemma C⁺.** There are `C, c, N` such that for `0 < r ≤ min(r_0^*, 1/2)`, `b ∈ R`, `u ∈ S^{d−1}` and `κ > 0` with +`k := κr ≤ 1`, + + |r^{−2}(A_r − A_0)(b, κr, u) − (𝒜^{cand} − 𝒜^{con})(b, κ, u)| ≤ C r (1 + κ) (1 + |b|)^N e^{−cb²}. (C⁺.1) + +*Proof.* Follow #218's proof of Lemma C on its coupling space, with `T`, `A_0 = D_y²F_0(0)`, `Δ := det A_0`, +`Y = (f₄/12)Δ + 3k tr(adj(A_0)B) − q` and `Y_0 = (f₄^{(0)}/12)Δ − (γ^{(0)})ᵀadj(A_0)γ^{(0)}/4` as there. +- *Step C1* is unchanged: (C.2) there gives `|r^{−2}F_d(K_M)F_{d−1}(K_S) − w_κ(A_0, Y)| ≤ Cr(1 + κ)T^N`. This is + already linear in `κ`. Case 1's bounds are `24ηκ|Δ| + η²` and `2η(12κ|Δ| + 3η)` with `η = Cr(1 + k)T^{N₁}`, and + Case 3's only `κ²` is `w_κ ≤ 36κ²r²T^{2m} = 36k²T^{2m}`, with `|m_Mm_S| ≤ C(k + η)²T^{2m}`. The `k²` parts are + absorbed by `k² ≤ k = κr`, and the `η²` parts by `r² ≤ r`. +- *Step C2⁺.* #218 Step C2 gives `|Y − Y_0| ≤ 3k|tr(adj(A_0)B)| + Cr²T^N`. Also `|Y| + |Y_0| ≤ CT^N`, since + `|f₄|, |γ|, ‖B‖, ‖A_0‖ ≤ T` and `k ≤ 1`. By Lemma L, + `|w_κ(A_0, Y) − w_κ(A_0, Y_0)| ≤ |Y − Y_0|(|Y| + |Y_0|) ≤ C(k + r²)T^{N′}`. With Step C1 and `E[T^{N′}] ≤ CP^{N′}`, + + |E_Q[r^{−2}F_d(K_M)F_{d−1}(K_S)] − E_0[w_κ(A, Y) | v_0(b, k)]| ≤ C r(1 + κ) P^N, + + because `k + r² = r(κ + r) ≤ r(1 + κ)`. (On the right, as in #218, `A` and `Y` are the cusp objects of #218 §0 under + the contact law at `v_0(b, k)`; `(A_0, Y_0)` has that law.) #218 had `Cκ(κr + r²)T^N` for this step, from the + constant `12κ|Δ|`. +- *Step C3* is unchanged except for one estimate. The density step costs `|π_r(v_r) − π_0(v_0(b, k))|·E_0[w_κ] ≤ + Cr²P²·(1 + κ)²P^N`, and `r²(1 + κ)² = (r + k)² ≤ 2(r + k) = 2r(1 + κ)` because `r + k ≤ 2` (control R6). +- The identity `r^{−2}A_0(b, κr, u) = 12π_0(v_0(b, k))·36κ²E_0[Δ²1{A < 0} | v_0(b, k)]` and the parity step that moves the + target from `v_0(b, k)` to `v_0(b, 0)` are #218's. The latter costs `O(k(1 + |b|)^Ne^{−cb²})`, "with no growth in + `κ`", because it uses `|min(Y², c) − min(Ȳ², c)| ≤ (|Y| + |Ȳ|)|Y − Ȳ|`, which is (L.1). + +Collecting, with `P^Ne^{−c(b² + k²)} ≤ C(1 + |b|)^Ne^{−cb²}`, gives (C⁺.1). ∎ + +So the parity argument proposed at the end of #218 §3 is not needed for the exponent. Parity would sharpen the +contribution of the `3k tr(adj(A_0)B)` term from `O(k)` to `O((1 + κ)k²)`, and probably to `O(k²)` (Remark 2; not +proved), but `O(k) = O(κr)` is already within (C⁺.1). + +## 3. The elder cusp kernel + +**Lemma CE⁺.** There are `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 + κ) + κ²r^{3/2} + κ³r²) (1 + |b|)^N e^{−cb²}. (CE⁺.1) + +*Proof.* Follow #220's proof of Lemma CE. Step E1 is unchanged, and so is (2.3) there: + + |r^{−2}F_d(K_M)F_{d−1}(K_S)e − G(J′)| ≤ 2Cr(1 + κ)𝒩_r^N + w_κ(A, Y_r)1_𝔅, G(J′) := w_κ(A, Y_r)1{|φ_r| < 1/3}. + +Two steps change: Step E2 in its `𝔅_4` part, and Step E3. + +*Step E2⁺ (wrong decisions).* #220 shows `𝔅 ⊂ 𝔅_λ ∪ 𝔅_κ ∪ 𝔅_4 ∪ 𝔅_5`, and that (Q1)–(Q3) of Lemma Q hold off +`𝔅_λ ∪ 𝔅_κ`. So `𝔅 ⊂ 𝔅_λ ∪ 𝔅_κ ∪ 𝔅_4′ ∪ 𝔅_5` with `𝔅_4′ := 𝔅_4 ∖ (𝔅_λ ∪ 𝔅_κ)`. Keep #220's bounds for the +other three events: +- `𝔅_λ`: `Cκ²min(1, κ)(r³ + r^{3/2} + (r/κ)^{3/2})P^N ≤ C(r + κ²r^{3/2})P^N`, since `κ²r³ = k²r ≤ r` and + `κ^{1/2}r^{3/2} = k^{1/2}r ≤ r` (control R6); +- `𝔅_κ`: `Cr³P^N`; +- `𝔅_5`: `Cκ³r²P^N`. + +The new estimate is + + E_Q[w_κ(A, Y_r)1_{𝔅_4′}] ≤ C κ r P^N for every κ > 0. (3.1) + +*Proof of (3.1).* +- *Where `𝔅_4′` lives.* On `𝔅_4′`, (Q3) holds: `ε* ≤ κ/4`. So `||φ_r| − 1/3| ≤ 2ε*/(3κ) ≤ 1/6` and + `1/6 ≤ |φ_r| ≤ 1/2`, that is, `|f₄ − 3γᵀA^{−1}γ| = 72κ|φ_r| ≥ 12κ`. The weight vanishes unless `A < 0`, and then + `|γᵀA^{−1}γ| ≤ |γ|²/λ`. Hence + + 𝔅_4′ ∩ {w_κ > 0} ⊂ {|f₄| ≥ 6κ} ∪ {λ ≤ |γ|²/(2κ)} (3.2) + + (control R3). Also, as in #220, `𝔅_4` puts `f₄` in two `J″`-measurable intervals `I₄` of total length + `192ε*`, with `ε* = 80C₁𝒩_r r(1 + Γ)²` and `Γ = |γ|/λ`. +- *The `𝒩_r`-layers.* As in #220, on `{𝒩_r ∈ [2^j, 2^{j+1})}` replace `𝒩_r` in `ε*` by `2^{j+1}`, so that `I₄` + becomes `J″`-measurable. Bound `1{𝒩_r ≥ 2^j}` by (F4), `P(𝒩_r ≥ 2^j | J′) ≤ C_p2^{−jp}(P + |J′|)^p`, and then + integrate `f₄` given `J″` by (2.1). The layer value `2^{j+1}` of `𝒩_r` in `ε*` is absorbed by `2^{−jp}`, and the sum + over `j` converges for `p` large. Below, `ε*` stands for its layer value. +- *The first piece of (3.2).* There `1 ≤ |f₄|/(6κ)`, so `w_κ ≤ 36κ²Δ² ≤ 6κΔ²|f₄|`. Integrating `f₄` over `I₄` by + (2.1) gives at most `CκΔ²ε*(P + |J″|)^p`. Since `Δ² ≤ λ²‖A‖^{2m−2}`, `Δ²(1 + Γ)² ≤ (λ + |γ|)²‖A‖^{2m−2}`, which + is polynomial in `J″`. So this piece is `≤ CκrP^N`. +- *The second piece of (3.2).* Integrating `f₄` over `I₄` gives at most + `Cκ²Δ²ε*(P + |J″|)^p ≤ Cκ²r(λ + |γ|)²‖A‖^{2m−2}(P + |J″|)^p` (in the layer), and `(λ + |γ|)² ≤ 2‖A‖² + 2|γ|²` + since `λ ≤ ‖A‖`. This factor is polynomial in `J″` and does not depend on `κ`. Now condition on `J‴`, which + contains `γ`. Since `{λ ≤ |γ|²/(2κ)} ∩ {A < 0} ⊂ {|λ_max(A)| ≤ |γ|²/(2κ)}`, (2.2) with `ε = |γ|²/(2κ)` gives the + factor `C(P + |J‴|)^{n′}|γ|²/(2κ)`. So this piece is `≤ Cκ²r·κ^{−1}P^N = CκrP^N`. ∎ + +Collecting the four events, `E_Q[w_κ(A, Y_r)1_𝔅] ≤ C(r(1 + κ) + κ²r^{3/2} + κ³r²)P^N`. #220 had `Crκ²P^N` for +`𝔅_4`, which was the second source of `(1 + κ)²` in (CE.1). + +*Step E3⁺ (removing the `k`-term).* `G₀(J′) := w_κ(A, Y′)1{|φ_r| < 1/3} = w_κ^{eld}(A, Y′)`, as in #220. By Lemma L, + + |G − G₀| = |w_κ(A, Y_r) − w_κ(A, Y′)|1{|φ_r| < 1/3} ≤ 3k|tr(adj(A)B)|(|Y_r| + |Y′|) ≤ Ck(1 + |J′|)^N, + +so `E_Q|G − G₀| ≤ CkP^N = CκrP^N`. #220 had `Cκ²rP^N` here, from the constant `12κ|Δ|`. + +*Steps E4–E6* are unchanged. They cost `Cκ²r²P^N`, `Cr²(1 + κ)²P^N` and `Ck²(1 + |b|)^N`. Here `κ²r² = k² ≤ k = κr` +and `r²(1 + κ)² ≤ 2r(1 + κ)` (control R6). Collecting all steps gives (CE⁺.1). ∎ + +(CE⁺.1) implies #220's (CE.1), since `κ²r^{3/2} + κ³r² ≤ 2κ²r` when `r ≤ 1` and `κr ≤ 1` (control R6). The two +nonlinear terms come from two of Lemma Q's bad events: `κ²r^{3/2}` from `𝔅_λ`, where the transverse concavity is +below its margin `λ₂`, and `κ³r²` from `𝔅_5 = {|φ_r| > 1}`, which the shift `3k tr(adj(A)B)` between `Y_r` and `Y′` +lets a pair inside the typed window `|Y_r| < 6κ|Δ|` reach. Both attain `3/7` exactly at the split of §5 (Remark 1). + +## 4. The typed window + +*Proof of Proposition W⁺.* Fix `0 < r ≤ r_0^*`, `b ∈ R`, `u` and `0 ≤ k ≤ r`. Every fact used below holds on all of +`(0, r_0^*]`: +- (F1) holds pathwise for every `r ≤ r_0^*` and `k > 0` (#220 §2). It also holds at `k = 0`: #191 Steps 1–3 are the + same pathwise expansions there, and #198 Lemma W includes the pinned family at `k = 0` ("nothing below divides by + `k`"); +- (F3) and (2.1): `Cov_Q(J′)` is uniformly invertible on `(0, r_0^*]` (#218 Step F1); +- (F4): #218 (1.2) with `J₀ = J′`; +- (F5) and (2.2), as Schur complements in `Cov_Q(J′)`. + +*Step W1 (pathwise).* Put `R̄ := max(|R_M|, |R_S|) ≤ C_Rr²𝒩_r^{N₁}` (by (F1), with `k ≤ 1`; `C_R` is (F1)'s constant, not +Lemma Q's `C₁`) and `η := C_Rr𝒩_r^{N₁} ≥ R̄/r`. +- On `{W_r > 0}` the pair is typed, so `det K_M det K_S < 0`. The sign window of #198 §3, applied to (F1), gives + `|rY_r| ≤ 6k|Δ| + R̄` and `|det K_i| ≤ 12k|Δ| + 2R̄` (control R4). +- Dividing by `r`, `|Y_r| ≤ 6κ|Δ| + η`, and `W_r/r² = |det K_M det K_S| ≤ 4r²(6κ|Δ| + η)²`. Off `{W_r > 0}`, + `W_r = 0`. Hence, everywhere, + + W_r/r² ≤ 4r²(6κ|Δ| + η)² 1{|Y_r| ≤ 6κ|Δ| + η}. (4.1) + +*Step W2 (the window in `f₄`).* `Y_r` is affine in `f₄` with slope `Δ/12`, and its intercept is `J″`-measurable. So, +for a `J″`-measurable `η′`, `{|Y_r| ≤ 6κ|Δ| + η′}` is `{f₄ ∈ I}` for a `J″`-measurable interval `I` of length +`144κ + 24η′/|Δ|` (control R4); `Δ ≠ 0` almost surely. +- On `{𝒩_r ∈ [2^j, 2^{j+1})}`, `η ≤ η_j := C_Rr2^{(j+1)N₁}`. Bound `1{𝒩_r ≥ 2^j}` by (F4), then integrate `f₄` by + (2.1). Using also the trivial bound `1`, this gives + + E_Q[W_r/r²] ≤ C r² Σ_{j≥0} 2^{−jp} E_Q[(6κ|Δ| + η_j)² min(1, 144κ + 24η_j/|Δ|)(P + |J″|)^p]. + +- By `(x + y)²min(1, a + b) ≤ 2(x² + y²)(a + min(1, b))` for `x, y, a, b ≥ 0` (control R4), the integrand is at most + `C(κ²Δ² + η_j²)(κ + min(1, η_j/|Δ|))` times `(P + |J″|)^p`. + +*Step W3 (the four terms).* +- `κ³Δ²` contributes `Cκ³P^N`. +- `κ²Δ²min(1, η_j/|Δ|) ≤ κ²|Δ|η_j` contributes `Cκ²r2^{jN′}P^N`. +- `κη_j²` contributes `Cκr²2^{2jN′}P^N`. +- `η_j²min(1, η_j/|Δ|)`. Condition on `J‴`, so that `A` is Gaussian with covariance in `[cI, CI]` and mean + `O(P + |J‴|)` (F5). #218 Lemma D's second bound gives `E[(1 + ‖A‖)^n1{|Δ| < ε} | J‴] ≤ C(P + |J‴|)^{n′}ε` for every + `ε > 0`. Split `{|Δ| < s}`, `{2^is ≤ |Δ| < 2^{i+1}s}` for `0 ≤ i < ⌈log₂(1/s)⌉`, and `{|Δ| ≥ 1}`. This gives, for + `0 < s ≤ 1/2`, + + E[(1 + ‖A‖)^n min(1, s/|Δ|) | J‴] ≤ C(P + |J‴|)^{n′} s (4 + 2log₂(1/s)). (4.2) + + With `s = η_j ≥ C_Rr`, `log₂(1/η_j) ≤ log₂(1/(C_Rr))`, so the term contributes `Cr³log(2/r)2^{3(j+1)N₁}P^N`. (For + `s > 1/2` bound the minimum by `1 ≤ 2s`.) + +Taking `p` large, the sum over `j` converges, and + + E_Q[W_r/r²] ≤ C r²(κ³ + κ²r + κr² + r³log(2/r))P^N ≤ C r²(κ + r)²(κ + r log(2/r))P^N + +(control R5). This is (W⁺.1). + +*(W⁺.2)* follows with `r^{−2}A_r = 12π_r(v_r)r^{−2}E_Q[W_r/r²]`, `π_r(v_r) ≤ Ce^{−c(b² + k²)}` ([R] (R5)) and +`P^Ne^{−ck²} ≤ C(1 + |b|)^N`. + +*(W⁺.3).* At `k = 0`, `r^{d−1}Ψ_0(b, ru) = r^{−2}A_r(b, 0, u)`, as in #198's proof of (W.4) (#191 §2: the pin Jacobian, the +polar factor and the determinant scale). So (W⁺.2) at `κ = 0` gives `r^{d−1}Ψ_0(b, ru) ≤ Cr³log(2/r)(1 + |b|)^Ne^{−cb²}`. +Integrating over `b`, `u` and `r < ρ`, with `∫_0^ρ r³log(2/r) dr = (ρ⁴/4)(log(2/ρ) + 1/4)`, gives (W⁺.3). ∎ + +(W⁺.1) improves #198 (W.1), `E_Q[W_r/r²] ≤ C(k² + r⁴(1 + k)²)P^N = Cr²(κ² + r²)(…)` for `k ≤ r`, by the factor +`κ + r log(2/r)`. That factor is the conditional probability of the typed window, which (W.1) does not use. #198 notes +after its proof of Lemma W that the window `|rY| ≤ 6k|Δ| + O(r²)` is where the typed weight lives; (4.1)–(4.2) charge +it. The factor `log(2/r)` comes from integrating `f₄` alone, and may be an artifact: in the referee's `d = 2` +exploration (Gaussian kernel, Monte Carlo under the exact two-site regression), `E_Q[W_r/r²]/r² ≈ 0.03r³` at `k = 0` +for `r` from `0.4` down to `0.0125`, with no visible logarithm. The ledger does not need it removed. + +## 5. Proof of Theorems T⁺ and E3⁺ and of Corollary R⁺ + +*Setup.* Put `ρ_f := ℓ^{2/7}`, `ρ_c := ℓ^{2/9}`, `a := ℓ^{1/9}`, `s_f := ρ_fℓ^{−1/4} = ℓ^{1/28}` and +`s_c := ρ_cℓ^{−1/4} = ℓ^{−1/36}`. Take `ℓ` so small that `ρ_c ≤ r₂`, `ρ_c < r_0` and `a < r_0^*`. Then +`ℓ^{1/3} < ρ_f < ℓ^{1/4} < ρ_c < a`, `k = ℓ/r³ ≤ ℓ^{1/7} ≤ 1` on `[ρ_f, ∞)`, and `κ = ℓ/r⁴ ≤ ℓ^{1/9} ≤ 1` on `[ρ_c, ∞)`. + +*The candidate density.* Use #218 §4's decomposition `ν_cand − cℓ^{−1/3} − B_{d,L} = F + K + J₂ + J₃ + J₄ + J₅`, with its +fixed `r_0 ∈ (0, r_0^*]`, at these `ρ_f` and `ρ_c`. Its bounds on `F` and `J₂`–`J₅` hold for every +`ℓ^{1/3} ≤ ρ_f ≤ min(ℓ^{1/4}, r_0^*, 1/2)` and `ℓ^{1/4} < ρ_c < r_0`: +- `F = c₂ℓ^{1/3} + ρ_f∫∫A₂(b, 0, u) + O(ρ_f² + ρ_f⁵/ℓ + ℓρ_f^{−2})` (Lemma F and the finite part); +- `|J₂| ≤ Cρ_c³`, `|J₃| ≤ C(ℓ²ρ_c^{−7} + ℓρ_c^{−2})`, `0 ≤ −J₄ ≤ Cℓ²ρ_c^{−7}`, `|J₅| ≤ C_{r_0}ℓ`. + +For `K`, use (C⁺.1) with `κ = ℓ/r⁴` in place of (C.1). The error is +`C∫_{ρ_f}^{ρ_c}r(1 + ℓr^{−4}) dr ≤ C(ρ_c² + ℓρ_f^{−2})`. The rest of #218's treatment of `K` is unchanged: the +upper tail `O(ℓ²ρ_c^{−7})`, the lower end by Lemma O `O(ℓ^{1/4}s_f⁵) = O(ρ_f⁵/ℓ)`, and the cancellation of +`±ρ_f∫∫A₂(b, 0, u)` against `F`. So + + ν_cand − cℓ^{−1/3} − B_{d,L} − I^{cand}ℓ^{1/4} − c₂ℓ^{1/3} = O(ρ_f² + ρ_f⁵/ℓ + ℓρ_f^{−2} + ρ_c² + ℓ²ρ_c^{−7} + ρ_c³ + ℓρ_c^{−2} + ℓ). + +*The elder density.* Use #220 §4's identity at `r_0 = r_0^*`, +`ν_eld − cℓ^{−1/3} = F^{eld} + K^{eld} + I^{eld} − J₄ + ν_eld^{far,r_0^*}`, at these `ρ_f` and `ρ_c`. +- `F^{eld} = c₂ℓ^{1/3} + ρ_f∫∫A₂(b, 0, u) + O(ρ_f² + ρ_f⁵/ℓ + ℓρ_f^{−2})`. This is #220's bound; it uses `ρ_f ≤ ℓ^{1/4}` + (so `k ≥ r`) and `ρ_f ≤ r₂ ≤ r_0^{[K]}`, and the rejected fold mass is `O(ρ_f⁵/ℓ)` by [C7-K] (K2). +- `K^{eld}`: (CE⁺.1) with `κ = ℓ/r⁴` gives the error + + C∫_{ρ_f}^{ρ_c}(r + ℓr^{−3} + ℓ²r^{−13/2} + ℓ³r^{−10}) dr ≤ C(ρ_c² + ℓρ_f^{−2} + ℓ²ρ_f^{−11/2} + ℓ³ρ_f^{−9}). + + The rest is #220's: `K^{eld} = c₁ℓ^{1/4} − ρ_f∫∫A₂(b, 0, u) + O(ℓ^{1/4}s_f⁵ + ℓ^{1/4}s_c^{−7})` plus that error, by + (0.2), Lemma O′ with #218 Lemma O (`s ≤ s_f < 1` means `κ ≥ 1`), and the upper tail. +- `0 ≤ J₄ ≤ Cℓ²ρ_c^{−7}`. +- `I^{eld} = ∫_{ρ_c}^{r_0^*}∫∫r^{−2}A_r^{eld} ≥ 0`. + - On `[ρ_c, a]`, `e ≤ 1` and (W⁺.2) give `r^{−2}A_r^{eld} ≤ C(1 + log(2/ρ_c))(κ + r)³(1 + |b|)^Ne^{−cb²}`, using + `(κ + r)²(κ + rL) ≤ (1 + L)(κ + r)³` for `L = log(2/r) ≥ 0` and `log(2/r) ≤ log(2/ρ_c)`. Since + `(κ + r)³ ≤ 4(κ³ + r³)` (control R5), this integrates to at most `C log(1/ℓ)(ℓ³ρ_c^{−11} + a⁴)`. + - On `[a, r_0^*]`, Lemma S′ applies (`k ≤ r`). As in #220 §4 it gives at most `C(ℓ^{5/3}a^{−7} + ℓ^{2/3}a^{−2})`. + + So `0 ≤ I^{eld} ≤ C(ℓ^{5/9} + ℓ^{4/9})log(1/ℓ) + C(ℓ^{8/9} + ℓ^{4/9}) = O(ℓ^{4/9}log(1/ℓ))`. + +The terms `±ρ_f∫∫A₂(b, 0, u)` cancel as in #220, and `ℓ^{1/4}s_f⁵ = ρ_f⁵/ℓ`, `ℓ^{1/4}s_c^{−7} = ℓ²ρ_c^{−7}`. + +*The ledger* (control R1; exponents of `ℓ`): + +| Term | Source | Exponent | +|---|---|---| +| `ρ_f⁵/ℓ` | Lemma F's layer; the rejected fold mass; Lemma O/O′'s tail | **3/7** | +| `ℓρ_f^{−2}` | the finite part; the linear term `rκ` of (C⁺.1), (CE⁺.1) | **3/7** | +| `ℓ²ρ_f^{−11/2}` | `κ²r^{3/2}` of (CE⁺.1) (elder only) | **3/7** | +| `ℓ³ρ_f^{−9}` | `κ³r²` of (CE⁺.1) (elder only) | **3/7** | +| `ρ_f²` | Lemma F | 4/7 | +| `ρ_c²`, `ℓ²ρ_c^{−7}` | cusp errors; upper tail; `J₃`, `J₄` | 4/9 | +| `a⁴log`, `ℓ^{2/3}a^{−2}` | `I^{eld}` (Proposition W⁺; Lemma S′) | 4/9 | +| `ℓ³ρ_c^{−11}log`, `ℓρ_c^{−2}` | `I^{eld}`; `J₃` | 5/9 | +| `ρ_c³`, `ν_eld^{far,r_0^*}` (with #187) | `J₂`; the far part | 2/3 | +| `ℓ^{5/3}a^{−7}`, `ℓ` | `I^{eld}`; `J₅` | 8/9, 1 | + +The least exponent is `3/7`. Hence (T⁺.1) and (E3⁺.0). #198 Lemma F′ gives `0 ≤ ν_eld^{far,r_0^*} ≤ Cℓ^{1/3}`, and +#187's Theorem F at `ρ = r_0^*` gives `ν_eld^{far,r_0^*} ≤ C(r_0^*)ℓ^{2/3}`, which is (E3⁺.1); #220 §4 records that #187's +far density at `ρ = r_0^*` is the integral #198 (2.1) at `r_0 = r_0^*`. The equivalence for `θ ≤ 3/7` follows from +(E3⁺.0). Subtracting (E3⁺.0) from (T⁺.1) gives (R⁺.1); its second form uses #187. ∎ + +The splits are optimal for these error terms (control R1): `ρ_f = ℓ^{2/7}` balances `ρ_f⁵/ℓ` against `ℓρ_f^{−2}`, +`ρ_c = ℓ^{2/9}` balances `ρ_c²` against `ℓ²ρ_c^{−7}`, and `a = ℓ^{1/9}` balances `a⁴` against `ℓ^{2/3}a^{−2}`. + +## 6. Remarks + +1. **Why `3/7`.** Write the cusp errors per unit `r` at the fold end `r = ρ_f`, where `κ = ℓρ_f^{−4}`. At + `ρ_f = ℓ^{2/7}` one has `κ = ρ_f^{−1/2}`, and then the boundary layer `r⁴/ℓ = 1/κ`, the linear term `rκ = k`, and + the nonlinear terms `κ²r^{3/2}` and `κ³r²` are all equal to `ρ_f^{1/2}`. Times the length `ρ_f` of the interval, + each gives `ℓ^{3/7}`. + - The exponent is the balance of one family that increases with `ρ_f`, namely `ρ_f⁵/ℓ` (the `r³/k` layer of + Lemma F, the rejected fold mass of [C7-K] (K2), and the `κ^{−1}` tail of Lemma O/O′), against three that + decrease: `ℓρ_f^{−2}` (the finite part and the linear cusp error `rκ = k`), `ℓ²ρ_f^{−11/2}` and `ℓ³ρ_f^{−9}` (the + last two for the elder density only). + - The terms come in *matching* pairs. The `r³/k` layer of Lemma F matches the `κ^{−1}` tail of Lemma O, and the + `C¹`-truncation `A₂(k) − A₂(0) = O(k)` in the finite part matches the linear cusp error `rκ = k`. + - An exact max–min over the ledger (control R1; first observed by the referee) shows which pair blocks. + - Remove the family `ρ_f⁵/ℓ`, that is, suppose the leading coefficients of the layer, the tail and the elder fold + mass were computed and matched. Then both densities reach the next terms of the ledger, of order `ℓ^{4/9}` (with a + logarithm for the elder density), subject to the next-order remainder of that expansion. + - Remove instead only the linear pair `ℓρ_f^{−2}`, which needs the `O(r)`-correction `𝒜₃(κ)` of the cusp kernel; + formally `𝒜₃` produces the next term, of order `ℓ^{1/2}` (#218 §0). This helps the candidate density, which + reaches `ℓ^{4/9}`, but not the elder density: there `κ²r^{3/2}` and `κ³r²` balance `ρ_f⁵/ℓ` at the same + `ρ_f = ℓ^{2/7}`. + - So for the elder density, Lemma Q's bad events `𝔅_λ` and `𝔅_5` become the obstruction once the linear pair is + resolved; improving them alone would not change the exponent. +2. **Parity (a sketch and an exploration; not used).** #218's closing remark of §3 proposed a parity argument for its + `κ²`. Lemma L removes the `κ²` without it. Parity would give more. Under the contact law at `v_0(b, k)`, the odd + jets are `N(12kw, Σ_o)` and independent of the even ones ((F7)); `tr(adj(A)B)` is odd, while `Y′`, `∂_Yw_κ(A, Y′)` + and the elder window are even. So the first-order term of `w_κ(A, Y′ + 3k tr(adj(A)B)) − w_κ(A, Y′)` has mean `O(k²)`. + The second-order remainder is `O(k²)` inside the elder window `|Y′| < 2κ|Δ|`, where the kink at `6κ|Δ|` is crossed only + when `3k|tr(adj(A)B)| ≥ 4κ|Δ|`. For the candidate kernel the kink costs `O(κk²)` through the bounded density of + `f₄`, so the bound is `O((1 + κ)k²)`. `O(k²)` is expected but not proved: crossing the kink needs + `|f₄ − 3γᵀA^{−1}γ| ≈ 72κ`, hence `|f₄| ≳ κ` or `λ ≲ |γ|²/κ`, as in (3.2). In a `d = 2` toy model with these parities + (deterministic quadrature; project archive), the difference `D(k)` satisfies `|D(k)|/k² ≤ 4.4` for `k ≤ 1/40` and + `κ ∈ {1/2, 2, 8, 32}`, for both kernels. With parity broken, `D(k)/k` stays bounded uniformly in `κ`, as Lemma L + predicts. Neither refinement changes the ledger. +3. **The equal-height kernel near the diagonal.** Math- #211 §2 (blob `ed0d3fa8`) records a heuristic: "The referee + observed, heuristically, that at equal heights the two endpoint axial curvatures agree to leading order. That + suggests `r^{d−1}Ψ_0 = O(r³)` and `I(s) ∝ s^{4−d}` near `0`, …". For the torus kernel, (W⁺.2) at `k = 0` proves this + order up to the factor `log(2/r)`. In `d = 3` it gives `∫Ψ_0(b, se₁)db ≤ Cs log(2/s)` near `0`, consistent with the + roughly linear rise of `I(s)` in #211's Monte Carlo for the Gaussian kernel. The proof goes through the typed + window: at `k = 0` it forces `|Y_r| ≤ η = O(r)` (#198's remark after its proof of Lemma W), and this note's Step W2 + charges its conditional probability `O(min(1, r/|Δ|))`. +4. **The SIDE24 law.** With #207 §8 and #216 (Gaussian kernel, `d = 3`; numerical, not certified; #223 gives `c₂` in + closed form), `c = 0.0417759`, `c₁ = −0.2118484` and `c₂/c = 3.859496`. Under (E3⁺.1), + `ν_{3,24}(ℓ) = cℓ^{−1/3}(1 − 5.0711ℓ^{7/12} + 3.8595ℓ^{2/3} + O(ℓ^{16/21}))` up to the relative `O(e^{−L²/8})` of the + kernel comparison; #220 had `O(ℓ^{23/33})`. +5. **Consistency.** + - (C⁺.1) implies #218 (C.1), and (CE⁺.1) implies #220 (CE.1). + - (T⁺.1) implies #218 (T.1); (E3⁺.0) implies #220 (E3.0); (E3⁺.1) implies #220 (E3.3). + - (W⁺.1) implies #198 (W.1) for `k ≤ r`, since `(κ + r)²(κ + r log(2/r)) ≤ C(κ² + r²)`. (W⁺.3) implies (W.4). + - (R⁺.1) implies #220 (E3′.0) and, with `I^{cand} − c₁ > 0` (#207 (CU′.2)), shows again that the rejected density + approaches `B_{d,L}` from above. + +## 7. Sources (exact identities in `SOURCES.json`) + +| Tag | Path | Role | +|---|---|---| +| [R] | `frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md` (blob `247b3ecf`) | (R2)–(R5): pin densities, coupling, moments — consumed | +| [P] | `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` (blob `dfed3b8d`) | §2 finite-jet rank, §15 parity factorization, through #218 and #220 — 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 | +| [Z] | `frontiers/c7_zero_gap_limit_20260929/PROOF.md` (blob `5b6328ea`) | (Z2)–(Z3): `Ψ_0`, `B_{d,L}` — consumed | +| [C7-K] | `frontiers/c7_total_bounded_20260929/PROOF.md` (blob `28748b08`) | (K2): the rejected fold mass — consumed | +| #191 | `frontiers/remainder_vanishing_20260930/PROOF.md` (merged; blob `441152df`) | Lemma E Steps 1–3 (for (F1) at `k = 0`); §2: `r_0^*`, the `k = 0` identity — consumed | +| #198 | `frontiers/remainder_rate_20260930/PROOF.md` (merged; blob `abfb98ae`) | §3 (3.1), the sign window, (3.2); Lemma W with its `k = 0` clause, (W.1); the proof of (W.4); Lemma F′ — consumed | +| #187 | `frontiers/far_elder_rate_20260930/PROOF.md` (merged 1 Oct at `c2f1270`; blob `07260114`) | Theorem F at `ρ = r_0^*`, for (E3⁺.1) and (R⁺.1) only — consumed | +| #207 | `frontiers/cusp_second_order_20261001/PROOF.md` (unmerged; blob `f6df5a73`, head `782211f`) | §0, (CU.2), §7 — **consumed, unmerged** | +| #218 | `frontiers/candidate_third_order_20261001/PROOF.md` (unmerged; blob `70ca57ef`, head `0cf048d`) | Lemmas D, F, C, O; (1.2); (0.1); §4 — **consumed, unmerged** | +| #220 | `frontiers/elder_third_order_20261001/PROOF.md` (unmerged; blob `736a35de`, head `e481d23`) | §0; Lemma Q; §2 facts, Lemmas G, CE; Lemmas O′, H, S′; §4 — **consumed, unmerged** | +| #216, #223 | `frontiers/third_order_coefficient_20261001/NOTE.md`, `frontiers/c2_exact_20261001/NOTE.md` (unmerged) | values of `c₂`, Remark 4 — cited only | +| #211 | `frontiers/equal_height_mass_value_20261001/NOTE.md` (unmerged; blob `ed0d3fa8`, head `8e89fe8`) | the heuristic and Monte Carlo of Remark 3 — cited only | +| #188 | `frontiers/far_elder_flat_ridge_20260930/PROOF.md` (unmerged) | an alternative far bound — cited only | + +## 8. Exact controls (`r37_check.py`; stdlib; exact rationals; byte-identical under `-O`) + +- **R1** the ledger of §5. An error `r^pκ^q` on `[ρ_f, ρ_c]` integrates to `ℓ^q r^{p−4q+1}` at the dominating end. Checks: + - the least exponent is `3/7` for both densities, attained exactly by the terms marked in the table; + - every other term is `≥ 4/9`, and the intermediate separations give exactly `4/9`; + - the hypotheses on the splits; + - the optimality of `2/7`, `2/9` and `1/9` on rational grids; + - the regressions `4/11` (#218's T1) and `2/5` (#220's intermediate bound); + - that the old term `rκ²` would give `ℓ^{2/7}` at the new split; + - the max–min of Remark 1: without the `ρ_f⁵/ℓ` family both densities reach `4/9`; without only the linear pair the + candidate density reaches `4/9` and the elder density stays at `3/7`. +- **R2** Lemma L on random and edge rational instances, with equality instances, and instances where it improves on + the constant `2c` by a factor `≥ 100`. +- **R3** the inclusion (3.2): on scalar instances with `|q| ≤ |γ|²/λ`, and on matrix instances `A = −O diag(μ)Oᵀ` + (`m = 1, 2, 3`, rational orthogonal `O` by the Cayley transform, so `λ = min μ` exactly), where `q = γᵀA^{−1}γ` and + `|q| ≤ |γ|²/λ` are computed exactly; and that (Q3) puts `|φ_r|` in `[1/6, 1/2]` on `𝔅_4`. +- **R4** the sign window and (4.1) on random rational data; the exact length `144κ + 24η/|Δ|` of the `f₄`-window; the + splitting inequality of Step W2. +- **R5** `κ³ + κ²r + κr² + r³L ≤ (κ + r)²(κ + rL) ≤ (1 + L)(κ + r)³` for `L ≥ 0`, and `(κ + r)³ ≤ 4(κ³ + r³)`. +- **R6** the bookkeeping of Lemmas C⁺ and CE⁺, with `r = s²` and `κ = t²` (so that square roots are exact), and the + comparison of (CE⁺.1) with (CE.1). +- **Mutants.** Each fails only its own control, and an unknown label exits 2: + - M1 `ρ_f = ℓ^{3/11}`; + - M2 the old cusp error `rκ²`; + - M8 `ρ_c = ℓ^{1/4}`; + - M6 `a = ℓ^{2/15}` (R1, all four); + - M3 `max(|y|, |y′|)` in place of `|y| + |y′|` (R2); + - M4 `12κ` in place of `6κ` in (3.2) (R3); + - M5 `12η/|Δ|` in place of `24η/|Δ|` (R4); + - M7 `r²(1 + κ)² ≤ r` (R6). + +**What the controls do not test.** Lemmas C⁺ and CE⁺ and Proposition W⁺ as statements about random fields; the +conditional density facts (2.1)–(2.2), (4.2); the assembly. These are proved in prose. The controls test the +deterministic inequalities and the exponent arithmetic. + +## 9. Review slices + +- **A** §§1–2: Lemma L, and Lemma C⁺ as a change of #218's Step C2, with the bookkeeping of Step C3. +- **B** §3: Lemma CE⁺. The refined `𝔅_4′` estimate (3.1)–(3.2), with its use of (Q3), (2.1) and (2.2); Step E3⁺. +- **C** §§4–5: Proposition W⁺ ((4.1), the `f₄`-window, (4.2) and the dyadic layers); (W⁺.3); the assembly and the + ledger. diff --git a/frontiers/third_order_rate_20261001/README.md b/frontiers/third_order_rate_20261001/README.md new file mode 100644 index 000000000..484945db9 --- /dev/null +++ b/frontiers/third_order_rate_20261001/README.md @@ -0,0 +1,85 @@ +# The third-order lifetime laws with remainder `ℓ^{3/7}` + +**Author-side proof candidate (Anthropic Claude). Scientific effect: NONE. Nonauthor review required.** + +Object `CL-THIRD-ORDER-RATE-20261001-v1`. Full text: [`PROOF.md`](PROOF.md). + +## Result + +For every `d ≥ 2` and `L > 0`, as `ℓ ↓ 0`: + + ν_cand(ℓ) = c ℓ^{−1/3} + B_{d,L} + I^{cand} ℓ^{1/4} + c₂ ℓ^{1/3} + O(ℓ^{3/7}) (T⁺.1) + ν_eld(ℓ) = c ℓ^{−1/3} + c₁ ℓ^{1/4} + c₂ ℓ^{1/3} + ν_eld^{far,r_0^*}(ℓ) + O(ℓ^{3/7}) (E3⁺.0) + ν_eld(ℓ) = c ℓ^{−1/3} + c₁ ℓ^{1/4} + c₂ ℓ^{1/3} + O(ℓ^{3/7}) (with merged #187) (E3⁺.1) + ρ_rej(ℓ) = B_{d,L} + (I^{cand} − c₁) ℓ^{1/4} + O(ℓ^{3/7}) (with merged #187) (R⁺.1) + +Math- #218 and #220 proved these with `O(ℓ^{4/11})`. Also: +- the elder density from intermediate separations is `O(ℓ^{4/9}log(1/ℓ))`; #220 had `O(ℓ^{2/5})`; +- **Proposition W⁺**, the typed-window bound `E_Q[W_r/r²] ≤ Cr²(κ + r)²(κ + r log(2/r))P^N` for `k ≤ r`; +- at `k = 0`, the equal-height kernel satisfies `r^{d−1}Ψ_0(b, ru) = O(r³log(2/r))`, so the equal-height mass below + separation `ρ` is `O(ρ⁴log(2/ρ))`. This sharpens #198 (W.4) and proves, up to a factor `log(2/r)`, the order that + #211 suggests heuristically. + +## The three new ingredients + +| | Statement | Replaces | +|---|---|---| +| **Lemma L** | `|(c² − y²)₊ − (c² − y′²)₊| ≤ |y − y′|(|y| + |y′|)`: a Lipschitz constant free of `c = 6κ|det A|` (the inequality #218 Step C3 already uses, now applied where the global constant was) | the constant `12κ|det A|` in #218 Step C2 and #220 Step E3, the source of `(1 + κ)²` | +| **(3.1)–(3.2)** | on the elder decision's edge window, `|f₄| ≥ 6κ` or `λ ≤ |γ|²/(2κ)`, so the window costs `O(rκ)` | #220's `O(rκ²)` for `𝔅_4` | +| **Proposition W⁺** | the typed window `|Y| ≤ 6κ|det A| + O(r)` has conditional probability `O(κ + r/|det A|)` (`Y` is affine in `f₄`) | #198 (W.1), which does not charge the window | + +So the cusp kernels have errors `Cr(1 + κ)` (candidate, Lemma C⁺) and `C(r(1 + κ) + κ²r^{3/2} + κ³r²)` (elder, +Lemma CE⁺), where #218 and #220 have `Cr(1 + κ)²`. With the splits `ρ_f = ℓ^{2/7}`, `ρ_c = ℓ^{2/9}` and `a = ℓ^{1/9}`, +four error terms are exactly `ℓ^{3/7}` and all others are `O(ℓ^{4/9}log(1/ℓ))`. + +## Dependencies + +| | Sources | +|---|---| +| Consumed, unmerged | #207 (`f6df5a73` at `782211f`), #218 (`70ca57ef` at `0cf048d`), #220 (`736a35de` at `e481d23`) | +| Consumed, merged | [R], [P] with [E1]/[E2]/[REC], [Z], [C7-K], #191, #198, and #187 (`07260114`, merged 1 Oct at `c2f1270`; used only for (E3⁺.1) and the second form of (R⁺.1)) | +| Cited | #216, #223 (`c₂`); #211 (Remark 3); #188 | + +The packet cannot be integrated before #207, #218 and #220, and must be rebound if any of them changes. The workflow +checks every pin, including the current head (or the merge commit) of each consumed pull request. + +## Controls + +`r37_check.py` uses the standard library and exact rationals. Its output is `RESULTS.json`, byte-identical under `-O` +and on CPython 3.10–3.14. + +| Control | Checks | +|---|---| +| R1 | the exponent ledger: least `3/7`, attained exactly by the stated terms; others `≥ 4/9`; split hypotheses; optimality of the splits; regressions to `4/11` (#218) and `2/5` (#220); Remark 1's max–min | +| R2 | Lemma L, with equality instances | +| R3 | (3.2), on scalar instances and on exact rational matrix instances `m = 1, 2, 3` | +| R4 | the sign window, (4.1), the exact length of the `f₄`-window, the splitting inequality | +| R5, R6 | the bookkeeping of Proposition W⁺ and of Lemmas C⁺, CE⁺ | + +Mutants `M1`–`M8` each fail only their own control, and an unknown label exits 2: + + python3 -B -S r37_check.py # exit 0, output = RESULTS.json + python3 -B -S r37_check.py --mutant M1 # exit 1 + +## Review record + +- **Same-family referee.** A clean-context referee (Anthropic Claude) read the note against all ten sources at their + declared blobs. Verdict: **ACCEPT WITH MINOR FIXES**, with no major finding. Its two minor findings and twelve nits + are applied: + - Remark 1's account of which terms block a further improvement; + - the parity statements of §2 and Remark 2 are now consistent. +- **The referee's independent checks:** + - an exact ledger; + - Lemma L on 93,025 grid points; + - (3.2) on 5,400 matrix instances; + - 20,000 bookkeeping instances; + - a `d = 2` Gaussian-field Monte Carlo of Proposition W⁺. +- **Independence.** The referee is the same provider and the same GitHub account as the author, so it carries zero + organizational independence. Nonauthor review is required. The review slices are in PROOF §9. + +## Not claimed + +- sharpness of `3/7`; the formal next term is of order `ℓ^{1/2}`; +- certified constants; +- uniformity in `d` or `L`; +- the adjacent-pair density. diff --git a/frontiers/third_order_rate_20261001/RESULTS.json b/frontiers/third_order_rate_20261001/RESULTS.json new file mode 100644 index 000000000..8a2921cfb --- /dev/null +++ b/frontiers/third_order_rate_20261001/RESULTS.json @@ -0,0 +1,84 @@ +{ + "checks": { + "R1_exponent_ledger": { + "a": "l^1/9", + "candidate_least": "3/7", + "candidate_terms": { + "F: l rho_f^-2 (finite part)": "3/7", + "F: rho_f^2": "4/7", + "F: rho_f^5/l (Lemma F layer)": "3/7", + "J2: rho_c^3": "2/3", + "J3: l rho_c^-2": "5/9", + "J3: l^2 rho_c^-7": "4/9", + "J4: l^2 rho_c^-7": "4/9", + "J5: l": "1", + "K: Lemma C+ r^1 kappa^0": "4/9", + "K: Lemma C+ r^1 kappa^1": "3/7", + "K: l^2 rho_c^-7 (upper tail)": "4/9", + "K: rho_f^5/l (Lemma O tail)": "3/7" + }, + "elder_least": "3/7", + "elder_terms": { + "F: l rho_f^-2 (finite part)": "3/7", + "F: rho_f^2": "4/7", + "F: rho_f^5/l (Lemma F layer)": "3/7", + "F: rho_f^5/l (rejected fold mass, [C7-K] (K2))": "3/7", + "I: [a,r0*] l^(2/3) a^-2": "4/9", + "I: [a,r0*] l^(5/3) a^-7": "8/9", + "I: [rho_c,a] a^4 (log)": "4/9", + "I: [rho_c,a] l^3 rho_c^-11 (log)": "5/9", + "J4: l^2 rho_c^-7": "4/9", + "K: Lemma CE+ r^1 kappa^0": "4/9", + "K: Lemma CE+ r^1 kappa^1": "3/7", + "K: Lemma CE+ r^2 kappa^3": "3/7", + "K: Lemma CE+ r^3/2 kappa^2": "3/7", + "K: l^2 rho_c^-7 (upper tail)": "4/9", + "K: rho_f^5/l (Lemma O/O' tail)": "3/7", + "far: #187 Theorem F": "2/3" + }, + "hypotheses": true, + "intermediate_least": "4/9", + "passed": true, + "regression_218": "4/11", + "regression_220_intermediate": "2/5", + "remark1_maxmin": { + "drop_layer_cand": "4/9", + "drop_layer_eld": "4/9", + "drop_linear_cand": "4/9", + "drop_linear_eld": "3/7" + }, + "rho_c": "l^2/9", + "rho_f": "l^2/7" + }, + "R2_lemma_L": { + "equality_instances": 700, + "improvement_factor_le_1/100_instances": 2, + "instances": 6108, + "passed": true + }, + "R3_refined_B4": { + "instances": 6901, + "matrix_instances": 900, + "passed": true, + "second_alternative_only": 66 + }, + "R4_typed_window": { + "passed": true, + "splitting_instances": 3000, + "typed_instances": 5035, + "window_instances": 3000 + }, + "R5_W_plus_bookkeeping": { + "instances": 5000, + "passed": true + }, + "R6_C_plus_CE_plus_bookkeeping": { + "instances": 8000, + "passed": true + } + }, + "mutant": null, + "object": "CL-THIRD-ORDER-RATE-20261001-v1 controls", + "passed": true, + "scientific_effect": "NONE" +} diff --git a/frontiers/third_order_rate_20261001/SOURCES.json b/frontiers/third_order_rate_20261001/SOURCES.json new file mode 100644 index 000000000..e454caf62 --- /dev/null +++ b/frontiers/third_order_rate_20261001/SOURCES.json @@ -0,0 +1,233 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "object": "CL-THIRD-ORDER-RATE-20261001-v1", + "kind": "author-side proof candidate: the candidate and elder lifetime densities to third order with remainder O(l^(3/7)) in every d >= 2 (Theorems T+ and E3+), improving the O(l^(4/11)) of Math- #218 and #220: nu_cand = c l^(-1/3) + B_{d,L} + I^cand l^(1/4) + c2 l^(1/3) + O(l^(3/7)); nu_eld = c l^(-1/3) + c1 l^(1/4) + c2 l^(1/3) + nu_eld^{far,r_0^*} + O(l^(3/7)), and with merged #187 + O(l^(3/7)); rejected density B_{d,L} + (I^cand - c1) l^(1/4) + O(l^(3/7)); new: Lemma L (a kappa-free local Lipschitz bound for (c^2 - y^2)_+), Lemma C+ (candidate cusp kernel, error r(1 + kappa)), Lemma CE+ (elder cusp kernel, error r(1 + kappa) + kappa^2 r^(3/2) + kappa^3 r^2, through a refined bound on the edge window B_4), Proposition W+ (typed-window bound E_Q[W_r/r^2] <= C r^2 (kappa + r)^2 (kappa + r log(2/r)) P^N for k <= r; at k = 0 the equal-height kernel is O(r^3 log(2/r)) near the diagonal); intermediate elder mass O(l^(4/9) log(1/l))", + "author": "Anthropic Claude", + "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", + "read_at": { + "branch_base": "77b854cac6017ecdc0ea7abf6f978f9c6c9cb787" + }, + "consumed": [ + { + "path": "frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md", + "bytes": 17734, + "sha256": "380b7d0abdb0fe2de5a6564565af9560d3f1b1ce22fd5538927db0c52f4f3a4a", + "git_blob": "247b3ecf80bfbe896948d5d489b2d5842a81c481", + "tag": "R", + "use": "(R2)-(R5): pin densities (R5), coupling, moments" + }, + { + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "bytes": 40261, + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "tag": "P", + "use": "section 2 finite-jet rank and section 15 parity factorization, through #218 and #220" + }, + { + "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_zero_gap_limit_20260929/PROOF.md", + "bytes": 17592, + "sha256": "f0e563c45c41333f2bb6e5bf5cb98f0d3b592e2abf2af1c1b098c21ad77cb777", + "git_blob": "5b6328ea3d6afcbeb731698b3834e536f72d1bcb", + "tag": "Z", + "use": "(Z2)-(Z3): the equal-height kernel Psi_0 and B_{d,L}" + }, + { + "path": "frontiers/c7_total_bounded_20260929/PROOF.md", + "bytes": 14982, + "sha256": "16c0efe372c1b1f26460aaa109287fed78e6fbd2dd00a0530998db296278dd01", + "git_blob": "28748b086ec6761ef467dc67cba475fbdf8b7455", + "tag": "C7-K", + "use": "(K2): the rejected fold mass" + }, + { + "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): Lemma E Steps 1-3 (for (F1) at k = 0); section 2: r_0^* and the k = 0 identity r^(d-1) Psi_0(b, ru) = r^-2 A_r(b, 0, u)" + }, + { + "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): section 3 (3.1), the sign window and (3.2); Lemma W with its k = 0 clause, (W.1); the proof of (W.4); 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, with the blob #220 pins): Theorem F at the single separation rho = r_0^* (far elder density O(l^(2/3))), for (E3+.1) and the second form of (R+.1) 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; (0.2)/(CU.2), the coefficient c1; section 7 (through #218)", + "head": "782211f494aeef1a24b70fe76423c66afe2ea9dc", + "pr": "Math- #207" + }, + { + "path": "frontiers/candidate_third_order_20261001/PROOF.md", + "bytes": 37220, + "sha256": "6c1279164499d4fe2fbeee244b40dafa2159758d20f04826cd67d7602ea97fe4", + "git_blob": "70ca57ef05199e75417d7d57928c1e1c93bf944e", + "tag": "218", + "use": "Lemma D (1.1); (1.2); Lemma F (F.1)-(F.2); Lemma C and its proof (Steps C1-C3, (C.2)); Lemma O (O.1); (0.1), the coefficient c2; section 4: the decomposition F + K + J2 + ... + J5 and the bounds on F and J2-J5", + "head": "0cf048d18eb28a4ba37eba89c238a2910d4ca915", + "pr": "Math- #218" + }, + { + "path": "frontiers/elder_third_order_20261001/PROOF.md", + "bytes": 68890, + "sha256": "f3a64ad9551e02441eb3e3776aa72441c3c5a3b939a385e3031169a1608756a7", + "git_blob": "736a35de9d96e26372349f2a093feb40e47816ce", + "tag": "220", + "use": "section 0 (near/far identity, A^eld, c1); Lemma Q; section 2 (notation, facts (F1)-(F7), (2.1)-(2.2), Lemma G, Lemma CE and its proof, Steps E1-E6); Lemma O-prime; Lemma H (through Lemma S-prime); Lemma S-prime (S-prime.1); section 4: the decomposition F^eld + K^eld + I^eld - J4 and the bound on F^eld", + "head": "e481d230cba1f6f29d89c76c8086ee512a61c22e", + "pr": "Math- #220" + } + ], + "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 (Remark 4)", + "head": "04c08e1534122f210be888742fcd7a568e45b097", + "pr": "Math- #216" + }, + { + "path": "frontiers/c2_exact_20261001/NOTE.md", + "bytes": 14480, + "sha256": "598fc86a7c6b21bad438ef087e5aa7521f0fae08e25fa4f40f9b2ba635846dbb", + "git_blob": "a2798b87674ed5fc0d2144697e77ccb9b185b4ab", + "tag": "223", + "use": "c2 in closed form for the Gaussian kernel (Remark 4)", + "head": "b2247fd81712f131ad604d13125580bf1afe2f94", + "pr": "Math- #223" + }, + { + "path": "frontiers/equal_height_mass_value_20261001/NOTE.md", + "bytes": 16177, + "sha256": "9080a5dc567710e0668890cd209484db9026b19ff4707341487f289e2f7c7410", + "git_blob": "ed0d3fa8e4c28d181fa7d21efcde74933cc6f03c", + "tag": "211", + "use": "the heuristic r^(d-1) Psi_0 = O(r^3) quoted in Remark 3 and its Monte Carlo of I(s)", + "head": "8e89fe886368ae048e125c26f3ac51aa9bec83f6", + "pr": "Math- #211" + }, + { + "path": "frontiers/far_elder_flat_ridge_20260930/PROOF.md", + "bytes": 22806, + "sha256": "957f9c5e6557a558b2c055fa2a1f11ba301581995b8958658fad2edf47136f57", + "git_blob": "50cfbf4fcb9a3526f979eaedf885d42824a3c3a3", + "tag": "188", + "use": "an alternative far elder bound (cited only)", + "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" + }, + { + "tag": "Weyl", + "reference": "Weyl integration formula on symmetric matrices", + "use": "through #218 Lemma D" + }, + { + "tag": "Anderson", + "reference": "T. W. Anderson, Proc. Amer. Math. Soc. 6 (1955) 170-176", + "use": "through #218 (1.2)" + } + ], + "mutants": [ + "M1", + "M2", + "M3", + "M4", + "M5", + "M6", + "M7", + "M8" + ], + "replayed": [ + "r37_check.py" + ], + "referee": { + "kind": "clean-context same-family referee (Anthropic Claude subagent), before submission, with a delta check of the fixes", + "verdict": "ACCEPT WITH MINOR FIXES (no major finding; two minor findings and twelve nits, all applied); delta check: one required README correction (applied) and four optional items (applied)", + "report": "project archive V2_2/frontiers_third_order_rate_20261001/REFEREE_1.md", + "report_sha256": "eb62ad30af43f78521eff327cca7200a5a7ff56a17fb29a374e2f7153a035632", + "report_bytes": 19941, + "delta_report": "project archive V2_2/frontiers_third_order_rate_20261001/REFEREE_1_DELTA.md", + "delta_report_sha256": "9b8bf24df27d8157a25978ad30518cd99f641e7d2fb7acd7e75c38ff673339ab", + "delta_report_bytes": 7391, + "independent_checks": "source blobs; an exact independent ledger (least 3/7, others >= 4/9) and a max-min over the splits; Lemma L on 93,025 exact grid points; (3.2) on 5,400 exact matrix instances m = 1..4; 20,000 exact bookkeeping instances; sympy for Remark 4 and the integrals; (4.2) numerically; a d = 2 Gaussian-field Monte Carlo of Proposition W+ under the exact two-site regression (k = 0: E_Q[W_r/r^2]/r^2 ~ 0.03 r^3; ratios to W+ bounded)", + "independence": "same provider and GitHub account as the author; zero organizational independence" + }, + "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": 37046, + "sha256": "2fd71925c3e501b94acec8e2df3ee02300f91388280886a91cd730ee62341eed" + }, + { + "path": "README.md", + "bytes": 4991, + "sha256": "f45e9c9dc5bf24b1a54c8411a927d5abeb5261845a7745e8d8c6b87b847b3556" + }, + { + "path": "r37_check.py", + "bytes": 19191, + "sha256": "d52885b9eb8bcf6eef0447b07a832fa71c29f3173d584dd20c65ccc87ffa1966" + }, + { + "path": "RESULTS.json", + "bytes": 2234, + "sha256": "7f877f034baaa5b7c8a879a76dd2b825e57869478fdc396897cde1da9bf10ade" + } + ] +} diff --git a/frontiers/third_order_rate_20261001/r37_check.py b/frontiers/third_order_rate_20261001/r37_check.py new file mode 100644 index 000000000..d521770d5 --- /dev/null +++ b/frontiers/third_order_rate_20261001/r37_check.py @@ -0,0 +1,347 @@ +#!/usr/bin/env python3 +"""Exact controls for CL-THIRD-ORDER-RATE-20261001-v1 (frontiers/third_order_rate_20261001/PROOF.md). +Standard library only, exact rationals. Run: python3 -B -S r37_check.py (and with -O; output byte-identical). +Mutants: --mutant M1|...|M8 must exit 1; an unknown label exits 2. + + R1 the exponent ledger of section 5 with rho_f = l^(2/7), rho_c = l^(2/9), a = l^(1/9). An error r^p kappa^q + (kappa = l r^-4) on [rho_f, rho_c] integrates to l^q r^(p-4q+1) at the endpoint that dominates. Candidate: least + exponent 3/7, attained exactly by rho_f^5/l (twice: Lemma F's layer and Lemma O's tail) and l rho_f^-2 (twice: the + finite part and Lemma C+'s linear term). Elder: least 3/7, attained exactly by the same four terms, the rejected fold + mass rho_f^5/l, and Lemma CE+'s l^2 rho_f^-11/2 and l^3 rho_f^-9. Every other term is >= 4/9, and the intermediate + separations give exactly 4/9 (log). The hypotheses l^(1/3) < rho_f < l^(1/4) < rho_c < a and kappa <= 1 on + [rho_c, r0*] hold. Optimality: 2/7, 2/9 and 1/9 maximize the respective minima over rational grids. Regression: + #218's error r(1 + kappa)^2 at rho_f = l^(3/11) gives 4/11 (its T1), and #198 (W.1) with a = l^(2/15) gives 2/5 + on the intermediate separations (#220 X1). Remark 1's max-min over rho_f: without the rho_f^5/l family both + densities reach 4/9; without only the linear pair (l rho_f^-2) the candidate reaches 4/9 and the elder stays 3/7. + R2 Lemma L: |(c^2 - y^2)_+ - (c^2 - y'^2)_+| <= |y - y'| (|y| + |y'|) on random and edge rational instances, with + equality instances; the old constant 2c also holds, and the new bound is smaller by a factor <= 1/100 on some + instances with a nonzero difference. + R3 the refined B_4 estimate (Lemma CE+, Step E2+): if A <= -lam I, |q| <= |gamma|^2/lam and + |f4 - 3q| = 72 kappa |phi| with 1/6 <= |phi| <= 1/2, then |f4| >= 6 kappa or lam <= |gamma|^2/(2 kappa); on scalar + instances and on matrix instances A = -O diag(mu) O^T (m = 1, 2, 3; O rational orthogonal by the Cayley + transform), where q = gamma^T A^-1 gamma and |q| <= |gamma|^2/min(mu) are exact; and eps* <= kappa/4 with + ||phi| - 1/3| <= 2 eps*/(3 kappa) puts |phi| in [1/6, 1/2]. + R4 Proposition W+: the typed sign pattern (-6kD + rY + R_M)(6kD + rY + R_S) < 0 forces |rY| <= 6k|D| + max|R_i| and + |det K_M det K_S| <= r^2 (12 kappa |D| + 2 eta)^2, eta = max|R_i|/r; the f4-window + {|(f4/12) D + c0| <= 6 kappa |D| + eta} has length exactly 144 kappa + 24 eta/|D|; and the splitting inequality + (x + y)^2 min(1, a + b) <= 2 (x^2 + y^2)(a + min(1, b)) for x, y, a, b >= 0. + R5 Proposition W+ bookkeeping: kappa^3 + kappa^2 r + kappa r^2 + r^3 L <= (kappa + r)^2 (kappa + r L) + <= (1 + L)(kappa + r)^3 for L >= 0, and (kappa + r)^3 <= 4 (kappa^3 + r^3). + R6 Lemma C+/CE+ bookkeeping, with r = s^2, kappa = t^2, kappa r <= 1, r <= 1: kappa^2 min(1, kappa) r^3 <= r; + kappa^(1/2) min(1, kappa) r^(3/2) <= r; r^2 (1 + kappa)^2 <= 2 r (1 + kappa); kappa^2 r^2 <= kappa r; and the + new elder error is <= the old one: kappa^2 r^(3/2) + kappa^3 r^2 <= 2 kappa^2 r. +""" +import argparse +import json +import random +import sys +from fractions import Fraction as Fr + +MUTANT = None + + +def cusp_integral_exponent(p, q, ef, ec): + """l^q r^(p-4q+1) at the dominating endpoint of [rho_f, rho_c] (rho_f = l^ef, rho_c = l^ec); g = 0 is a log.""" + g = p - 4 * q + 1 + if g < 0: + return q + ef * g, 'rho_f' + if g > 0: + return q + ec * g, 'rho_c' + return q, 'log' + + +# ----------------------------------------------------------------------------------------------- R1 exponents +def ledger(ef, ec, ea, cand_forms, eld_forms): + one = Fr(1) + cand = {'F: rho_f^2': 2 * ef, 'F: rho_f^5/l (Lemma F layer)': 5 * ef - one, + 'F: l rho_f^-2 (finite part)': one - 2 * ef, + 'K: rho_f^5/l (Lemma O tail)': 5 * ef - one, 'K: l^2 rho_c^-7 (upper tail)': 2 - 7 * ec, + 'J2: rho_c^3': 3 * ec, 'J3: l^2 rho_c^-7': 2 - 7 * ec, 'J3: l rho_c^-2': one - 2 * ec, + 'J4: l^2 rho_c^-7': 2 - 7 * ec, 'J5: l': one} + for (p, q) in cand_forms: + e, _ = cusp_integral_exponent(p, q, ef, ec) + cand['K: Lemma C+ r^%s kappa^%s' % (p, q)] = e + eld = {'F: rho_f^2': 2 * ef, 'F: rho_f^5/l (Lemma F layer)': 5 * ef - one, + 'F: l rho_f^-2 (finite part)': one - 2 * ef, 'F: rho_f^5/l (rejected fold mass, [C7-K] (K2))': 5 * ef - one, + 'K: rho_f^5/l (Lemma O/O\' tail)': 5 * ef - one, 'K: l^2 rho_c^-7 (upper tail)': 2 - 7 * ec, + 'J4: l^2 rho_c^-7': 2 - 7 * ec, + 'I: [rho_c,a] l^3 rho_c^-11 (log)': 3 - 11 * ec, 'I: [rho_c,a] a^4 (log)': 4 * ea, + 'I: [a,r0*] l^(5/3) a^-7': Fr(5, 3) - 7 * ea, 'I: [a,r0*] l^(2/3) a^-2': Fr(2, 3) - 2 * ea, + 'far: #187 Theorem F': Fr(2, 3)} + for (p, q) in eld_forms: + e, _ = cusp_integral_exponent(p, q, ef, ec) + eld['K: Lemma CE+ r^%s kappa^%s' % (p, q)] = e + return cand, eld + + +def r1(): + ef = Fr(3, 11) if MUTANT == 'M1' else Fr(2, 7) + ec = Fr(1, 4) if MUTANT == 'M8' else Fr(2, 9) + ea = Fr(2, 15) if MUTANT == 'M6' else Fr(1, 9) + cand_forms = [(Fr(1), Fr(0)), (Fr(1), Fr(2) if MUTANT == 'M2' else Fr(1))] + eld_forms = [(Fr(1), Fr(0)), (Fr(1), Fr(1)), (Fr(3, 2), Fr(2)), (Fr(2), Fr(3))] + cand, eld = ledger(ef, ec, ea, cand_forms, eld_forms) + target = Fr(3, 7) + ok = min(cand.values()) == target and min(eld.values()) == target + want_c = sorted(['F: rho_f^5/l (Lemma F layer)', 'F: l rho_f^-2 (finite part)', 'K: rho_f^5/l (Lemma O tail)', + 'K: Lemma C+ r^1 kappa^1']) + want_e = sorted(['F: rho_f^5/l (Lemma F layer)', 'F: l rho_f^-2 (finite part)', + 'F: rho_f^5/l (rejected fold mass, [C7-K] (K2))', 'K: rho_f^5/l (Lemma O/O\' tail)', + 'K: Lemma CE+ r^1 kappa^1', 'K: Lemma CE+ r^3/2 kappa^2', 'K: Lemma CE+ r^2 kappa^3']) + ok &= sorted(k for k, v in cand.items() if v == target) == want_c + ok &= sorted(k for k, v in eld.items() if v == target) == want_e + ok &= all(v >= Fr(4, 9) for k, v in cand.items() if v != target) + ok &= all(v >= Fr(4, 9) for k, v in eld.items() if v != target) + inter = [v for k, v in eld.items() if k.startswith('I:')] + ok &= min(inter) == Fr(4, 9) + # hypotheses: l^(1/3) < rho_f < l^(1/4) < rho_c < a < 1 (exponents reversed); kappa <= 1 on [rho_c, r0*] + q = Fr(1, 4) + hyp = Fr(1, 3) > ef > q > ec > ea > 0 and 1 - 4 * ec >= 0 and 1 - 4 * ea >= 0 and 1 - 3 * ef >= 0 + ok &= hyp + # optimality on rational grids: rho_f, rho_c and a maximize the minima of the terms that depend on them + grid = sorted({Fr(i, n) for n in range(2, 241) for i in range(1, n)}) + fdep = lambda f: min(5 * f - 1, 1 - 2 * f, cusp_integral_exponent(Fr(3, 2), Fr(2), f, ec)[0], + cusp_integral_exponent(Fr(2), Fr(3), f, ec)[0]) + fbest = max((g for g in grid if q < g < Fr(1, 3)), key=fdep) + cbest = max((g for g in grid if Fr(1, 9) < g < q), key=lambda c: min(2 * c, 2 - 7 * c, 3 - 11 * c)) + abest = max((g for g in grid if 0 < g < Fr(2, 9)), key=lambda a: min(4 * a, Fr(2, 3) - 2 * a)) + ok &= fbest == Fr(2, 7) and fdep(fbest) == target and cbest == Fr(2, 9) and abest == Fr(1, 9) + # regression: #218 (error r(1 + kappa)^2, rho_f = l^(3/11)) and #220's intermediate split (W.1, a = l^(2/15)) + old_c, _ = ledger(Fr(3, 11), Fr(2, 9), Fr(1, 9), [(Fr(1), Fr(0)), (Fr(1), Fr(1)), (Fr(1), Fr(2))], []) + reg218 = min(old_c.values()) + reg220 = min(2 - 7 * Fr(2, 9), 3 * Fr(2, 15), Fr(5, 3) - 7 * Fr(2, 15), Fr(2, 3) - 2 * Fr(2, 15)) + ok &= reg218 == Fr(4, 11) and reg220 == Fr(2, 5) + # the old linear-in-kappa^2 term at the new split would be l^(2/7): the improvement of Lemma C+ is needed + ok &= cusp_integral_exponent(Fr(1), Fr(2), Fr(2, 7), Fr(2, 9))[0] == Fr(2, 7) + # Remark 1: max over rho_f = l^f (1/4 < f < 1/3, rational grid) of the least exponent, with a family removed + def best(drop, elder): + vals = [] + for f in (g for g in grid if q < g < Fr(1, 3)): + c_, e_ = ledger(f, Fr(2, 9), Fr(1, 9), cand_forms, eld_forms) + terms = e_ if elder else c_ + keep = [v for k, v in terms.items() if not any(dd in k for dd in drop)] + vals.append(min(keep)) + return max(vals) + layer = ('rho_f^5/l',) + linear = ('l rho_f^-2', 'r^1 kappa^1') + pair = {'drop_layer_cand': best(layer, False), 'drop_layer_eld': best(layer, True), + 'drop_linear_cand': best(linear, False), 'drop_linear_eld': best(linear, True)} + ok &= pair == {'drop_layer_cand': Fr(4, 9), 'drop_layer_eld': Fr(4, 9), 'drop_linear_cand': Fr(4, 9), + 'drop_linear_eld': Fr(3, 7)} + return {'rho_f': 'l^' + str(ef), 'rho_c': 'l^' + str(ec), 'a': 'l^' + str(ea), + 'candidate_least': str(min(cand.values())), 'elder_least': str(min(eld.values())), + 'intermediate_least': str(min(inter)), 'hypotheses': bool(hyp), + 'regression_218': str(reg218), 'regression_220_intermediate': str(reg220), + 'remark1_maxmin': {k: str(v) for k, v in sorted(pair.items())}, + 'candidate_terms': {k: str(v) for k, v in sorted(cand.items())}, + 'elder_terms': {k: str(v) for k, v in sorted(eld.items())}, 'passed': bool(ok)} + + +# ----------------------------------------------------------------------------------------------- R2 Lemma L +def wplus(c, y): + v = c * c - y * y + return v if v > 0 else Fr(0) + + +def r2(rng): + ok = True + eq = small = 0 + insts = [] + for _ in range(6000): + c = Fr(rng.randint(0, 60), rng.randint(1, 12)) + y = Fr(rng.randint(-90, 90), rng.randint(1, 12)) + yp = Fr(rng.randint(-90, 90), rng.randint(1, 12)) + insts.append((c, y, yp)) + for c in (Fr(0), Fr(1), Fr(7, 3)): + for y in (-c, c, Fr(0), c / 2, -c / 2, 2 * c + 1): + for yp in (-c, c, Fr(0), c / 3, 3 * c, -3 * c - 1): + insts.append((c, y, yp)) + for (c, y, yp) in insts: + lhs = abs(wplus(c, y) - wplus(c, yp)) + fac = max(abs(y), abs(yp)) if MUTANT == 'M3' else abs(y) + abs(yp) + rhs = abs(y - yp) * fac + ok &= lhs <= rhs + ok &= lhs <= 2 * c * abs(y - yp) # the old constant, also valid + if lhs == rhs and lhs > 0: + eq += 1 + if lhs > 0 and 100 * rhs <= 2 * c * abs(y - yp): + small += 1 + ok &= eq > 0 and small > 0 + return {'instances': len(insts), 'equality_instances': eq, 'improvement_factor_le_1/100_instances': small, + 'passed': bool(ok)} + + +# ----------------------------------------------------------------------------------------------- R3 refined B_4 +def matmul(X, Y): + return [[sum(X[i][k] * Y[k][j] for k in range(len(Y))) for j in range(len(Y[0]))] for i in range(len(X))] + + +def inverse(X): + n = len(X) + M = [list(X[i]) + [Fr(int(i == j)) for j in range(n)] for i in range(n)] + for col in range(n): + piv = next(i for i in range(col, n) if M[i][col] != 0) + M[col], M[piv] = M[piv], M[col] + pv = M[col][col] + M[col] = [v / pv for v in M[col]] + for i in range(n): + if i != col and M[i][col] != 0: + fac = M[i][col] + M[i] = [a - fac * b for a, b in zip(M[i], M[col])] + return [row[n:] for row in M] + + +def cayley(K): + n = len(K) + I = [[Fr(int(i == j)) for j in range(n)] for i in range(n)] + return matmul([[I[i][j] - K[i][j] for j in range(n)] for i in range(n)], + inverse([[I[i][j] + K[i][j] for j in range(n)] for i in range(n)])) + + +def r3(rng): + ok = True + insts = [] + for _ in range(4000): + kap = Fr(rng.randint(1, 400), rng.randint(1, 20)) + lam = Fr(rng.randint(1, 300), rng.randint(1, 30)) + g2 = Fr(rng.randint(0, 900), rng.randint(1, 30)) # |gamma|^2 + q = (g2 / lam) * Fr(rng.randint(-1000, 1000), 1000) # |q| <= |gamma|^2 / lam + phi = Fr(rng.choice((-1, 1))) * (Fr(1, 6) + Fr(rng.randint(0, 600), 1800)) # 1/6 <= |phi| <= 1/2 + insts.append((kap, lam, g2, q, phi)) + insts.append((Fr(1), Fr(1), Fr(1), Fr(1, 2), Fr(-1, 6))) # |f4| = 21/2: separates 6 kappa from 12 kappa + nmat = second = 0 + for m in (1, 2, 3): # matrix instances: A = -O diag(mu) O^T + for _ in range(300): + K = [[Fr(0)] * m for _ in range(m)] + for i in range(m): + for j in range(i + 1, m): + v = Fr(rng.randint(-9, 9), rng.randint(1, 5)) + K[i][j], K[j][i] = v, -v + O = cayley(K) + mu = [Fr(rng.randint(1, 400), rng.randint(1, 40)) for _ in range(m)] + gam = [Fr(rng.randint(-60, 60), rng.randint(1, 6)) for _ in range(m)] + Og = [sum(O[i][j] * gam[i] for i in range(m)) for j in range(m)] # O^T gamma + q = -sum(Og[j] * Og[j] / mu[j] for j in range(m)) # gamma^T A^-1 gamma + Ainv = [[-sum(O[i][l] * O[j][l] / mu[l] for l in range(m)) for j in range(m)] for i in range(m)] + ok &= q == sum(gam[i] * Ainv[i][j] * gam[j] for i in range(m) for j in range(m)) + A = [[-sum(O[i][l] * O[j][l] * mu[l] for l in range(m)) for j in range(m)] for i in range(m)] + ok &= matmul(A, Ainv) == [[Fr(int(i == j)) for j in range(m)] for i in range(m)] + lam, g2 = min(mu), sum(g * g for g in gam) + ok &= abs(q) <= g2 / lam + kap = Fr(rng.randint(1, 400), rng.randint(1, 20)) + phi = Fr(rng.choice((-1, 1))) * (Fr(1, 6) + Fr(rng.randint(0, 600), 1800)) + insts.append((kap, lam, g2, q, phi)) + nmat += 1 + for (kap, lam, g2, q, phi) in insts: + f4 = 3 * q + 72 * kap * phi + thr = 12 * kap if MUTANT == 'M4' else 6 * kap + ok &= abs(f4) >= thr or lam <= g2 / (2 * kap) + if abs(f4) < 6 * kap: + second += 1 + for _ in range(2000): # (Q3) puts |phi| in [1/6, 1/2] on B_4 + kap = Fr(rng.randint(1, 400), rng.randint(1, 20)) + eps = kap / 4 * Fr(rng.randint(0, 1000), 1000) + dev = 2 * eps / (3 * kap) * Fr(rng.randint(-1000, 1000), 1000) + aphi = Fr(1, 3) + dev + ok &= Fr(1, 6) <= aphi <= Fr(1, 2) + ok &= second > 0 + return {'instances': len(insts) + 2000, 'matrix_instances': nmat, 'second_alternative_only': second, + 'passed': bool(ok)} + + +# ----------------------------------------------------------------------------------------------- R4 typed window +def r4(rng): + ok = True + typed = 0 + for _ in range(6000): + k = Fr(rng.randint(0, 40), rng.randint(1, 20)) + r = Fr(rng.randint(1, 20), 20) + D = Fr(rng.choice((-1, 1)) * rng.randint(1, 80), rng.randint(1, 20)) + Y = Fr(rng.randint(-200, 200), rng.randint(1, 20)) + RM = Fr(rng.randint(-50, 50), rng.randint(1, 40)) + RS = Fr(rng.randint(-50, 50), rng.randint(1, 40)) + kM, kS = -6 * k * D + r * Y + RM, 6 * k * D + r * Y + RS + if kM * kS < 0: + typed += 1 + Rb = max(abs(RM), abs(RS)) + eta, kap = Rb / r, k / r + ok &= abs(r * Y) <= 6 * k * abs(D) + Rb + ok &= abs(kM * kS) <= r * r * (12 * kap * abs(D) + 2 * eta) ** 2 + ok &= abs(Y) <= 6 * kap * abs(D) + eta + for _ in range(3000): + D = Fr(rng.choice((-1, 1)) * rng.randint(1, 80), rng.randint(1, 20)) + c0 = Fr(rng.randint(-200, 200), rng.randint(1, 20)) + kap = Fr(rng.randint(0, 60), rng.randint(1, 20)) + eta = Fr(rng.randint(0, 60), rng.randint(1, 20)) + half = 6 * kap * abs(D) + eta + x1, x2 = (-c0 - half) * 12 / D, (-c0 + half) * 12 / D + length = abs(x2 - x1) + claimed = 144 * kap + (12 if MUTANT == 'M5' else 24) * eta / abs(D) + ok &= length == claimed + lo, hi = min(x1, x2), max(x1, x2) + for x in (lo, hi, (lo + hi) / 2): + ok &= abs(x / 12 * D + c0) <= half + for x in (lo - 1, hi + 1): + ok &= abs(x / 12 * D + c0) > half + for _ in range(3000): # (x + y)^2 min(1, a + b) <= 2(x^2 + y^2)(a + min(1, b)) + x, y = Fr(rng.randint(0, 90), rng.randint(1, 9)), Fr(rng.randint(0, 90), rng.randint(1, 9)) + a, b = Fr(rng.randint(0, 40), rng.randint(1, 40)), Fr(rng.randint(0, 40), rng.randint(1, 40)) + ok &= (x + y) ** 2 * min(Fr(1), a + b) <= 2 * (x * x + y * y) * (a + min(Fr(1), b)) + ok &= typed > 500 + return {'typed_instances': typed, 'window_instances': 3000, 'splitting_instances': 3000, 'passed': bool(ok)} + + +# ----------------------------------------------------------------------------------------------- R5 W+ bookkeeping +def r5(rng): + ok = True + for _ in range(5000): + kap = Fr(rng.randint(0, 100), rng.randint(1, 100)) + r = Fr(rng.randint(1, 100), 100) + L = Fr(rng.randint(0, 400), 20) + lhs = kap ** 3 + kap * kap * r + kap * r * r + r ** 3 * L + mid = (kap + r) ** 2 * (kap + r * L) + ok &= lhs <= mid <= (1 + L) * (kap + r) ** 3 and (kap + r) ** 3 <= 4 * (kap ** 3 + r ** 3) + return {'instances': 5000, 'passed': bool(ok)} + + +# ----------------------------------------------------------------------------------------------- R6 C+/CE+ bookkeeping +def r6(rng): + ok = True + n = 0 + for _ in range(8000): + s = Fr(rng.randint(1, 60), 60) # r = s^2 in (0, 1] + t = Fr(rng.randint(1, 1000), 1000) / s # kappa = t^2, kappa r = (t s)^2 <= 1 + r, kap = s * s, t * t + n += 1 + mn = min(Fr(1), kap) + ok &= kap * kap * mn * r ** 3 <= r + ok &= t * mn * s ** 3 <= r # kappa^(1/2) min(1, kappa) r^(3/2) <= r + bound = r if MUTANT == 'M7' else 2 * r * (1 + kap) + ok &= r * r * (1 + kap) ** 2 <= bound + ok &= kap * kap * r * r <= kap * r + ok &= kap * kap * s ** 3 + kap ** 3 * r * r <= 2 * kap * kap * r # new elder error <= old r (1 + kappa)^2 part + ok &= n == 8000 + return {'instances': n, '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-THIRD-ORDER-RATE-20261001-v1 controls', 'scientific_effect': 'NONE', 'mutant': MUTANT, + 'checks': {'R1_exponent_ledger': r1(), 'R2_lemma_L': r2(rng), 'R3_refined_B4': r3(rng), + 'R4_typed_window': r4(rng), 'R5_W_plus_bookkeeping': r5(rng), + 'R6_C_plus_CE_plus_bookkeeping': r6(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()) From 5dbe15cdc5f6d67b37dcefb176e9ad7433d6f77e Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 1 Oct 2026 15:23:20 +0000 Subject: [PATCH 2/2] Third-order rate 3/7: rebind #220 to its status-only update (c8767dde at 70dcf31) #220's PROOF changed 736a35de -> c8767dde by a status-only update (#187 listed as merged; Lemma S' range r <= r_0^* <= 1 and sign stated; X8 negative witness); every part consumed here is unchanged. #207's head moved to b12ff46 by a guarded main-only merge (blob f6df5a73 unchanged). #223 merged at f9ebba1 and moves to cited_only. RESULTS.json is unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .github/workflows/third-order-rate.yml | 1 + frontiers/third_order_rate_20261001/PROOF.md | 20 +++++---- frontiers/third_order_rate_20261001/README.md | 4 +- .../third_order_rate_20261001/SOURCES.json | 42 +++++++++---------- 4 files changed, 37 insertions(+), 30 deletions(-) diff --git a/.github/workflows/third-order-rate.yml b/.github/workflows/third-order-rate.yml index 333fcf109..666bdbc6b 100644 --- a/.github/workflows/third-order-rate.yml +++ b/.github/workflows/third-order-rate.yml @@ -19,6 +19,7 @@ name: Third-order rate 3/7 exact controls - 'frontiers/cusp_second_order_20261001/PROOF.md' - 'frontiers/candidate_third_order_20261001/PROOF.md' - 'frontiers/elder_third_order_20261001/PROOF.md' + - 'frontiers/c2_exact_20261001/NOTE.md' workflow_dispatch: permissions: diff --git a/frontiers/third_order_rate_20261001/PROOF.md b/frontiers/third_order_rate_20261001/PROOF.md index 4f6dbf252..110ed33a5 100644 --- a/frontiers/third_order_rate_20261001/PROOF.md +++ b/frontiers/third_order_rate_20261001/PROOF.md @@ -25,22 +25,27 @@ ingredients. **Dependencies (consumed, unmerged).** 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`, blob `f6df5a73`, head `782211f`): §0 cusp objects, +- Math- #207 (`frontiers/cusp_second_order_20261001/PROOF.md`, blob `f6df5a73`, head `b12ff46`): §0 cusp objects, (0.2)/(CU.2) (the coefficient `c₁`), §7 (through #218). - Math- #218 (`frontiers/candidate_third_order_20261001/PROOF.md`, blob `70ca57ef`, head `0cf048d`): Lemma D (1.1), (1.2), Lemma F (F.1)–(F.2), Lemma C and its proof (Steps C1–C3, (C.2)), Lemma O (O.1), (0.1) (`c₂`), and §4 (the decomposition `F + K + J₂ + … + J₅` and the bounds on `F`, `J₂`–`J₅`). -- Math- #220 (`frontiers/elder_third_order_20261001/PROOF.md`, blob `736a35de`, head `e481d23`): §0 (the near/far +- Math- #220 (`frontiers/elder_third_order_20261001/PROOF.md`, blob `c8767dde`, head `70dcf31`): §0 (the near/far identity, `𝒜^{eld}`, `c₁`), Lemma Q, §2 (notation, facts (F1)–(F7), (2.1)–(2.2), Lemma G, Lemma CE and its proof, Steps E1–E6), Lemma O′ (O′.1), Lemma H (through Lemma S′), Lemma S′ (S′.1), and §4 (the decomposition `F^{eld} + K^{eld} + I^{eld} − J₄` and the bound on `F^{eld}`). +*Rebound on 1 October 2026, 15:40 UTC.* #220's PROOF changed from blob `736a35de` (head `e481d23`) to `c8767dde` +(head `70dcf31`) by a status-only update with no mathematical change: #187 is listed as merged, Lemma S′ states its +range `r ≤ r_0^* ≤ 1` and sign `−H̃ > 0`, and X8 has a negative witness. Every part of #220 consumed here is +unchanged. #207's head moved to `b12ff46` by a guarded main-only merge; its blob is unchanged. + **Merged inputs.** [R] with (R2)–(R5); [P] with [E1], [E2] and [REC] (§2 finite-jet rank, §15 parity); [Z]; [C7-K] (K2); Math- #191 (`441152df`: Lemma E Steps 1–3, for (F1) at `k = 0`; §2, `r_0^*` and the `k = 0` identity); Math- #198 (`abfb98ae`: (3.1), the sign window and (3.2) of §3, Lemma W with its `k = 0` clause, (W.1), the `k = 0` identity in the proof of (W.4), Lemma F′); Math- #187 (`07260114`, merged on 1 October 2026 at `c2f1270`: Theorem F at the single -separation `ρ = r_0^*`). **Cited only:** Math- #216 and #223 (values of `c₂`), #211 (blob `ed0d3fa8`; the -equal-height mass and a heuristic quoted in Remark 3), #188. +separation `ρ = r_0^*`). **Cited only:** Math- #216 and #223 (values of `c₂`; #223 merged on 1 October at `f9ebba1`), +#211 (blob `ed0d3fa8`; the equal-height mass and a heuristic quoted in Remark 3), #188. ## 0. Statement @@ -421,10 +426,11 @@ The splits are optimal for these error terms (control R1): `ρ_f = ℓ^{2/7}` ba | #191 | `frontiers/remainder_vanishing_20260930/PROOF.md` (merged; blob `441152df`) | Lemma E Steps 1–3 (for (F1) at `k = 0`); §2: `r_0^*`, the `k = 0` identity — consumed | | #198 | `frontiers/remainder_rate_20260930/PROOF.md` (merged; blob `abfb98ae`) | §3 (3.1), the sign window, (3.2); Lemma W with its `k = 0` clause, (W.1); the proof of (W.4); Lemma F′ — consumed | | #187 | `frontiers/far_elder_rate_20260930/PROOF.md` (merged 1 Oct at `c2f1270`; blob `07260114`) | Theorem F at `ρ = r_0^*`, for (E3⁺.1) and (R⁺.1) only — consumed | -| #207 | `frontiers/cusp_second_order_20261001/PROOF.md` (unmerged; blob `f6df5a73`, head `782211f`) | §0, (CU.2), §7 — **consumed, unmerged** | +| #207 | `frontiers/cusp_second_order_20261001/PROOF.md` (unmerged; blob `f6df5a73`, head `b12ff46`) | §0, (CU.2), §7 — **consumed, unmerged** | | #218 | `frontiers/candidate_third_order_20261001/PROOF.md` (unmerged; blob `70ca57ef`, head `0cf048d`) | Lemmas D, F, C, O; (1.2); (0.1); §4 — **consumed, unmerged** | -| #220 | `frontiers/elder_third_order_20261001/PROOF.md` (unmerged; blob `736a35de`, head `e481d23`) | §0; Lemma Q; §2 facts, Lemmas G, CE; Lemmas O′, H, S′; §4 — **consumed, unmerged** | -| #216, #223 | `frontiers/third_order_coefficient_20261001/NOTE.md`, `frontiers/c2_exact_20261001/NOTE.md` (unmerged) | values of `c₂`, Remark 4 — cited only | +| #220 | `frontiers/elder_third_order_20261001/PROOF.md` (unmerged; blob `c8767dde`, head `70dcf31`) | §0; Lemma Q; §2 facts, Lemmas G, CE; Lemmas O′, H, S′; §4 — **consumed, unmerged** | +| #216 | `frontiers/third_order_coefficient_20261001/NOTE.md` (unmerged) | values of `c₂`, Remark 4 — cited only | +| #223 | `frontiers/c2_exact_20261001/NOTE.md` (merged 1 Oct at `f9ebba1`; blob `a2798b87`) | `c₂` in closed form, Remark 4 — cited only | | #211 | `frontiers/equal_height_mass_value_20261001/NOTE.md` (unmerged; blob `ed0d3fa8`, head `8e89fe8`) | the heuristic and Monte Carlo of Remark 3 — cited only | | #188 | `frontiers/far_elder_flat_ridge_20260930/PROOF.md` (unmerged) | an alternative far bound — cited only | diff --git a/frontiers/third_order_rate_20261001/README.md b/frontiers/third_order_rate_20261001/README.md index 484945db9..e13ae7a22 100644 --- a/frontiers/third_order_rate_20261001/README.md +++ b/frontiers/third_order_rate_20261001/README.md @@ -36,9 +36,9 @@ four error terms are exactly `ℓ^{3/7}` and all others are `O(ℓ^{4/9}log(1/ | | Sources | |---|---| -| Consumed, unmerged | #207 (`f6df5a73` at `782211f`), #218 (`70ca57ef` at `0cf048d`), #220 (`736a35de` at `e481d23`) | +| Consumed, unmerged | #207 (`f6df5a73` at `b12ff46`), #218 (`70ca57ef` at `0cf048d`), #220 (`c8767dde` at `70dcf31`, after its status-only update; rebound from `736a35de`) | | Consumed, merged | [R], [P] with [E1]/[E2]/[REC], [Z], [C7-K], #191, #198, and #187 (`07260114`, merged 1 Oct at `c2f1270`; used only for (E3⁺.1) and the second form of (R⁺.1)) | -| Cited | #216, #223 (`c₂`); #211 (Remark 3); #188 | +| Cited | #216 and #223 (`c₂`; #223 merged 1 Oct); #211 (Remark 3); #188 | The packet cannot be integrated before #207, #218 and #220, and must be rebound if any of them changes. The workflow checks every pin, including the current head (or the merge commit) of each consumed pull request. diff --git a/frontiers/third_order_rate_20261001/SOURCES.json b/frontiers/third_order_rate_20261001/SOURCES.json index e454caf62..1cccc27e4 100644 --- a/frontiers/third_order_rate_20261001/SOURCES.json +++ b/frontiers/third_order_rate_20261001/SOURCES.json @@ -2,11 +2,12 @@ "schema": 1, "scientific_effect": "NONE", "object": "CL-THIRD-ORDER-RATE-20261001-v1", + "rebind": "2026-10-01 15:40 UTC: #220 PROOF 736a35de (head e481d23) -> c8767dde (head 70dcf31), a status-only update with no mathematical change (#187 merged; Lemma S-prime range and sign stated; X8 witness); #207 head 782211f -> b12ff46 (guarded main-only merge, blob unchanged); #223 merged (cited_only)", "kind": "author-side proof candidate: the candidate and elder lifetime densities to third order with remainder O(l^(3/7)) in every d >= 2 (Theorems T+ and E3+), improving the O(l^(4/11)) of Math- #218 and #220: nu_cand = c l^(-1/3) + B_{d,L} + I^cand l^(1/4) + c2 l^(1/3) + O(l^(3/7)); nu_eld = c l^(-1/3) + c1 l^(1/4) + c2 l^(1/3) + nu_eld^{far,r_0^*} + O(l^(3/7)), and with merged #187 + O(l^(3/7)); rejected density B_{d,L} + (I^cand - c1) l^(1/4) + O(l^(3/7)); new: Lemma L (a kappa-free local Lipschitz bound for (c^2 - y^2)_+), Lemma C+ (candidate cusp kernel, error r(1 + kappa)), Lemma CE+ (elder cusp kernel, error r(1 + kappa) + kappa^2 r^(3/2) + kappa^3 r^2, through a refined bound on the edge window B_4), Proposition W+ (typed-window bound E_Q[W_r/r^2] <= C r^2 (kappa + r)^2 (kappa + r log(2/r)) P^N for k <= r; at k = 0 the equal-height kernel is O(r^3 log(2/r)) near the diagonal); intermediate elder mass O(l^(4/9) log(1/l))", "author": "Anthropic Claude", "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", "read_at": { - "branch_base": "77b854cac6017ecdc0ea7abf6f978f9c6c9cb787" + "branch_base": "f9ebba17f5cc590232b2fb2cd37b04b996abc143" }, "consumed": [ { @@ -98,7 +99,7 @@ "git_blob": "f6df5a7356a54771b0052e42a864a140709903ad", "tag": "207", "use": "section 0 cusp objects; (0.2)/(CU.2), the coefficient c1; section 7 (through #218)", - "head": "782211f494aeef1a24b70fe76423c66afe2ea9dc", + "head": "b12ff464b3534b6899a90cc250c585b1caf5dfec", "pr": "Math- #207" }, { @@ -113,16 +114,25 @@ }, { "path": "frontiers/elder_third_order_20261001/PROOF.md", - "bytes": 68890, - "sha256": "f3a64ad9551e02441eb3e3776aa72441c3c5a3b939a385e3031169a1608756a7", - "git_blob": "736a35de9d96e26372349f2a093feb40e47816ce", + "bytes": 70544, + "sha256": "74b5f031ba5be6f50b5e543636136df1d9b5fad0fcd2c8210320cfef02f80e37", + "git_blob": "c8767ddecf1041d234f685e95af582073a7be393", "tag": "220", "use": "section 0 (near/far identity, A^eld, c1); Lemma Q; section 2 (notation, facts (F1)-(F7), (2.1)-(2.2), Lemma G, Lemma CE and its proof, Steps E1-E6); Lemma O-prime; Lemma H (through Lemma S-prime); Lemma S-prime (S-prime.1); section 4: the decomposition F^eld + K^eld + I^eld - J4 and the bound on F^eld", - "head": "e481d230cba1f6f29d89c76c8086ee512a61c22e", + "head": "70dcf310fc68f7d2b6949f035a09acf54f0cff7d", "pr": "Math- #220" } ], - "cited_only": [], + "cited_only": [ + { + "path": "frontiers/c2_exact_20261001/NOTE.md", + "bytes": 14480, + "sha256": "598fc86a7c6b21bad438ef087e5aa7521f0fae08e25fa4f40f9b2ba635846dbb", + "git_blob": "a2798b87674ed5fc0d2144697e77ccb9b185b4ab", + "tag": "223", + "use": "Math- #223 (merged 2026-10-01 at f9ebba1): c2 in closed form for the Gaussian kernel (Remark 4)" + } + ], "cited_unmerged": [ { "path": "frontiers/third_order_coefficient_20261001/NOTE.md", @@ -134,16 +144,6 @@ "head": "04c08e1534122f210be888742fcd7a568e45b097", "pr": "Math- #216" }, - { - "path": "frontiers/c2_exact_20261001/NOTE.md", - "bytes": 14480, - "sha256": "598fc86a7c6b21bad438ef087e5aa7521f0fae08e25fa4f40f9b2ba635846dbb", - "git_blob": "a2798b87674ed5fc0d2144697e77ccb9b185b4ab", - "tag": "223", - "use": "c2 in closed form for the Gaussian kernel (Remark 4)", - "head": "b2247fd81712f131ad604d13125580bf1afe2f94", - "pr": "Math- #223" - }, { "path": "frontiers/equal_height_mass_value_20261001/NOTE.md", "bytes": 16177, @@ -211,13 +211,13 @@ "files": [ { "path": "PROOF.md", - "bytes": 37046, - "sha256": "2fd71925c3e501b94acec8e2df3ee02300f91388280886a91cd730ee62341eed" + "bytes": 37626, + "sha256": "5de5a6c7b942a71675c812000ade30c16766f02ee388e8dc3e1c51dde5297f7d" }, { "path": "README.md", - "bytes": 4991, - "sha256": "f45e9c9dc5bf24b1a54c8411a927d5abeb5261845a7745e8d8c6b87b847b3556" + "bytes": 5068, + "sha256": "99ee83fd8fe442554db32d43c912b40fd41edf3a684827a9f5a94c73873b6a13" }, { "path": "r37_check.py",