From 7262001f55c69a43ae752da829fead41a2b79926 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 1 Oct 2026 09:28:30 +0000 Subject: [PATCH 1/2] Theorem T: the candidate density to third order in every d >= 2 nu_cand(l) = c l^{-1/3} + B_{d,L} + I_cand l^{1/4} + c2 l^{1/3} + O(l^{4/11}), with c2 the fold-scale Hadamard finite part of the r^2 coefficient of [R]'s two-point kernel (the coefficient Math- #216 computes: 0.16123405 for SIDE24). Corollary: a rate O(l^{1/3}) for #207's (CU'.1). New lemmas: F (fold expansion A_r = A_0 + r^2 A_2 + O(r^3(1 + 1/k)), the r^3/k term being the boundary layer of the typed region near det A = 0), C (the candidate cusp kernel with rate O(r(1 + kappa)^2)), O (overlap: the cusp loss tends to A_2(b, 0) at rate 1/kappa), D (eigenvalue/determinant layers). Consumes unmerged #191, #198, #207. Stdlib exact controls T1-T5 (T5 checks the product structure on exactly pinned polynomial fields in d = 2, 3), mutants M1-M4. Clean-context referee pass applied (no major finding). Scientific effect NONE. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .github/workflows/candidate-third-order.yml | 110 ++++ .../candidate_third_order_20261001/PROOF.md | 504 ++++++++++++++++++ .../candidate_third_order_20261001/README.md | 68 +++ .../RESULTS.json | 123 +++++ .../SOURCES.json | 212 ++++++++ .../thmT_check.py | 329 ++++++++++++ 6 files changed, 1346 insertions(+) create mode 100644 .github/workflows/candidate-third-order.yml create mode 100644 frontiers/candidate_third_order_20261001/PROOF.md create mode 100644 frontiers/candidate_third_order_20261001/README.md create mode 100644 frontiers/candidate_third_order_20261001/RESULTS.json create mode 100644 frontiers/candidate_third_order_20261001/SOURCES.json create mode 100644 frontiers/candidate_third_order_20261001/thmT_check.py diff --git a/.github/workflows/candidate-third-order.yml b/.github/workflows/candidate-third-order.yml new file mode 100644 index 000000000..74fc228d2 --- /dev/null +++ b/.github/workflows/candidate-third-order.yml @@ -0,0 +1,110 @@ +name: Candidate third-order exact controls + +'on': + pull_request: + paths: + - 'frontiers/candidate_third_order_20261001/**' + - '.github/workflows/candidate-third-order.yml' + # bound merged sources (consumed and cited_only in SOURCES.json) and the pinned unmerged dependencies + - 'frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md' + - 'imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md' + - 'imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md' + - 'reviews/d1_section9_borel_repair_20260925/REPAIR.md' + - 'reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md' + - 'frontiers/c7_zero_gap_limit_20260929/PROOF.md' + - 'frontiers/c7_total_bounded_20260929/PROOF.md' + - 'frontiers/remainder_vanishing_20260930/PROOF.md' + - 'frontiers/remainder_rate_20260930/PROOF.md' + - 'frontiers/cusp_second_order_20261001/PROOF.md' + workflow_dispatch: + +permissions: + contents: 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/candidate_third_order_20261001').resolve() + manifest = json.loads((root / 'SOURCES.json').read_text()) + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest['files']] + ['SOURCES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest['files']: + path = root / entry['path'] + if path.is_symlink(): + raise ValueError('symlink: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('packet file identity mismatch: ' + entry['path']) + def same(data, entry): + framed = b'blob ' + str(len(data)).encode() + b'\0' + data + return len(data) == entry['bytes'] and hashlib.sha256(data).hexdigest() == entry['sha256'] and hashlib.sha1(framed).hexdigest() == entry['git_blob'] + for entry in manifest['consumed'] + manifest['cited_only']: + if not same(pathlib.Path(entry['path']).read_bytes(), entry): + raise ValueError('merged source drifted: ' + 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']) + for kind in ('consumed_unmerged', 'cited_unmerged'): + for entry in manifest.get(kind, []): + tree_path = pathlib.Path(entry['path']) + if kind == 'consumed_unmerged' and tree_path.exists(): + data, where = tree_path.read_bytes(), 'tree' + else: + 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) + print(json.dumps({kind + '_bound': entry['path'], 'git_blob': entry['git_blob'], 'head': entry['head'], 'via': where})) + script = str(root / 'thmT_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/candidate_third_order_20261001/PROOF.md b/frontiers/candidate_third_order_20261001/PROOF.md new file mode 100644 index 000000000..70ca57ef0 --- /dev/null +++ b/frontiers/candidate_third_order_20261001/PROOF.md @@ -0,0 +1,504 @@ +# The candidate density to third order: `ν_cand(ℓ) = cℓ^{−1/3} + B_{d,L} + I^{cand}ℓ^{1/4} + c₂ℓ^{1/3} + O(ℓ^{4/11})` + +Object: CL-CANDIDATE-THIRD-ORDER-20261001-v1. +Author: Anthropic Claude (claude.ai session `session_01NMeKEismAyeqgdB4sy2NJU`), 1 October 2026. +Before submission, a clean-context same-family referee read the whole note (`REFEREE_1.md` in the project archive). It +found no major issue, and its five minor findings and eight nits are applied: +- (1.2) is restricted to jets with uniformly invertible covariance; +- the uniform nondegeneracy of the free jets is proved on all of `(0, r_0^*]`; +- the elder requirements of Remark 1 are corrected; +- the relation to Math- #216's computation is stated exactly; +- control T5 is described as implemented, and a `d = 3` case is added. +Disposition: AUTHOR-SIDE PROOF CANDIDATE; NONAUTHOR REVIEW REQUIRED. Scientific effect: NONE — no register, graph, +STATUS, PROOF_INDEX, prize or Boolean change; no numerical constant is certified. Same GitHub account as every lane; +zero organizational independence. +**Dependencies (unmerged, consumed):** +- Math- #191 (`frontiers/remainder_vanishing_20260930/PROOF.md`, v1.1 blob `441152df`): Lemma E, Steps 1–4, its + dominating variable `T` and the good event; §2 (2.1)–(2.2); the admissible radius `r_0^*`. +- Math- #198 (`frontiers/remainder_rate_20260930/PROOF.md`, v1.1 blob `abfb98ae`): (3.1), the sign window, (W.4); (W.1) + only through #207 Lemma L. +- Math- #207 (`frontiers/cusp_second_order_20261001/PROOF.md`, v1.1 blob `f6df5a73`): §0 (the cusp objects), the + candidate part of Theorem CU.4's definitions, Lemma CU.5's nondegeneracy of the free jets, §7 (Lemma L (7.1)–(7.2), + the far identity, the decomposition of `B_{d,L}`, the integral (7.3)). + +This note cannot be integrated before those three and must be rebound if any of them changes. +**Merged inputs:** [R], [P] with [E1]/[E2]/[REC], and [Z] (Z2)–(Z3). The numerical value of `c₂` is Math- #216's +(cited, not consumed; §5). + +## 0. Statement + +Setting and notation are those of [R] (`frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md`, blob `247b3ecf`), +#191 §0, #198 §0 and #207 §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` with heights `b`, `b − kr³` and zero gradients; +- the pin vector `U_r` and target `v_r = (b − kr³/2, −kr², 0, 12k, 0, …, 0)` with density `π_r`, the pinned law + `Q = Q_{r,b,k}`, the coupling `(F_r, F_0)` of [R] (R3)–(R4), and `P = 1 + |b| + k`; +- the scaled endpoint Hessians `K_M`, `K_S` of [R] §4, the filtered determinants `F_j`, + `Z_r/r² = E_Q[F_d(K_M)F_{d−1}(K_S)]`, `A_r = 12π_r(v_r)Z_r/r²`, and the contact kernel + `A_0 = 12π_0(v_0)z_0`, `z_0 = 36k²E[(det A_0)²1{A_0 < 0}]`, `A_0 = D_y²F_0(0)`; +- the candidate density `ν_cand(ℓ) = ∫_0^{r_0}∫_R∫_{S^{d−1}} r^{−2}A_r(b, ℓ/r³, u) dσ db dr + ν_cand^{far,r_0}(ℓ)` (#191 + (2.1); the far part as in #207 §7), `c = c_{d,L}` of [P] (15.2), and `B_{d,L}` of [Z] (Z3). + +**Cusp objects (#207 §0).** +- The jets at `0` under the contact law at the zero-gap target `v_0(b, 0)`: `f₄ = ∂_u⁴f(0)`, `γ = ∇_Θ∂_u²f(0)`, + `A = D_Θ²f(0)`, `Δ = det A` and `Y = (f₄/12)Δ − γᵀadj(A)γ/4`. `E_0[· | b]` is the expectation under that law. +- With `κ > 0`, the candidate and contact cusp kernels are + `𝒜^{cand}(b, κ, u) = 12π_0(u; v_0(b, 0))E_0[(36κ²Δ² − Y²)1{A < 0, |Y| < 6κ|Δ|} | b]` and + `𝒜^{con}(b, κ, u) = 12π_0(u; v_0(b, 0))E_0[36κ²Δ²1{A < 0} | b]`. So + `𝒜^{cand} − 𝒜^{con} = −12π_0E_0[min(Y², 36κ²Δ²)1{A < 0} | b]`. +- `I^{cand} := ∫_{S^{d−1}}∫_R∫_0^∞(𝒜^{cand} − 𝒜^{con})(b, s^{−4}, u) ds db dσ(u)`, which equals + `−12·(8/7)6^{1/4}∫∫π_0E_0[|Y|^{7/4}|Δ|^{1/4}1{A<0} | b] db dσ` (#207 (7.3)). + +**The fold coefficient.** Lemma F below shows that at fixed `(b, k, u)`, `A_r = A_0 + r²A₂ + O(r³(1 + k^{−1}))`. The +coefficient `A₂(b, k, u)` is `C¹` in `k ∈ [0, ∞)`, and its value at `k = 0` is +`A₂(b, 0, u) = −12π_0(u; v_0(b, 0))E_0[Y²1{A < 0} | b]`. Define + + c₂ := (1/3) ∫_{S^{d−1}} ∫_R ∫_0^∞ [A₂(b, k, u) − A₂(b, 0, u)] k^{−4/3} dk db dσ(u). (0.1) + +This is the Hadamard finite part at `k = 0` of `(1/3)∫∫∫A₂k^{−4/3}`. It is the coefficient that Math- #216 defines. Its +numerical values there, for the Gaussian kernel, are `0.22152441` in `d = 2` and `0.16123405` in `d = 3` (§5). + +**Theorem T (the candidate density to third order).** For every `d ≥ 2` and `L > 0`, as `ℓ ↓ 0`, + + ν_cand(ℓ) = c ℓ^{−1/3} + B_{d,L} + I^{cand} ℓ^{1/4} + c₂ ℓ^{1/3} + O(ℓ^{4/11}). (T.1) + +The integral (0.1) converges absolutely. + +**Corollary T′ (a rate for #207's (CU′.1)).** +`ν_cand(ℓ) − cℓ^{−1/3} − B_{d,L} − I^{cand}ℓ^{1/4} = O(ℓ^{1/3})`. This settles, for the candidate density, the open item +"a rate for the `o(ℓ^{1/4})`" of #207 §0 and of the concordance (§9 item 6). + +**How it works.** Three scales meet. +- *Fold scale `r ≍ ℓ^{1/3}`.* Here `k ≍ 1`, and the kernel has the even expansion `A_r = A₀ + r²A₂ + …`. Integrating + `A₂` in `r` produces `c₂ℓ^{1/3}`, but `∫A₂k^{−4/3}dk` diverges at `k = 0`, because `A₂(b, 0) ≠ 0`. +- *Cusp scale `r ≍ ℓ^{1/4}`.* Here `κ = k/r ≍ 1`, and #207's cusp kernels apply, with an explicit rate `O(r(1 + κ)²)` + (Lemma C). They produce `I^{cand}ℓ^{1/4}`. +- *Overlap.* As `κ → ∞` the cusp loss `𝒜^{cand} − 𝒜^{con}` tends to `A₂(b, 0)` at rate `κ^{−1}` (Lemma O). The two + scales therefore match: the divergent part of the fold integral is exactly the part of the cusp integral that the + finite part removes. +- *Larger separations.* They need no elder decision: Lemma L of #207 bounds the gap dependence. + +**What is not claimed.** +- No statement about the elder density `ν_eld` or the rejected density beyond #207. The `ℓ^{1/3}` term of `ν_eld` needs + three things not supplied here (§5, Remark 1): + - an elder version of Lemma C (a quantitative Proposition CU.3); + - a bound `o(ℓ^{1/3})` for elder pairs at intermediate separations `ℓ^{1/4} ≪ r ≤ r₁`; + - a far elder bound `o(ℓ^{1/3})`, which exists only in the unmerged candidates #187 and #188. +- No certified numerical value of `c₂`, `I^{cand}` or `B_{d,L}`. +- No sharpness of the exponent `4/11`. Formally the next term is of order `ℓ^{1/2}`. +- No uniformity in `d` or `L`; no finite-radius band. +- Nothing beyond the existential scope of [R], [Z], #191, #198 and #207. + +## 1. Two Gaussian facts + +**Lemma D (eigenvalue and determinant layers).** Let `G` be a random symmetric `m × m` matrix whose law has a density +bounded by `C_φ exp(−c_φ|G − μ|²)` on `Sym(m) ≅ R^{m(m+1)/2}`. For every `n ≥ 0` there is +`C = C(m, n, C_φ, c_φ)`, independent of `μ`, such that for `ε > 0` + + E[(1 + ‖G‖)^n 1{|λ_max(G)| < ε}] ≤ C(1 + |μ|)^{n′} ε, E[(1 + ‖G‖)^n 1{|det G| < ε}] ≤ C(1 + |μ|)^{n′} ε, n′ := n + m(m−1)/2. (1.1) + +*Proof.* Use eigenvalue coordinates `G = OΛOᵀ`, under which Lebesgue measure on `Sym(m)` is +`c_m|V(λ)| dλ dO`, with `V(λ) = ∏_{i 0`. Then `|λ_{i*}| < ε/D`. Since `|λ_{i*}| ≤ |λ_j|`, each factor `|λ_{i*} − λ_j| ≤ 2|λ_j|`, so + `|V(λ)| ≤ 2^{m−1}D|V′|`, where `V′` is the Vandermonde product of the other `m − 1` eigenvalues. +- Integrating `λ_{i*}` over an interval of length `2ε/D` against a density at most `C_φ` gives at most + `2^m C_φ ε|V′|`. The factor `D` cancels. +- The remaining integral of `(1 + max|λ_j|)^n|V′|` against the Gaussian bound in the other eigenvalues is + `≤ C(1 + |μ|)^{n′}`. Summing over the `m` choices of `i*` gives (1.1). ∎ + +(For `m = 1` both statements are the bounded density of a Gaussian variable.) + +**Conditional moments of `T`.** Let `T := 1 + k + ‖F_r‖_{C⁹} + ‖F_0‖_{C⁹} + r^{−2}‖F_r − F_0‖_{C⁴}`. This is #191's +dominating variable with larger norm indices; [R] (R4) holds for every finite derivative order, so `‖T‖_p ≤ C_pP`. +Let `J₀` be a finite vector of derivatives of `F_r` at `0` whose covariance under `Q` is uniformly invertible for +`r ≤ r_0^*`. Any vector of free jets qualifies (§2, Step F1). +- Under the coupling (R3), `F_r`, `F_0` and `(F_r − F_0)/r²` are affine images of one Gaussian field `F`. Their + coefficients are bounded uniformly in `r ≤ r_0^{[R]}` by (R2). +- Conditionally on `J₀`, `F` is Gaussian. Because `Cov_Q(J₀)` is uniformly invertible, the regression coefficients + are bounded uniformly in `r`, so the conditional mean has `C^q` norms `≤ C(P + |J₀|)`. The conditional covariance is at + most `Cov F`, so the conditional `C^q`-norm moments of the centred part are dominated by those of `F` (Anderson's + inequality). +- Hence + + E[T^p | J₀] ≤ C_p (P + |J₀|)^p. (1.2) + + The hypothesis is needed. For a pinned jet such as `∂_u²F_r(0)`, whose `Q`-variance is `O(r⁴)`, conditioning on an + `O(1)` value forces `f₄ ≍ r^{−2}`. + +## 2. The fold expansion + +**Lemma F.** There are `C, c, N` and a function `A₂(b, k, u)` such that for `0 < r ≤ min(r_0^*, 1/2)`, `k > 0`, +`b ∈ R` and `u ∈ S^{d−1}` + + |A_r(b, k, u) − A_0(b, k, u) − r² A₂(b, k, u)| ≤ C r³ (1 + k^{−1}) P^N e^{−c(b² + k²)}. (F.1) + +Moreover, `A₂(b, ·, u)` extends to a `C¹` function on `[0, ∞)` with + + |A₂(b, k, u)| + |∂_kA₂(b, k, u)| ≤ C P^N e^{−c(b² + k²)}, A₂(b, 0, u) = −12π_0(u; v_0(b, 0)) E_0[Y² 1{A < 0} | b]. (F.2) + +*Proof.* Fix `N₀ = 9`. Write `f = F_r` and `A := D_y²f(0)`. + +*Step F1 (free jets and the product polynomial).* Let `J` be the vector of all partial derivatives of `f` at `0` of +order `≤ N₀`, in the frame `(u, Θ)`. +- The *pinned* jets are `f(0)`, `∂_uf(0)`, `∂_u²f(0)`, `∂_u³f(0)`, `∇_Θf(0)` and `∇_Θ∂_uf(0)`. The others are *free*; + write `J′` for them. `A` and `f₄` are free. +- *The free jets are uniformly nondegenerate under `Q`.* For each `r ∈ (0, r_0^*]`, `(J′, U_r)` is an invertible linear + image of distinct derivative functionals at the three distinct sites `0` and `±ru/2`. These are linearly independent, + by [P] §2: "Any finite list of distinct derivative evaluation functionals at distinct sites is linearly independent." + At `r = 0`, `(J′, U_0)` is a list of distinct jets at one point, again independent. The Gram matrix of `(J′, U_r)` is + continuous on the compact set `[0, r_0^*] × {frames}`, so it is uniformly invertible there. Hence `Cov_Q(J′)`, the + Schur complement, is uniformly invertible. #207 Lemma CU.5 makes the same argument for `r ≤ r₁`. +- Each pin row is a centred difference rule. Taylor's formula with integral remainder writes it as the corresponding + pinned jet plus a polynomial in `r` and the higher jets, plus an error `≤ Cr^{N₀−3}T`. Here `T` (§1) controls the + `C⁹` norms. For example + `(f_x(S) − f_x(M))/r = ∂_u²f(0) + (r²/24)∂_u⁴f(0) + … `, the series that #191 Step 1 truncates at second order. +- Under `Q` the rows equal their targets. Hence each pinned jet equals a polynomial in `(J′, r, b, k)` up to + `O(r^{N₀−3}T)`. The `1/r` and `1/r²` of the rows are absorbed because the rules are centred. +- Expanding the entries of `K_M`, `K_S` at `x = ∓r/2` by Taylor's formula to the same order and substituting gives, for + `r ≤ 1`, a polynomial `Φ(J′; r, k)` with + + −det K_M det K_S = Φ(J′; r, k) + ϱ, |ϱ| ≤ C r⁴ T^{n₀}. (2.1) + + The entry `α_i = f_xx(x_i)/r` has an explicit `1/r`. It is a polynomial once `∂_u²f(0)` is replaced by its pin + expansion `−(r²/24)f₄ − …`. This is the mechanism of #191 (1.1). +- Write `Φ = Φ₀ + rΦ₁ + r²Φ₂ + r³Φ₃(J′; r, k)`, with `|Φ₃| ≤ C(1 + k)²(1 + |J′|)^{n₀}` for `r ≤ 1`. +- By #191 Lemma E, Steps 1–3, and #198 (3.1), + `det K_M = −6kΔ_r + rY + O(r²)` and `det K_S = +6kΔ_r + rY + O(r²)`, with the *same* `Y`. Here + `Δ_r = det A` and `Y = (f₄/12)Δ_r + 3k tr(adj(A)B) − γᵀadj(A)γ/4`. #191 states this with its coupled `A_0`; with + `A = D_y²F_r(0)` the same expansions hold, since #191 replaced `A` by `A_0` only through `‖A − A_0‖ ≤ r²T`. Hence + + Φ₀ = 36k²Δ_r², Φ₁ = −[(−6kΔ_r)Y + Y(6kΔ_r)] = 0, Φ₂|_{k=0} = −Y²|_{k=0}. (2.2) + + The last identity holds because at `k = 0` both determinants are `rY + O(r²)`. +- (2.2) is an identity of polynomials in `J′`, not only pathwise. Apply (2.1) and the expansions above to the pinned + polynomial fields of degree `≤ N₀ − 1` with arbitrary free jets: for these `ϱ = 0` and `T < ∞`, so the coefficients of + `r⁰`, `r¹` and (at `k = 0`) `r²` in `Φ − 36k²Δ_r²` and `Φ + r²Y²` must vanish identically. Control T5 checks (2.2) + exactly on such fields in `d = 2` and `d = 3`. + +*Step F2 (the typed indicator and its layers).* Let `υ := C₁rT(1 + T/k)` and +`G := {λ_max(A) ≤ −υ} ∩ {k ≥ C₁rT}`. This is #191 Step 4's good event (#191's `u`) with `A` in place of `A_0`. Its +proof uses only `‖A_i − A‖ ≤ (r/2)‖F_r‖_{C³} ≤ rT` and `‖β_i‖ ≤ CT`, which hold for `A`. +- *On `G`.* `K_M`, `K_S` have indices `d`, `d − 1` and `A < 0`. So `F_d(K_M)F_{d−1}(K_S) = −det K_M det K_S`, and by + (2.1) this equals `Φ1{A<0} + ϱ`. +- *On `{λ_max(A) ≥ rT}`.* `λ_max(A_M) ≥ rT − (r/2)T > 0`, so `F_d(K_M) = 0`. Also `1{A<0} = 0`. +- *On the rest of `G^c`.* This set lies in `{|λ_max(A)| < υ} ∪ {k < C₁rT}`. There, #191 Step 4's three cases bound + both `F_d(K_M)F_{d−1}(K_S)` and `|Φ|1{A<0}` (the latter through (2.1)) by `C r²(k + T)²T^{N₂}`. + +Hence + + |E_Q[F_d(K_M)F_{d−1}(K_S)] − E_Q[Φ 1{A<0}]| ≤ C r⁴P^N + E[g(T)(1{k < C₁rT} + 1{|λ_max(A)| < υ})], g(t) := Cr²(k + t)²t^{N₂}. + +Bound the two layer terms separately. +- *First term.* `E[g(T)1{T > k/(C₁r)}] ≤ (C₁r/k)E[g(T)T] ≤ Cr³k^{−1}P^N`. +- *Second term: dyadic split.* Since `T ≥ 1` and `υ` increases with `T`, split by `T ∈ [2^j, 2^{j+1})`, with + `υ_j := C₁r2^{j+1}(1 + 2^{j+1}/k)`: + + E[g(T)1{|λ_max(A)| < υ}] ≤ Σ_{j≥0} g(2^{j+1}) E[1{|λ_max(A)| < υ_j} P(T ≥ 2^j | A)] + ≤ Σ_{j≥0} g(2^{j+1}) C_p 2^{−jp} E[(P + ‖A‖)^p 1{|λ_max(A)| < υ_j}]. + + The second line uses (1.2) with `J₀ = A`. +- *The law of `A`.* Under `Q`, `A` is a Gaussian vector with mean `O(P)` and uniformly nondegenerate covariance + (Step F1). This also makes (1.2) applicable with `J₀ = A`. +- So Lemma D gives `E[(P + ‖A‖)^p1{|λ_max(A)| < υ_j}] ≤ CP^{2p+m(m−1)/2}υ_j`. Taking `p > N₂ + 4`, the sum is + `≤ Cr³(1 + k^{−1})P^N`. + +Hence + + E_Q[F_d(K_M)F_{d−1}(K_S)] = E_Q[Φ(J′; r, k)1{A<0}] + O(r³(1 + k^{−1})P^N). (2.3) + +*Step F3 (smoothness of the pinned law in `r`).* Under `Q`, `J′` is Gaussian with mean `μ_r` and covariance `Γ_r`, both +built from `Cov(J′, U_r)`, `Cov(U_r)` and `v_r`. +- The rows of `U_r` are centred, so they are even functionals of `r`. The covariances are therefore smooth even + functions of `r`, and `Γ_r` is uniformly nondegenerate (Step F1). +- The target is `v_r = v_0 + r²(0, −k, 0, …) + r³(−k/2, 0, …)`. Hence + `μ_r = μ_0 + r²μ_2 + r³μ_3 + O(r⁴P)` with `|μ_3| ≤ Ck`, and `Γ_r = Γ_0 + r²Γ_2 + O(r⁴)`. +- For `g = Ψ(J′)1{A<0}` with `Ψ` a polynomial, `E_{N(μ,Γ)}[g]` is a smooth function of `(μ, Γ)`: differentiate the + Gaussian density under the integral. Its derivatives are bounded by `E[|g|(1 + |J′|)^n]`-type moments. +- So `E_Q[Φ₀1{A<0}] = 36k²(e_0 + r²e_2 + O(r³(1 + k)P^N))` and `E_Q[Φ₂1{A<0}] = E_0[Φ₂1{A<0}] + O(r²P^N)`. The + `r³`-term contributes `O(r³(1 + k)²P^N)`. Here `e_0 = E_0[Δ²1{A<0} | v_0(b, k)]` and `E_0` is the law at `r = 0`, which + is the contact law at `v_0(b, k)`, the law of the jets of `F_0`. +- Likewise `π_r(v_r) = π_0(v_0) + r²π_2 + O(r³(1 + k)P^Ne^{−c(b²+k²)})`. The density of `U_r` is smooth in `(r², v)` + with uniformly nondegenerate covariance, as in the proof of [R] (R5). +- Multiplying, with (2.3) and `A_0 = 12π_0(v_0)·36k²e_0`, gives (F.1) with + + A₂ := 12[π_2·36k²e_0 + π_0(v_0)(36k²e_2 + E_0[Φ₂1{A<0} | v_0(b, k)])]. (2.4) + +*Properties (F.2).* +- Every ingredient of (2.4) is a polynomial in `k`, or a Gaussian expectation whose target is affine in `k`, times + `π_0(v_0(b, k)) ≤ Ce^{−c(b²+k²)}`. This gives the bounds and the `C¹` extension to `k = 0`. +- At `k = 0` the first two terms vanish, because of the factor `k²`. By (2.2), the third is + `−12π_0(v_0(b, 0))E_0[Y²1{A<0} | v_0(b, 0)]`. +- At `r = 0` the free jets have the contact law. So `Y` is #207's `Y` and `E_0[· | v_0(b, 0)]` is #207's `E_0[· | b]`. ∎ + +(*The surrogate.* Replace the true typed indicator by `1{A < 0}`. The surrogate kernel `12π_r(v_r)E_Q[Φ1{A<0}]` is +smooth in `r` at every `k ≥ 0`, with no boundary layer, and by Step F3 its `r²`-coefficient is `A₂`. Step F2 shows that +the replacement changes `A_r` by `O(r³(1 + k^{−1}))`; this is the boundary layer of the typed region near `det A = 0`. + +Math- #216 computes a numerical approximation of this surrogate in three steps: +- it truncates the jets at order `N = 12, 10, 8` (`d = 1, 2, 3`); +- it conditions them on the correspondingly truncated pin rows, which differ from `Q` by `O(r^{N−3})`-type terms; +- it extracts the `r²`-coefficient by least squares on `(1, r², r³, r⁴)` over five separations, then integrates by + Gauss–Legendre quadrature. + +For `N ≥ 6` the exact `r²`-coefficient of the truncated surrogate equals `A₂`, so #216's values are numerical +approximations of (0.1), not exact evaluations.) + +## 3. The cusp kernel with a rate + +**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.* Work on the coupling space with `T` as in §1 and `Δ := det A_0`, where `A_0 = D_y²F_0(0)`. As in [R] and +#191, `A_0` denotes both this matrix and the contact kernel; the meaning is clear from context. With this `T`, +`‖A_i − A_0‖ ≤ (r/2)‖F_r‖_{C³} + ‖F_r − F_0‖_{C²} ≤ (r/2 + r²)T ≤ rT` for `r ≤ 1/2`, which is [R] (R9). + +*Step C1 (pathwise comparison).* By #198 (3.1), +`det K_M = r(Y − 6κΔ) + R_M` and `det K_S = r(Y + 6κΔ) + R_S`, with `|R_i| ≤ Cr²(1 + k)T^{N₁}` and +`Y = (f₄/12)Δ + 3k tr(adj(A_0)B) − q`. Here `B = ∂_xD_y²F_r(0)`, `q = γᵀadj(A_0)γ/4`, and `f₄`, `γ = ∇_y∂_x²F_r(0)` are +jets of `F_r` (#191 (1.5)). Put `m_i := det K_i/r`, `η := Cr(1 + k)T^{N₁} ≥ |R_i|/r`, and + + w_κ(A, Y) := (36κ²(det A)² − Y²) 1{A < 0, |Y| < 6κ|det A|} = (36κ²(det A)² − Y²)_+ 1{A < 0}. + +Then `r^{−2}F_d(K_M)F_{d−1}(K_S) = |m_Mm_S|1{typed}`. There are three cases. +- *Case 1: `λ_max(A_0) < −rT`.* Since `‖A_i − A_0‖ ≤ rT`, `A_M, A_S < 0`. By Haynsworth's inertia additivity + (#191 Step 4), `index K_i = m + 1{s·det K_i < 0}`, where `s := (−1)^m = sign Δ`. + - So `typed ⟺ s m_M < 0 < s m_S`. Because `sΔ = |Δ|`, the limit indicator is + `1{|Y| < 6κ|Δ|} ⟺ s(Y − 6κΔ) < 0 < s(Y + 6κΔ)`. + - *If both hold:* `|m_Mm_S − (Y − 6κΔ)(Y + 6κΔ)| ≤ 2η(|Y| + 6κ|Δ|) + η² ≤ 24ηκ|Δ| + η²`. + - *If exactly one holds:* for some `i`, the factor `Y ∓ 6κΔ` and `m_i` differ in sign or one of them vanishes. Hence + `|Y ∓ 6κΔ| ≤ |R_i|/r ≤ η`, and the other factor is `≤ 12κ|Δ| + η` in modulus. Both weights are then + `≤ 2η(12κ|Δ| + 3η)`. +- *Case 2: `λ_max(A_0) > rT`.* Then `λ_max(A_M) > 0`, so `F_d(K_M) = 0`. Also `1{A_0 < 0} = 0`, so both weights vanish. +- *Case 3: `|λ_max(A_0)| ≤ rT`.* Then `|Δ| ≤ rT·T^{m−1}`, so `w_κ ≤ 36κ²r²T^{2m}`. If the pair is typed, the sign + window of #198 §3 gives `|m_i| ≤ 12κ|Δ| + 2η`, so `|m_Mm_S| ≤ C(κr + η)²T^{2m}`. + +In all cases, since `|Δ| ≤ T^m` and `κr = k ≤ 1`, + + |r^{−2}F_d(K_M)F_{d−1}(K_S) − w_κ(A_0, Y)| ≤ C r (1 + κ) T^{N}. (C.2) + +*Step C2 (to the contact jets).* Let `Y_0 := (f₄^{(0)}/12)Δ − (γ^{(0)})ᵀadj(A_0)γ^{(0)}/4`, built from the jets of +`F_0`. Then `|Y − Y_0| ≤ 3κr|tr(adj(A_0)B)| + Cr²T^N`: the `C⁴`-jets of `F_r` and `F_0` differ by `≤ r²T`. +- `w_κ(A, ·)` is Lipschitz with constant `12κ|det A|`. If both values are positive, + `|Y² − Y′²| ≤ (|Y| + |Y′|)|Y − Y′| ≤ 12κ|Δ||Y − Y′|`. If only `w(A, Y) > 0`, then + `w(A, Y) ≤ (6κ|Δ| − |Y|)·12κ|Δ| ≤ 12κ|Δ||Y − Y′|`. +- Hence `|w_κ(A_0, Y) − w_κ(A_0, Y_0)| ≤ Cκ(κr + r²)T^N`. +- `(A_0, Y_0)` are jets of `F_0`, whose law is the contact law at `v_0(b, k)`. With (C.2) and `E[T^N] ≤ CP^N`, + + |r^{−2}Z_r/r² − E_0[w_κ(A, Y) | v_0(b, k)]| ≤ C r(1 + κ)²P^N. + +*Step C3 (densities and the target).* By (R5), `|π_r(v_r) − π_0(v_0(b, k))| ≤ Cr²P²e^{−c(b²+k²)}`, and +`E_0[w_κ] ≤ C(1 + κ)²P^N`. Also `r^{−2}A_0(b, κr, u) = 12π_0(v_0(b, k))36κ²E_0[Δ²1{A<0} | v_0(b, k)]` exactly. Hence + + r^{−2}(A_r − A_0)(b, κr, u) = −12π_0(v_0(b, k))E_0[min(Y², 36κ²Δ²)1{A<0} | v_0(b, k)] + O(r(1 + κ)²P^Ne^{−c(b²+k²)}). + +It remains to move the target from `v_0(b, k)` to `v_0(b, 0)`, which uses the parity factorization of [P] §15. +- *Parity.* The covariance of the field is even, so jets of even and odd order at `0` are uncorrelated, hence + independent. The pin rows split the same way: `f`, `∂_u²f`, `∇_Θ∂_uf` are even; `∂_uf`, `∂_u³f`, `∇_Θf` are odd. + The target's even part is `(b, 0, 0)`, and its odd part is `(0, 12k, 0)`. +- *Even jets.* The conditional law of the even jets `(A, f₄)` does not depend on `k`. +- *Odd jets.* The odd jets have a `k`-independent covariance and a mean shift `12k·w` with `w` fixed. In particular + `γ = γ̄ + 12k w_γ`, with `γ̄` the `k = 0` version. +- *Density.* `π_0(v_0(b, k)) = p_even(b, 0, 0)p_odd(0, 12k, 0)`, and the second factor is + `p_odd(0, 0, 0)(1 + O(k²))`. +- *The integrand.* `|min(Y², c) − min(Ȳ², c)| ≤ (|Y| + |Ȳ|)|Y − Ȳ|` for every `c ≥ 0`. The shift of `γ` moves `Y` by + `≤ Ck(|γ̄| + k)‖A‖^{m−1}`, so the expectation moves by `O(kP^N)`, with no growth in `κ`. +- Hence the two targets differ by `O(k(1 + |b|)^Ne^{−cb²}) = O(κr(…))`, which proves (C.1). ∎ + +(The `κ²` in (C.1) comes only from the `3k tr(adj(A_0)B)` term in `Y`. That term is odd in the odd jets. A parity +argument would reduce its expected contribution to `O(k²)`, and (C.1) to `O(r(1 + κ))`. This would improve the +exponent `4/11` in (T.1) to `3/7`; it is not needed here.) + +## 4. The overlap and the proof of Theorem T + +**Lemma O (overlap).** For `κ ≥ 1`, + + 0 ≤ (𝒜^{cand} − 𝒜^{con})(b, κ, u) − A₂(b, 0, u) ≤ C κ^{−1} (1 + |b|)^N e^{−cb²}. (O.1) + +*Proof.* +- By (F.2) and the definitions, the difference is `12π_0E_0[(Y² − 36κ²Δ²)_+1{A<0} | b] ≥ 0`. It is at most + `12π_0E_0[Y²1{|Δ| < |Y|/(6κ)} | b]`. +- *Dyadic split.* Split by `|Y| ∈ [2^{j−1}, 2^j)` for `j ≥ 1`, and `|Y| < 1` for `j = 0`. Given `A`, the jets `(f₄, γ)` + are Gaussian with mean affine in `(A, b)` and bounded covariance. `Y` is a polynomial in them with coefficients + polynomial in `A`, so `P(|Y| ≥ t | A) ≤ C_p t^{−p}(1 + |b| + ‖A‖)^{n_p}`. +- Under `E_0[· | b]`, `A` is a nondegenerate Gaussian symmetric matrix with mean `O(1 + |b|)`. By Lemma D, + + E_0[Y²1{|Δ| < |Y|/(6κ)}] ≤ Σ_{j≥0} 4^j E_0[1{|det A| < 2^j/(6κ)} min(1, C_p2^{−(j−1)p}(1 + |b| + ‖A‖)^{n_p})] + ≤ Σ_j 4^j C_p 2^{−(j−1)p}(1 + |b|)^{n_p+m(m−1)/2} · 2^j/κ ≤ Cκ^{−1}(1 + |b|)^{n_p+m(m−1)/2}. + + Take `p > 3`; the factor `π_0 ≤ Ce^{−cb²}` completes the proof. ∎ + +(The mechanism, concentration on `|Δ| ≲ |Y|/κ` with mass `≍ 1/κ`, is the one #207 Remark 1 records for the rejected +cusp mass.) + +**Proof of Theorem T.** + +*Setup.* Put `ρ_f := ℓ^{1/4 + 1/44}` and `ρ_c := ℓ^{1/4 − 1/36}`. Fix `r_0 ∈ (0, r_0^*]` and take `ℓ` so small that +`ρ_c < r_0` and `ℓρ_f^{−3} ≤ 1`. By #191 (2.1) and #207 §7's decomposition of `B_{d,L}`, + + ν_cand(ℓ) − cℓ^{−1/3} − B_{d,L} = F + K + J₂ + J₃ + J₄ + J₅, + +with the integrands taken at `(b, ℓ/r³, u)` unless stated otherwise, and inner integrals `db dσ(u)`: +- `F := ∫_0^{ρ_f}∫∫ r^{−2}(A_r − A_0)`; +- `K := ∫_{ρ_f}^{ρ_c}∫∫ r^{−2}(A_r − A_0)`; +- `J₂ := −∫_0^{ρ_c}∫∫ r^{−2}A_r(b, 0, u)`; +- `J₃ := ∫_{ρ_c}^{r_0}∫∫ r^{−2}[A_r(b, ℓ/r³, u) − A_r(b, 0, u)]`; +- `J₄ := −∫_{ρ_c}^∞∫∫ r^{−2}A_0`; +- `J₅ := ∫_{dist(0,y)≥r_0}∫(Ψ_ℓ^{cand} − Ψ_0) db dy`. + +Here #207 §7 records `cℓ^{−1/3} = ∫_0^∞∫∫r^{−2}A_0` and +`B_{d,L} = ∫_0^{r_0}∫∫r^{−2}A_r(b, 0, u) + ∫_{dist≥r_0}∫Ψ_0`. The far candidate density is `∫_{dist≥r_0}∫Ψ_ℓ^{cand}`. + +*`F`: the fold region.* Here `k = ℓ/r³ ≥ r`. +- By (F.1), `r^{−2}(A_r − A_0) = A₂(b, ℓ/r³, u) + E_F` with `|E_F| ≤ C(r + r/k)(1 + |b|)^Ne^{−cb²}`, using + `P^Ne^{−ck²} ≤ C(1 + |b|)^N`. Here `r/k = r⁴/ℓ`. +- So `|∫E_F| ≤ C(ρ_f² + ρ_f⁵/ℓ)`. +- With `k = ℓ/r³`, `dr = −(1/3)ℓ^{1/3}k^{−4/3}dk` and `K₀ := ℓ/ρ_f³`, we have + `ℓ^{1/3}K₀^{−1/3} = ρ_f` and + + ∫_0^{ρ_f} A₂(b, ℓ/r³, u) dr = (ℓ^{1/3}/3)∫_{K₀}^∞ A₂ k^{−4/3} dk + = (ℓ^{1/3}/3)∫_0^∞ (A₂(k) − A₂(0)) k^{−4/3} dk + ρ_f A₂(b, 0, u) − (ℓ^{1/3}/3)∫_0^{K₀}(A₂(k) − A₂(0))k^{−4/3}dk. + +- The integrals converge absolutely by (F.2). The last term is `O(ℓ^{1/3}K₀^{2/3}) = O(ℓρ_f^{−2})`, uniformly with the + factor `(1 + |b|)^Ne^{−cb²}`. +- So `F = c₂ℓ^{1/3} + ρ_f∫∫A₂(b, 0, u) + O(ρ_f² + ρ_f⁵/ℓ + ℓρ_f^{−2})`. The convergence of (0.1) is part of this. + +*`K`: the cusp region.* Here `k = ℓ/r³ ≤ ℓρ_f^{−3} ≤ 1`. +- By (C.1) with `κ = ℓ/r⁴`, `r^{−2}(A_r − A_0) = (𝒜^{cand} − 𝒜^{con})(b, ℓ/r⁴, u) + E_K`, where + `∫_{ρ_f}^{ρ_c}|E_K| ≤ C∫_{ρ_f}^{ρ_c} r(1 + ℓr^{−4})² dr ≤ C(ρ_c² + ℓρ_f^{−2} + ℓ²ρ_f^{−6})`. +- With `r = sℓ^{1/4}`, the main term is `ℓ^{1/4}∫_σ^S(𝒜^{cand} − 𝒜^{con})(b, s^{−4}, u) ds`, where + `σ = ρ_fℓ^{−1/4} = ℓ^{1/44}` and `S = ρ_cℓ^{−1/4} = ℓ^{−1/36}`. +- *Upper tail.* `|𝒜^{cand} − 𝒜^{con}| ≤ 12π_0·36κ²E_0[Δ²] ≤ Cs^{−8}(…)`, so `∫_S^∞ = O(S^{−7})`. +- *Lower end.* By Lemma O, `∫_0^σ(𝒜^{cand} − 𝒜^{con}) ds = σA₂(b, 0, u) + O(σ⁵)`. +- So `K = ℓ^{1/4}·(the I^{cand} integrand) − ρ_f∫∫A₂(b, 0, u) + O(ℓ^{1/4}σ⁵ + ℓ^{1/4}S^{−7} + ρ_c² + ℓρ_f^{−2} + ℓ²ρ_f^{−6})`. + +*The overlap cancels.* The terms `±ρ_f∫∫A₂(b, 0, u)` of `F` and `K` cancel. Note `ℓ^{1/4}σ⁵ = ρ_f⁵/ℓ` and +`ℓ^{1/4}S^{−7} = ℓ²ρ_c^{−7}`. + +*`J₂`–`J₅`.* +- `|J₂| ≤ Cρ_c³` by #198 (W.4). +- `|J₃| ≤ C∫_{ρ_c}^∞(ℓ²r^{−8} + ℓr^{−3}) dr ≤ C(ℓ²ρ_c^{−7} + ℓρ_c^{−2})` by #207 (7.1); here `k ≤ 1`. +- `0 ≤ −J₄ ≤ Cℓ²ρ_c^{−7}`, since `A_0 ≤ k²H`. +- `|J₅| ≤ C_{r_0}ℓ` by #207 (7.2). + +*Exponents.* With `ρ_f = ℓ^{1/4+1/44}` and `ρ_c = ℓ^{1/4−1/36}`: + +| Term | Exponent | +|---|---| +| `ρ_f²` | `6/11` | +| `ρ_f⁵/ℓ` | `4/11` | +| `ℓρ_f^{−2}` | `5/11` | +| `ℓ²ρ_f^{−6}` | `4/11` | +| `ρ_c²` | `4/9` | +| `ρ_c³` | `2/3` | +| `ℓ²ρ_c^{−7}` | `4/9` | +| `ℓρ_c^{−2}` | `5/9` | +| `ℓ` | `1` | + +The least is `4/11`. So +`ν_cand − cℓ^{−1/3} − B_{d,L} = I^{cand}ℓ^{1/4} + c₂ℓ^{1/3} + O(ℓ^{4/11})`, which is (T.1). The exponents are checked +exactly by checker T1. ∎ + +## 5. Remarks + +1. **The elder density.** For `ν_eld` the same decomposition needs the following. + - *An elder Lemma C.* This is a quantitative Proposition CU.3 of #207. The decision's height margin is + `κ·min(1, 12||φ| − 1/3|)`, linear in the distance from the window's edge. + - Suppose the elder cusp error is `C r^θ(1 + κ)^N(1 + |b|)^Ne^{−cb²}`. In this ledger, + `θ > max(2/5, (N + 1)/4)` suffices. The fold end needs `θ > (N + 1)/4`, given `ρ_f = ℓ^{1/4+a}` with + `a > 1/60`. The top end needs `θ > 2/5`, given `ρ_c = ℓ^{1/4−b}` with `b > 1/84`. + - Lemma C's candidate rate, `θ = 1` with `N = 2`, meets this. + - The bare condition `θ > 1/3` would need a sharper treatment of the `S^{−7}` tails (referee M-3). + - *The fold-region elder deficit.* `A_r − A_r^{eld} ≤ Cr³/k` ([C7-K] (K2)) contributes `O(ρ_f⁵/ℓ)`, like the boundary + layer in `F`. This input is available. + - *Intermediate separations.* The elder density from `ρ_c ≤ r ≤ r₁` must be `o(ℓ^{1/3})`. On file, #198's Lemma B + gives `O(ℓ^{1/3}ρ^{−1})` and #207's Lemma CU.5 route gives `o(ℓ^{1/4})`; neither suffices. + - *The far part.* `ν_eld^{far,r₁} = o(ℓ^{1/3})` is needed. #198's Lemma F′ (`O(ℓ^{1/3})`) does not suffice. The + unmerged candidates Math- #187 (`O(ℓ^{2/3})`) and #188 (`O(ℓ^N)`) would. + + The formal value of the elder `ℓ^{1/3}` coefficient is the same `c₂` (Math- #216). +2. **The value of `c₂`.** By the parenthetical remark after Lemma F, Math- #216's `c2_check.py` computes a numerical + approximation of (0.1). It uses truncated jets and pin rows, a least-squares fit in `r` over five separations, and + Gauss–Legendre quadrature. The exact `r²`-coefficient of its truncated surrogate is `A₂`. + - For the Gaussian kernel `e^{−|z|²/2}` (the SIDE24 covariance up to factors `1 + O(e^{−L²/8})`): + `c₂ = 0.22152441` (`d = 2`), `0.16123405` (`d = 3`); `c₂/c = 3.017759`, `3.859496`. + - These are numerical values, stable to `≤ 7·10⁻¹⁰` under the variations of #216 §2.4; they are not certified. + - With #207's `I^{cand}` (`−0.1772744` in `d = 2`; `−0.1394041` in `d = 3`; exploration), the SIDE24 candidate + density is `ν_cand ≈ 0.0417759ℓ^{−1/3} + B_{3,24} − 0.1394041ℓ^{1/4} + 0.1612340ℓ^{1/3}`. The value + `B_{3,24} ≈ 10.21` comes from Math- #211 (exploration). +3. **Monte Carlo.** Math- #216 §3 compares the full-field Monte Carlo with the *adjacent*-pair density, not with + `ν_cand`. Formally the two have the same `ℓ^{−1/3}`, `ℓ^{1/4}` and `ℓ^{1/3}` coefficients, but adjacent pairs have no + `B_{d,L}` term; nothing on file proves the adjacent-pair expansion. Theorem T is the Kac–Rice statement; the Monte + Carlo is exploration. +4. **`d = 1`.** In `d = 1` the analogous structure is Math- #214's Proposition 2.2. There, part (c) is the fold + coefficient `B₂^{(1)}`, part (d) is the cusp, and the finite part is `B₂^{(2)}`. Its proof is self-contained (Rice + formula on the circle). +5. **What Lemma C adds to #207.** #207's CU.4 is a limit at fixed `κ` with dominated convergence. Lemma C gives the rate + `O(r(1 + κ)²)` uniformly for `κr ≤ 1`, for the candidate kernel. Only the candidate kernel is treated: the + elder mark needs Proposition CU.3, whose margins are not quantified in #207. + +## 6. Sources (exact identities in `SOURCES.json`) + +| Tag | Path | Role | +|---|---|---| +| [R] | `frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md` (blob `247b3ecf`) | (R2)–(R5), (R9), §4 scaled Hessians, Lemma R3.2, §5 eigenvalue coordinates — consumed | +| [P] | `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` (blob `dfed3b8d`) | §2 finite-jet rank, §4 regression, §§9–10 as [E2], §15 parity factorization and (15.2) — consumed | +| [E1] | `imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md` (blob `213594d6`) | reading rule | +| [E2] | `reviews/d1_section9_borel_repair_20260925/REPAIR.md` (blob `fe9b9ce4`) | §9 replacement | +| [REC] | `reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md` (blob `75da2597`) | reading rule | +| [Z] | `frontiers/c7_zero_gap_limit_20260929/PROOF.md` (blob `5b6328ea`) | (Z2)–(Z3): `Ψ_0`, `B_{d,L}` — consumed | +| #191 | `frontiers/remainder_vanishing_20260930/PROOF.md` (unmerged; v1.1 blob `441152df`) | Lemma E Steps 1–4, `T`, §2 (2.1), `r_0^*` — **consumed, unmerged** | +| #198 | `frontiers/remainder_rate_20260930/PROOF.md` (unmerged; v1.1 blob `abfb98ae`) | (3.1), the sign window, (W.4) — **consumed, unmerged**; (W.1) only through #207 Lemma L | +| #207 | `frontiers/cusp_second_order_20261001/PROOF.md` (unmerged; v1.1 blob `f6df5a73`) | §0 cusp objects; Lemma CU.5's nondegeneracy of free jets; §7 Lemma L (7.1)–(7.2), the far identity, the decomposition of `B_{d,L}`, (7.3) — **consumed, unmerged** | +| [C7-K] | `frontiers/c7_total_bounded_20260929/PROOF.md` (blob `28748b08`) | (K2), in Remark 1 only — cited | +| #216 | `frontiers/third_order_coefficient_20261001/` (unmerged) | numerical values of `c₂` — cited only | +| #214 | `frontiers/d1_third_order_law_20261001/PROOF.md` (unmerged) | the `d = 1` analogue — cited only | +| #187, #188 | `frontiers/far_elder_rate_20260930/PROOF.md`, `frontiers/far_elder_flat_ridge_20260930/PROOF.md` (unmerged) | far elder bounds, in Remark 1 only — cited only | +| #211 | `frontiers/equal_height_mass_value_20261001/` (unmerged) | `B_{3,24} ≈ 10.21`, in Remark 2 only — cited only | + +## 7. Exact controls (`thmT_check.py`; stdlib; exact rationals; byte-identical under `-O`) + +- **T1** the exponent ledger of §4 with `ρ_f = ℓ^{1/4+1/44}`, `ρ_c = ℓ^{1/4−1/36}`: every exponent `≥ 4/11`, with equality + exactly for `ρ_f⁵/ℓ` and `ℓ²ρ_f^{−6}`, and `4/11 > 1/3`; the hypotheses `ρ_f < ℓ^{1/4} < ρ_c` and `ℓρ_f^{−3} ≤ 1`. +- **T2** the pathwise case analysis of Step C1 on random rational data: the two weights, the case bounds + `24ηκ|Δ| + η²` and `2η(12κ|Δ| + 3η)`, and Case 3's sign-window bound. +- **T3** the Lipschitz bound of Step C2 (constant `12κ|Δ|`) and the identity + `(36κ²Δ² − Y²)_+ − 36κ²Δ² = −min(Y², 36κ²Δ²)`. +- **T4** Lemma D's Vandermonde inequality `∏_{j≠i*}|λ_{i*} − λ_j| ≤ 2^{m−1}∏_{j≠i*}|λ_j|` for random rational spectra, + `m = 1…5`. +- **T5** the product structure (2.2) on exactly pinned polynomial fields in `d = 2` and `d = 3`. + - Polynomial fields of degree 7 with random rational free jets are used. + - The pinned jets are solved from the pin rows symbolically, as exact polynomials in `r`. + - `det K_i = det H_i/r` is computed exactly as a polynomial in `r`, at `k = 0` and at random rational `k > 0`. + - The constant terms are `∓6kΔ`, and `det K_M`, `det K_S` share the `r¹` coefficient + `Y = (f₄/12)Δ + 3k tr(adj(A)B) − γᵀadj(A)γ/4`. + - The product has constant term `−36k²Δ²` and no `r¹` term. At `k = 0` its `r²` coefficient is `Y²`. +- **Mutants.** Each exits 1: + - M1 `ρ_f = ℓ^{1/4+1/40}`; + - M2 drop the factor `2^{m−1}` in T4; + - M3 Lipschitz constant `6κ|Δ|` in T3; + - M4 a one-sided axial row in T5, which produces an `r¹` term. + + An unknown label exits 2. + +**What the controls do not test.** Lemma D, (1.2), Steps F2–F3, Step C3, Lemma O and the assembly as statements about +random fields; these are proved in prose. T5 tests the deterministic structure (2.2) on polynomial fields only. + +## 8. Review slices + +- **A** §1–§2: Lemma D (eigenvalue coordinates, the Vandermonde cancellation), (1.2), and Lemma F. For Lemma F: + - the pin reduction (2.1); + - (2.2) against #191 and #198; + - the good event and the dyadic layer bound (2.3); + - the smoothness in `r²` (Step F3) and the properties (F.2). +- **B** §3: Lemma C. The three cases (Haynsworth, the sign window), the Lipschitz step, and the parity factorization + for the target shift. +- **C** §4: Lemma O, the decomposition `F + K + J₂ + … + J₅`, the finite-part manipulation, the overlap cancellation and + the exponents. diff --git a/frontiers/candidate_third_order_20261001/README.md b/frontiers/candidate_third_order_20261001/README.md new file mode 100644 index 000000000..4761618c0 --- /dev/null +++ b/frontiers/candidate_third_order_20261001/README.md @@ -0,0 +1,68 @@ +# The candidate density to third order (CL-CANDIDATE-THIRD-ORDER-20261001-v1) + +Author-side proof candidate. Anthropic Claude, 1 October 2026. Scientific effect NONE. Nonauthor review required. + +**Statement (Theorem T).** For every `d ≥ 2` and `L > 0`, as `ℓ ↓ 0`, + + ν_cand(ℓ) = c ℓ^{−1/3} + B_{d,L} + I^{cand} ℓ^{1/4} + c₂ ℓ^{1/3} + O(ℓ^{4/11}). + +- `c` is the leading constant. +- `B_{d,L}` is the equal-height mass of [Z]. +- `I^{cand} = (3^{1/4}/2)c₁` is #207's cusp coefficient. +- `c₂` is the Hadamard finite part `(1/3)∫∫∫[A₂(b, k, u) − A₂(b, 0, u)]k^{−4/3}`. Here `A₂` is the `r²`-coefficient of + [R]'s two-point kernel at fixed `(b, k, u)`, and `A₂(b, 0, u) = −12π₀E₀[Y²1{A<0} | b]`. + +This is the `ℓ^{1/3}` coefficient that Math- #216 defines and computes numerically: `0.22152441` in `d = 2` and +`0.16123405` in `d = 3` (SIDE24) for the Gaussian kernel. Here it is proved to be the third coefficient of the candidate +density in every dimension. + +**Corollary T′.** `ν_cand − cℓ^{−1/3} − B_{d,L} − I^{cand}ℓ^{1/4} = O(ℓ^{1/3})`. This is a rate for #207's (CU′.1), and +it closes the open item "a rate for the `o(ℓ^{1/4})`" for the candidate density. + +**The three new lemmas.** +- **Lemma F (fold expansion).** `A_r = A₀ + r²A₂ + O(r³(1 + k^{−1}))`. The `r¹` term vanishes by the cancellation of + #191 and #198. The `r³/k` remainder is the boundary layer of the typed region near `det A = 0`, bounded through an + eigenvalue-layer estimate (Lemma D). +- **Lemma C (cusp kernel with a rate).** + `|r^{−2}(A_r − A₀)(b, κr) − (𝒜^{cand} − 𝒜^{con})(b, κ)| ≤ Cr(1 + κ)²(…)` for `κr ≤ 1`. This is a quantitative form of + #207's CU.4 for the candidate kernel. The proof is a pathwise case analysis (Haynsworth, the sign window), followed + by a parity argument for the target. +- **Lemma O (overlap).** `(𝒜^{cand} − 𝒜^{con})(b, κ) = A₂(b, 0) + O(κ^{−1})`. This makes the fold-scale finite part match + the cusp integral. + +**The assembly.** It splits `ν_cand − cℓ^{−1/3} − B_{d,L}` at `ρ_f = ℓ^{1/4+1/44}` (fold | cusp) and at +`ρ_c = ℓ^{1/4−1/36}` (cusp | intermediate). #207's Lemma L handles the intermediate and far separations. The exponent +`4/11 = 1/3 + 1/33` is the least in the ledger; checker T1 checks it exactly. + +**Not claimed:** +- the elder density's `ℓ^{1/3}` term. That needs an elder Lemma C, a bound for intermediate elder separations, and a far + elder bound (Remark 1); +- certified constants; +- sharpness of `4/11`; +- uniformity in `d` and `L`. + +**Dependencies.** +- *Consumed, unmerged:* Math- #191, #198 and #207. This packet must be rebound if any of them changes. +- *Merged:* [R], [P] (with [E1], [E2], [REC]) and [Z]. +- *Cited:* #216, #214, #187, #188, #211 and [C7-K]. + +**Files.** +- `PROOF.md`. +- `thmT_check.py`: standard library, exact rationals. Its output is `RESULTS.json`, byte-identical under `-O` and on + CPython 3.10–3.14. The controls are: + - **T1** the exponent ledger; + - **T2** Lemma C's case analysis; + - **T3** its Lipschitz step; + - **T4** Lemma D's Vandermonde inequality; + - **T5** the product structure (2.2) on exactly pinned polynomial fields in `d = 2, 3`. + + Mutants M1–M4 exit 1, and an unknown label exits 2. +- `SOURCES.json`: the exact identities of all sources. + +**Review record.** Before submission, a clean-context same-family referee read the whole note. It reported no major +issue; its five minor findings and eight nits are applied. Same account, zero organizational independence. + +**Review slices** (PROOF §8): +- **A** Lemma D, (1.2) and Lemma F; +- **B** Lemma C; +- **C** Lemma O and the assembly. diff --git a/frontiers/candidate_third_order_20261001/RESULTS.json b/frontiers/candidate_third_order_20261001/RESULTS.json new file mode 100644 index 000000000..1f25b3f2b --- /dev/null +++ b/frontiers/candidate_third_order_20261001/RESULTS.json @@ -0,0 +1,123 @@ +{ + "checks": { + "T1_exponent_ledger": { + "exponents": { + "l": "1", + "l rho_c^-2": "5/9", + "l rho_f^-2": "5/11", + "l^2 rho_c^-7": "4/9", + "l^2 rho_f^-6": "4/11", + "rho_c^2": "4/9", + "rho_c^3": "2/3", + "rho_f^2": "6/11", + "rho_f^5/l": "4/11" + }, + "least": "4/11", + "margin_over_1/3": "1/33", + "passed": true + }, + "T2_lemma_C_cases": { + "cases_both": 2101, + "cases_exactly_one": 567, + "cases_neither": 1332, + "passed": true, + "sign_window_cases": 2412 + }, + "T3_lipschitz": { + "passed": true, + "trials": 4000 + }, + "T4_vandermonde": { + "m": [ + 1, + 2, + 3, + 4, + 5 + ], + "passed": true, + "trials_per_m": 800 + }, + "T5_pinned_product_d2_d3": { + "passed": true, + "trials": [ + { + "common_Y": true, + "const_ok": true, + "d": 2, + "deg_product": 18, + "k": "0", + "r1_zero": true, + "r2_is_Y2_at_k0": true + }, + { + "common_Y": true, + "const_ok": true, + "d": 2, + "deg_product": 18, + "k": "241/100", + "r1_zero": true, + "r2_is_Y2_at_k0": null + }, + { + "common_Y": true, + "const_ok": true, + "d": 2, + "deg_product": 18, + "k": "0", + "r1_zero": true, + "r2_is_Y2_at_k0": true + }, + { + "common_Y": true, + "const_ok": true, + "d": 2, + "deg_product": 18, + "k": "32/25", + "r1_zero": true, + "r2_is_Y2_at_k0": null + }, + { + "common_Y": true, + "const_ok": true, + "d": 3, + "deg_product": 28, + "k": "0", + "r1_zero": true, + "r2_is_Y2_at_k0": true + }, + { + "common_Y": true, + "const_ok": true, + "d": 3, + "deg_product": 28, + "k": "27/20", + "r1_zero": true, + "r2_is_Y2_at_k0": null + }, + { + "common_Y": true, + "const_ok": true, + "d": 3, + "deg_product": 28, + "k": "0", + "r1_zero": true, + "r2_is_Y2_at_k0": true + }, + { + "common_Y": true, + "const_ok": true, + "d": 3, + "deg_product": 28, + "k": "49/25", + "r1_zero": true, + "r2_is_Y2_at_k0": null + } + ] + } + }, + "mutant": null, + "object": "CL-CANDIDATE-THIRD-ORDER-20261001-v1 controls", + "passed": true, + "scientific_effect": "NONE" +} diff --git a/frontiers/candidate_third_order_20261001/SOURCES.json b/frontiers/candidate_third_order_20261001/SOURCES.json new file mode 100644 index 000000000..8dfd053ba --- /dev/null +++ b/frontiers/candidate_third_order_20261001/SOURCES.json @@ -0,0 +1,212 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "object": "CL-CANDIDATE-THIRD-ORDER-20261001-v1", + "kind": "author-side proof candidate: the candidate (Kac-Rice max/index-(d-1)) lifetime density to third order in every d >= 2, nu_cand = c l^(-1/3) + B_{d,L} + I_cand l^(1/4) + c2 l^(1/3) + O(l^(4/11)), with c2 the fold-scale Hadamard finite part (the coefficient of Math- #216); Corollary: a rate O(l^(1/3)) for (CU-prime.1) of Math- #207", + "author": "Anthropic Claude", + "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", + "read_at": { + "branch_base": "3e0a91b69892b9717564c592e7a966492a81566a" + }, + "consumed": [ + { + "path": "frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md", + "bytes": 17734, + "sha256": "380b7d0abdb0fe2de5a6564565af9560d3f1b1ce22fd5538927db0c52f4f3a4a", + "git_blob": "247b3ecf80bfbe896948d5d489b2d5842a81c481", + "tag": "R", + "use": "(R2)-(R5), (R9): coupling, moments, pin densities; section 4 scaled Hessians; Lemma R3.2; section 5 eigenvalue coordinates" + }, + { + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "bytes": 40261, + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "tag": "P", + "use": "section 2 linear independence of distinct derivative functionals; section 4 regression; sections 9-10 as [E2]; section 15 parity factorization and (15.2)" + }, + { + "path": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", + "bytes": 1782, + "sha256": "bad7ef609c4ad8c41ad6af562c1b6807921e19a9d556ed793ad1a0db6e202028", + "git_blob": "213594d6ca6a86fb938110f4d166d9ce275a02d0", + "tag": "E1", + "use": "reading rule" + }, + { + "path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", + "bytes": 9062, + "sha256": "845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f", + "git_blob": "fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a", + "tag": "E2", + "use": "section 9 replacement" + }, + { + "path": "reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md", + "bytes": 23312, + "sha256": "451b9d7ffee072a73fc904cab891b6693e3f233808b89df10cce1b57036b65da", + "git_blob": "75da2597971510f843f8d90c743950cb8c177342", + "tag": "REC", + "use": "reading rule" + }, + { + "path": "frontiers/c7_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}" + } + ], + "consumed_unmerged": [ + { + "path": "frontiers/remainder_vanishing_20260930/PROOF.md", + "bytes": 25353, + "sha256": "0cb5b949261476f10e539677e2744e3288752474393af25ba787e67b1350f32a", + "git_blob": "441152dfc1d8d00cb268cebdb0394212a5bfacdb", + "tag": "191", + "use": "Lemma E Steps 1-4 (expansions (1.1)-(1.6), the good event and its three layer cases), the dominating variable T, section 2 (2.1), r_0^*", + "head": "abae6d0b08f39a6b244308c4e351327c1ef56890", + "pr": "Math- #191" + }, + { + "path": "frontiers/remainder_rate_20260930/PROOF.md", + "bytes": 33131, + "sha256": "0b690df6ac40707ca06783f5641d8b480277c716df75b1031d84ee53a0575f72", + "git_blob": "abfb98ae41d66a86d3cb094162db6547d0f29e7e", + "tag": "198", + "use": "(3.1) with the (1 + k)-quantified remainder, the sign window of section 3, (W.4); (W.1) only through #207 Lemma L", + "head": "a28d13c91ef17ffd2c129322457845cd09e713ac", + "pr": "Math- #198" + }, + { + "path": "frontiers/cusp_second_order_20261001/PROOF.md", + "bytes": 52605, + "sha256": "cffc1b83ac364da58bd650c3c301ea1babd38e19af54f74010bdc120edce38a8", + "git_blob": "f6df5a7356a54771b0052e42a864a140709903ad", + "tag": "207", + "use": "section 0 cusp objects; Lemma CU.5 nondegeneracy argument (extended in Step F1); section 7: Lemma L (7.1)-(7.2), the far identity, the decomposition of B_{d,L}, (7.3)", + "head": "826b8be512e86f2de73c33d6ac7a76908dc2e0e6", + "pr": "Math- #207" + } + ], + "cited_only": [ + { + "path": "frontiers/c7_total_bounded_20260929/PROOF.md", + "bytes": 14982, + "sha256": "16c0efe372c1b1f26460aaa109287fed78e6fbd2dd00a0530998db296278dd01", + "git_blob": "28748b086ec6761ef467dc67cba475fbdf8b7455", + "tag": "C7-K", + "use": "(K2), in Remark 1 only (the fold-region elder deficit)" + } + ], + "cited_unmerged": [ + { + "path": "frontiers/third_order_coefficient_20261001/NOTE.md", + "bytes": 16930, + "sha256": "8f06d00cd248529b8939941bc02541eaca6aafc0f9dba4fc10cebc925c839646", + "git_blob": "3b5ffffad53ac15bb513c273d1bcf4289180b7e8", + "tag": "216", + "use": "definition and numerical values of c2 (Remark 2)", + "head": "605af74ce462ed5a26bb488c65c0b4097d6bd3fa", + "pr": "Math- #216" + }, + { + "path": "frontiers/d1_third_order_law_20261001/PROOF.md", + "bytes": 44378, + "sha256": "279ed88ff2debd570e6426aec53cc93aabc7a298731cd9b25c45667a2c11077b", + "git_blob": "873532b955dbf7684edc1a53ba169c7216f778ab", + "tag": "214", + "use": "the d = 1 analogue (Remark 4)", + "head": "f4a58df9247dfa9ada2b756ecd7629c0b2faf5b5", + "pr": "Math- #214" + }, + { + "path": "frontiers/far_elder_rate_20260930/PROOF.md", + "bytes": 16413, + "sha256": "67f606327b66a2b4f1b8c67a57d119ac9ddfd2ce827ca8cb0c4daefa31904a3b", + "git_blob": "37dcf6ef933251c8890ab653cafd648610779342", + "tag": "187", + "use": "far elder bound O(l^(2/3)) (Remark 1)", + "head": "ecd47e7b1d447eefec963b1fa8395777db09a190", + "pr": "Math- #187" + }, + { + "path": "frontiers/far_elder_flat_ridge_20260930/PROOF.md", + "bytes": 22806, + "sha256": "957f9c5e6557a558b2c055fa2a1f11ba301581995b8958658fad2edf47136f57", + "git_blob": "50cfbf4fcb9a3526f979eaedf885d42824a3c3a3", + "tag": "188", + "use": "far elder bound O(l^N) (Remark 1)", + "head": "85f0586a468c2b2f73af0e340d251e33a52caade", + "pr": "Math- #188" + }, + { + "path": "frontiers/equal_height_mass_value_20261001/NOTE.md", + "bytes": 16177, + "sha256": "9080a5dc567710e0668890cd209484db9026b19ff4707341487f289e2f7c7410", + "git_blob": "ed0d3fa8e4c28d181fa7d21efcde74933cc6f03c", + "tag": "211", + "use": "B_{3,24} ~ 10.21 (Remark 2, exploration)", + "head": "8e89fe886368ae048e125c26f3ac51aa9bec83f6", + "pr": "Math- #211" + } + ], + "cited_external": [ + { + "tag": "Weyl", + "reference": "Weyl integration formula on symmetric matrices (eigenvalue coordinates, Vandermonde factor)", + "use": "Lemma D" + }, + { + "tag": "Haynsworth", + "reference": "E. V. Haynsworth, inertia additivity of the Schur complement (1968)", + "use": "Lemma C, Case 1; Lemma F, Step F2 (through #191 Step 4)" + }, + { + "tag": "Anderson", + "reference": "T. W. Anderson, The integral of a symmetric unimodal function over a symmetric convex set (1955)", + "use": "(1.2): conditional moments dominated by unconditional ones" + } + ], + "mutants": [ + "M1", + "M2", + "M3", + "M4" + ], + "replayed": [ + "thmT_check.py" + ], + "referee": { + "kind": "clean-context same-family referee (Anthropic Claude subagent), before submission", + "verdict": "ACCEPT WITH MINOR FIXES (no major finding; five minor findings and eight nits, all applied)", + "report": "project archive V2_2/frontiers_candidate_third_order_20261001/REFEREE_1.md", + "report_sha256": "9f25ccfc0da9cc266bce412b0dd090486110b2736cce0fe64a41473c664ce679", + "report_bytes": 15735, + "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": 37220, + "sha256": "6c1279164499d4fe2fbeee244b40dafa2159758d20f04826cd67d7602ea97fe4" + }, + { + "path": "README.md", + "bytes": 3705, + "sha256": "a2696c1596430829a1585723e16a51f191186c897c74dc015331da0fac78c2e0" + }, + { + "path": "thmT_check.py", + "bytes": 13798, + "sha256": "5bdb81d980e9d21cd28de0159d9adbb9a2caccaaec5a2d80b4d45f329ae4949a" + }, + { + "path": "RESULTS.json", + "bytes": 2193, + "sha256": "769fe2b9469666ee0e60838717734d18e97ed28424e25108f2296bd2d04f74d0" + } + ] +} diff --git a/frontiers/candidate_third_order_20261001/thmT_check.py b/frontiers/candidate_third_order_20261001/thmT_check.py new file mode 100644 index 000000000..ecde5abbb --- /dev/null +++ b/frontiers/candidate_third_order_20261001/thmT_check.py @@ -0,0 +1,329 @@ +#!/usr/bin/env python3 +"""Exact controls for CL-CANDIDATE-THIRD-ORDER-20261001-v1 (frontiers/candidate_third_order_20261001/PROOF.md). +Standard library only, exact rationals. Run: python3 -B -S thmT_check.py (and with -O; output byte-identical). +Mutants: --mutant M1|M2|M3|M4 must exit 1; an unknown label exits 2. + + T1 the exponent ledger of section 4 (rho_f = l^(1/4+1/44), rho_c = l^(1/4-1/36)): every exponent >= 4/11, equality + exactly for rho_f^5/l and l^2 rho_f^-6, 4/11 > 1/3; rho_f < l^(1/4) < rho_c and l rho_f^-3 <= 1 for l <= 1 + T2 Lemma C, Step C1: the pathwise case analysis on random rational data (Case 1 weights and bounds; the sign window) + T3 Lemma C, Step C2: the Lipschitz constant 12 kappa |Delta| of w_kappa in Y, and (36k^2D^2 - Y^2)_+ - 36k^2D^2 = -min + T4 Lemma D: the Vandermonde inequality prod_{j != i*} |l_i* - l_j| <= 2^(m-1) prod_{j != i*} |l_j|, m = 1..5 + T5 (2.2) on exactly pinned polynomial fields of degree 7 in d = 2 and d = 3 (pinned jets solved symbolically as + polynomials in r): det K_i = det H_i / r has constant term -+6k Delta and common r^1 coefficient + Y = (f4/12) Delta + 3k tr(adj(A) B) - gamma^T adj(A) gamma / 4; the product has constant term -36 k^2 Delta^2, no + r^1 term, and r^2 coefficient Y^2 at k = 0 +""" +import argparse +import json +import random +import sys +from fractions import Fraction as Fr +from math import factorial + +MUTANT = None + + +# ----------------------------------------------------------------------------------------------- T1 exponents +def t1(): + q = Fr(1, 4) + af, ac = Fr(1, 44), Fr(1, 36) + if MUTANT == 'M1': + af = Fr(1, 40) + ef, ec = q + af, q - ac # rho_f = l^ef, rho_c = l^ec + terms = {'rho_f^2': 2 * ef, 'rho_f^5/l': 5 * ef - 1, 'l rho_f^-2': 1 - 2 * ef, 'l^2 rho_f^-6': 2 - 6 * ef, + 'rho_c^2': 2 * ec, 'rho_c^3': 3 * ec, 'l^2 rho_c^-7': 2 - 7 * ec, 'l rho_c^-2': 1 - 2 * ec, 'l': Fr(1)} + least = min(terms.values()) + ok = (least == Fr(4, 11) and sorted(k for k, v in terms.items() if v == least) == ['l^2 rho_f^-6', 'rho_f^5/l'] + and Fr(4, 11) > Fr(1, 3) and ef > q > ec and 1 - 3 * ef >= 0) + return {'exponents': {k: str(v) for k, v in sorted(terms.items())}, 'least': str(least), 'margin_over_1/3': str(least - Fr(1, 3)), + 'passed': bool(ok)} + + +# ----------------------------------------------------------------------------------------------- T2, T3 Lemma C +def rnd(rng, lo=-3, hi=3, den=97): + return Fr(rng.randint(lo * den, hi * den), den) + + +def w_kappa(kap, D, Y): + v = 36 * kap * kap * D * D - Y * Y + return v if v > 0 else Fr(0) + + +def t2(rng): + n_both = n_one = n_none = n_win = 0 + ok = True + for _ in range(4000): + s = rng.choice((1, -1)) # s = (-1)^m = sign(Delta) when A_0 < 0 + kap = Fr(rng.randint(1, 400), 100) + D = s * Fr(rng.randint(1, 300), 100) + eta = Fr(rng.randint(0, 60), 100) + rM, rS = Fr(rng.randint(-100, 100), 100) * eta, Fr(rng.randint(-100, 100), 100) * eta # |rho_i| <= eta + # put Y near the window edges half the time, to exercise the disagreement case + if rng.random() < 0.5: + Y = rng.choice((1, -1)) * 6 * kap * abs(D) + Fr(rng.randint(-100, 100), 100) * eta + else: + Y = rnd(rng) * 6 * kap * abs(D) / 2 + mM, mS = Y - 6 * kap * D + rM, Y + 6 * kap * D + rS + typed = s * mM < 0 < s * mS + lim = abs(Y) < 6 * kap * abs(D) + a = abs(mM * mS) if typed else Fr(0) + w = w_kappa(kap, D, Y) + if lim != (w > 0): + ok = False + if typed and lim: + n_both += 1 + ok &= abs(a - w) <= 24 * eta * kap * abs(D) + eta * eta + elif typed or lim: + n_one += 1 + b = 2 * eta * (12 * kap * abs(D) + 3 * eta) + ok &= a <= b and w <= b + else: + n_none += 1 + ok &= a == 0 and w == 0 + # the sign window (#198 section 3): opposite signs force |m_i| <= 12 kappa |Delta| + 2 eta + if mM * mS < 0: + n_win += 1 + ok &= abs(mM) <= 12 * kap * abs(D) + 2 * eta and abs(mS) <= 12 * kap * abs(D) + 2 * eta + return {'cases_both': n_both, 'cases_exactly_one': n_one, 'cases_neither': n_none, 'sign_window_cases': n_win, + 'passed': bool(ok and n_both > 100 and n_one > 100 and n_none > 100)} + + +def t3(rng): + ok = True + lip = 6 if MUTANT == 'M3' else 12 + for _ in range(4000): + kap = Fr(rng.randint(1, 400), 100) + D = rnd(rng) + Y, Y2 = rnd(rng, -9, 9), rnd(rng, -9, 9) + if rng.random() < 0.5: + Y2 = Y + Fr(rng.randint(-20, 20), 1000) + ok &= abs(w_kappa(kap, D, Y) - w_kappa(kap, D, Y2)) <= lip * kap * abs(D) * abs(Y - Y2) + ok &= w_kappa(kap, D, Y) - 36 * kap * kap * D * D == -min(Y * Y, 36 * kap * kap * D * D) + return {'trials': 4000, 'passed': bool(ok)} + + +# ----------------------------------------------------------------------------------------------- T4 Lemma D +def t4(rng): + ok = True + for m in range(1, 6): + for _ in range(800): + lam = [rnd(rng, -5, 5, 31) for _ in range(m)] + if any(x == 0 for x in lam): + continue + i = min(range(m), key=lambda j: abs(lam[j])) + lhs = Fr(1) + rhs = Fr(2 ** (m - 1)) if MUTANT != 'M2' else Fr(1) + for j in range(m): + if j != i: + lhs *= abs(lam[i] - lam[j]) + rhs *= abs(lam[j]) + ok &= lhs <= rhs + return {'m': [1, 2, 3, 4, 5], 'trials_per_m': 800, 'passed': bool(ok)} + + +# ----------------------------------------------------------------------------------------------- T5 pinned polynomials +def padd(p, q): + out = list(p) + [Fr(0)] * max(0, len(q) - len(p)) + for i, c in enumerate(q): + out[i] += c + return out + + +def pmul(p, q): + out = [Fr(0)] * (len(p) + len(q) - 1) + for i, a in enumerate(p): + if a: + for j, b in enumerate(q): + out[i + j] += a * b + return out + + +def pscale(p, c): + return [c * x for x in p] + + +def trim(p): + while len(p) > 1 and p[-1] == 0: + p = p[:-1] + return p + + +def rpow(n): # the monomial r^n as a polynomial in r + return [Fr(0)] * n + [Fr(1)] + + +def axis_odd_sum(c, D, h, shift, skip): + """sum_{i odd} c[(i+shift,0..)] h^(i-1) r^(i-1) / i! over available coefficients, skipping index `skip`""" + out = [Fr(0)] + for i in range(1, D + 2, 2): + key = c.get(i + shift) + if key is None or i + shift == skip: + continue + out = padd(out, pmul(pscale(rpow(i - 1), h ** (i - 1) / factorial(i)), key)) + return out + + +def axis_even_sum(c, D, h, skip): + out = [Fr(0)] + for i in range(0, D + 2, 2): + key = c.get(i) + if key is None or i == skip: + continue + out = padd(out, pmul(pscale(rpow(i), h ** i / factorial(i)), key)) + return out + + +def pinned_field(free, b, k, D, m): + """free: dict multi-index (i, j_1..j_m) -> Fr, the free Taylor coefficients of f = sum c_a x^i y^j / (i! j!). + Returns dict multi-index -> polynomial in r: the pinned coefficients solved exactly from the pin rows of [R] section 2.""" + c = {key: [val] for key, val in free.items()} + h = Fr(1, 2) + z = (0,) * m + ax = {i: c[(i,) + z] for i in range(D + 1) if (i,) + z in c} + # row 3: (f_x(S) - f_x(M))/r = sum_{i odd} c_{i+1} h^(i-1) r^(i-1)/i! = 0 + ax[2] = pscale(axis_odd_sum(ax, D, h, 1, 2), Fr(-1)) + # row 4: (6/r^2)[f_x(M) + f_x(S) - 2(f(S) - f(M))/r] = c_3 + sum_{j odd >= 5} 12 (j-1) h^(j-1) / j! r^(j-3) c_j = 12k + rest = [Fr(0)] + for j in range(5, D + 1, 2): + if j in ax: + rest = padd(rest, pmul(pscale(rpow(j - 3), Fr(12 * (j - 1)) * h ** (j - 1) / factorial(j)), ax[j])) + if MUTANT == 'M4': # a one-sided axial row: an odd-order perturbation of c_3 + rest = padd(rest, pmul(pscale(rpow(1), Fr(1, 2)), ax[4])) + ax[3] = padd([12 * k], pscale(rest, Fr(-1))) + # row 2: (f(S) - f(M))/r = sum_{i odd} c_i h^(i-1) r^(i-1)/i! = -k r^2 + ax[1] = padd(pscale(rpow(2), -k), pscale(axis_odd_sum(ax, D, h, 0, 1), Fr(-1))) + # row 1: (f(M) + f(S))/2 = sum_{i even} c_i (h r)^i / i! = b - k r^3 / 2 + ax[0] = padd(padd([b], pscale(rpow(3), -k / 2)), pscale(axis_even_sum(ax, D, h, 0), Fr(-1))) + for i in range(4): + c[(i,) + z] = ax[i] + # transverse rows, one pair per transverse direction l + for l in range(m): + e = tuple(1 if t == l else 0 for t in range(m)) + tr = {i: c[(i,) + e] for i in range(D) if (i,) + e in c} + c[(0,) + e] = pscale(axis_even_sum(tr, D, h, 0), Fr(-1)) # (f_yl(M) + f_yl(S))/2 = 0 + c[(1,) + e] = pscale(axis_odd_sum(tr, D, h, 0, 1), Fr(-1)) # (f_yl(S) - f_yl(M))/r = 0 + return c + + +def deriv_at(c, alpha, sign, D): + """d^alpha f at (sign h r, 0, ..., 0) as a polynomial in r; alpha = (a_x, a_y1, ..., a_ym)""" + h = Fr(1, 2) * sign + out = [Fr(0)] + for i in range(0, D + 1): + key = c.get((alpha[0] + i,) + tuple(alpha[1:])) + if key is None: + continue + out = padd(out, pmul(pscale(rpow(i), h ** i / factorial(i)), key)) + return out + + +def det_poly(M): + n = len(M) + if n == 1: + return M[0][0] + if n == 2: + return padd(pmul(M[0][0], M[1][1]), pscale(pmul(M[0][1], M[1][0]), Fr(-1))) + out = [Fr(0)] + for j in range(n): + minor = [[M[i][t] for t in range(n) if t != j] for i in range(1, n)] + out = padd(out, pscale(pmul(M[0][j], det_poly(minor)), Fr((-1) ** j))) + return out + + +def det_num(M): + n = len(M) + if n == 1: + return M[0][0] + return sum(((-1) ** j) * M[0][j] * det_num([[M[i][t] for t in range(n) if t != j] for i in range(1, n)]) for j in range(n)) + + +def adj_num(M): + n = len(M) + if n == 1: + return [[Fr(1)]] + return [[((-1) ** (i + j)) * det_num([[M[a][b] for b in range(n) if b != i] for a in range(n) if a != j]) for j in range(n)] + for i in range(n)] + + +def multi_indices(d, D): + out = [] + def rec(prefix, left, slots): + if slots == 0: + out.append(tuple(prefix)) + return + for v in range(left + 1): + rec(prefix + [v], left - v, slots - 1) + rec([], D, d) + return out + + +def t5(rng): + D = 7 + ok = True + rows = [] + for d in (2, 3): + m = d - 1 + pinned = {(i,) + (0,) * m for i in range(4)} + for l in range(m): + e = tuple(1 if t == l else 0 for t in range(m)) + pinned |= {(0,) + e, (1,) + e} + for trial in range(4): + k = Fr(0) if trial % 2 == 0 else Fr(rng.randint(1, 300), 100) + b = rnd(rng) + free = {a: rnd(rng, -2, 2, 13) for a in multi_indices(d, D) if a not in pinned} + c = pinned_field(free, b, k, D, m) + det = {} + k1 = {} + unit = lambda t: tuple(1 if s == t else 0 for s in range(d)) + # transverse jets at 0 + A = [[free[(0,) + tuple(unit(1 + l)[1:][s] + unit(1 + q)[1:][s] for s in range(m))] for q in range(m)] for l in range(m)] + B = [[free[(1,) + tuple(unit(1 + l)[1:][s] + unit(1 + q)[1:][s] for s in range(m))] for q in range(m)] for l in range(m)] + gam = [free[(2,) + unit(1 + l)[1:]] for l in range(m)] + f4 = free[(4,) + (0,) * m] + Dl = det_num(A) + adjA = adj_num(A) + trAB = sum(adjA[i][j] * B[j][i] for i in range(m) for j in range(m)) + q = sum(gam[i] * adjA[i][j] * gam[j] for i in range(m) for j in range(m)) / 4 + Y = f4 / 12 * Dl + 3 * k * trAB - q + for name, sg in (('M', -1), ('S', 1)): + H = [[deriv_at(c, tuple(unit(a)[t] + unit(bb)[t] for t in range(d)), sg, D) for bb in range(d)] for a in range(d)] + dh = trim(det_poly(H)) + if dh[0] != 0: + ok = False + dk = trim(dh[1:]) + det[name] = dk + k1[name] = dk[1] if len(dk) > 1 else Fr(0) + if dk[0] != sg * 6 * k * Dl: # det K_M = -6k Delta + ..., det K_S = +6k Delta + ... + ok = False + prod = trim(pmul(det['M'], det['S'])) + c0 = prod[0] + c1 = prod[1] if len(prod) > 1 else Fr(0) + c2 = prod[2] if len(prod) > 2 else Fr(0) + good = (c0 == -36 * k * k * Dl ** 2 and c1 == 0 and k1['M'] == Y and k1['S'] == Y and (k != 0 or c2 == Y * Y)) + ok &= good + rows.append({'d': d, 'k': str(k), 'deg_product': len(prod) - 1, 'const_ok': c0 == -36 * k * k * Dl ** 2, + 'r1_zero': c1 == 0, 'common_Y': k1['M'] == Y and k1['S'] == Y, + 'r2_is_Y2_at_k0': (c2 == Y * Y) if k == 0 else None}) + return {'trials': rows, 'passed': bool(ok)} + + +def main(): + global MUTANT + ap = argparse.ArgumentParser() + ap.add_argument('--mutant', default=None) + args = ap.parse_args() + if args.mutant is not None and args.mutant not in ('M1', 'M2', 'M3', 'M4'): + sys.stderr.write('unknown mutant label\n') + return 2 + MUTANT = args.mutant + rng = random.Random(20261001) + out = {'object': 'CL-CANDIDATE-THIRD-ORDER-20261001-v1 controls', 'scientific_effect': 'NONE', 'mutant': MUTANT, + 'checks': {'T1_exponent_ledger': t1(), 'T2_lemma_C_cases': t2(rng), 'T3_lipschitz': t3(rng), + 'T4_vandermonde': t4(rng), 'T5_pinned_product_d2_d3': t5(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 7f09d34f2558a79be964e64cc5e2382c3352bf4d Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 1 Oct 2026 09:42:40 +0000 Subject: [PATCH 2/2] Theorem T workflow: reject symlinked or non-blob sources (Codex P2 4153982206) Every source read from the checkout (merged consumed/cited, and a landed consumed dependency) must now be the recorded regular-file blob in the checked-out tree (git ls-tree: mode 100644, type blob, recorded blob id) and a regular file on disk; a symlink (mode 120000), a broken link, or an untracked file at a consumed path fails the job. Unlanded sources are bound through the API by head, path and blob as before. Negative test: a symlinked merged source is rejected. No change to the packet files. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .github/workflows/candidate-third-order.yml | 37 ++++++++++++++++++--- 1 file changed, 32 insertions(+), 5 deletions(-) diff --git a/.github/workflows/candidate-third-order.yml b/.github/workflows/candidate-third-order.yml index 74fc228d2..3bd2c8cd2 100644 --- a/.github/workflows/candidate-third-order.yml +++ b/.github/workflows/candidate-third-order.yml @@ -57,9 +57,32 @@ jobs: 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']: - if not same(pathlib.Path(entry['path']).read_bytes(), entry): - raise ValueError('merged source drifted: ' + entry['path']) + 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 @@ -84,10 +107,14 @@ jobs: return base64.b64decode(blob['content']) for kind in ('consumed_unmerged', 'cited_unmerged'): for entry in manifest.get(kind, []): - tree_path = pathlib.Path(entry['path']) - if kind == 'consumed_unmerged' and tree_path.exists(): - data, where = tree_path.read_bytes(), 'tree' + # 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)