diff --git a/.github/workflows/elder-cusp-parity.yml b/.github/workflows/elder-cusp-parity.yml new file mode 100644 index 000000000..16b1c8be4 --- /dev/null +++ b/.github/workflows/elder-cusp-parity.yml @@ -0,0 +1,159 @@ +name: Elder cusp kernel parity exact controls + +'on': + pull_request: + paths: + - 'frontiers/elder_cusp_parity_20261002/**' + - '.github/workflows/elder-cusp-parity.yml' + # bound merged sources (consumed and cited in SOURCES.json); the cited unmerged sources are bound through the API + - '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_total_bounded_20260929/PROOF.md' + - 'frontiers/remainder_vanishing_20260930/PROOF.md' + - 'frontiers/remainder_rate_20260930/PROOF.md' + - 'frontiers/cusp_second_order_20261001/PROOF.md' + - 'frontiers/candidate_third_order_20261001/PROOF.md' + - 'frontiers/elder_third_order_20261001/PROOF.md' + - 'frontiers/third_order_rate_20261001/PROOF.md' + - 'frontiers/c2_finite_jet_transfer_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/elder_cusp_parity_20261002').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 / 'ecp_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', 'M99'], capture_output=True, timeout=600).returncode + if rc != 2: + raise RuntimeError('unknown mutant label not rejected with exit 2') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/frontiers/elder_cusp_parity_20261002/PROOF.md b/frontiers/elder_cusp_parity_20261002/PROOF.md new file mode 100644 index 000000000..16a1db065 --- /dev/null +++ b/frontiers/elder_cusp_parity_20261002/PROOF.md @@ -0,0 +1,592 @@ +# The elder cusp kernel: the candidate rate, and no linear term at fixed `κ` + +Object: CL-ELDER-CUSP-PARITY-20261002-v1. +Author: Anthropic Claude (claude.ai session `session_01NMeKEismAyeqgdB4sy2NJU`), 2 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.** At the cusp scale `k = κr`, the elder kernel `r^{−2}A_r^{eld}(b, κr, u)` tends to the elder cusp kernel +`𝒜^{eld}(b, κ, u)`. Math- #229 (merged) proves this with error `C(r(1 + κ) + κ²r^{3/2} + κ³r²)` (its Lemma CE⁺), while the +candidate kernel has error `Cr(1 + κ)` (Lemma C⁺ there). The two extra terms come from two bad events of Math- #220's +Lemma Q, which decides the elder mark from the window field. Math- #237 (open) proves that the candidate cusp kernel has +no `O(r)` term after the birth height is integrated out; its Remark 3 records that the elder kernel has none *formally*, +without a proof. This note proves the following. +- **Lemma Q′** (§1): Lemma Q with relaxed margins. `Γ = |γ|/λ` is replaced by `Γ̃ = |A^{−1}γ|`, the ridge maximizer is + located in a ball of radius `ϱ = max(1, 8ḡ/λ)` instead of `1`, and every `φ` is decided, not only `|φ| ≤ 1`. +- **Proposition CE⁺⁺** (§2): the elder cusp kernel with the candidate's error `Cr(1 + κ)`. On the typed window, Lemma Q′ + needs only `λ ≳ 𝒩r(1 + |γ| + ‖B‖)(1 + |f₄|/κ)`. This removes #229's two elder-only ledger rows. The exponent `3/7` of + #229 does not change (Remark 2). +- **Theorem N** (§§3–5): for `κ` in a fixed compact subset of `(0, ∞)`, the elder and candidate cusp kernels have no + `O(r)` term, pointwise in the birth height `b`: the error is `O(r²)`. The proof computes the `O(r)` term. The edges of + the elder window and the typed weight both move at first order by multiples of one jet polynomial, + + Q₁ := f₅/120 − ηᵀA^{−1}γ/12 + γᵀA^{−1}BA^{−1}γ/8, + + the coefficient of the ridge correction `rQ₁X(X² − ¼)²`. The edges `|φ| = 1/3` move to `|φ| = 1/3 + rQ₁/(2κ)`, and the + weight changes by `12κrΔ²Q₁`. `Q₁` is odd under the point reflection of the jets, and every zeroth-order quantity is + even, so the parity factorization (#220 (F7)) makes the `O(r)` term `O(rk)`. +- **Corollary N′** (§6): in every fixed cusp window `κ₀ ≤ ℓ/r⁴ ≤ κ₁`, the elder, candidate and rejected densities are a + constant times `ℓ^{1/4}` plus `O(ℓ^{3/4})`. There is no term of order `ℓ^{1/2}`. + +An elder analogue of #237's Theorem P, the whole elder density with a remainder beyond `ℓ^{1/2}`, needs the two ends +`κ → ∞` and `κ → 0`, where Theorem N is not uniform. Remark 1 says where the argument stops. + +**Dependencies (consumed; all merged).** +- Math- #220 (`frontiers/elder_third_order_20261001/PROOF.md`, blob `c8767dde`; merged at `0d79778`): §0; §1 (the setting, + `𝔓`, Lemma CU.1′ (1.1) and its proof, Lemma S (1.2), Lemma Q and its proof, (M1)–(M6)); §2 (notation, (F1)–(F7), + (2.1)–(2.2), Lemma G, Lemma CE and its proof, Steps E1–E6). +- Math- #229 (`frontiers/third_order_rate_20261001/PROOF.md`, blob `110ed33a`; merged at `6f74f7a`): Lemma L (L.1); Lemma CE⁺ + (CE⁺.1) and its proof (Step E2⁺ with (3.1)–(3.2), Step E3⁺); §5 (the ledger, for Remarks 1–2). +- Math- #218 (`frontiers/candidate_third_order_20261001/PROOF.md`, blob `70ca57ef`; merged at `fb6ee97`): Lemma D (1.1) and + (1.2); Step F1, (2.1)–(2.2); Lemma C, Step C1 (its three cases) and Step C3. +- Math- #232 (`frontiers/c2_finite_jet_transfer_20261001/PROOF.md`, blob `54cc4a1a`; merged at `7fe06b0`): §2, (2.1)–(2.4). +- Math- #207 (`frontiers/cusp_second_order_20261001/PROOF.md`, blob `f6df5a73`; merged at `566b1a1`): §0 (the cusp objects + and the cusp polynomial (0.2)); Theorem CU.2 and Proposition CU.3, through #220; §4 (4.1). + +**Merged inputs.** [R] (R2)–(R5); [P] §2 (finite-jet rank) and §15 (parity factorization), through #218 and #220; +Math- #191 (`441152df`: Lemma E Step 3, the exchange `det H_M(−r) = det H_S(r)`). +**Cited only.** Math- #237 (open: Lemma Π, the expansion of Lemma Ω (a) here; Lemma K; its cusp-scale statement after +Lemma U; Remarks 3–4), Math- #238 (open: Lemma W, the `d = 1` form of Lemma Q″), Math- #216 (open: the Monte Carlo of the +lifetime densities), Math- #198 (through #220). + +## 0. Statement + +Setting and notation are those of #220 §§0–2 and #229 §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)`, the elder mark `e`, and 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`; so `r^{−2}A_r^{eld} = 12π_r(v_r)E_Q[ω_re]` + with the *weight* `ω_r := r^{−2}F_d(K_M)F_{d−1}(K_S)`; +- the free jets `J′ ⊃ J″ ⊃ J‴` of `f = F_r` at `0` (order `≤ 9`; `J″ = J′ ∖ {f₄}`, `J‴ = J″ ∖ {A}`), `𝒩 = 𝒩_r = 1 + k + ‖F_r‖_{C⁹}`, + and the contact law at `v_0(b, k)`, with expectation `E_{v_0(b,k)}`; +- jets at `0`: `A = D_Θ²f`, `B = ∂_uA`, `C = ∂_u²A`, `γ = ∇_Θ∂_u²f`, `η = ∇_Θ∂_u³f`, `f₄ = ∂_u⁴f`, `f₅ = ∂_u⁵f`; `Δ = det A`, + `J = adj A`, `Δ_B = tr(JB)`, `Δ_C = tr(JC)`, `Δ_BB = D²det(A)[B, B]`, `J_B = D adj(A)[B]`; `λ = λ_min(−A)` on `{A < 0}`; +- `Y′ = (f₄/12)Δ − γᵀJγ/4`, `Y_r = Y′ + 3kΔ_B`, `φ_r = (f₄ − 3γᵀA^{−1}γ)/(72κ) = Y′/(6κΔ)`, + `w_κ(A, Y) = (36κ²Δ² − Y²)₊1{A < 0}` and `w_κ^{eld}(A, Y) = w_κ(A, Y)1{|Y| < 2κ|Δ|}`; +- the cusp kernels `𝒜^{cand}`, `𝒜^{eld}` and `𝒜^{con}` (#220 §0, #218 §0). + +New notation, on `{A < 0}`: + + Γ̃ := |A^{−1}γ|, q := γᵀA^{−1}γ, z := f₄ − 3q = 72κφ_r, + Q₁ := f₅/120 − ηᵀA^{−1}γ/12 + γᵀA^{−1}BA^{−1}γ/8, P₁ := (Δ²/120)f₅ − (Δ/12)γᵀJη + (1/8)γᵀJBJγ = Δ²Q₁. (0.1) + +`P₁` is a polynomial in the jets, defined for every `A`. The *parity map* `𝒫` negates the jets of odd order (`γ`, `B`, `f₅`, +…) and fixes those of even order (`A`, `C`, `η`, `f₄`, …), as in #237 §0. `Δ`, `q`, `z`, `Y′` and `Γ̃` are `𝒫`-invariant; +`Q₁` and `P₁` change sign. Finally `w₀ := 36κ²Δ² − Y′² = (Δ²/144)(5184κ² − z²)`. + +**Lemma Q′ (the elder decision with relaxed margins).** Deterministic; stated in §1. + +**Proposition CE⁺⁺ (the elder cusp kernel with the candidate rate).** There are `r₂′ > 0` and `C, c, N` such that for +`0 < r ≤ r₂′`, `b ∈ R`, `u ∈ S^{d−1}` and `κ > 0` with `κr ≤ 1`, + + |r^{−2}(A_r^{eld} − A_0)(b, κr, u) − (𝒜^{eld} − 𝒜^{con})(b, κ, u)| ≤ C r (1 + κ) (1 + |b|)^N e^{−cb²}. (CE⁺⁺.1) + +**Theorem N (no linear term at fixed `κ`).** Let `K ⊂ (0, ∞)` be compact. There are `r_K > 0` and `C, c, N` such that for +`0 < r ≤ r_K`, `κ ∈ K`, `b ∈ R` and `u ∈ S^{d−1}`, + + |r^{−2}(A_r^{eld} − A_0)(b, κr, u) − (𝒜^{eld} − 𝒜^{con})(b, κ, u)| ≤ C r² (1 + |b|)^N e^{−cb²}, (N.1) + |r^{−2}(A_r − A_0)(b, κr, u) − (𝒜^{cand} − 𝒜^{con})(b, κ, u)| ≤ C r² (1 + |b|)^N e^{−cb²}. (N.2) + +The proof identifies the `O(r)` term (§5, Steps N4–N5): it is `12π_0(v_0(b, k))·r·E_{v_0(b,k)}[Q₁Ψ_κ]`, where `Ψ_κ`, the +`𝒫`-invariant functional (5.3), collects the edge densities and the first-order weight; it is `O(rk)` by parity. + +**Corollary N′ (cusp windows).** Let `0 < κ₀ < κ₁ < ∞` and `* ∈ {eld, cand, rej}`, with `A_r^{rej} := A_r − A_r^{eld}` and +`𝒜^{rej} := 𝒜^{cand} − 𝒜^{eld}`. As `ℓ ↓ 0`, + + ∫_{(ℓ/κ₁)^{1/4}}^{(ℓ/κ₀)^{1/4}}∫_R∫_{S^{d−1}} r^{−2}A_r^*(b, ℓ/r³, u) dσ(u) db dr + = ℓ^{1/4} ∫_{κ₁^{−1/4}}^{κ₀^{−1/4}}∫_R∫_{S^{d−1}} 𝒜^*(b, s^{−4}, u) dσ(u) db ds + O(ℓ^{3/4}). (N′.1) + +So the part of each density from the separations with `ℓ/r⁴ ∈ [κ₀, κ₁]` has no term of order `ℓ^{1/2}`. + +**What is not claimed.** +- Nothing about the whole elder or rejected density beyond #229: (E3⁺.0)–(E3⁺.1) with remainder `O(ℓ^{3/7})` stand. + Theorem N is not uniform as `κ → ∞` or `κ → 0`, and Corollary N′ excludes both ends (Remark 1). +- The constants of Theorem N depend on `K`. No uniformity in `d` or `L`. +- No certified numerical value. The numerics of Remarks 3–4 are exploration. +- Nothing beyond the existential scope of [R], [P], #191, #207, #218, #220, #229 and #232. + +## 1. The elder decision with relaxed margins + +The setting is #220 §1: `f ∈ C⁵(X)`, `𝒩 ≥ max(1, ‖f‖_{C⁵})`, `0 < r ≤ r_Q`, `κ > 0`, and `M = −ru/2`, `S = ru/2` critical +points with `f(M) = b` and `f(S) = b − κr⁴`; `Φ(X, Ξ) = rXu + r²ΘΞ`, `𝔉 = r^{−4}(f∘Φ − b)`, the cusp polynomial +`𝔓(X, Ξ) = 2κ(X + ½)²(X − 1) + (f₄/24)(X² − ¼)² + ½(X² − ¼)γ·Ξ + ½ΞᵀAΞ`, and for `A < 0`, `Ξ*(X) = −½(X² − ¼)A^{−1}γ` and +`g(X) = 𝔓(X, Ξ*(X)) = κ[2(X + ½)²(X − 1) + 3φ(X² − ¼)²]` with `φ = (f₄ − 3γᵀA^{−1}γ)/(72κ)`. `C₁ = C₁(d)` is the constant of +#220 (1.1). + +**Lemma Q′.** Suppose `A ≤ −λI` with `λ > 0`, and put + + Γ̃ := |A^{−1}γ|, M̃ := (35/8)Γ̃, ε̃ := 220 C₁𝒩r(1 + Γ̃)², R′ := 5M̃ + 4 + 3((κ + 1)/λ)^{1/2}. + +Assume +- (Q′1) `𝒩(3r + r²R′) ≤ λ/2` and `6r + 2r²R′ ≤ L/4`; +- (Q′2) `2C₁𝒩r ≤ λ` and `5r(1 + M̃) ≤ 1`; +- (Q′3) `ε̃ ≤ κ/4`; +- (Q′4) `||φ| − 1/3| > 2ε̃/(3κ)`. + +Then + + e(f) = 1{d_f(M) = f(S)} = 1{|φ| < 1/3}. (1.1′) + +Moreover, under (Q′1)–(Q′2) alone: for each `X ∈ [−3, 2]`, `𝔉(X, ·)` has a unique maximizer `Ξ_𝔉(X)` over `{|Ξ| ≤ R′}`, with + + |Ξ_𝔉(X) − Ξ*(X)| ≤ 2C₁𝒩r(1 + M̃)/λ ≤ 1 + M̃; (1.2′) + +the ridge `g_𝔉(X) := 𝔉(X, Ξ_𝔉(X))` is `C²` with `g_𝔉(−½) = 0`, `g_𝔉(½) = −κ` and `g_𝔉′(±½) = 0`; and `h := g_𝔉 − g` satisfies + + ε₀ := sup|h|, ε₁ := sup|h′|, ε₂ := sup|h″| ≤ ε̃ on [−3, 2], |h(X)| ≤ (ε₂/2)(X ∓ ½)². (1.3′) + +*Proof.* Follow #220's proof of Lemma Q. Steps Q2 and Q6 change, and `R′` replaces `R`. +- *Step Q1* is unchanged with `R′`: by (Q′1), `Φ` embeds a neighbourhood of `𝒲′ := [−3, 2] × {|Ξ| ≤ R′}`, and + `∂_Ξ²𝔉 ≤ −(λ/2)I` on `𝒲′`. +- *Step Q2′ (the ridge).* Fix `X ∈ [−3, 2]`; then `|Ξ*(X)| ≤ ½(35/4)Γ̃ = M̃`. Put `ḡ := C₁𝒩r(1 + M̃)` and + `ϱ := max(1, 8ḡ/λ)`; by (Q′2), `ϱ ≤ 4(1 + M̃)`. The ball `{|Ξ − Ξ*| ≤ ϱ}` lies in `{|Ξ| ≤ 5M̃ + 4} ⊂ 𝒲′`, and there + `r|Ξ| ≤ 1` by (Q′2), so #220 (1.1) applies. + - *The maximizer.* `∂_Ξ𝔓(X, Ξ*) = 0`, so `|∂_Ξ𝔉(X, Ξ*)| ≤ ḡ` by (1.1). On the sphere `|Ξ − Ξ*| = ϱ`, strong concavity + gives `𝔉(X, Ξ) ≤ 𝔉(X, Ξ*) + ḡϱ − (λ/4)ϱ² < 𝔉(X, Ξ*)`. So the maximizer over `{|Ξ| ≤ R′}` is unique and lies in the + open ball, where `∂_Ξ𝔉 = 0`; strong concavity gives `|Ξ_𝔉 − Ξ*| ≤ 2ḡ/λ`, and `2ḡ/λ ≤ 1 + M̃` by (Q′2). This is (1.2′). + `g_𝔉` is `C²`, and `g_𝔉″` is the Schur complement of `∂_Ξ²𝔉` in `Hess 𝔉` at `(X, Ξ_𝔉)`, as in #220. + - *The vector `γ`.* Let `D̄ := ∫_0^1∂_Ξ²𝔉(X, Ξ* + t(Ξ_𝔉 − Ξ*)) dt`. Then `Ξ_𝔉 − Ξ* = −D̄^{−1}∂_Ξ𝔉(X, Ξ*)`, and + `‖D̄ − A‖ ≤ λ/2` (Step Q1), so `|D̄^{−1}γ| ≤ |A^{−1}γ| + ‖D̄^{−1}‖‖D̄ − A‖|A^{−1}γ| ≤ 2Γ̃`. Hence + + |γ·(Ξ_𝔉 − Ξ*)| ≤ 2Γ̃ḡ. (1.4′) + + #220 bounds the same quantity by `|γ||Ξ_𝔉 − Ξ*|`. Replacing `Γ` by `Γ̃` here, and below, is what relaxes the margins. + - *`C⁰` and `C¹`.* As in #220, `ε₀ ≤ C₁𝒩r(1 + |Ξ_𝔉|)² ≤ 4C₁𝒩r(1 + M̃)²`. Since `g_𝔉′(X) = ∂_X𝔉(X, Ξ_𝔉)` (the envelope + identity), `g′(X) = ∂_X𝔓(X, Ξ*)` and `∂_X𝔓` depends on `Ξ` only through `Xγ·Ξ`, (1.1) and (1.4′) give + `ε₁ ≤ 4C₁𝒩r(1 + M̃)² + 6Γ̃ḡ`. + - *`C²`.* Take `(a, b, D) = (∂_X²𝔓, Xγ, A)` at `(X, Ξ*)` and the blocks `(a′, b′, D′)` of `Hess 𝔉` at `(X, Ξ_𝔉)`. + `∂_X²𝔓` depends on `Ξ` only through `γ·Ξ`, so `|a′ − a| ≤ 2ḡ + 2Γ̃ḡ` by (1.1) and (1.4′). Also `|b′ − b| ≤ β̄ := 2ḡ` and + `‖D′ − D‖ ≤ C₁𝒩r ≤ λ/2`. With `|D^{−1}b| = |X|Γ̃ ≤ 3Γ̃`, `|D′^{−1}b| ≤ 6Γ̃` and `|D′^{−1}b′| ≤ 6Γ̃ + 2β̄/λ`, the identity + `b′ᵀD′^{−1}b′ − bᵀD^{−1}b = (b′ − b)ᵀD′^{−1}(b′ + b) + bᵀD′^{−1}(D − D′)D^{−1}b` gives + `ε₂ ≤ |a′ − a| + β̄(12Γ̃ + 2β̄/λ) + 18C₁𝒩rΓ̃²`, and `2β̄²/λ ≤ 2β̄(1 + M̃)` by (Q′2). + - *Collecting.* With `M̃ = (35/8)Γ̃`: `ε₀/(C₁𝒩r) ≤ 4 + 35Γ̃ + (1225/16)Γ̃²`, `ε₁/(C₁𝒩r) ≤ 4 + 41Γ̃ + (1645/16)Γ̃²` and + `ε₂/(C₁𝒩r) ≤ 6 + (279/4)Γ̃ + (3333/16)Γ̃²`. Each is at most `220(1 + Γ̃)²` coefficientwise (control X1). +- *Step Q3* is unchanged: on `|Ξ| = R′`, `|Ξ − Ξ_𝔉| ≥ R′ − (2M̃ + 1) ≥ 3((κ + 1)/λ)^{1/2}`, so #220 (1.4) holds: + `𝔉(X, Ξ) ≤ g_𝔉(X) − (9/4)(κ + 1)`. *Steps Q4–Q5* are unchanged. Step Q4 gives the pin values and the last bound in (1.3′). +- *Step Q6′ (the decision).* By (Q′3)–(Q′4), `ε₂ ≤ ε̃ ≤ κ/4` and `ε₀ ≤ ε̃ < (3/2)κ||φ| − 1/3|`. Cases E (`|φ| < 1/3`), R⁺ for + `1/3 < φ ≤ 1` and R⁻ for `−1 ≤ φ < −1/3` are #220's, word for word. Two cases are new. + - *Case R⁺, `φ > 1`.* On `[−3, −½]`, `1 + 2φX ≤ 1 − φ < 0`, so `g′ = 6κ(X² − ¼)(1 + 2φX) ≤ 0` (M6). Hence + `min_{[−3,−½]}g = g(−½) = 0` and `g_𝔉 ≥ −ε₀ > −κ` there, while `g_𝔉(−3) ≥ g(−3) − ε₀ > 0`, as + `g(−3) = κ(−50 + (3675/16)φ) > 179κ` (M5). The ridge curve from `M` to `X = −3` stays above `f(S)` and ends above `b`. + So `d_f(M) > f(S)` and `e = 0`. + - *Case R⁻, `φ < −1`.* By (M1), `g + κ = κ(X − ½)²[2(X + 1) + 3φ(X + ½)²]`. On `[½, 2]` the bracket is at most + `−(3X² + X − 5/4)`, which vanishes at `X = ½` and decreases for `X > −1/6`. So `g ≤ −κ` and `g_𝔉 < 0` on `[½, 2]`; on + `[−3/2, ½]`, (M3) and (1.3′) give `g_𝔉 ≤ 0`. On the boundary of `𝒟′ = (−3/2, 2) × {|Ξ| < R′}`: + `g_𝔉(−3/2) ≤ κ(−5 + 12φ) + ε₀ < −(5/4)κ` and `g_𝔉(2) ≤ κ(25/2 + (675/16)φ) + ε₀ < −(5/4)κ` (M5); and `𝔉 ≤ −(9/4)(κ + 1)` + at `|Ξ| = R′`. #220's trap argument of Case R⁻, with `t* = −(5/4)κ`, gives `e = 0`. ∎ + +So Lemma Q′ needs neither #220's condition `8C₁𝒩r(1 + 5Γ) ≤ λ` nor `|φ| ≤ 1`. The first is the source of the term +`(𝒩r|γ|)^{1/2}` in #220's margin `λ₂`, and so of `κ²r^{3/2}` in #229 (CE⁺.1); the second is the source of `𝔅_5 = {|φ_r| > 1}`, +and so of `κ³r²`. + +## 2. The elder cusp kernel with the candidate rate + +*Proof of Proposition CE⁺⁺.* Take `r₂′ ≤ r₂ = min(r_0^*, 1/2, r_Q)` (#220 Lemma CE). For `κ ≤ 1`, #229 (CE⁺.1) already gives +(CE⁺⁺.1), since `κ²r^{3/2} + κ³r² ≤ 2r` when `κ, r ≤ 1`. +Let `κ ≥ 1`. Follow #229's proof of Lemma CE⁺, that is, #220's proof of Lemma CE with Steps E2⁺ and E3⁺, with Lemma Q′ in +place of Lemma Q in Step E1. Then #220 (2.3) holds with `𝔅′`, the event that (Q′1)–(Q′4) fail for `f = F_r` and +`𝒩 = 𝒩_r`, in place of `𝔅`. Steps E3⁺–E6 are unchanged and cost `CκrP^N + Cκ²r²P^N + Cr²(1 + κ)²P^N + Ck²(1 + |b|)^N`, +which is `≤ Cr(1 + κ)P^N` for `κr ≤ 1` (#229, control R6). It remains to show + + E_Q[w_κ(A, Y_r)1_{𝔅′}] ≤ C κ r P^N (κ ≥ 1, κr ≤ 1). (2.1) + +- *The typed window controls `Γ̃`.* On `{w_κ(A, Y_r) > 0}`, `A < 0` and `|Y_r| < 6κ|Δ|`. Since `Y_r = 6κΔφ_r + 3kΔ_B` and + `|Δ_B|/|Δ| = |tr(A^{−1}B)| ≤ m‖B‖/λ`, `|φ_r| < 1 + rm‖B‖/(2λ)`. Also `|q| ≥ λΓ̃²` (as `−A ≥ λI`) and + `3|q| ≤ |f₄| + 72κ|φ_r|`. Hence + + Γ̃² ≤ (|f₄| + 72κ)/(3λ) + 12κrm‖B‖/λ² on {w_κ(A, Y_r) > 0}. (2.2) + +- *The conditions.* `r ≤ r₂′ ≤ r_Q` and `𝒩 ≥ 1`. Bound `Γ̃ ≤ |γ|/λ` in (Q′1)–(Q′2), and use (2.2) in (Q′3). As in #220's + Step E2, (Q′1)–(Q′3) hold on `{w_κ(A, Y_r) > 0}` as soon as `κ ≥ C₂′𝒩r` and + + λ ≥ λ₂′ := C₂′ 𝒩 r (1 + |γ| + ‖B‖)(1 + |f₄|/κ), C₂′ = C₂′(d, L). (2.3) + + In detail: (Q′1) holds if `λ ≥ 18𝒩r`, `λ ≥ 48𝒩r²`, `λ² ≥ (525/2)𝒩r²|γ|` and `λ ≥ 18^{2/3}2^{1/3}𝒩r` (the last from + `r(κ + 1) ≤ 2`, as in #220), together with `λ ≥ (700/L)r²|γ|` and `λ ≥ (96/L)²r⁴(κ + 1)`; (Q′2) holds if `λ ≥ 2C₁𝒩r` + and `λ ≥ (175/4)r|γ|` (with `r ≤ 1/10`); and by (2.2), (Q′3) holds if `κ ≥ 3520C₁𝒩r`, `λ ≥ 2347C₁𝒩r(|f₄| + 72κ)/κ` and + `λ² ≥ 84480mC₁𝒩r²‖B‖`. Each is implied by (2.3) for a suitable `C₂′`, using `(𝒩x)^{1/2} ≤ 𝒩(1 + x)` and `r ≤ 1` (control X1 + records the constants). So + + 𝔅′ ∩ {w_κ > 0} ⊂ 𝔅_λ′ ∪ 𝔅_κ′ ∪ 𝔅_4′, 𝔅_λ′ := {λ < λ₂′}, 𝔅_κ′ := {κ < C₂′𝒩r}, + 𝔅_4′ := {||φ_r| − 1/3| ≤ 2ε̃/(3κ)} ∖ (𝔅_λ′ ∪ 𝔅_κ′) (as in #229). + +- *`𝔅_4′`.* This is #229's (3.1) with `ε̃` in place of `ε*`. On `𝔅_4′ ∩ {w_κ > 0}`, (Q′3) holds, so `1/6 ≤ |φ_r| ≤ 1/2`, and `|f₄| ≥ 6κ` or + `λ ≤ |γ|²/(2κ)` (#229 (3.2)); `𝔅_4′` puts `f₄` in two `J″`-measurable intervals (after #220's `𝒩`-layers) of total length + `192ε̃`; and `Δ²(1 + Γ̃)² ≤ 2Δ² + 2|Jγ|²` is a polynomial in `J″`. #229's two pieces give `CκrP^N`. +- *`𝔅_κ′`.* `Cr³P^N`, as #220's `𝔅_κ`. +- *`𝔅_λ′`.* Put `t₁ := 2C₂′𝒩r(1 + |γ| + ‖B‖)`, so that `λ₂′ ≤ t₁max(1, |f₄|/κ)`, and use #220's `𝒩`-layers. + - On `{λ < t₁}`, integrate `f₄` over the typed interval (length `144κ`), bound `Δ² ≤ t₁²‖A‖^{2m−2}`, and apply #220 (2.2) + given `J‴`: the contribution is `≤ Cκ²E[t₁³(P + |J‴|)^N] ≤ Cκ²r³P^N ≤ CκrP^N`. + - On `{t₁ ≤ λ < t₁|f₄|/κ}`, `w_κ ≤ 36κ²λ²‖A‖^{2m−2}` and `1 ≤ (t₁|f₄|/(κλ))^{5/2}`. So the contribution is at most + `36κ^{−1/2}E[t₁^{5/2}|f₄|^{5/2}λ^{−1/2}‖A‖^{2m−2}] ≤ Cκ^{−1/2}r^{5/2}P^N`: by Hölder's inequality it suffices that + `E[λ^{−3/4} | J‴] ≤ C(P + |J‴|)^n`, which is #218 Lemma D (1.1) in dyadic layers of `λ`. For `κ ≥ 1` this is `≤ CrP^N`. + +This proves (2.1), hence (CE⁺⁺.1). ∎ + +## 3. The ridge and the decision to second order + +The first-order part of the window field is the polynomial + + 𝔔(X, Ξ) := (f₅/120)X(X² − ¼)² + (1/6)X(X² − ¼)η·Ξ + ½XΞᵀBΞ. (3.0) + +For #232's exact pinned family (2.4), in the window coordinates `x = rX`, `y = r²Ξ`, `r^{−4}(f − b) = 𝔓 + r𝔔 + (r²/4)X²ΞᵀCΞ` +(control X3). + +**Lemma CU.1″ (second-order weighted Taylor bounds).** In the setting of §1 with `𝒩 ≥ max(1, ‖f‖_{C⁶})`, there is +`C₈ = C₈(d)` such that on `{|X| ≤ 3, r|Ξ| ≤ 1}` + + |𝔉 − 𝔓 − r𝔔| ≤ C₈𝒩r²(1 + |Ξ|)³, |∂_Ξ(𝔉 − 𝔓 − r𝔔)| ≤ C₈𝒩r²(1 + |Ξ|)². (3.1) + +*Proof.* This is #220's proof of Lemma CU.1′, one order further, with the same three sources. +- *Pin corrections.* With `𝒩 ≥ ‖f‖_{C⁶}`, the pinned jets differ from the values that produce `𝔓 + r𝔔` by `O(𝒩r⁵)` (`∂_uf`), + `O(𝒩r⁴)` (`∂_u²f`, `∇_Θf`) and `O(𝒩r³)` (`∂_u³f`, `∇_Θ∂_uf`); `f(0)` cancels against `b = f(M)`. After rescaling they + contribute `O(𝒩r²)(1 + |Ξ|)`. +- *Dropped monomials.* These are `x^iy^j` with `i + 2|j| ≥ 6` and `i + |j| ≤ 5`, with coefficients bounded by `C𝒩`. Each + becomes `r^aX^iΞ^j` with `a = i + 2|j| − 4 ≥ 2` and `|j| ≤ a + 1`. On `r|Ξ| ≤ 1`, `r^a|Ξ|^{|j|} ≤ r²|Ξ|^{|j|−a+2}`, and + `|j| − a + 2 ≤ 3`. +- *Remainder.* `|∂^αρ₆(x, y)| ≤ C𝒩(|x| + |y|)^{6−|α|}`; at `(rX, r²Ξ)`, `|x| + |y| ≤ 4r`, so `q` derivatives in `Ξ` give + `C𝒩r^{2+q}`. + +A derivative in `Ξ` lowers the power of `|Ξ|` by one. Control X3 checks on pinned polynomial fields in `d = 2, 3` that every +monomial `r^aX^iΞ^j` of `𝔉 − 𝔓 − r𝔔` has `a ≥ 2` and `|j| ≤ a + 1`. ∎ + +**Lemma R₂ (the ridge to second order).** Assume (Q′1)–(Q′2) and `𝒩 ≥ max(1, ‖f‖_{C⁶})`. For `X ∈ [−3, 2]`, + + |h(X) − rQ₁X(X² − ¼)²| ≤ ε₂′ := C₉[𝒩r²(1 + Γ̃)³ + 𝒩²r²(1 + Γ̃)²/λ], C₉ = C₉(d). (3.2) + +*Proof.* Write `𝔉 = 𝔓 + r𝔔 + ℜ`. By substitution, `𝔔(X, Ξ*(X)) = Q₁X(X² − ¼)²` (control X4). +- *Lower bound.* `g_𝔉(X) ≥ 𝔉(X, Ξ*) = g + rQ₁X(X² − ¼)² + ℜ(X, Ξ*)`. +- *Upper bound.* With `v := Ξ_𝔉 − Ξ*`, `𝔓(X, Ξ_𝔉) = g + ½vᵀAv ≤ g − (λ/2)|v|²`. `𝔔` is quadratic in `Ξ` with `∂_Ξ²𝔔 = XB`, so + `r𝔔(X, Ξ_𝔉) ≤ r𝔔(X, Ξ*) + r|∂_Ξ𝔔(X, Ξ*)||v| + (3r/2)‖B‖|v|²`, and `(3r/2)‖B‖ ≤ (3/2)𝒩r ≤ λ/4` by (Q′1). Hence + + g_𝔉 − g − rQ₁X(X² − ¼)² ≤ |ℜ(X, Ξ_𝔉)| + r|∂_Ξ𝔔||v| − (λ/4)|v|² ≤ |ℜ(X, Ξ_𝔉)| + r²|∂_Ξ𝔔(X, Ξ*)|²/λ. + +Here `|∂_Ξ𝔔(X, Ξ*)| = |(1/6)X(X² − ¼)η + XBΞ*| ≤ C𝒩(1 + Γ̃)`; and by (3.1) and (1.2′), `|ℜ| ≤ C₈𝒩r²(2 + 2M̃)³` at `Ξ*` and at +`Ξ_𝔉`, where `r|Ξ| ≤ 1`. ∎ + +**The model near the edges** (control X2). Put `δ_e := 1/96`, `J_± := {φ : |φ ∓ 1/3| ≤ δ_e}`, `X₃ := −1/(2φ)`, + + Ψ(φ) := (φ + 1)³(3φ − 1)/(16φ³) = (g(X₃) + κ)/κ, Ψ₋(φ) := (φ − 1)³(3φ + 1)/(16φ³) = g(X₃)/κ (3.3) + +(#220 (M4)), `c₃ := 281/128` and `c₄ := (c₃/2)(9/44)²`. For `φ ∈ J₊`: +- `X₃ ∈ [−48/31, −16/11] ⊂ (−3, −5/4)`, and `g″ ≥ c₃κ` on `[−3, −5/4]` (`g″/(6κ) = 6φX² + 2X − φ/2` is decreasing in `X` and + increasing in `φ` there, and equals `281/768` at `(φ, X) = (31/96, −5/4)`); +- `g′ ≥ 0` on `[X₃, −½]`, so `g ≥ g(−5/4) ≥ g(X₃) + c₄κ` on `[−5/4, −½]`; and `g(−3) ≥ 24κ`; +- `g ≤ −(κ/2)(X + ½)²` on `[X₃, ½]`; and (M2) holds on `[−½, 2]`, with `g(2) ≥ (125/64)κ`. + +For `φ ∈ J₋` the mirror statements hold on `[½, 2]`: `X₃ ∈ [16/11, 48/31]`, `g″ ≤ −c₃κ` on `[5/4, 2]`, `g′ ≥ 0` on `[½, X₃]`, +so `g ≤ g(5/4) ≤ g(X₃) − c₄κ` on `[½, 5/4]`; `g(2) ≤ −(112/100)κ`; `|g(X₃)| ≤ κ/7`; `g + κ ≥ (κ/2)(X − ½)²` on `[−½, X₃]`; and +(M3) holds on `[−3/2, ½]` with `g(−3/2) ≤ −7κ`. Finally, for `|t| ≤ δ_e`, + + Ψ(1/3 + t) = 12t + Ψ₂(t)t², Ψ₋(−1/3 + t) = 12t + Ψ₂⁻(t)t², X₃(X₃² − ¼)² = ∓6 + ω_±(t)t (φ = ±1/3 + t), (3.4) + +with `|Ψ₂|, |Ψ₂⁻| ≤ 90` and `|ω_±| ≤ 120`. (`Ψ(1/3 + t) = 12t − 81t² + …`, and on `J₊`, `X₃(X₃² − ¼)² = −6 + 99t + …`.) + +**Lemma Q″ (the decision near the edges).** Assume (Q′1)–(Q′2) and `ε̃ ≤ c_eκ` with `c_e := 1/200`. +- (a) If `φ ∈ J₊`: `e = 1` if `min_{[−3,−½]}g_𝔉 < −κ`, and `e = 0` if `min_{[−3,−½]}g_𝔉 > −κ`. Moreover + `min_{[−3,−½]}g_𝔉 = κΨ(φ) − κ + h(X₃) + θ` with `−ε₁²/(2c₃κ) ≤ θ ≤ 0`. +- (b) If `φ ∈ J₋`: `e = 1` if `max_{[½,2]}g_𝔉 > 0`, and `e = 0` if `max_{[½,2]}g_𝔉 < 0`. Moreover + `max_{[½,2]}g_𝔉 = κΨ₋(φ) + h(X₃) + θ` with `0 ≤ θ ≤ ε₁²/(2c₃κ)`. +- (c) If moreover (3.2) holds and `ζ := r|Q₁|/κ ≤ c_e`, then with `t := φ ∓ 1/3` on `J_±`, + + e = 1{±t < rQ₁/(2κ)} unless |t ∓ rQ₁/(2κ)| ≤ ϑ := C₁₀[ζ² + ε₂′/κ + ε̃²/κ²]. (3.5) + + In `z = 72κφ`: near both edges, `e = 1{|z| < 24κ + 36rQ₁}` unless `||z| − 24κ − 36rQ₁| ≤ 72κϑ`. + +*Proof.* (a) *Location of the minimum.* `ε₀ ≤ ε̃ < c₄κ/2`. `min_{[−3,−½]}g_𝔉 ≤ g_𝔉(X₃) ≤ g(X₃) + ε₀`, while +`g_𝔉 ≥ g − ε₀ > g(X₃) + ε₀` on `[−5/4, −½]` and at `X = −3`. So every minimizer `X̂` lies in `(−3, −5/4)`, where `g″ ≥ c₃κ` +and `g′(X₃) = 0`. There `g(X̂) ≥ g(X₃) + (c₃κ/2)(X̂ − X₃)²` and `h(X̂) ≥ h(X₃) − ε₁|X̂ − X₃|`, so +`g_𝔉(X̂) ≥ g(X₃) + h(X₃) − ε₁²/(2c₃κ)`; and `g_𝔉(X̂) ≤ g_𝔉(X₃) = g(X₃) + h(X₃)`. With (3.3) this is the formula for the minimum. + +*The decision.* Suppose `g_𝔉(X̂) < −κ`, and let `𝒟 := (X̂, ½) × {|Ξ| < R′}`. +- At `X = X̂`, `𝔉 ≤ g_𝔉(X̂) < −κ`. At `X = ½`, `𝔉 ≤ −κ`, with equality only at `S`. +- On `[X̂, ½]`, `g_𝔉 ≤ 0`. On `[X̂, −5/4]`, `g` is convex, so `g ≤ max(g(X̂), g(−5/4))`, with `g(X̂) < −κ + ε₀` and + `g(−5/4) ≤ −9κ/32`; so `g_𝔉 ≤ g + ε₀ < 0`. On `[−5/4, ½]`, `g ≤ −(κ/2)(X + ½)²` and `|h| ≤ (ε₂/2)(X + ½)²`. So, at + `|Ξ| = R′`, `𝔉 ≤ −(9/4)(κ + 1)` by #220 (1.4). + +As in #220's Case E, the path component of `{f > f(S)}` containing `M` lies in `Φ(𝒟)` and has supremum `≤ b`, so +`d_f(M) ≤ f(S)`; and #220's path of Case E (on `[−½, 2]`, by (M2), (1.3′) and `g(2) ≥ (125/64)κ`) gives `d_f(M) ≥ f(S)`. So +`e = 1`. If instead `g_𝔉 > −κ` on `[−3, −½]`, the ridge curve from `M` to `X = −3` stays above `f(S)` and ends above `b`, +since `g_𝔉(−3) ≥ 24κ − ε₀ > 0`; so `e = 0`. + +(b) The mirror argument on `[½, 2]`: maximizers `X̂` of `g_𝔉` lie in `(5/4, 2)`, and the formula is proved as in (a). +- If `g_𝔉(X̂) > 0`, the ridge curve from `M` through `S` to `X̂` stays at or above `f(S)`: on `[−½, X₃]`, + `g_𝔉 + κ ≥ ((κ − ε₂)/2)(X − ½)² ≥ 0`, and between `X₃` and `X̂`, `g ≥ min(g(X₃), g(X̂)) ≥ −κ/7 − ε₀` (concavity on + `[5/4, 2]`), so `g_𝔉 > −κ`. It ends above `b`, so `d_f(M) ≥ f(S)`; and (M3) with `g(−3/2) ≤ −7κ` gives #220's left trap, + so `d_f(M) ≤ f(S)` and `e = 1`. +- If `g_𝔉(X̂) < 0`, then `g_𝔉 ≤ 0` on `[−3/2, 2]`, `g_𝔉(2) ≤ −(112/100)κ + ε₀ < −(111/100)κ` and `g_𝔉(−3/2) < −(111/100)κ`. + #220's trap of Case R⁻, with `t* := −(111/100)κ`, gives `e = 0`. + +(c) Take `J₊`. By (a), (3.3), (3.4) and (3.2): `e = 1` if `12κt + κΨ₂t² + rQ₁(−6 + ω₊t) + h₂ + θ < 0`, and `e = 0` if the +left side is `> 0`. Here `h₂ := h(X₃) − rQ₁X₃(X₃² − ¼)²`, so `|h₂| ≤ ε₂′`, and `−ε₁²/(2c₃κ) ≤ θ ≤ 0`. So +`e ≠ 1{t < rQ₁/(2κ)}` only if + + |12κt − 6rQ₁| ≤ 90κt² + 120r|Q₁||t| + ε₂′ + ε₁²/(2c₃κ) =: E(t). + +On this event, `|t| ≤ δ_e` gives `90κt² ≤ κ|t|`, and `120r|Q₁| ≤ κ` as `ζ ≤ c_e`; so `10κ|t| ≤ 6r|Q₁| + ε₂′ + ε₁²/(2c₃κ)`, +that is `|t| ≤ C(ζ + ε₂′/κ + ε̃²/κ²)`. Substituting back, `12κ|t − rQ₁/(2κ)| ≤ E(t) ≤ Cκ(ζ² + ε₂′/κ + ε̃²/κ²)` when +`ε₂′ ≤ κ`; if `ε₂′ > κ`, then `ϑ ≥ C₁₀ ≥ 1 > |t ∓ rQ₁/(2κ)|` and (3.5) holds trivially. This is (3.5) on `J₊`. On `J₋` the same +computation with (b), `Ψ₋` and `ω₋` gives `e = 1{t > −rQ₁/(2κ)}` up to the same window. In `z`, `t = (z ∓ 24κ)/(72κ)`. ∎ + +Lemma Q″ (c) is the form for `d ≥ 2` of #238's Lemma W (W.2), where the window field is one-dimensional and the edges are +`±1/3 − η(∓3/2)/12` up to `O(ε²)`, `η` the perturbation of the field. Here the perturbation of the ridge is +`η = rQ₁X(X² − ¼)²`, and `−η(∓3/2)/(12κ) = ±rQ₁/(2κ)`. + +## 4. The weight inside the elder window + +**Lemma Ω.** (a) For `0 < r ≤ r_0^*` and `0 < k ≤ 1`, pathwise, + + det K_M = −6kΔ + rU − r²V + O(r³(1 + k)𝒩^N), det K_S = 6kΔ + rU + r²V + O(r³(1 + k)𝒩^N), + −det K_M det K_S = 36k²Δ² + r²(12kΔV − U²) + O(r⁴(1 + k)^N𝒩^N), (4.1) + +with `U := Y_r` and `V := (3k/4)(Δ_C + Δ_BB) + (f₄/24)Δ_B + (f₅/120)Δ − (1/12)γᵀJη − (1/8)γᵀJ_Bγ` (#232 (2.2)). + +(b) As polynomials in the jets, + + 36κ²Δ² + 12kΔV − U² = w₀ + 12kP₁ + 9k²[Δ(Δ_C + Δ_BB) − Δ_B²]. (4.2) + +(c) `P₁ = Δ²Q₁` on `{A invertible}`; `P₁` and `Q₁` are `𝒫`-odd; `w₀` is `𝒫`-invariant. + +*Proof.* (a) By #218 Step F1, applied to each factor and to the product, `det K_M`, `det K_S` and `−det K_M det K_S` equal +polynomials in `(J′; r, k)` up to `O(r³(1 + k)T^N)`, resp. `O(r⁴T^{n₀})` (#218 (2.1)). The coefficients are identities of +polynomials, which may be read off on exactly pinned polynomial fields. #232 (2.1)–(2.3) give the coefficients up to `r²`. +On pinned polynomial fields, `−det H(−r/2)det H(r/2)/r²` is even in `r`: the pinned jets that enter the Hessians are even in +`r` (#191 Lemma E Step 3: `det H_M(−r) = det H_S(r)`). So the product has no `r³` term. #220 replaces `T` by `𝒩_r` in +the same way, as in its own-jet form (F1). Control X3 checks the coefficients of `r⁰, …, r³` on pinned polynomial fields in +`d = 2, 3, 4`. #237 Lemma Π +states the same expansion. + +(b) Expand `U² = (Y′ + 3kΔ_B)²` and `V = V_o + (3k/4)(Δ_C + Δ_BB)`. The first-order part is `k(12ΔV_o − 6Y′Δ_B)`, and + + 12ΔV_o − 6Y′Δ_B = (Δ²/10)f₅ − ΔγᵀJη + (3/2)γᵀ(Δ_BJ − ΔJ_B)γ = 12P₁, + +because `ΔJ_B = Δ_BJ − JBJ`: for invertible `A`, `J = ΔA^{−1}` gives `J_B = Δ_BA^{−1} − ΔA^{−1}BA^{−1}`, and the identity of +polynomials extends to all `A` (control X4). + +(c) `J = ΔA^{−1}`; the parity of each monomial is read off its odd factors (control X4). ∎ + +So inside the elder window the weight is `w₀ + 12κrΔ²Q₁ + O(r² + k²)`. On `{A invertible}`, `V_o = ΔQ₁ + α₄Δ_B` with +`α₄ := z/24` (control X4), and `Y′ = 2Δα₄`: the first-order parts `12kΔV_o` of `12kΔV` and `−6kY′Δ_B` of `−U²` combine into +`12kΔ²Q₁`, a multiple of the same polynomial that moves the edges. + +## 5. Proof of Theorem N + +Fix `K = [κ₀, κ₁]`. Constants may depend on `K`, `d` and `L`. Take `r_K ≤ min(r_0^*, 1/2, r_Q, 1/κ₁)` small, write +`𝒩 = 𝒩_r`, and let `0 < r ≤ r_K`, `κ ∈ K` and `k = κr`. + +*Step N1 (the good event).* Let `𝔊` be the event that +- `A < 0` and `λ ≥ λ₃ := C₁₁𝒩r(1 + |γ| + ‖B‖)(1 + |f₄|)`; +- `𝒩 ≤ c₁₁/r` (so `|f₅| ≤ c₁₁/r`); +- `|Δ| ≥ C₁₂r𝒩^{N₂}(1 + ‖B‖)`, `N₂ := max(N₁, m − 1)` (`N₁` of #220 (F1)), + +with `C₁₁`, `C₁₂` large and `c₁₁` small. On `𝔊`: +- *Typing.* Case 1 of #218 Step C1 holds (`λ_max(A) < −r𝒩`, with `𝒩` in place of #218's `T` as in #220 (F2)), so the pair + is typed iff `s·det K_M < 0 < s·det K_S` (`s = (−1)^m`). By #220 (F1), `s·det K_M = −6k|Δ| + r·sY_r + O(r²𝒩^{N₁})` and `s·det K_S = 6k|Δ| + r·sY_r + O(r²𝒩^{N₁})`, with + `|Y_r| ≤ (|z|/12)|Δ| + 3κr|Δ_B|` and `|Δ_B| ≤ m𝒩^{m−1}‖B‖`. The margin on `|Δ|` gives: on `{|z| ≤ 30κ}` the pair is typed; + every typed pair has `|φ_r| < 1 + C/(κ₀C₁₂) < 3`; and no pair is anti-typed (`s·det K_M > 0 > s·det K_S`). +- *The margins.* On typed pairs, `|φ_r| < 3`, so `Γ̃² ≤ |q|/λ ≤ (|f₄| + 216κ)/(3λ)`. So (Q′1)–(Q′3) hold with `ε̃ ≤ c_eκ` + (as in §2), and `ζ = r|Q₁|/κ ≤ c_e`: `r‖B‖Γ̃² ≤ (1 + 216κ₁)/(3C₁₁)`, `r|η|Γ̃ ≤ ((1 + 216κ₁)c₁₁/(3C₁₁))^{1/2}` and + `r|f₅| ≤ r𝒩 ≤ c₁₁`. Lemma Q′ decides `e` off `J₊ ∪ J₋` (`2ε̃/(3κ) < δ_e`), Lemma R₂ holds (`‖f‖_{C⁶} ≤ 𝒩`), and Lemma Q″ + decides `e` on `J_±`; off `J_±`, `1{|φ_r| < 1/3} = 1{|z| < 24κ + 36rQ₁}`, since `r|Q₁|/(2κ) ≤ c_e/2 < δ_e`. +- *The weight.* On typed pairs, `ω_r = −r^{−2}det K_M det K_S = w₀ + 12kP₁ + ε_ω` with `|ε_ω| ≤ C(r² + k²)𝒩^N`, by (4.1)–(4.2). + Typed pairs with `|z| > 30κ` have `|φ_r| > 5/12`, so `e = 0`. + +Put + + G_r(J′) := (w₀ + 12kP₁)1{A < 0, |z| < 24κ + 36rQ₁, r|Q₁| ≤ c_eκ}. (5.1) + +Since `36r|Q₁| ≤ 36c_eκ < 6κ`, the window of `G_r` lies in `{|z| < 30κ}`. Hence, on `𝔊`, `ω_re = G_r(J′) + ε_ω1{|z| < 24κ + 36rQ₁}`, +except on the edge windows `{||z| − 24κ − 36rQ₁| ≤ 72κϑ}` of (3.5). + +*Step N2 (the exceptional events).* + + E_Q|ω_re − G_r(J′)| ≤ C r² P^N. (5.2) + +- *On `𝔊`.* `E|ε_ω| ≤ C(r² + k²)P^N`. For the edge windows, the integration in `f₄` needs an event that does not involve + `f₄`. Put `𝔊″ := {A < 0, λ ≥ C₁₁𝒩r(1 + |γ| + ‖B‖), 𝒩 ≤ c₁₁/r, Γ̃² ≤ (1 + 216κ₁)/(3C₁₁𝒩r)}`; by the margins of Step N1, + `𝔊 ∩ {typed} ⊂ 𝔊″`. + - On `𝔊″`, `ζ ≤ c_e` and `ε̃ ≤ c_eκ` as in Step N1, and `ε₂′/κ ≤ C(C₁₁^{−1} + r^{1/2})/κ₀`. So `ϑ ≤ ϑ̄`, a small constant, + and the edge windows are two `f₄`-intervals of length `144κϑ` within `(36c_e + 72ϑ̄)κ ≤ κ` of `3q ± 24κ`; after #220's + `𝒩`-layers they are `J″`-measurable. + - On `𝔊 ∩ {typed}`, `k|P₁| = κr|Q₁|Δ² ≤ c_eκ²Δ²`, so there `ω_r, |G_r| ≤ Cκ²Δ² + |ε_ω|`. The `|ε_ω|` part is bounded + without the window. For `Cκ²Δ²1_{𝔊″}` on the windows, integrate `f₄` given `J″`. The powers of `Γ̃` in `ϑ` are at most + four, besides `(1 + Γ̃)²/λ`. Use `Δ² ≤ λ²‖A‖^{2m−2}` and `Γ̃² ≤ |q|/λ`: `Δ²Γ̃⁴ ≤ ‖A‖^{2m−2}q²`, + `Δ²Γ̃³ ≤ λ^{1/2}‖A‖^{2m−2}|q|^{3/2}` and `Δ²Γ̃²/λ ≤ ‖A‖^{2m−2}|q|`. On the windows, `f₄ = 3q ± 24κ + O(κ)`, and the + Gaussian decay of the conditional density of `f₄` (#220 (F3)) gives `(1 + |q|)²sup_{windows}p_{f₄} ≤ C(1 + |m₄| + κ)²`. + The windows cost `Cr²P^N`. +- *`A ≮ 0`.* `G_r = 0`. By #218 Step C1 (Cases 2 and 3), `E_Q[ω_r1{λ_max(A) ≥ −r𝒩}] ≤ Cr(k + r)²P^N ≤ Cr³P^N`. +- *`A < 0`, `λ < λ₃`.* By #220 (F2), `ω_r ≤ w_κ(A, Y_r) + Cr(1 + κ)𝒩^N`; and `|G_r| ≤ C(κ²Δ² + k|P₁|)1{|z| < 25κ}`. The `𝔅_λ′` + computation of §2, with `λ₃` in place of `λ₂′`, gives `C(r³ + r^{5/2})P^N` for the terms `w_κ` and `κ²Δ²`. The terms + `Cr(1 + κ)𝒩^N` and `k|P₁|` contribute `Cr·E[λ₃(…)] ≤ Cr²P^N`: since `λ₃` involves `f₄`, apply #218 Lemma D to `A` given + `J′ ∖ {A}` (a Schur complement in `Cov_Q(J′)`, as in #220 (F5)). +- *`𝒩 > c₁₁/r`.* Probability `≤ C_pr^pP^p` (#220 (F4)), with polynomial weights: `Cr²P^N`. +- *`|Δ| < C₁₂r𝒩^{N₂}(1 + ‖B‖)`.* There `ω_r ≤ 36κ²Δ² + Cr𝒩^N` and `|G_r| ≤ 36κ²Δ² + Ck|P₁|`. By #218 Lemma D, + `E[(1 + ‖A‖)^n1{|Δ| < ε} | J‴] ≤ C(P + |J‴|)^{n′}ε`; in `𝒩`-layers, this costs `Cr²P^N`. + +*Step N3 (to the contact law).* `|G_r(j)| ≤ C(1 + |j|)^N`, since `w₀` and `P₁` are polynomials. By #220 (F6) and Lemma G (a), +`|E_Q[G_r] − E_{v_0(b,k)}[G_r]| ≤ Cr²P^N`. + +*Step N4 (the expansion).* Under the contact law at `v_0(b, k)`, given all free jets except `f₄`, `f₄` is Gaussian with +variance `σ₄² ∈ [c, C]` and a mean `m₄` that depends only on the even jets (#220 (F3) at `r = 0`, and (F7)). Let `p_z` be the +conditional density of `z = f₄ − 3q`. With `δ := 36rQ₁`, `12kP₁ = (κΔ²/3)δ`, so `E[G_r | rest] = I(δ)1{|δ| ≤ 36c_eκ}`, where + + I(s) := ∫_{|z| < 24κ + s} [(Δ²/144)(5184κ² − z²) + (κΔ²/3)s] p_z(z) dz (|s| < 24κ). + +`I(0) = E[w_κ^{eld}(A, Y′) | rest]`, since `|Y′| < 2κ|Δ| ⟺ |z| < 24κ`. Since `w₀ = 32κ²Δ²` at `z = ±24κ`, + + I′(0) = Ψ_κ/36, Ψ_κ := 1152κ²Δ²[p_z(24κ) + p_z(−24κ)] + 12κΔ²·P(|z| < 24κ | rest), (5.3) + +and `δI′(0) = rQ₁Ψ_κ`. For `|δ| ≤ 36c_eκ`, `|I(δ) − I(0) − δI′(0)| ≤ ½δ²sup_{|s| ≤ 36c_eκ}|I″(s)|`, with +`|I″(s)| ≤ CΔ²(κ + κ²)sup_{23κ ≤ |x| ≤ 25κ}(p_z + |p_z′|)(x)`. For `|δ| > 36c_eκ`, `|I(0)| + |δI′(0)| ≤ |I(0)|(δ/(36c_eκ))² + C|δ|²Ψ_κ/κ`, +where `|I(0)| ≤ 36κ²Δ²·P(|z| < 24κ | rest)`. Now `p_z(x) = p_{f₄}(x + 3q)`, and +`Δ²δ² ≤ Cr²‖A‖^{2m−2}(f₅²λ² + |η|²|q|λ + ‖B‖²q²)`, by `|Q₁| ≤ |f₅|/120 + |η|Γ̃/12 + ‖B‖Γ̃²/8`, `Γ̃² ≤ |q|/λ` and +`Δ² ≤ λ²‖A‖^{2m−2}`. Every term above carries `p_z` or `P(|z| < 24κ | rest)` on `|z| ≤ 25κ`, so the Gaussian decay of +`p_{f₄}` in `q` absorbs the powers of `q`, as in Step N2. Hence + + E_{v_0(b,k)}[G_r] = E_{v_0(b,k)}[w_κ^{eld}(A, Y′)] + r·E_{v_0(b,k)}[Q₁Ψ_κ] + O(r²P^N). (5.4) + +*Step N5 (parity).* By #220 (F7), under the contact law at `v_0(b, k)`, the even free jets `E` are independent of the odd +ones, `O ~ N(12kw, Σ_o)`. Write `Q₁Ψ_κ = G(E, O)`. `Q₁` is odd in `O`. `Ψ_κ` depends on `O` only through `q`, which is even, +because the conditional law of `f₄` depends only on `E`. So `G(e, −o) = −G(e, o)`, and `E_{v_0(b,0)}[Q₁Ψ_κ] = 0`. Moreover +`|Q₁Ψ_κ| ≤ C(1 + κ)²|P₁|·(1 + sup p_z) ≤ C(1 + |j|)^N`, so Lemma G (a), moving the odd mean from `0` to `12kw`, gives + + |E_{v_0(b,k)}[Q₁Ψ_κ]| ≤ C k (1 + |b|)^N. (5.5) + +By #220 Step E6, `E_{v_0(b,k)}[w_κ^{eld}] = E_{v_0(b,0)}[w_κ^{eld}] + O(k²(1 + |b|)^N)`. + +*Step N6 (assembly).* By [R] (R5), as in #220 Step E5, `|π_r(v_r) − π_0(v_0(b, k))| ≤ Cr²P²e^{−c(b² + k²)}`; by (F7), +`π_0(v_0(b, k)) = p_e(b, 0, 0)p_o(0, 12k, 0) = π_0(v_0(b, 0))e^{−a′k²}` for some `a′ > 0`; and `E_Q[ω_re] ≤ C(1 + κ)²P^N`. +With (5.2)–(5.5), + + r^{−2}A_r^{eld}(b, κr, u) = 12π_0(v_0(b, 0))E_{v_0(b,0)}[w_κ^{eld}(A, Y′)] + O(r²(1 + |b|)^Ne^{−cb²}) + = 𝒜^{eld}(b, κ, u) + O(r²(1 + |b|)^Ne^{−cb²}), + +using `rk = κr²`, `k² = κ²r²` and `P^Ne^{−ck²} ≤ C(1 + |b|)^N`. Also `r^{−2}A_0(b, κr, u) = 𝒜^{con}(b, κ, u)e^{−a′k²}` (#218 +Step C3 and (F7): the even-jet law does not depend on `k`), and `𝒜^{con} ≤ Cκ²(1 + |b|)^Ne^{−cb²}`. Subtracting gives (N.1). + +*Proof of (N.2).* The same steps, with the typed window in place of the elder window. +- *Step N1.* In Case 1, `ω_r = (−r^{−2}det K_M det K_S)₊ − (−r^{−2}det K_M det K_S)1_{anti}`: a typed pair has + `det K_M det K_S < 0`, a pair that is neither typed nor anti-typed has `det K_M det K_S ≥ 0`. On `𝔊` there are no anti-typed + pairs, so `ω_r = (w₀ + 12kP₁ + ε_ω)₊`. +- *Steps N2–N3* with `G_r^{cand} := (w₀ + 12kP₁)₊1{A < 0, r|Q₁| ≤ c_eκ}`, using `|(x + ε)₊ − x₊| ≤ |ε|`. Its support lies in + `{|z| < 73κ}`. +- *Step N4.* `|(w₀ + ε)₊ − (w₀)₊ − ε1{w₀ > 0}| ≤ |ε|1{|w₀| ≤ |ε|}` with `ε = 12kP₁`. Since `5184κ² − z² = (72κ − |z|)(72κ + |z|)`, + `{|w₀| ≤ 12k|P₁|}` puts `z` in two windows of half-width `24r|Q₁|` around `±72κ`, and the Gaussian decay of Step N2 gives + `O(κr²P^N)`. So `E[G_r^{cand} | rest] = E[w_κ(A, Y′) | rest] + rQ₁Ψ_κ^{cand} + O(r²…)` with + `Ψ_κ^{cand} := 12κΔ²P(|z| < 72κ | rest)`, which is `𝒫`-invariant. There is no edge term, because the typed weight vanishes + at the edges of the typed window. +- *Step N5.* (5.5) holds for `Ψ_κ^{cand}`, and `E_{v_0(b,k)}[w_κ(A, Y′)] = E_{v_0(b,0)}[w_κ(A, Y′)] + O(k²(1 + |b|)^N)` by #220 + Lemma G (b), as in #218 Step C3 with #229 Lemma L. +- *Step N6* as above. ∎ + +## 6. Proof of Corollary N′ + +Let `r₋ := (ℓ/κ₁)^{1/4}` and `r₊ := (ℓ/κ₀)^{1/4}`, and take `ℓ` so small that `r₊ ≤ r_K` for `K = [κ₀, κ₁]`. For `r ∈ [r₋, r₊]`, +`κ := ℓ/r⁴ ∈ K` and `ℓ/r³ = κr`. By (N.1), (N.2) and Step N6, + + r^{−2}A_r^*(b, ℓ/r³, u) = 𝒜^*(b, ℓ/r⁴, u) + O(r²(1 + |b|)^Ne^{−cb²}) (* ∈ {eld, cand}), + +and the difference gives `* = rej`. Integrate over `u`, `b` and `r ∈ [r₋, r₊]`. With `r = ℓ^{1/4}s`, +`∫_{r₋}^{r₊}𝒜^*(b, ℓ/r⁴, u) dr = ℓ^{1/4}∫_{κ₁^{−1/4}}^{κ₀^{−1/4}}𝒜^*(b, s^{−4}, u) ds`, and the error is at most +`C∫_{r₋}^{r₊}r² dr ≤ (C/3)κ₀^{−3/4}ℓ^{3/4}` (control X6). ∎ + +## 7. Remarks + +1. **Where the argument stops.** Theorem N is a statement at fixed `κ`. The linear term `rE[Q₁Ψ_κ]` is `O(rk)` for *every* + `κ` by (5.5), so formally the elder kernel has no `O(r)` term at any `κ`, and the formal `ℓ^{1/2}` term of #218 §0 and + #229 §0 does not arise from the cusp scale. What is not uniform is the remainder. + - *`κ → ∞` (the fold side).* In the soft region `λ ≈ |γ|²/κ`, `Γ̃ ≈ κ/|γ|`, and the edge shift `rQ₁/(2κ)` has size + `≈ k‖B‖/|γ|²` instead of `r`: the expansion is in `k`, not in `r`. At the fold scale `k ≍ 1` the decision in this + region depends on the higher transverse jets: with `Ξ ≈ κ`, the monomial `r²Ξ³` of the window field has relative size + `≈ k²`. The constants of Theorem N grow polynomially in `κ`, which is not enough for #229's ledger at `ρ_f`. + - *`κ → 0` (the intermediate side).* The elder window has width `48κ` in `f₄`, and the edges move by `36r|Q₁|`. For + `κ ≲ r` the expansion does not apply, and the intermediate elder mass is #229's `O(ℓ^{4/9}log(1/ℓ))`. + - *What would follow from uniformity.* Suppose (N.1) held with error `C(r² + k²)` uniformly for `r ≤ κ ≤ 1/r`. Then #229's + decomposition, with `ρ_c = ℓ^{1/5}` and #237's Lemma K for the finite part, would give the elder density with remainder + `O(ℓ^{4/9}log(1/ℓ))`, from the intermediate separations. It would not go beyond `ℓ^{1/2}`: the fold family `ρ_f⁵/ℓ` + would balance `ℓ²ρ_f^{−5}` at `ℓ^{1/2}` (control X6). Going beyond `ℓ^{1/2}` needs, as for the candidate in #237, a + uniform two-scale description that removes the fold family, here including the rejected fold mass of [C7-K] (K2). +2. **#229's ledger.** With (CE⁺⁺.1) in place of (CE⁺.1), the rows `ℓ²ρ_f^{−11/2}` and `ℓ³ρ_f^{−9}` of #229 §5 disappear. The + elder's fold and cusp rows are then the candidate's; the elder keeps its intermediate rows (`ℓ^{4/9}log(1/ℓ)`). The least + exponent is still `3/7`, from `ρ_f⁵/ℓ` against `ℓρ_f^{−2}` (control X6). #229 Remark 1 observed that for the elder density Lemma Q's bad events would become the obstruction once the linear + pair is resolved; after Proposition CE⁺⁺ they no longer are. +3. **Numerical evidence** (exploration; project archive `V2_2/frontiers_elder_cusp_parity_20261002/exploration/`; not part of + the proof). `d = 2`, Gaussian kernel `e^{−|z|²/2}`. + - *Quadrature* (`cusp_quad.py`). `𝒜^{cand}` and `𝒜^{eld}` under the contact law. At `(b, κ) = (0, ½), (0, 1), (0, 2), (1, 1)`: + `𝒜^{cand} = 0.119692, 0.495998, 2.003851, 0.640405` and `𝒜^{eld} = 0.111331, 0.489836, 2.000088, 0.637500`. + - *Monte Carlo of the kernels at `r > 0`* (`elder_f4int.py`). The free jets of order `≤ 8` are sampled under the exact pinned + law, with common random numbers across `r ∈ {0.005, 0.01, 0.015, 0.02, 0.03, 0.04}` and antithetic odd jets + (`N = 20000`). The pinned jets are solved from the pin rows, `f₄` is integrated in closed form, and the elder set in `f₄` + is an interval found by bisection on the ridge conditions. Cubic fits `g₀ + g₁r + g₂r² + g₃r³` give `g₀` within `0.3` + standard errors of the quadrature for the candidate and the elder kernels, and within `0.9` standard errors for the + rejected kernel at `b = 0` (`2.1` at `b = 1`). + - *The linear coefficient.* For the rejected kernel, `g₁/𝒜^{cand} = +0.007 ± 0.006, +0.003 ± 0.007, +0.003 ± 0.009, + −0.003 ± 0.003` at the four points: consistent with zero. (Relative to the rejected kernel itself the uncertainties + are `±0.09` at `κ = ½` up to `±5` at `κ = 2`.) The natural scale is the absolute first-order integrand `E|Q₁Ψ_κ^{rej}|` + (`first_order_scale.py`): `0.020, 0.031, 0.040, 0.016`. Relative to it, the fitted `g₁` is `0.04 ± 0.04` at `κ = ½`. + - *The candidate's cubic fit.* Its `g₁` is `19`–`44` standard errors from zero for `κ ≥ 1` (up to `0.03` relative), a fit + artefact: with `g₀ + g₁r + g₂r² + g₄r⁴` instead, the point estimates drop to `−6·10⁻⁵`, `−2.5·10⁻³` and `−5.5·10⁻⁵` + (`κ = 1`, `κ = 2`, and `b = 1`), at most `1.3·10⁻³` relative. +4. **The Monte Carlo of #216** (project archive `V2_2/numerics_lifetime_mc_20261001/results/mc{2,3}_final.json`; `altfit.py`). + #237 Remark 4 found that the elder and rejected residuals about the three-term law are not consistent with zero, with an + `ℓ^{1/2}` coefficient in joint `ℓ^{1/2} + ℓ^{3/4}` fits. On `[10⁻⁴, 0.3]` (19 bins, 17 degrees of freedom), the fits + `ℓ^{1/2} + ℓ^{3/4}` and `ℓ^{2/3} + ℓ^{3/4}` are comparable, with `χ²` in that order: `10.4` and `11.9` (elder, `d = 2`), `18.0` + and `20.6` (rejected adjacent pairs, `nR`, `d = 2`), `8.0` and `6.9` (elder, `d = 3`), `8.1` and `9.3` (rejected adjacent + pairs, `d = 3`); `|Δχ²| ≤ 2.6`. On this range `ℓ^{2/3}` and `ℓ^{3/4}` are nearly collinear: their fitted amplitudes + (`±0.14` to `±0.22`) cancel. The data do not single out `ℓ^{1/2}`, and Theorem N gives no reason to expect it from the + cusp scale. +5. **Consistency.** + - (CE⁺⁺.1) implies #229 (CE⁺.1), which implies #220 (CE.1). + - (N.2), integrated in `b`, agrees with #237's cusp-scale consequence of Lemma U (`O((1 + κ)²r²)`). + - Lemma Ω (a) is #237 Lemma Π, and #232 (2.3) with the `r³` term removed by evenness. Since `V_o = ΔQ₁ + α₄Δ_B`, #232's `V` + contains `Q₁` as well. + - Lemma Q″ is the `d ≥ 2` form of #238 Lemma W. + +## 8. Sources (exact identities in `SOURCES.json`) + +| Tag | Path | Role | +|---|---|---| +| [R] | `frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md` (blob `247b3ecf`) | (R2)–(R5): pin densities, 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 | +| #191 | `frontiers/remainder_vanishing_20260930/PROOF.md` (blob `441152df`) | Lemma E Step 3 (evenness) — consumed | +| #207 | `frontiers/cusp_second_order_20261001/PROOF.md` (blob `f6df5a73`) | §0, (0.2), Theorem CU.2, Proposition CU.3, (4.1) — consumed | +| #218 | `frontiers/candidate_third_order_20261001/PROOF.md` (blob `70ca57ef`) | Lemma D, (1.2), Step F1, Step C1, Step C3 — consumed | +| #220 | `frontiers/elder_third_order_20261001/PROOF.md` (blob `c8767dde`) | §1 (Lemma CU.1′, Lemma S, Lemma Q, (M1)–(M6)); §2 ((F1)–(F7), Lemma G, Lemma CE) — consumed | +| #229 | `frontiers/third_order_rate_20261001/PROOF.md` (blob `110ed33a`) | Lemma L, Lemma CE⁺, §5 — consumed | +| #232 | `frontiers/c2_finite_jet_transfer_20261001/PROOF.md` (blob `54cc4a1a`) | §2 (2.1)–(2.4) — consumed | +| #237 | `frontiers/candidate_parity_rate_20261001/PROOF.md` (open PR; blob `a97bf528`) | Lemma Π, Lemma K, Lemma U, Remarks 3–4 — cited | +| #238 | `frontiers/d1_sharp_remainder_20261001/PROOF.md` (open PR; blob `3b2ec970`) | Lemma W — cited | +| #216 | `frontiers/third_order_coefficient_20261001/NOTE.md` (open PR) | Monte Carlo — cited | + +## 9. Exact controls (`ecp_check.py`; stdlib; exact rationals; byte-identical under `-O` and on CPython 3.10–3.14) + +- **X1** Lemma Q′ and Proposition CE⁺⁺: the polynomial bounds for `ε₀`, `ε₁`, `ε₂` and the constant `220` (exact polynomial + arithmetic); `|q| ≥ λΓ̃²` and the Frobenius-norm form of `|tr(A^{−1}B)| ≤ m‖B‖/λ` on random negative definite rational + matrices (`m = 1, 2, 3`); `κ²r^{3/2} + κ³r² ≤ 2r` on a rational grid; and, as recorded arithmetic that cannot fail, + `ϱ ≤ 4(1 + M̃)`, the slack on `|Ξ| = R′`, the constants of (2.3) and the exponents of the `5/2`-power step. +- **X2** the model ridge: (M1), (M4) and (3.3) as identities; the new cases of Step Q6′; on `J_±`, the constants `c₃` and `c₄`, + the bounds on `g(−3)`, `g(2)`, `g(−3/2)`, `g(X₃)` and the brackets, by exact monotonicity; the expansions (3.4) with + `|Ψ₂|, |Ψ₂⁻| ≤ 90` and `|ω_±| ≤ 120`. +- **X3** pinned polynomial fields: in `d = 2, 3` with `k = κr`, the window field `𝔓 + r𝔔 + O(r²)`, with every monomial of + `𝔉 − 𝔓 − r𝔔` having `a ≥ 2` and `|j| ≤ a + 1`, and #232's family (2.4) in window coordinates and with its pins; in + `d = 2, 3, 4` at fixed `k`, Lemma Ω (a): the coefficients of `r⁰, …, r³` of `det K_M`, `det K_S` and `−det K_M det K_S`. +- **X4** the identities of Lemma Ω (b)–(c): `ΔJ_B = Δ_BJ − JBJ` (`m = 1, 2, 3`, including singular `A`), (4.2), `P₁ = Δ²Q₁`, + `V_o = ΔQ₁ + α₄Δ_B`, `𝔔(X, Ξ*) = Q₁X(X² − ¼)²`, and the parities. +- **X5** the first-order bookkeeping: `w₀(±24κ) = 32κ²Δ²`, `12kP₁ = (κΔ²/3)·36rQ₁`, the edge shift `36rQ₁` in `z` from + `rQ₁/(2κ)` in `φ`, the linear edge equations, `I′(0) = Ψ_κ/36` on polynomial test densities, and the half-width `24r|Q₁|` + of the candidate's kink windows. +- **X6** Corollary N′ and the ledgers: the substitution `r = ℓ^{1/4}s`; `∫_{r₋}^{r₊}r²dr ≤ κ₀^{−3/4}ℓ^{3/4}/3`; #229's ledger + with and without the elder rows (least exponent `3/7` at `ρ_f = ℓ^{2/7}` in both); the conditional ledger of Remark 1. + +Mutants, each breaking one control: `M1` (X3: `f₅/60` in `𝔔`), `M2` (X4: the sign of `ηᵀA^{−1}γ/12` in `Q₁`), `M3` (X5: the +edge shift `18rQ₁`), `M4` (X2: `|ω_±| ≤ 100`), `M5` (X1: the constant `200`), `M6` (X3: the saddle at `r/2 + r⁴`, which breaks +the evenness in Lemma Ω (a)), `M7` (X6: `ρ_f = ℓ^{1/4}`). An unknown mutant label exits `2`. + +## 10. Review slices + +- **A** §§1–2: Lemma Q′ (Steps Q2′ and Q6′) and Proposition CE⁺⁺ (the conditions (2.3) and the three bad events). +- **B** §3: Lemma CU.1″, Lemma R₂, the model near the edges and Lemma Q″. +- **C** §4 and Steps N4–N5: Lemma Ω, the identity `12ΔV_o − 6Y′Δ_B = 12P₁`, the expansion (5.4) and the parity (5.5). +- **D** Steps N1–N3 and N6, and (N.2): the good event, the exceptional events (5.2) and the candidate case. +- **E** §§6–7 and the controls: Corollary N′, the ledger remarks and the exploration. diff --git a/frontiers/elder_cusp_parity_20261002/README.md b/frontiers/elder_cusp_parity_20261002/README.md new file mode 100644 index 000000000..6cd85bf3d --- /dev/null +++ b/frontiers/elder_cusp_parity_20261002/README.md @@ -0,0 +1,87 @@ +# The elder cusp kernel: the candidate rate, and no linear term at fixed `κ` + +**Author-side proof candidate (Anthropic Claude). Scientific effect: NONE. Nonauthor review required.** + +Object `CL-ELDER-CUSP-PARITY-20261002-v1`. Full text: [`PROOF.md`](PROOF.md). + +## Results + +| | Statement | Compared with | +|---|---|---| +| **Lemma Q′** (§1) | #220's elder decision lemma with relaxed margins: `Γ = \|γ\|/λ` becomes `Γ̃ = \|A^{−1}γ\|`, the ridge maximizer is located in a ball of radius `max(1, 8ḡ/λ)`, and every `φ` is decided (two new cases, `φ > 1` and `φ < −1`). | #220 Lemma Q needs `8C₁𝒩r(1 + 5Γ) ≤ λ` and `\|φ\| ≤ 1`. | +| **Proposition CE⁺⁺** (§2) | The elder cusp kernel with error `Cr(1 + κ)`, the candidate's rate. | #229 (CE⁺.1): `C(r(1 + κ) + κ²r^{3/2} + κ³r²)`. The two elder-only rows of #229's ledger disappear; `3/7` is unchanged. | +| **Theorem N** (§§3–5) | For `κ` in a compact subset of `(0, ∞)`: the elder and the candidate cusp kernels have **no `O(r)` term**, pointwise in the birth height; the error is `O(r²)`. | #237 (open) proves this for the candidate after the `b`-integral (Lemma U); its Remark 3 records the elder case as formal only. | +| **Corollary N′** (§6) | In every fixed window `κ₀ ≤ ℓ/r⁴ ≤ κ₁`, the elder, candidate and rejected densities are `(const)·ℓ^{1/4} + O(ℓ^{3/4})`: no `ℓ^{1/2}` term. | The formal `ℓ^{1/2}` term of #218 §0 and #229 §0 would come from an `O(r)` cusp correction. | + +**The mechanism.** Both first-order effects at the cusp scale are multiples of one jet polynomial, + + Q₁ = f₅/120 − ηᵀA^{−1}γ/12 + γᵀA^{−1}BA^{−1}γ/8, + +the coefficient of the quintic ridge correction `rQ₁X(X² − ¼)²`: +- the edges of the elder window move from `|φ| = 1/3` to `|φ| = 1/3 + rQ₁/(2κ)` (Lemma Q″, the `d ≥ 2` form of #238's Lemma W); +- the typed weight changes by `12κrΔ²Q₁`: in #232's expansion, the first-order parts of `12kΔV` and `−U²` combine into + `12kΔ²Q₁` (Lemma Ω, via `ΔJ_B = Δ_BJ − JBJ`). + +`Q₁` is odd under the point reflection of the jets and every zeroth-order quantity is even. So the `O(r)` term is +`r·E[Q₁Ψ_κ]` with `Ψ_κ` even, which is `O(rk)` by the parity factorization (#220 (F7)). + +**What is not claimed.** Nothing about the whole elder density beyond #229's `O(ℓ^{3/7})`. Theorem N is not uniform as +`κ → ∞` (the soft region `λ ≈ |γ|²/κ`, where the expansion is in `k`, not `r`) or as `κ → 0` (the intermediate +separations). Remark 1 of `PROOF.md` gives the conditional ledger: a uniform version would give `ℓ^{4/9}log(1/ℓ)`, still +short of `ℓ^{1/2}`, because the fold family `ρ_f⁵/ℓ` balances `ℓ²ρ_f^{−5}` at `ℓ^{1/2}`. + +## Dependencies + +| | Sources | +|---|---| +| Consumed (all merged) | #220 (`c8767dde`, merged at `0d79778`): §1 (Lemma CU.1′, Lemma S, Lemma Q, (M1)–(M6)), §2 ((F1)–(F7), Lemma G, Lemma CE). #229 (`110ed33a`, merged at `6f74f7a`): Lemma L, Lemma CE⁺, §5. #218 (`70ca57ef`): Lemma D, (1.2), Step F1, Step C1, Step C3. #232 (`54cc4a1a`): §2 (2.1)–(2.4). #207 (`f6df5a73`): §0, Theorem CU.2, Proposition CU.3, (4.1). [R], [P], #191 (Lemma E Step 3) | +| Cited (open) | #237 (Lemma Π, Lemma K, Lemma U, Remarks 3–4), #238 (Lemma W), #216 (Monte Carlo) | + +## Controls + +`ecp_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 (under a second). + +| Control | Checks | +|---|---| +| X1 | Lemma Q′'s `C⁰`, `C¹`, `C²` polynomial bounds and the constant `220`; `\|q\| ≥ λΓ̃²` and the trace bound on random negative definite rational matrices; the constants of the sufficient conditions (2.3). | +| X2 | The model ridge: (M1), (M4), the new cases of Step Q6′, the constants near the edges (`c₃ = 281/128`, `c₄`), and the expansions (3.4) with `\|Ψ₂\| ≤ 90`, `\|ω_±\| ≤ 120`, proved by exact Bernstein positivity on `\|t\| ≤ 1/96`. | +| X3 | Pinned polynomial fields: the window field is `𝔓 + r𝔔 + O(r²)` with the monomial bound of Lemma CU.1″ (`d = 2, 3`); #232's family (2.4) in window coordinates; Lemma Ω (a) at orders `r⁰`–`r³` (`d = 2, 3, 4`). | +| X4 | `ΔJ_B = Δ_BJ − JBJ` (including singular `A`), (4.2), `P₁ = Δ²Q₁`, `V_o = ΔQ₁ + α₄Δ_B`, `𝔔(X, Ξ*) = Q₁X(X² − ¼)²`, and the parities. | +| X5 | The first-order bookkeeping: edge values of `w₀`, the edge shift `36rQ₁`, `I′(0) = Ψ_κ/36` on polynomial test densities, the candidate's kink windows. | +| X6 | Corollary N′'s integral, #229's ledger with and without the elder-only rows (`3/7` both), and the conditional ledger of Remark 1. | + +Mutants `M1`–`M7` each fail exactly their own control, and an unknown label exits 2. + + python3 -B -S ecp_check.py # exit 0, output = RESULTS.json + python3 -B -S ecp_check.py --mutant M3 # exit 1 + +The controls check exact algebra, model constants and arithmetic. The probabilistic estimates are proved in prose only. + +## Exploration (not part of the proof) + +`d = 2`, Gaussian kernel (project archive `V2_2/frontiers_elder_cusp_parity_20261002/exploration/`; numpy, scipy, mpmath): +- `cusp_quad.py`: `𝒜^{cand}`, `𝒜^{eld}` by quadrature under the contact law. +- `elder_f4int.py`: the kernels at `r > 0` by Monte Carlo under the exact pinned law. Common random numbers across six `r`, + antithetic odd jets, `f₄` integrated in closed form, the elder interval in `f₄` by bisection. The fitted levels agree with + the quadrature. The rejected kernel's linear coefficient is consistent with zero at all four `(b, κ)` points; at `κ = ½` + it is `0.04 ± 0.04` of the absolute first-order scale `E|Q₁Ψ_κ|` (`first_order_scale.py`). +- `altfit.py`: on #216's archived Monte Carlo, two-power residual fits with `ℓ^{2/3} + ℓ^{3/4}` and with `ℓ^{1/2} + ℓ^{3/4}` + are comparable (`|Δχ²| ≤ 2.6`); the data do not single out `ℓ^{1/2}`. + +## Review record + +One clean-context same-family referee (an Anthropic Claude subagent) read the note, the checker and the consumed +sources at their declared blobs, re-derived Lemmas Q′, R₂, Q″ and Ω and Steps N1–N6 by hand, verified the Lemma Ω identity +symbolically, the model constants with mpmath, and the edge location `±(1/3 + rQ₁/(2κ)) + O(r²)` numerically on #232's +exact family. Verdict: **no blocking error**. One MAJOR finding and eleven MINOR ones, all applied before submission: +- MAJOR: in Step N2 the edge windows were integrated in `f₄` on an event that involves `f₄`. The `f₄`-free event `𝔊″` is + now introduced, on which the windows have bounded width and lie near `3q ± 24κ`, and the term `k|P₁|` is bounded by + `c_eκ²Δ²` there. +- MINOR: conditioning for Lemma D when the threshold involves `f₄`; the definition of `𝔅_4′` (as #229's); `r₂′ ≤ r₂`; the + orders of the pin corrections in Lemma CU.1″; the citation (F1); the exponent `N₂` in the margin on `|Δ|`; `≥ 0` in the + case identity; Remarks 2–4 (the candidate fit artefact, the `χ²` order, the rejected-adjacent counts); the description + of the controls and the mutants. + +Same GitHub account and same provider as the author: zero organizational-independence credit. Nonauthor review is +required for every slice (`PROOF.md` §10). diff --git a/frontiers/elder_cusp_parity_20261002/RESULTS.json b/frontiers/elder_cusp_parity_20261002/RESULTS.json new file mode 100644 index 000000000..e560d8b10 --- /dev/null +++ b/frontiers/elder_cusp_parity_20261002/RESULTS.json @@ -0,0 +1,79 @@ +{ + "X1": { + "constant": 220, + "eps0": [ + "4", + "35", + "1225/16" + ], + "eps1": [ + "4", + "41", + "1645/16" + ], + "eps2": [ + "6", + "279/4", + "3333/16" + ] + }, + "X2": { + "Psi2_bound": 90, + "c3": "281/128", + "c4": "22761/495616", + "c_e": "1/200", + "delta_e": "1/96", + "omega_bound": 120, + "second_order_coefficients": { + "Psi2_at_0": "-81", + "Psi2m_at_0": "81", + "omega_at_0": "99", + "omegam_at_0": "99" + } + }, + "X3_Omega_fields_checked": 6, + "X3_window_fields_checked": 9, + "X4_instances_checked": 24, + "X6": { + "conditional_least": "4/9", + "conditional_ledger_remark_1": { + "a^4 log (intermediate)": "4/9", + "l rho_c^-2": "3/5", + "l^(2/3) a^-2 (intermediate)": "4/9", + "l^2 rho_c^-7": "3/5", + "l^2 rho_f^-5": "1/2", + "l^3 rho_c^-11 log": "4/5", + "rho_c^3": "3/5", + "rho_f^2": "3/5", + "rho_f^5/l": "1/2" + }, + "least_with_elder_rows": "3/7", + "least_without_elder_rows": "3/7", + "ledger_229": { + "a^4 log": "4/9", + "l": "1", + "l rho_c^-2": "5/9", + "l rho_f^-2": "3/7", + "l^(2/3) a^-2": "4/9", + "l^(5/3) a^-7": "8/9", + "l^2 rho_c^-7": "4/9", + "l^2 rho_f^-11/2 (elder only)": "3/7", + "l^3 rho_c^-11 log": "5/9", + "l^3 rho_f^-9 (elder only)": "3/7", + "rho_c^2": "4/9", + "rho_c^3": "2/3", + "rho_f^2": "4/7", + "rho_f^5/l": "3/7" + } + }, + "controls": { + "X1_lemma_Q_prime_and_CE": true, + "X2_model_ridge_and_edges": true, + "X3_pinned_fields_and_Omega_a": true, + "X4_Q1_identities_and_parity": true, + "X5_first_order_bookkeeping": true, + "X6_corollary_and_ledgers": true + }, + "object": "CL-ELDER-CUSP-PARITY-20261002-v1", + "scientific_effect": "NONE" +} diff --git a/frontiers/elder_cusp_parity_20261002/SOURCES.json b/frontiers/elder_cusp_parity_20261002/SOURCES.json new file mode 100644 index 000000000..72bb0aa83 --- /dev/null +++ b/frontiers/elder_cusp_parity_20261002/SOURCES.json @@ -0,0 +1,207 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "object": "CL-ELDER-CUSP-PARITY-20261002-v1", + "kind": "author-side proof candidate: the elder cusp kernel with the candidate rate and without a linear term at fixed kappa, in every d >= 2. Lemma Q-prime (the elder decision of Math- #220 with relaxed margins: Gamma~ = |A^-1 gamma|, the ridge maximizer in a ball of radius max(1, 8 gbar/lambda), every phi decided); Proposition CE++ (the elder cusp kernel with error C r (1 + kappa), improving Math- #229 (CE+.1); 3/7 unchanged); Theorem N (for kappa in a compact subset of (0, inf), the elder and candidate cusp kernels are the cusp kernels + O(r^2), pointwise in the birth height: the O(r) term is r E[Q1 Psi_kappa] with Q1 = f5/120 - eta^T A^-1 gamma/12 + gamma^T A^-1 B A^-1 gamma/8 odd and Psi_kappa even, hence O(rk)); Corollary N-prime (in every fixed cusp window kappa0 <= l/r^4 <= kappa1 the elder, candidate and rejected densities are const l^(1/4) + O(l^(3/4)): no l^(1/2) term)", + "author": "Anthropic Claude", + "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", + "read_at": { + "branch_base": "6f74f7a77bae15d6aa07506bab38977e34dcc449" + }, + "consumed": [ + { + "path": "frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md", + "bytes": 17734, + "sha256": "380b7d0abdb0fe2de5a6564565af9560d3f1b1ce22fd5538927db0c52f4f3a4a", + "git_blob": "247b3ecf80bfbe896948d5d489b2d5842a81c481", + "tag": "R", + "use": "(R2)-(R5): pin densities (R5), 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 (the elder mark is Borel)" + }, + { + "path": "reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md", + "bytes": 23312, + "sha256": "451b9d7ffee072a73fc904cab891b6693e3f233808b89df10cce1b57036b65da", + "git_blob": "75da2597971510f843f8d90c743950cb8c177342", + "tag": "REC", + "use": "reading rule" + }, + { + "path": "frontiers/remainder_vanishing_20260930/PROOF.md", + "bytes": 25353, + "sha256": "0cb5b949261476f10e539677e2744e3288752474393af25ba787e67b1350f32a", + "git_blob": "441152dfc1d8d00cb268cebdb0394212a5bfacdb", + "tag": "191", + "use": "Math- #191 (merged): Lemma E Step 3, det H_M(-r) = det H_S(r) (evenness of the product in Lemma Omega (a))" + }, + { + "path": "frontiers/cusp_second_order_20261001/PROOF.md", + "bytes": 52605, + "sha256": "cffc1b83ac364da58bd650c3c301ea1babd38e19af54f74010bdc120edce38a8", + "git_blob": "f6df5a7356a54771b0052e42a864a140709903ad", + "tag": "207", + "use": "Math- #207 (merged 2026-10-01 at 566b1a1): section 0 (cusp objects, the cusp polynomial (0.2)); Theorem CU.2 and Proposition CU.3 through #220; section 4 (4.1)" + }, + { + "path": "frontiers/candidate_third_order_20261001/PROOF.md", + "bytes": 37220, + "sha256": "6c1279164499d4fe2fbeee244b40dafa2159758d20f04826cd67d7602ea97fe4", + "git_blob": "70ca57ef05199e75417d7d57928c1e1c93bf944e", + "tag": "218", + "use": "Math- #218 (merged 2026-10-01 at fb6ee97): Lemma D (1.1) and (1.2); Step F1 (2.1)-(2.2); Lemma C Step C1 (its three cases) and Step C3" + }, + { + "path": "frontiers/elder_third_order_20261001/PROOF.md", + "bytes": 70544, + "sha256": "74b5f031ba5be6f50b5e543636136df1d9b5fad0fcd2c8210320cfef02f80e37", + "git_blob": "c8767ddecf1041d234f685e95af582073a7be393", + "tag": "220", + "use": "Math- #220 (merged 2026-10-01 at 0d79778): section 0; section 1 (the setting, Lemma CU.1-prime (1.1) and its proof, Lemma S (1.2), Lemma Q and its proof, (M1)-(M6)); section 2 (notation, (F1)-(F7), (2.1)-(2.2), Lemma G, Lemma CE and its proof, Steps E1-E6)" + }, + { + "path": "frontiers/third_order_rate_20261001/PROOF.md", + "bytes": 37626, + "sha256": "5de5a6c7b942a71675c812000ade30c16766f02ee388e8dc3e1c51dde5297f7d", + "git_blob": "110ed33a57902bef11873807e722fde3888b59fb", + "tag": "229", + "use": "Math- #229 (merged 2026-10-01 at 6f74f7a): Lemma L (L.1); Lemma CE+ (CE+.1) and its proof (Step E2+ with (3.1)-(3.2), Step E3+); section 5 (the ledger, for Remarks 1-2)" + }, + { + "path": "frontiers/c2_finite_jet_transfer_20261001/PROOF.md", + "bytes": 25581, + "sha256": "971101de946fd711207454c2cd4bbc36729ca9b7c07262e122ff1d54bf5dfa16", + "git_blob": "54cc4a1ae274842bc2c01f9c207549e7b07de7bc", + "tag": "232", + "use": "Math- #232 (merged 2026-10-01 at 7fe06b0): section 2 (2.1)-(2.4) (the endpoint determinants to second order and the exact pinned family)" + } + ], + "consumed_unmerged": [], + "cited_only": [ + { + "path": "frontiers/c7_total_bounded_20260929/PROOF.md", + "bytes": 14982, + "sha256": "16c0efe372c1b1f26460aaa109287fed78e6fbd2dd00a0530998db296278dd01", + "git_blob": "28748b086ec6761ef467dc67cba475fbdf8b7455", + "tag": "C7-K", + "use": "(K2): the rejected fold mass (Remark 1)" + }, + { + "path": "frontiers/remainder_rate_20260930/PROOF.md", + "bytes": 33131, + "sha256": "0b690df6ac40707ca06783f5641d8b480277c716df75b1031d84ee53a0575f72", + "git_blob": "abfb98ae41d66a86d3cb094162db6547d0f29e7e", + "tag": "198", + "use": "Math- #198 (merged): (3.1) and the sign window, through #220 (F1)" + } + ], + "cited_unmerged": [ + { + "path": "frontiers/candidate_parity_rate_20261001/PROOF.md", + "bytes": 53499, + "sha256": "9d58a29bf725d0756c8d11b5a9aa538782e83bee62242bcb1a869d2b95ccce94", + "git_blob": "a97bf528b4e073c6e12fd2d4616be77e8bbae16b", + "tag": "237", + "use": "Math- #237 (open): Lemma Pi (the expansion of Lemma Omega (a)), Lemma K and Lemma U (Remark 1), the cusp-scale statement after Lemma U (Remark 5), Remarks 3-4", + "head": "0add03bb806b6237e6aa0b29b06bedec54863e79", + "pr": "Math- #237" + }, + { + "path": "frontiers/d1_sharp_remainder_20261001/PROOF.md", + "bytes": 41236, + "sha256": "ab3ef0aff42ec75346c321f57d7b2048ccb28b00bdaf7bd6fa0fd64793a3ce7c", + "git_blob": "3b2ec970507d4703619362464a068ed489ba833b", + "tag": "238", + "use": "Math- #238 (open): Lemma W, the d = 1 form of Lemma Q-double-prime", + "head": "0582232ef5b458dc47cd15ff97bbd536cbed2f71", + "pr": "Math- #238" + }, + { + "path": "frontiers/third_order_coefficient_20261001/NOTE.md", + "bytes": 24186, + "sha256": "ae15c0ee173b9d01d258536a11780cc4b128c57811d1fb5db9db391ffc759ee5", + "git_blob": "aa078a9cbfc3aa859c089596892e34a8293831eb", + "tag": "216", + "use": "Math- #216 (open): the full-field Monte Carlo of the lifetime densities (Remark 4)", + "head": "04c08e1534122f210be888742fcd7a568e45b097", + "pr": "Math- #216" + } + ], + "cited_external": [ + { + "tag": "Bernstein", + "reference": "Bernstein-basis positivity on an interval (with bisection)", + "use": "control X2: exact certificates of the bounds |Psi2| <= 90 and |omega| <= 120 on |t| <= 1/96" + }, + { + "tag": "Haynsworth", + "reference": "E. V. Haynsworth, inertia additivity of the Schur complement (1968)", + "use": "through #218 Lemma C Step C1 (the typing rule in Case 1)" + } + ], + "mutants": { + "M1": "X3", + "M2": "X4", + "M3": "X5", + "M4": "X2", + "M5": "X1", + "M6": "X3", + "M7": "X6" + }, + "replayed": [ + "ecp_check.py" + ], + "referee": { + "kind": "one clean-context same-family referee (an Anthropic Claude subagent) before submission", + "verdict": "no BLOCKING error; one MAJOR finding (Step N2: the edge windows were integrated in f4 on an event that involves f4; repaired with the f4-free event G-double-prime) and eleven MINOR findings, all applied before submission", + "report": "project archive V2_2/frontiers_elder_cusp_parity_20261002/REFEREE_A.md", + "sha256": "68434ae46a9122728d61fa0975d5d783ebc50ebc7a4808980bb32768de0716d7", + "bytes": 7804, + "limits": "same provider and same GitHub account as the author: organizational-independence credit 0; not a nonauthor review" + }, + "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. Nothing is merged by its author.", + "files": [ + { + "path": "PROOF.md", + "bytes": 51848, + "sha256": "35b9c5943cf35919f2046ba194945ba759be654edf5d5ad77ba17b1f5c5377fd" + }, + { + "path": "README.md", + "bytes": 7376, + "sha256": "7443c5533d5f0e1039255f86f10eef0b5f13c9f0285094c57cff79281c6c83cc" + }, + { + "path": "ecp_check.py", + "bytes": 38573, + "sha256": "673c553c629cb09fdead24b7ae2a390ec55ed6a197007bc5e5c0e1c53525a177" + }, + { + "path": "RESULTS.json", + "bytes": 1636, + "sha256": "0ce8309e90b1c38870c04af3c4e7fb9a501f0551010ccae917eebbad76bf63dd" + } + ] +} diff --git a/frontiers/elder_cusp_parity_20261002/ecp_check.py b/frontiers/elder_cusp_parity_20261002/ecp_check.py new file mode 100644 index 000000000..82e8e035e --- /dev/null +++ b/frontiers/elder_cusp_parity_20261002/ecp_check.py @@ -0,0 +1,806 @@ +#!/usr/bin/env python3 +"""Exact controls for CL-ELDER-CUSP-PARITY-20261002-v1 (Lemma Q', Proposition CE++, Theorem N, Corollary N'). + +Standard library only; exact rationals throughout; deterministic (a fixed linear congruential generator). +Output: RESULTS.json (sorted keys), byte-identical under -O. Usage: + python3 -B -S ecp_check.py # exit 0, prints RESULTS.json + python3 -B -S ecp_check.py --mutant M3 # exit 1 (only its control fails) + unknown mutant label -> exit 2 + +Controls + X1 Lemma Q' and Proposition CE++: the polynomial bounds for eps0, eps1, eps2 (units C1 N r, in Gamma~ with + M~ = (35/8) Gamma~) and the constant 220; rho <= 4(1 + M~); the slack on |Xi| = R'; |q| >= lambda Gamma~^2 and + |tr(A^-1 B)| <= m ||B|| / lambda on random negative definite rational matrices (m = 1, 2, 3); the constants of the + sufficient conditions (2.3); kappa^2 r^(3/2) + kappa^3 r^2 <= 2r for kappa, r <= 1; the exponents of the 5/2-power step + X2 the model ridge g = 2(X + 1/2)^2 (X - 1) + 3 phi (X^2 - 1/4)^2 (kappa = 1): (M1) and (3.3) as identities; the new + cases phi > 1 and phi < -1 of Step Q6'; on J+- = {|phi -+ 1/3| <= 1/96} the constants c3 = 281/128 and c4, the + bounds on g(-3), g(2), g(-3/2), g(X3) and the brackets, by exact monotonicity; the expansions (3.4) with + |Psi2|, |Psi2^-| <= 90 and |omega_+-| <= 120 (exact Bernstein positivity on the interval) + X3 pinned polynomial fields: in d = 2, 3 with k = kappa r, the window field is P + r Q + O(r^2) and every monomial + r^a X^i Xi^j of F - P - r Q has a >= 2 and |j| <= a + 1; Math- #232's family (2.4) in window coordinates is + P + r Q + (r^2/4) X^2 Xi^T C Xi; Lemma Omega (a) in d = 2, 3, 4 at fixed k: the coefficients of r^0..r^3 of + det K_M, det K_S and -det K_M det K_S (odd coefficients of the product vanish) + X4 Lemma Omega (b)-(c): Delta J_B = Delta_B J - J B J (m = 1, 2, 3, including singular A); (4.2); P1 = Delta^2 Q1; + V_o = Delta Q1 + alpha4 Delta_B; Q(X, Xi*) = Q1 X (X^2 - 1/4)^2; the parities of Q1, P1, w0, q, z, Y' + X5 the first-order bookkeeping: w0(+-24 kappa) = 32 kappa^2 Delta^2; 12 k P1 = (kappa Delta^2/3) 36 r Q1; the edge + shift 36 r Q1 in z from r Q1/(2 kappa) in phi; the edge equations 12 kappa t -+ 6 r Q1 = 0; I'(0) = Psi/36 on + polynomial test densities (exact antiderivatives); the candidate kink window half-width 24 r |Q1| + X6 Corollary N' and the ledgers: the substitution r = l^(1/4) s; int_{r-}^{r+} r^2 dr <= kappa0^(-3/4) l^(3/4)/3; + Math- #229's ledger with and without the elder-only rows (least exponent 3/7 at rho_f = l^(2/7) in both); the + conditional ledger of Remark 1 (fold family balanced at 1/2, intermediate 4/9) +""" +import json +import sys +from fractions import Fraction as Fr +from itertools import product + +MUTANTS = ('M1', 'M2', 'M3', 'M4', 'M5', 'M6', 'M7') +MUT = None + + +# ----------------------------------------------------------------------------------------------- deterministic rationals +class LCG: + def __init__(self, seed): + self.s = seed % (2 ** 61 - 1) + + def nxt(self): + self.s = (self.s * 437799614237992725 + 1) % (2 ** 61 - 1) + return self.s + + def rat(self, num, den): + return Fr(self.nxt() % (2 * num + 1) - num, 1 + self.nxt() % den) + + +# ----------------------------------------------------------------------------------------------- polynomials in one variable +class RP: + """Polynomial in one variable (r, or t) with rational coefficients, ascending.""" + __slots__ = ('c',) + + def __init__(self, c=None): + c = [Fr(x) for x in (c or [])] + while c and c[-1] == 0: + c.pop() + self.c = c + + def __add__(self, o): + o = o if isinstance(o, RP) else RP([o]) + n = max(len(self.c), len(o.c)) + return RP([(self.c[i] if i < len(self.c) else 0) + (o.c[i] if i < len(o.c) else 0) for i in range(n)]) + + __radd__ = __add__ + + def __neg__(self): + return RP([-x for x in self.c]) + + def __sub__(self, o): + return self + (-(o if isinstance(o, RP) else RP([o]))) + + def __rsub__(self, o): + return RP([o]) - self + + def __mul__(self, o): + if not isinstance(o, RP): + return RP([x * o for x in self.c]) + if not self.c or not o.c: + return RP() + out = [Fr(0)] * (len(self.c) + len(o.c) - 1) + for i, a in enumerate(self.c): + if a: + for j, b in enumerate(o.c): + out[i + j] += a * b + return RP(out) + + __rmul__ = __mul__ + + def __pow__(self, n): + out = RP([1]) + for _ in range(n): + out = out * self + return out + + def co(self, n): + return self.c[n] if n < len(self.c) else Fr(0) + + def div_r(self, n=1): + if any(self.co(i) != 0 for i in range(n)): + raise ArithmeticError('not divisible by r^%d' % n) + return RP(self.c[n:]) + + def ev(self, x): + s = Fr(0) + for a in reversed(self.c): + s = s * x + a + return s + + def deriv(self): + return RP([i * self.c[i] for i in range(1, len(self.c))]) + + def integ(self): + return RP([0] + [self.c[i] / (i + 1) for i in range(len(self.c))]) + + def compose(self, q): + out = RP() + for a in reversed(self.c): + out = out * q + a + return out + + def even(self): + return all(self.co(i) == 0 for i in range(1, len(self.c), 2)) + + +T = RP([0, 1]) + + +def binom(n, k): + out = 1 + for i in range(k): + out = out * (n - i) // (i + 1) + return out + + +def bernstein_positive(p, a, b, depth=14): + """True if p > 0 on [a, b] is certified by positive Bernstein coefficients (with bisection).""" + q = p.compose(RP([a, b - a])) + n = max(len(q.c) - 1, 0) + coeffs = [sum((Fr(binom(j, i), binom(n, i)) * q.co(i) for i in range(j + 1)), Fr(0)) for j in range(n + 1)] + if all(x > 0 for x in coeffs): + return True + if coeffs[0] <= 0 or coeffs[-1] <= 0 or depth == 0: + return False + m = (a + b) / 2 + return bernstein_positive(p, a, m, depth - 1) and bernstein_positive(p, m, b, depth - 1) + + +def fact(n): + out = 1 + for i in range(2, n + 1): + out *= i + return out + + +def monomials(m, D, tmax=None): + out = [] + for tot in range(D + 1): + for a in range(tot + 1): + for bs in product(range(tot - a + 1), repeat=m): + if sum(bs) == tot - a and (tmax is None or sum(bs) <= tmax): + out.append((a,) + bs) + return out + + +_POW = {} + + +def xpow(x, n): + key = (tuple(x.c), n) + v = _POW.get(key) + if v is None: + v = RP([1]) if n == 0 else xpow(x, n - 1) * x + _POW[key] = v + return v + + +def dat(field, alpha, x): + """partial^alpha f at (x, 0, ..., 0); x an RP in r.""" + m = len(alpha) - 1 + tot = RP() + for mono, coef in field.items(): + if mono[0] < alpha[0] or any(mono[j] != alpha[j] for j in range(1, m + 1)): + continue + k = fact(mono[0]) // fact(mono[0] - alpha[0]) + for j in range(1, m + 1): + k *= fact(mono[j]) + tot = tot + coef * k * xpow(x, mono[0] - alpha[0]) + return tot + + +HALF, MHALF = RP([0, Fr(1, 2)]), RP([0, Fr(-1, 2)]) +SADDLE_M6 = RP([0, Fr(1, 2), 0, 0, 1]) # r/2 + r^4: an asymmetric displacement of the saddle (mutant M6) + + +def pinned(m): + e = lambda j: tuple(1 if i == j else 0 for i in range(m)) + return [(0,) + (0,) * m, (1,) + (0,) * m, (2,) + (0,) * m, (3,) + (0,) * m] + [(0,) + e(j) for j in range(m)] + [(1,) + e(j) for j in range(m)] + + +def row(field, m, i): + """[R] section 2's centred pin rows (0: midpoint height, 1: (f(+) - f(-))/r, 2: (f_x(+) - f_x(-))/r, 3: T_r, + then the m transverse averages and the m transverse differences), as RPs in r.""" + z = (0,) * m + f = lambda al, x: dat(field, al, x) + if i == 0: + return (f((0,) + z, MHALF) + f((0,) + z, HALF)) * Fr(1, 2) + if i in (1, 3): + R2 = (f((0,) + z, HALF) - f((0,) + z, MHALF)).div_r(1) + return R2 if i == 1 else ((f((1,) + z, MHALF) + f((1,) + z, HALF) - R2 * 2) * 6).div_r(2) + if i == 2: + return (f((1,) + z, HALF) - f((1,) + z, MHALF)).div_r(1) + j = i - 4 + ej = tuple(1 if t == j % m else 0 for t in range(m)) + if j < m: + return (f((0,) + ej, MHALF) + f((0,) + ej, HALF)) * Fr(1, 2) + return (f((0,) + ej, HALF) - f((0,) + ej, MHALF)).div_r(1) + + +def pin_field(free, m, tgt): + """Solve the pinned monomials (as RPs in r) for the target RPs tgt of the 4 + 2m rows.""" + pins = pinned(m) + field = {mo: RP([v]) for mo, v in free.items()} + for mo in pins: + field[mo] = RP() + order = [2, 0, 3, 1] + [4 + j for j in range(m)] + [4 + m + j for j in range(m)] + for _ in range(3): + for ri in order: + mo = pins[ri] + field[mo] = RP() + rest = row(field, m, ri) + field[mo] = RP([1]) + unit = row(field, m, ri) - rest + if len(unit.c) != 1 or unit.c[0] == 0: + raise ArithmeticError('row %d not unit-triangular' % ri) + field[mo] = (tgt[ri] - rest) * (1 / unit.c[0]) + chk = [row(field, m, i) for i in range(4 + 2 * m)] + if any((chk[i] - tgt[i]).c for i in range(len(chk))): + raise ArithmeticError('pins not satisfied') + return field + + +def rdet(M): + n = len(M) + if n == 1: + return M[0][0] + s = RP() + for j in range(n): + minor = [[M[i][jj] for jj in range(n) if jj != j] for i in range(1, n)] + t = M[0][j] * rdet(minor) + s = s + (t if j % 2 == 0 else -t) + return s + + +def hess(field, m, x): + d = m + 1 + H = [[None] * d for _ in range(d)] + for i in range(d): + for j in range(d): + al = [0] * d + al[i] += 1 + al[j] += 1 + H[i][j] = dat(field, tuple(al), x) + return H + + +def dets_of(field, m): + KM = rdet(hess(field, m, MHALF)).div_r(1) + KS = rdet(hess(field, m, HALF if MUT != 'M6' else SADDLE_M6)).div_r(1) + return -(KM * KS), KM, KS + + +# ----------------------------------------------------------------------------------------------- matrices over Q +def mdet(M): + n = len(M) + if n == 0: + return Fr(1) + if n == 1: + return M[0][0] + s = Fr(0) + for j in range(n): + minor = [[M[i][jj] for jj in range(n) if jj != j] for i in range(1, n)] + s += (-1) ** j * M[0][j] * mdet(minor) + return s + + +def madj(M): + n = len(M) + if n == 1: + return [[Fr(1)]] + return [[(-1) ** (i + j) * mdet([[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 mmul(A, B): + return [[sum((A[i][k] * B[k][j] for k in range(len(B))), Fr(0)) for j in range(len(B[0]))] for i in range(len(A))] + + +def mvec(A, v): + return [sum((A[i][k] * v[k] for k in range(len(v))), Fr(0)) for i in range(len(A))] + + +def dot(u, v): + return sum((a * b for a, b in zip(u, v)), Fr(0)) + + +def quad(u, M, v): + return dot(u, mvec(M, v)) + + +def minv(M): + D = mdet(M) + return [[x / D for x in row_] for row_ in madj(M)] + + +def jets_of(field, m): + g = lambda mono: field[mono].co(0) if mono in field else Fr(0) + e = lambda j: tuple(1 if i == j else 0 for i in range(m)) + + def sym(xp, md, mo): + return [[(md * g((xp,) + tuple(2 if t == i else 0 for t in range(m))) if i == j else + mo * g((xp,) + tuple(1 if t in (i, j) else 0 for t in range(m)))) for j in range(m)] for i in range(m)] + return (sym(0, 2, 1), sym(1, 2, 1), sym(2, 4, 2), [2 * g((2,) + e(j)) for j in range(m)], + [6 * g((3,) + e(j)) for j in range(m)], 24 * g((4,) + (0,) * m), 120 * g((5,) + (0,) * m)) + + +def det_adj_t(A, B): + """det(A + tB) and adj(A + tB) as RPs in t.""" + m = len(A) + M = [[RP([A[i][j], B[i][j]]) for j in range(m)] for i in range(m)] + if m == 1: + return M[0][0], [[RP([1])]] + adj = [[rdet([[M[a][b] for b in range(m) if b != i] for a in range(m) if a != j]) * (-1) ** (i + j) + for j in range(m)] for i in range(m)] + return rdet(M), adj + + +def UVparts(A, B, C, gam, eta, f4, f5, k): + """Delta, Delta_B, Delta_C, Delta_BB, J, J_B, Y', U, V of Lemma Omega (#232 (2.2)).""" + dt, at = det_adj_t(A, B) + D, DB, DBB = dt.co(0), dt.co(1), 2 * dt.co(2) + J = [[x.co(0) for x in row_] for row_ in at] + JB = [[x.co(1) for x in row_] for row_ in at] + m = len(A) + DC = sum((J[i][j] * C[j][i] for i in range(m) for j in range(m)), Fr(0)) + Yp = f4 / 12 * D - quad(gam, J, gam) / 4 + U = Yp + 3 * k * DB + V = (Fr(3, 4) * k * (DC + DBB) + f4 / 24 * DB + f5 / 120 * D - quad(gam, J, eta) / 12 - quad(gam, JB, gam) / 8) + return D, DB, DC, DBB, J, JB, Yp, U, V + + +# ----------------------------------------------------------------------------------------------- X1 +def control_X1(): + ok = True + G = RP([0, 1]) # Gamma~ + Mt = G * Fr(35, 8) # M~ + one = RP([1]) + gbar = one + Mt # gbar / (C1 N r) + eps0 = (one + Mt) * (one + Mt) * 4 + eps1 = (one + Mt) * (one + Mt) * 4 + G * gbar * 6 + beta = gbar * 2 + eps2 = (gbar * 2 + G * gbar * 2) + beta * G * 12 + beta * (one + Mt) * 2 + G * G * 18 + const = 220 if MUT != 'M5' else 200 + bound = (one + G) * (one + G) * const + ok &= eps0.c == [4, 35, Fr(1225, 16)] and eps1.c == [4, 41, Fr(1645, 16)] and eps2.c == [6, Fr(279, 4), Fr(3333, 16)] + ok &= all(bound.co(i) >= e.co(i) for e in (eps0, eps1, eps2) for i in range(3)) + # rho = max(1, 8 gbar/lambda) <= 4(1 + M~) when lambda >= 2 C1 N r; ball radius M~ + rho <= 5 M~ + 4; slack on |Xi| = R' + ok &= 8 * Fr(1, 2) == 4 # 8 C1 N r (1 + M~) / (2 C1 N r) = 4 (1 + M~) + for g in (Fr(0), Fr(1, 3), Fr(5), Fr(40)): + m_ = Fr(35, 8) * g + ok &= m_ + 4 * (1 + m_) == 5 * m_ + 4 and (5 * m_ + 4) - (2 * m_ + 1) >= 0 and 5 * m_ + 4 <= 5 * (1 + m_) + # |q| >= lambda0 |A^-1 gamma|^2 and tr(A^-1 B)^2 lambda0^2 <= m^2 ||B||_F^2 for A = -(lambda0 I + M^T M) + rng = LCG(20261002) + for m in (1, 2, 3): + for _ in range(6): + lam0 = Fr(1 + rng.nxt() % 5, 1 + rng.nxt() % 4) + Mm = [[rng.rat(5, 3) for _ in range(m)] for _ in range(m)] + MtM = mmul([list(x) for x in zip(*Mm)], Mm) + A = [[-(lam0 if i == j else 0) - MtM[i][j] for j in range(m)] for i in range(m)] + B0 = [[rng.rat(5, 3) for _ in range(m)] for _ in range(m)] + B = [[(B0[i][j] + B0[j][i]) / 2 for j in range(m)] for i in range(m)] + gam = [rng.rat(6, 4) for _ in range(m)] + Ai = minv(A) + v = mvec(Ai, gam) + q = dot(gam, v) + ok &= -q >= lam0 * dot(v, v) + tr = sum((mmul(Ai, B)[i][i] for i in range(m)), Fr(0)) + ok &= tr * tr * lam0 * lam0 <= m * m * sum((B[i][j] ** 2 for i in range(m) for j in range(m)), Fr(0)) + # constants of the sufficient conditions (2.3) and of (Q'3) in section 2 + ok &= 3 * 6 == 18 and 4 * 12 == 48 and 5 * Fr(35, 8) * 12 == Fr(525, 2) + ok &= (18 ** 2) * 2 == 648 # (18^(2/3) 2^(1/3))^3 = 18^2 * 2 = (18 sqrt 2)^2 + ok &= 10 * Fr(35, 8) * 16 == 700 and 6 * 16 == 96 and 5 * Fr(35, 8) * 2 == Fr(175, 4) + ok &= 220 * 2 * 8 == 3520 and Fr(7040, 3) <= 2347 and 12 * 7040 == 84480 + # kappa^2 r^(3/2) + kappa^3 r^2 <= 2 r for kappa, r <= 1 (r = s^2) + for kap, s in product([Fr(i, 7) for i in range(0, 8)], [Fr(i, 9) for i in range(1, 10)]): + r = s * s + ok &= kap ** 2 * r * s + kap ** 3 * r * r <= 2 * r + # the 5/2-power step: kappa^2 lambda^2 (t1 f4/(kappa lambda))^(5/2) = kappa^(-1/2) t1^(5/2) f4^(5/2) lambda^(-1/2) + ok &= Fr(2) - Fr(5, 2) == Fr(-1, 2) and Fr(-1, 2) * Fr(3, 2) == Fr(-3, 4) + return ok, {'eps0': [str(x) for x in eps0.c], 'eps1': [str(x) for x in eps1.c], 'eps2': [str(x) for x in eps2.c], + 'constant': const} + + +# ----------------------------------------------------------------------------------------------- X2 +def g_model(phi, X): + return 2 * (X + Fr(1, 2)) ** 2 * (X - 1) + 3 * phi * (X * X - Fr(1, 4)) ** 2 + + +def control_X2(): + ok = True + grid = [Fr(i, 7) for i in range(-25, 18)] + phis = [Fr(i, 5) for i in range(-9, 10) if i != 0] + for phi, X in product(phis, grid): + g = g_model(phi, X) + ok &= g + 1 == (X - Fr(1, 2)) ** 2 * (2 * (X + 1) + 3 * phi * (X + Fr(1, 2)) ** 2) + ok &= g == (X + Fr(1, 2)) ** 2 * (2 * (X - 1) + 3 * phi * (X - Fr(1, 2)) ** 2) + for phi in phis + [Fr(31, 96), Fr(33, 96), Fr(-31, 96), Fr(-33, 96)]: + X3 = -1 / (2 * phi) + ok &= g_model(phi, X3) + 1 == (phi + 1) ** 3 * (3 * phi - 1) / (16 * phi ** 3) + ok &= g_model(phi, X3) == (phi - 1) ** 3 * (3 * phi + 1) / (16 * phi ** 3) + ok &= 1 + 2 * phi * X3 == 0 + # derivative g' = 6 (X^2 - 1/4)(1 + 2 phi X) (as a polynomial identity in X at rational phi) + for phi in phis: + gp = (RP([Fr(1, 2), 1]) ** 2 * RP([-1, 1]) * 2 + RP([Fr(-1, 4), 0, 1]) ** 2 * (3 * phi)).deriv() + ok &= not (gp - RP([Fr(-1, 4), 0, 1]) * RP([1, 2 * phi]) * 6).c + # new cases of Step Q6'. phi > 1: on [-3, -1/2], X^2 - 1/4 >= 0 and 1 + 2 phi X <= 1 - phi < 0 (corners suffice: + # 1 + 2 phi X is bilinear); g(-3) = -50 + (3675/16) phi > 179 at phi = 1 and increasing. + for phi, X in product((Fr(1), Fr(5), Fr(10 ** 6)), (Fr(-3), Fr(-1, 2))): + ok &= 1 + 2 * phi * X <= 1 - phi + ok &= g_model(Fr(1), Fr(-3)) == -50 + Fr(3675, 16) and -50 + Fr(3675, 16) > 179 + # phi < -1: bracket 2(X + 1) + 3 phi (X + 1/2)^2 <= -(3X^2 + X - 5/4) <= 0 on [1/2, 2] + brk = RP([Fr(-5, 4), 1, 3]) + ok &= brk.ev(Fr(1, 2)) == 0 and all(brk.deriv().ev(X) > 0 for X in (Fr(1, 2), Fr(2))) # derivative 6X + 1, linear + ok &= -5 + 12 * Fr(-1) == -17 and Fr(25, 2) + Fr(675, 16) * Fr(-1) < Fr(-29) + # J+ = [31/96, 33/96]: c3, X3, g', c4, g(-3), the bracket beta <= -1/2 on [X3, 1/2], g(-5/4) <= -9/32 + Jp = (Fr(31, 96), Fr(33, 96)) + Jm = (Fr(-33, 96), Fr(-31, 96)) + c3 = Fr(281, 128) + for phi, X in product(Jp, (Fr(-3), Fr(-5, 4))): + ok &= 12 * phi * X + 2 < 0 # g''/6 decreasing in X (bilinear: corners) + ok &= 6 * Fr(-5, 4) ** 2 - Fr(1, 2) > 0 # g''/6 increasing in phi for |X| >= 5/4 + v = 6 * Jp[0] * Fr(25, 16) + 2 * Fr(-5, 4) - Jp[0] / 2 + ok &= v == Fr(281, 768) and 6 * v == c3 + ok &= -1 / (2 * Jp[0]) == Fr(-48, 31) and -1 / (2 * Jp[1]) == Fr(-16, 11) and Fr(-3) < Fr(-48, 31) and Fr(-16, 11) < Fr(-5, 4) + c4 = c3 / 2 * (Fr(16, 11) - Fr(5, 4)) ** 2 + ok &= Fr(16, 11) - Fr(5, 4) == Fr(9, 44) and c4 == c3 / 2 * Fr(81, 1936) and Fr(1, 200) < c4 / 2 + ok &= -50 + Fr(3675, 16) * Jp[0] >= 24 + for phi in Jp: + X3 = -1 / (2 * phi) + beta = 2 * (X3 - 1) + 3 * phi * (X3 - Fr(1, 2)) ** 2 + ok &= beta == (3 * phi + 1) * (phi - 1) / (4 * phi) and beta <= Fr(-1, 2) and 3 * phi * phi <= 1 + ok &= 2 * (Fr(1, 2) - 1) + 0 == -1 # beta(1/2) = -1; beta convex in X (beta'' = 6 phi > 0) + ok &= -Fr(1, 2) * (Fr(-5, 4) + Fr(1, 2)) ** 2 == Fr(-9, 32) + ok &= Fr(25, 2) + Fr(675, 16) * Fr(-1, 4) >= Fr(125, 64) # g(2) >= 125/64 for phi >= -1/4 (#220 (M5)) + # J- = [-33/96, -31/96]: mirror statements + for phi, X in product(Jm, (Fr(5, 4), Fr(2))): + ok &= 12 * phi * X + 2 < 0 + vm = 6 * Jm[1] * Fr(25, 16) + 2 * Fr(5, 4) - Jm[1] / 2 + ok &= vm == Fr(-281, 768) + ok &= -1 / (2 * Jm[1]) == Fr(48, 31) and -1 / (2 * Jm[0]) == Fr(16, 11) and Fr(5, 4) < Fr(16, 11) and Fr(48, 31) < 2 + ok &= Fr(25, 2) + Fr(675, 16) * Jm[1] <= Fr(-112, 100) + ok &= -5 + 12 * Jm[1] <= -7 + for phi in Jm: + X3 = -1 / (2 * phi) + bp = 2 * (X3 + 1) + 3 * phi * (X3 + Fr(1, 2)) ** 2 + ok &= bp == (3 * phi - 1) * (phi + 1) / (4 * phi) and bp >= Fr(1, 2) and 3 * phi * phi <= 1 + ok &= abs(g_model(phi, X3)) <= Fr(1, 7) + # (3.4): Psi(1/3 + t) = 12 t + Psi2 t^2, Psi_-(-1/3 + t) = 12 t + Psi2^- t^2, X3 (X3^2 - 1/4)^2 = -+6 + omega t + lo, hi = Fr(-1, 96), Fr(1, 96) + cpsi = 90 + comg = 120 if MUT != 'M4' else 100 + fits = {} + for sgn in (1, -1): + a = RP([sgn * Fr(4, 3), 1]) # phi + 1 = +-4/3 + t ... (for sgn = -1: phi - 1 = -4/3 + t) + d = RP([sgn * Fr(1, 3), 1]) # phi = +-1/3 + t + M_ = a ** 3 * 3 - d ** 3 * 192 # Psi - 12 t = t M_ / (16 d^3) + M1 = M_.div_r(1) + den = d ** 3 * 16 + s_ = 1 if sgn == 1 else -1 # sign of den on the interval + ok &= bernstein_positive(den * (s_ * cpsi) - M1, lo, hi) and bernstein_positive(den * (s_ * cpsi) + M1, lo, hi) + # check the identity at sample points: Psi(+-1/3 + t) = 12 t + t^2 M1/den + for t in (Fr(1, 200), Fr(-1, 150)): + phi = sgn * Fr(1, 3) + t + Psi = ((phi + 1) ** 3 * (3 * phi - 1) / (16 * phi ** 3)) if sgn == 1 else ((phi - 1) ** 3 * (3 * phi + 1) / (16 * phi ** 3)) + ok &= Psi == 12 * t + t * t * M1.ev(t) / den.ev(t) + fits['Psi2_at_0' if sgn == 1 else 'Psi2m_at_0'] = str(M1.ev(Fr(0)) / den.ev(Fr(0))) + # omega: X3 = -1/(2 phi) = -+3/(2 +- 6 t) ... computed as X3 = -sgn*3/(2 + sgn*6t) + base = RP([2, sgn * 6]) # 2 + 6t (sgn = 1) or 2 - 6t (sgn = -1) + inner = RP([8, -sgn * 6, -9]) # 8 -+ 6t - 9t^2 + Nw = base ** 5 * 6 - inner ** 2 * 3 # (sgn = 1): t omega (2 + 6t)^5 = 6 base^5 - 3 inner^2 + if sgn == -1: + Nw = -Nw # (sgn = -1): t omega (2 - 6t)^5 = 3 inner^2 - 6 base^5 + N1 = Nw.div_r(1) + ok &= bernstein_positive(base ** 5 * comg - N1, lo, hi) and bernstein_positive(base ** 5 * comg + N1, lo, hi) + for t in (Fr(1, 200), Fr(-1, 150)): + phi = sgn * Fr(1, 3) + t + X3 = -1 / (2 * phi) + ok &= X3 * (X3 * X3 - Fr(1, 4)) ** 2 == -sgn * 6 + t * N1.ev(t) / base.ev(t) ** 5 + fits['omega_at_0' if sgn == 1 else 'omegam_at_0'] = str(N1.ev(Fr(0)) / base.ev(Fr(0)) ** 5) + ok &= fits['Psi2_at_0'] == '-81' and fits['Psi2m_at_0'] == '81' and fits['omega_at_0'] == '99' and fits['omegam_at_0'] == '99' + ok &= cpsi * Fr(1, 96) <= 1 and comg * Fr(1, 200) <= 1 # 90 kappa t^2 <= kappa |t|; 120 r |Q1| <= kappa + return ok, {'c3': str(c3), 'c4': str(c4), 'delta_e': '1/96', 'c_e': '1/200', 'Psi2_bound': cpsi, 'omega_bound': comg, + 'second_order_coefficients': fits} + + +# ----------------------------------------------------------------------------------------------- X3 +def window_terms(field, m): + """r^-4 (f(rX, r^2 Xi) - f(M)) as {(power of r, i, j-tuple): coefficient}; f(M) = f(-r/2, 0).""" + out = {} + for mono, coef in field.items(): + a, bs = mono[0], mono[1:] + for n, c in enumerate(coef.c): + if c: + key = (n + a + 2 * sum(bs) - 4, a, bs) + out[key] = out.get(key, 0) + c + fM = dat(field, (0,) * (m + 1), MHALF) + for n, c in enumerate(fM.c): + if c: + key = (n - 4, 0, (0,) * m) + out[key] = out.get(key, 0) - c + return {k: v for k, v in out.items() if v != 0} + + +def model_terms(m, kap, A, B, C, gam, eta, f4, f5, with_C=False, mutQ=False): + """P + r Q (+ (r^2/4) X^2 Xi^T C Xi) as {(power of r, i, j-tuple): coefficient}.""" + z = (0,) * m + e = lambda j: tuple(1 if t == j else 0 for t in range(m)) + ee = lambda i, j: tuple((1 if t == i else 0) + (1 if t == j else 0) for t in range(m)) + out = {} + + def add(key, v): + if v: + out[key] = out.get(key, 0) + v + for (i, c) in ((3, 2 * kap), (1, -Fr(3, 2) * kap), (0, -kap / 2)): # 2 kappa (X + 1/2)^2 (X - 1) + add((0, i, z), c) + for (i, c) in ((4, 1), (2, Fr(-1, 2)), (0, Fr(1, 16))): # (f4/24)(X^2 - 1/4)^2 + add((0, i, z), f4 / 24 * c) + for j in range(m): + add((0, 2, e(j)), gam[j] / 2) + add((0, 0, e(j)), -gam[j] / 8) + for jj in range(m): + add((0, 0, ee(j, jj)), A[j][jj] / 2) + q5 = f5 / 120 if not mutQ else f5 / 60 + for (i, c) in ((5, 1), (3, Fr(-1, 2)), (1, Fr(1, 16))): # (f5/120) X (X^2 - 1/4)^2 + add((1, i, z), q5 * c) + for j in range(m): + add((1, 3, e(j)), eta[j] / 6) + add((1, 1, e(j)), -eta[j] / 24) + for jj in range(m): + add((1, 1, ee(j, jj)), B[j][jj] / 2) + if with_C: + add((2, 2, ee(j, jj)), C[j][jj] / 4) + return {k: v for k, v in out.items() if v != 0} + + +def control_X3(): + ok = True + nwin = 0 + rng = LCG(20261003) + # (i) window fields of pinned polynomial fields with k = kappa r (d = 2, 3) + for m, deg, trials in ((1, 9, 3), (2, 8, 2)): + pins = set(pinned(m)) + for _ in range(trials): + free = {mo: rng.rat(9, 5) for mo in monomials(m, deg) if mo not in pins} + kap = Fr(1 + rng.nxt() % 7, 1 + rng.nxt() % 3) + bp = rng.rat(5, 3) + tgt = [RP([bp]), RP([0, 0, 0, -kap]), RP(), RP([0, 12 * kap])] + [RP()] * (2 * m) + fld = pin_field(free, m, tgt) + A, B, C, gam, eta, f4, f5 = jets_of(fld, m) + W = window_terms(fld, m) + ok &= all(k[0] >= 0 for k in W) + Mdl = model_terms(m, kap, A, B, C, gam, eta, f4, f5, mutQ=(MUT == 'M1')) + for k_, v in Mdl.items(): + if W.get(k_, 0) != v: + ok = False + for k_, v in W.items(): + if k_[0] <= 1 and Mdl.get(k_, 0) != v: + ok = False + if k_[0] >= 2: + ok &= sum(k_[2]) <= k_[0] + 1 + nwin += 1 + # (ii) Math- #232's family (2.4) in window coordinates (d = 2, 3), and its pins + for m in (1, 2): + for _ in range(2): + kap = Fr(1 + rng.nxt() % 5, 2) + f4, f5 = rng.rat(7, 3), rng.rat(7, 3) + gam = [rng.rat(5, 3) for _ in range(m)] + eta = [rng.rat(5, 3) for _ in range(m)] + sym = lambda: (lambda M0: [[(M0[i][j] + M0[j][i]) / 2 for j in range(m)] for i in range(m)])([[rng.rat(5, 3) for _ in range(m)] for _ in range(m)]) + A, B, C = sym(), sym(), sym() + # f(x, y) = 2k(x - r)(x + r/2)^2 + (f4/24)(x^2 - r^2/4)^2 + (f5/120) x (x^2 - r^2/4)^2 + # + sum_i y_i [(gam_i/2)(x^2 - r^2/4) + (eta_i/6) x (x^2 - r^2/4)] + (1/2) y^T [A + x B + (x^2/2) C] y + fld = {} + z = (0,) * m + e = lambda j: tuple(1 if t == j else 0 for t in range(m)) + ee = lambda i, j: tuple((1 if t == i else 0) + (1 if t == j else 0) for t in range(m)) + + def add(mono, rp): + fld[mono] = fld.get(mono, RP()) + rp + k = RP([0, kap]) # k = kappa r + # 2k (x - r)(x + r/2)^2 = 2k (x^3 - (3/4) r^2 x - r^3/4) + add((3,) + z, k * 2) + add((1,) + z, k * RP([0, 0, Fr(-3, 2)])) + add((0,) + z, k * RP([0, 0, 0, Fr(-1, 2)])) + add((4,) + z, RP([f4 / 24])) + add((2,) + z, RP([0, 0, -f4 / 48])) + add((0,) + z, RP([0, 0, 0, 0, f4 / 384])) + add((5,) + z, RP([f5 / 120])) + add((3,) + z, RP([0, 0, -f5 / 240])) + add((1,) + z, RP([0, 0, 0, 0, f5 / 1920])) + for j in range(m): + add((2,) + e(j), RP([gam[j] / 2])) + add((0,) + e(j), RP([0, 0, -gam[j] / 8])) + add((3,) + e(j), RP([eta[j] / 6])) + add((1,) + e(j), RP([0, 0, -eta[j] / 24])) + for jj in range(m): + mult = Fr(1, 2) + add((0,) + ee(j, jj), RP([A[j][jj] * mult])) + add((1,) + ee(j, jj), RP([B[j][jj] * mult])) + add((2,) + ee(j, jj), RP([C[j][jj] * mult / 2])) + # pins: f(M) = 0, f(S) = -k r^3, gradients zero at both + ok &= not dat(fld, (0,) * (m + 1), MHALF).c + ok &= not (dat(fld, (0,) * (m + 1), HALF) + RP([0, kap]) * RP([0, 0, 0, 1])).c + for i in range(m + 1): + al = tuple(1 if t == i else 0 for t in range(m + 1)) + ok &= not dat(fld, al, MHALF).c and not dat(fld, al, HALF).c + W = window_terms(fld, m) + Mdl = model_terms(m, kap, A, B, C, gam, eta, f4, f5, with_C=True, mutQ=(MUT == 'M1')) + ok &= W == Mdl + nwin += 1 + # (iii) Lemma Omega (a) at fixed k (d = 2, 3, 4) + nom = 0 + for m, deg, trials, tmax in ((1, 9, 3, None), (2, 8, 2, None), (3, 9, 1, 2)): + pins = set(pinned(m)) + for _ in range(trials): + free = {mo: rng.rat(9, 5) for mo in monomials(m, deg, tmax) if mo not in pins} + k = rng.rat(6, 4) + if k == 0: + k = Fr(1, 3) + bp = rng.rat(5, 3) + tgt = [RP([bp]), RP([0, 0, -k]), RP(), RP([12 * k])] + [RP()] * (2 * m) + fld = pin_field(free, m, tgt) + Pi, KM, KS = dets_of(fld, m) + A, B, C, gam, eta, f4, f5 = jets_of(fld, m) + D, DB, DC, DBB, J, JB, Yp, U, V = UVparts(A, B, C, gam, eta, f4, f5, k) + ok &= KM.co(0) == -6 * k * D and KS.co(0) == 6 * k * D + ok &= KM.co(1) == U and KS.co(1) == U and KM.co(2) == -V and KS.co(2) == V + ok &= Pi.co(0) == 36 * k * k * D * D and Pi.co(1) == 0 and Pi.co(2) == 12 * k * D * V - U * U and Pi.co(3) == 0 + ok &= Pi.even() + nom += 1 + return ok, nwin, nom + + +# ----------------------------------------------------------------------------------------------- X4 +def control_X4(): + ok = True + rng = LCG(20261004) + n = 0 + for m in (1, 2, 3): + for trial in range(8): + sym = lambda: (lambda M0: [[(M0[i][j] + M0[j][i]) / 2 for j in range(m)] for i in range(m)])([[rng.rat(6, 4) for _ in range(m)] for _ in range(m)]) + A, B, C = sym(), sym(), sym() + if trial == 0 and m >= 2: # a singular A + A[0] = [Fr(0)] * m + for i in range(m): + A[i][0] = Fr(0) + gam = [rng.rat(6, 4) for _ in range(m)] + eta = [rng.rat(6, 4) for _ in range(m)] + f4, f5, k, kap = rng.rat(9, 4), rng.rat(9, 4), rng.rat(5, 4), rng.rat(5, 2) + D, DB, DC, DBB, J, JB, Yp, U, V = UVparts(A, B, C, gam, eta, f4, f5, k) + JBJ = mmul(mmul(J, B), J) + ok &= all(D * JB[i][j] == DB * J[i][j] - JBJ[i][j] for i in range(m) for j in range(m)) + P1 = D * D / 120 * f5 - D / 12 * quad(gam, J, eta) + quad(gam, JBJ, gam) / 8 + w0 = 36 * kap * kap * D * D - Yp * Yp + ok &= 36 * kap * kap * D * D + 12 * k * D * V - U * U == w0 + 12 * k * P1 + 9 * k * k * (D * (DC + DBB) - DB * DB) + Vo = V - Fr(3, 4) * k * (DC + DBB) + ok &= 12 * D * Vo - 6 * Yp * DB == 12 * P1 + if D != 0: + Ai = minv(A) + sgnQ = 1 if MUT != 'M2' else -1 + Q1 = f5 / 120 - sgnQ * quad(eta, Ai, gam) / 12 + quad(gam, mmul(mmul(Ai, B), Ai), gam) / 8 + ok &= P1 == D * D * Q1 + q = quad(gam, Ai, gam) + alpha4 = (f4 - 3 * q) / 24 + ok &= Vo == D * Q1 + alpha4 * DB and Yp == 2 * D * alpha4 + # Q(X, Xi*) = Q1 X (X^2 - 1/4)^2 with Xi* = -(1/2)(X^2 - 1/4) A^-1 gamma + for X in (Fr(-3), Fr(-3, 2), Fr(1, 3), Fr(2)): + s = X * X - Fr(1, 4) + xi = [-s / 2 * x for x in mvec(Ai, gam)] + Qv = f5 / 120 * X * s * s + X * s / 6 * dot(eta, xi) + X / 2 * quad(xi, B, xi) + ok &= Qv == Q1 * X * s * s + # parities: (gamma, B, f5) -> -(...), (A, C, eta, f4) fixed + nB = [[-x for x in row_] for row_ in B] + D2, DB2, DC2, DBB2, J2, JB2, Yp2, U2, V2 = UVparts(A, nB, C, [-x for x in gam], eta, f4, -f5, k) + Q1n = -f5 / 120 - sgnQ * quad(eta, Ai, [-x for x in gam]) / 12 + quad([-x for x in gam], mmul(mmul(Ai, nB), Ai), [-x for x in gam]) / 8 + P1n = D2 * D2 / 120 * (-f5) - D2 / 12 * quad([-x for x in gam], J2, eta) + quad([-x for x in gam], mmul(mmul(J2, nB), J2), [-x for x in gam]) / 8 + qn = quad([-x for x in gam], Ai, [-x for x in gam]) + ok &= Q1n == -Q1 and P1n == -P1 and qn == q and Yp2 == Yp and D2 == D + n += 1 + return ok, n + + +# ----------------------------------------------------------------------------------------------- X5 +def control_X5(): + ok = True + rng = LCG(20261005) + shift = 36 if MUT != 'M3' else 18 + for _ in range(6): + kap, D, r, Q1 = Fr(1 + rng.nxt() % 9, 1 + rng.nxt() % 4), rng.rat(7, 3), Fr(1, 1 + rng.nxt() % 50), rng.rat(9, 4) + if D == 0: + D = Fr(2, 3) + k = kap * r + w0 = lambda z: D * D / 144 * (5184 * kap * kap - z * z) + ok &= w0(24 * kap) == 32 * kap * kap * D * D and w0(-24 * kap) == 32 * kap * kap * D * D + ok &= 12 * k * (D * D * Q1) == kap * D * D / 3 * (36 * r * Q1) + # edge shift: phi = 1/3 + r Q1/(2 kappa) <=> z = 72 kappa phi = 24 kappa + shift r Q1 + ok &= 72 * kap * (Fr(1, 3) + r * Q1 / (2 * kap)) == 24 * kap + shift * r * Q1 + # edge equations 12 kappa t + Psi... linear parts: 12 kappa t - 6 r Q1 = 0 (J+) and 12 kappa t + 6 r Q1 = 0 (J-) + ok &= 12 * kap * (r * Q1 / (2 * kap)) - 6 * r * Q1 == 0 and 12 * kap * (-r * Q1 / (2 * kap)) + 6 * r * Q1 == 0 + # I'(0) = Psi/36 on a polynomial test density p (exact antiderivatives) + p = RP([rng.rat(5, 3) for _ in range(5)]) + S = RP([0, 1]) # s + upper = RP([24 * kap, 1]) # 24 kappa + s + integrand = (RP([5184 * kap * kap, 0, -1]) * (D * D / 144)) * p # w0(z) p(z) as a polynomial in z + F1 = integrand.integ() + F0 = p.integ() + I = (F1.compose(upper) - F1.compose(-upper)) + S * (kap * D * D / 3) * (F0.compose(upper) - F0.compose(-upper)) + Ip0 = I.co(1) + Psi = 1152 * kap * kap * D * D * (p.ev(24 * kap) + p.ev(-24 * kap)) + 12 * kap * D * D * (F0.ev(24 * kap) - F0.ev(-24 * kap)) + ok &= Ip0 == Psi / 36 + # candidate kink: |w0| <= 12 k |P1| => |72 kappa - |z|| <= 24 r |Q1| (since 72 kappa + |z| >= 72 kappa) + ok &= Fr(1728) / 72 == 24 and 12 * 144 == 1728 + return ok + + +# ----------------------------------------------------------------------------------------------- X6 +def control_X6(): + ok = True + # substitution r = l^(1/4) s: l/r^4 = s^-4; r- = (l/kappa1)^(1/4) <-> s = kappa1^(-1/4); dr = l^(1/4) ds + ok &= Fr(1, 4) * 4 == 1 + # int_{r-}^{r+} r^2 dr = (r+^3 - r-^3)/3 <= r+^3/3 = kappa0^(-3/4) l^(3/4)/3 (checked at l = c^4, kappa = d^4) + for c, d0, d1 in ((Fr(1, 10), Fr(1, 2), Fr(2)), (Fr(1, 3), Fr(1), Fr(3))): + l = c ** 4 + rp, rm = c / d0, c / d1 # (l/kappa0)^(1/4), (l/kappa1)^(1/4) + ok &= (rp ** 3 - rm ** 3) / 3 <= rp ** 3 / 3 and rp ** 3 == (c ** 3) / d0 ** 3 + # Math- #229's ledger at rho_f = l^(2/7), rho_c = l^(2/9), a = l^(1/9) + sf = Fr(2, 7) if MUT != 'M7' else Fr(1, 4) + sc, sa = Fr(2, 9), Fr(1, 9) + rows_ = {'rho_f^5/l': 5 * sf - 1, 'l rho_f^-2': 1 - 2 * sf, 'l^2 rho_f^-11/2 (elder only)': 2 - Fr(11, 2) * sf, + 'l^3 rho_f^-9 (elder only)': 3 - 9 * sf, 'rho_f^2': 2 * sf, 'rho_c^2': 2 * sc, 'l^2 rho_c^-7': 2 - 7 * sc, + 'a^4 log': 4 * sa, 'l^(2/3) a^-2': Fr(2, 3) - 2 * sa, 'l^3 rho_c^-11 log': 3 - 11 * sc, 'l rho_c^-2': 1 - 2 * sc, + 'rho_c^3': 3 * sc, 'l^(5/3) a^-7': Fr(5, 3) - 7 * sa, 'l': Fr(1)} + least_with = min(rows_.values()) + without = {k: v for k, v in rows_.items() if 'elder only' not in k} + least_without = min(without.values()) + ok &= least_with == Fr(3, 7) and least_without == Fr(3, 7) + ok &= sorted(k for k, v in without.items() if v == least_without) == ['l rho_f^-2', 'rho_f^5/l'] + # the conditional ledger of Remark 1: uniform (r^2 + k^2) on r <= kappa <= 1/r, rho_c = l^(1/5), Lemma K + tf, tc = Fr(3, 10), Fr(1, 5) + cond = {'rho_f^5/l': 5 * tf - 1, 'l^2 rho_f^-5': 2 - 5 * tf, 'rho_f^2': 2 * tf, 'rho_c^3': 3 * tc, + 'l^2 rho_c^-7': 2 - 7 * tc, 'l^3 rho_c^-11 log': 3 - 11 * tc, 'l rho_c^-2': 1 - 2 * tc, + 'a^4 log (intermediate)': 4 * sa, 'l^(2/3) a^-2 (intermediate)': Fr(2, 3) - 2 * sa} + ok &= cond['rho_f^5/l'] == cond['l^2 rho_f^-5'] == Fr(1, 2) + ok &= min(cond.values()) == Fr(4, 9) and Fr(1) / 5 == tc + # the fold-family pair alone cannot exceed 1/2: max over sigma of min(5 sigma - 1, 2 - 5 sigma) is 1/2 + grid = [Fr(i, 600) for i in range(120, 241)] + ok &= max(min(5 * s - 1, 2 - 5 * s) for s in grid) == Fr(1, 2) + ok &= Fr(3, 5) > Fr(1, 2) > Fr(4, 9) > Fr(3, 7) + return ok, {'ledger_229': {k: str(v) for k, v in rows_.items()}, 'least_with_elder_rows': str(least_with), + 'least_without_elder_rows': str(least_without), + 'conditional_ledger_remark_1': {k: str(v) for k, v in cond.items()}, 'conditional_least': str(min(cond.values()))} + + +def main(argv): + global MUT + if len(argv) == 2 and argv[0] == '--mutant': + if argv[1] not in MUTANTS: + print('unknown mutant label', file=sys.stderr) + return 2 + MUT = argv[1] + elif argv: + print('usage: ecp_check.py [--mutant M1..M7]', file=sys.stderr) + return 2 + x1, x1d = control_X1() + x2, x2d = control_X2() + x3, nwin, nom = control_X3() + x4, n4 = control_X4() + x5 = control_X5() + x6, x6d = control_X6() + res = {'object': 'CL-ELDER-CUSP-PARITY-20261002-v1', 'scientific_effect': 'NONE', + 'controls': {'X1_lemma_Q_prime_and_CE': x1, 'X2_model_ridge_and_edges': x2, 'X3_pinned_fields_and_Omega_a': x3, + 'X4_Q1_identities_and_parity': x4, 'X5_first_order_bookkeeping': x5, 'X6_corollary_and_ledgers': x6}, + 'X1': x1d, 'X2': x2d, 'X3_window_fields_checked': nwin, 'X3_Omega_fields_checked': nom, + 'X4_instances_checked': n4, 'X6': x6d} + ok = all(res['controls'].values()) + if MUT is None: + print(json.dumps(res, indent=1, sort_keys=True)) + return 0 if ok else 1 + + +if __name__ == '__main__': + sys.exit(main(sys.argv[1:]))