From 854491b76f8d07c1041ee4f8d92b6228b058100e Mon Sep 17 00:00:00 2001 From: "Claude Fable 5.1" Date: Wed, 30 Sep 2026 12:37:07 +0000 Subject: [PATCH 1/5] Far elder density: living bars have flat components, nu_eld^far = O(ell^N) for every N (author-side candidate) frontiers/far_elder_flat_ridge_20260930/ (CL-FAR-ELDER-FLAT-RIDGE-20260930-v1): PROOF.md, flat_ridge_check.py, RESULTS.json, README.md, SOURCES.json; workflow far-elder-flat-ridge.yml. - Lemma 1 (deterministic): on the component of a maximum x0 in {f > t}, t at or above the death level of its bar, |grad f|^2 <= 2K (b - f) with K >= sup ||D^2 f|| (uphill segment; [P] section 8 maximin) - Lemma 2: a far death forces the component across every sphere of radius < rho (cone at the index-(d-1) saddle) - Theorem G: nu_eld^{far,rho}(ell) <= C_N ell^N for 0 < ell <= 1 and every N (N flat sites on separated shells, Fubini first-moment bound with the [P] section 2 N-site nondegeneracy, Borell-TIS on the regression residual) - successor in rate to Math-#187 (O(ell^(2/3))), which is cited only; nothing unmerged is consumed - exact controls (stdlib): Lemma 1 on an explicit two-maximum landscape by union-find (4873/4884 points, K = 21), uphill segment, near cubic consistency, Lemma 3 constants, exponent ledger, shell geometry; mutants M1-M5 - clean-context referee pass applied before landing (far-pin genericity, (2.a) restated from [P], Remark 1 three-way split, Remark 5 manuscript scope, K = 21 and factor-2 mutant) Scientific effect NONE. No register, GRAPH, STATUS, PROOF_INDEX, prize or Boolean change. Author will not merge. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .github/workflows/far-elder-flat-ridge.yml | 64 ++++ .../far_elder_flat_ridge_20260930/PROOF.md | 291 ++++++++++++++++++ .../far_elder_flat_ridge_20260930/README.md | 31 ++ .../RESULTS.json | 67 ++++ .../SOURCES.json | 127 ++++++++ .../flat_ridge_check.py | 284 +++++++++++++++++ 6 files changed, 864 insertions(+) create mode 100644 .github/workflows/far-elder-flat-ridge.yml create mode 100644 frontiers/far_elder_flat_ridge_20260930/PROOF.md create mode 100644 frontiers/far_elder_flat_ridge_20260930/README.md create mode 100644 frontiers/far_elder_flat_ridge_20260930/RESULTS.json create mode 100644 frontiers/far_elder_flat_ridge_20260930/SOURCES.json create mode 100644 frontiers/far_elder_flat_ridge_20260930/flat_ridge_check.py diff --git a/.github/workflows/far-elder-flat-ridge.yml b/.github/workflows/far-elder-flat-ridge.yml new file mode 100644 index 000000000..c68ffb44e --- /dev/null +++ b/.github/workflows/far-elder-flat-ridge.yml @@ -0,0 +1,64 @@ +name: Far elder flat-ridge exact controls + +'on': + pull_request: + paths: + - 'frontiers/far_elder_flat_ridge_20260930/**' + - '.github/workflows/far-elder-flat-ridge.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-controls: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('frontiers/far_elder_flat_ridge_20260930').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']) + for entry in manifest['consumed'] + manifest['cited_only']: + data = pathlib.Path(entry['path']).read_bytes() + framed = b'blob ' + str(len(data)).encode() + b'\0' + data + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256'] or hashlib.sha1(framed).hexdigest() != entry['git_blob']: + raise ValueError('merged source drifted: ' + entry['path']) + script = str(root / 'flat_ridge_check.py') + expected = (root / 'RESULTS.json').read_bytes() + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], check=True, capture_output=True, timeout=600).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in manifest['mutants']: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], capture_output=True, timeout=600).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + rc = subprocess.run([sys.executable, *flags, script, '--mutant', 'M9'], capture_output=True, timeout=600).returncode + if rc != 2: + raise RuntimeError('unknown mutant label not rejected with exit 2') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/frontiers/far_elder_flat_ridge_20260930/PROOF.md b/frontiers/far_elder_flat_ridge_20260930/PROOF.md new file mode 100644 index 000000000..50cfbf4fc --- /dev/null +++ b/frontiers/far_elder_flat_ridge_20260930/PROOF.md @@ -0,0 +1,291 @@ +# Living bars have flat components: the far elder density is `O(ℓ^N)` for every `N` + +Object: CL-FAR-ELDER-FLAT-RIDGE-20260930-v1. +Author: Anthropic Claude (claude.ai session `session_01NMeKEismAyeqgdB4sy2NJU`), 30 September 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 claimed. Same GitHub account as +every lane; zero organizational independence. Successor in rate to Math- #187 (`CL-FAR-ELDER-RATE-20260930-v1`, +`O(ℓ^{2/3})`), which it does not modify and whose barrier lemma it does not use. + +## 0. Statement + +Fixed `d ≥ 2`, torus `X = R^d/(LZ^d)`, the variance-one periodized Gaussian field of [P] §1, and a fixed +separation `ρ ∈ (0, L/4]`. For `y ∈ X` with `dist(0, y) ≥ ρ` write, as in [P] §14 and Math- #187 §0, + + O_y = (f(0), ∇f(0), f(y), ∇f(y)), v_{b,ℓ} = (b, 0, b − ℓ, 0), + p_y(v) = the Gaussian density of O_y at v, Q_{y,b,ℓ} = the regression law given O_y = v_{b,ℓ}, + W(f) = |det H_0 det H_y| 1{H_0 < 0, index H_y = d − 1}, e_y(f) = the Borel ordinary elder mark + ([P] §8: the global superlevel elder death partner of the maximum at 0 is the saddle at y), + +and the far elder density per unit volume at lifetime `ℓ` (the canonical marked Kac–Rice version, [P] §9 read as +[E2]; height Jacobian 1 on this domain, [P] §14) + + ν_eld^{far,ρ}(ℓ) = ∫_{dist(0,y) ≥ ρ} ∫_R p_y(v_{b,ℓ}) E_{Q_{y,b,ℓ}}[W(f) e_y(f)] db dy. (0.1) + +[P] §14's argument gives `ν_eld^{far,ρ}(ℓ) ≤ C` on `(0, 1]` ((14.1) is its case `ρ = r_0`); [Z] gives +`ν_eld^{far,ρ}(ℓ) → 0` with no rate; Math- #187 gives `O(ℓ^{2/3})`. The SIDE24 manuscript's Proposition A.3.2 / A.3.2′ asserts `O(ℓ)` without a valid proof (July audit +F-02). + +**Theorem G.** For every `ρ ∈ (0, L/4]` and every integer `N ≥ 1` there is `C = C(d, L, ρ, N) < ∞` such that + + ν_eld^{far,ρ}(ℓ) ≤ C ℓ^N, 0 < ℓ ≤ 1. (0.2) + +Consequently, for `0 < t ≤ 1`, `E N_eld^{far,ρ}(0, t] ≤ C t^{N+1}/(N+1)` per unit volume, and for every real `q` +(however negative) `E Σ_{far elder bars, ℓ_i ≤ t} ℓ_i^q < ∞`: the far elder population has all inverse-lifetime +moments. + +The proof rests on a deterministic inequality that holds on the superlevel component of *every* living bar. + +**Lemma 1 (flat components).** Let `f ∈ C²(X)` and `K > 0` with `K ≥ sup_X ‖D²f‖_op`. Let `x_0` be a local maximum, +`b = f(x_0)`, and let `t < b` be such that the connected component `C_t` of `x_0` in the open set `{f > t}` +contains no point with `f > b`. Then for every `p ∈ C_t` + + |∇f(p)|² ≤ 2K (b − f(p)) ≤ 2K (b − t). (1.1) + +The hypothesis holds exactly for `t ≥ b − ℓ(x_0)`, where `ℓ(x_0)` is the lifetime of the `H_0` bar of `x_0` under +the superlevel filtration with the elder rule ([P] §8): as long as the bar is alive, its component contains no +older (higher) maximum, and a component with a point above `b` would contain one (§1). + +**Lemma 2 (crossing).** If the death partner `y` of `x_0` satisfies `dist(x_0, y) ≥ ρ`, then for `t = b − ℓ(x_0)` +the component `C_t` meets every sphere `∂B(x_0, r)`, `0 < r < ρ`, and on `C_t` one has `b − ℓ(x_0) < f ≤ b` and +`|∇f| < (2Kℓ(x_0))^{1/2}`. + +**Lemma 3 (near-critical balls).** If `|∇f(p)| ≤ (2K_0ℓ)^{1/2}`, `b − ℓ < f(p) ≤ b`, `sup‖D²f‖ ≤ K_0` and +`r_ℓ = (ℓ/K_0)^{1/2}`, then every `q ∈ B(p, r_ℓ)` satisfies `|∇f(q)| ≤ 3(K_0ℓ)^{1/2}` and `|f(q) − b| ≤ 3ℓ`. + +**What is not claimed.** No statement about the far *rejected* density (which stays of order one: [U] (U1) gives it +the lower bound `c_* > 0` at `ρ = r_0`, and [Z] identifies its limit); no near-pair statement (Lemma 1 is +consistent with the near law but adds nothing there, §4); no numerical `C`; no uniformity in `L`, `d`, `N` or +`ρ ↓ 0`; nothing about the true order of `ν_eld^{far,ρ}` beyond (0.2) (§4 records the expectation that it is +super-polynomially small; no rate is conjectured). + +## 1. Proofs of the deterministic lemmas + +**Lemma 1.** Let `p ∈ C_t` with `g = ∇f(p) ≠ 0` (for `g = 0` there is nothing to prove), `e = g/|g|`, and +`φ(s) = f(p + se)` for `0 ≤ s ≤ |g|/K` (a straight segment in the flat torus; only the values along it are used). +Since `‖D²f‖ ≤ K`, `φ'(s) = ⟨∇f(p + se), e⟩ ≥ |g| − Ks ≥ 0` on that range, so `φ` is nondecreasing and +`φ(s) ≥ f(p) > t`: the segment lies in `{f > t}` and is connected to `p`, hence lies in `C_t`. By hypothesis +`φ(s) ≤ b` there. At `s = |g|/K`, + + b ≥ φ(|g|/K) ≥ f(p) + ∫_0^{|g|/K} (|g| − Ku) du = f(p) + |g|²/(2K), + +which is (1.1); the second inequality is `f(p) > t`. ∎ + +*The hypothesis for living bars.* In [P] §8 the ordinary death level of a maximum `x_0` is the superlevel maximin +`d_f(x_0) = sup{ min_γ f : γ a path from x_0 to a point above b }` and `ℓ(x_0) = b − d_f(x_0)`. If `C_t` contained a +point `z` with `f(z) > b`, then, `C_t` being open and connected (hence path-connected), a path inside +`C_t ⊂ {f > t}` from `x_0` to `z` would give `d_f(x_0) ≥ min_γ f > t`, i.e. `t < b − ℓ(x_0)`. So for every +`t ≥ b − ℓ(x_0)` — the death level included — `C_t ⊂ {f ≤ b}`, and Lemma 1 applies. (For an essential maximum, +`d_f = −∞` and every `t` qualifies.) + +**Lemma 2.** With `t = b − ℓ(x_0)` and `C := C_t`: the mark `e_y = 1` is the event `d_f(x_0) = f(y)` of [P] §8, +which on the Morse distinct-value locus says that the component of `x_0` in `{f > s}` merges, as `s` decreases +through `t = f(y)`, with a component containing a higher maximum, at the index-`(d − 1)` saddle `y` ([P] §1 counts +negative eigenvalues, so `y` has `d − 1` negative and one positive direction). Locally at `y`, +`f = t + u² − |w|²` in Morse coordinates (`u ∈ R`, `w ∈ R^{d−1}`), so `{f > t}` near `y` is the double cone +`{|u| > |w|}`; each nappe lies in one component of `{f > t}`, and `C` contains one of them — otherwise the handle +at `y` would leave `C` a component of `{f > s}` for `s` slightly below `t`, forcing `d_f(x_0) < t`. Each nappe has +`y` in its closure, so `y ∈ cl(C)`. A connected set `C ∋ x_0` with a closure point at distance `≥ ρ` meets every +sphere `∂B(x_0, r)`, `0 < r < ρ`: otherwise `C ⊂ {dist < r} ∪ {dist > r}`, two disjoint open sets, so +`C ⊂ {dist < r}` and `cl(C) ⊂ {dist ≤ r}`, excluding `y`. The bounds are (1.1) with `b − f(p) < b − t = ℓ(x_0)`. ∎ + +**Lemma 3.** For `q ∈ B(p, r_ℓ)`: `|∇f(q)| ≤ |∇f(p)| + K_0r_ℓ ≤ (√2 + 1)(K_0ℓ)^{1/2} < 3(K_0ℓ)^{1/2}` and +`|f(q) − f(p)| ≤ |∇f(p)|r_ℓ + K_0r_ℓ²/2 ≤ (√2 + 1/2)ℓ`, so `|f(q) − b| ≤ (1 + √2 + 1/2)ℓ < 3ℓ` (checker F4). ∎ + +## 2. Fixed-separation Gaussian facts (as in Math- #187 §2, with `N` further sites) + +Fix `N ≥ 1`. For `y ∈ D_ρ := {dist(0, y) ≥ ρ}` and sites `q = (q_1, …, q_N)` with + + dist(0, q_j) ≥ ρ/(4N), dist(q_i, q_j) ≥ ρ/(4N) (i ≠ j), dist(q_j, y) ≥ ρ/4, (2.0) + +put `V_y = (O_y, H_0, H_y)` and `Z_q = (f(q_1), ∇f(q_1), …, f(q_N), ∇f(q_N))` (`N(d + 1)` coordinates). All entries +of `(V_y, Z_q)` are distinct derivative evaluations at `N + 2` distinct sites, so by [P] §2 (distinct-site rank of +the Fourier-summable covariance) their joint covariance is positive definite; it is continuous in `(y, q)`, hence +uniformly positive definite on the compact set of configurations (2.0). Consequently: + +(a) the covariance of `V_y` is a principal submatrix of the covariance of `(V_y, Z_q)`, hence uniformly positive + definite on `D_ρ`; so the joint density of `V_y` at `(v_{b,ℓ}, H_0, H_y)` is at most + `C exp[−c(|v_{b,ℓ}|² + |H_0|² + |H_y|²)] ≤ C exp[−c(b² + |H_0|² + |H_y|²)]` (as `|v_{b,ℓ}| ≥ |b|`), i.e. + + p_y(v_{b,ℓ}) · density(H_0, H_y | O_y = v_{b,ℓ}) ≤ C exp[−c(b² + |H_0|² + |H_y|²)], (2.a) + + uniformly for `y ∈ D_ρ`, `b ∈ R`, `0 < ℓ ≤ 1` (this is the [P] §14 bound behind (14.1), restated; Math- #187 + (2.1) is the same statement). Integrating `|det H_0 det H_y|` against it, `p_y(v_{b,ℓ}) E[W | O_y = v_{b,ℓ}] ≤ + C exp(−cb²)` and `∫_{D_ρ}∫_R p_y(v_{b,ℓ}) E_Q[W] db dy ≤ C` for `0 < ℓ ≤ 1`; + +(b) the conditional law of `Z_q` given `V_y` is Gaussian with covariance the Schur complement of the joint + covariance, uniformly positive definite on (2.0); its density is therefore bounded by a constant + `C_N = C(d, L, ρ, N)` **uniformly in the conditioning values** (the conditional covariance does not depend on + them). Hence for every `b`, `H_0`, `H_y`, `ℓ ≤ 1` and `K_0 ≥ 1`, + + Q( |f(q_j) − b| ≤ 3ℓ and |∇f(q_j)| ≤ 3(K_0ℓ)^{1/2} for all j | V_y ) ≤ C_N (6ℓ)^N (ω_d 3^d (K_0ℓ)^{d/2})^N + = C'_N K_0^{dN/2} ℓ^{N(1 + d/2)}; (2.1) + +(c) regressing the field on `V_y` (the argument of [P] §4, applied at the two far sites `0`, `y` instead of the + near pins): `f = m + g` with `g` a centred Gaussian field independent of `V_y`, + `‖m‖_{C²} ≤ C(1 + |b| + |H_0| + |H_y|)` for `ℓ ≤ 1`, and `sup_X ‖D²g‖_op` a.s. finite with + `E sup_X ‖D²g‖_op ≤ C` and `σ_*² := sup_{x ∈ X, |v| = 1} Var(vᵀD²g(x)v) ≤ C`, uniformly on `D_ρ` (the + regression coefficients are fixed smooth covariance derivatives times the uniformly bounded inverse + covariance of `V_y`, and `g`'s covariance is dominated by the field's). Since `‖A‖_op = sup_{|v|=1} |vᵀAv|` + for symmetric `A`, the Borell–TIS inequality (Adler–Taylor, *Random Fields and Geometry*, Theorem 2.1.1) + applied to the centred Gaussian process `(x, v, ±) ↦ ±vᵀD²g(x)v` on the compact `X × S^{d−1} × {±}` gives, + for `u > 0`, + + P( sup_X ‖D²g‖_op > E sup_X ‖D²g‖_op + u ) ≤ exp(−u²/(2σ_*²)); (2.2) + +(d) for every `y ∈ D_ρ`, `b ∈ R` and `ℓ > 0`, the law `Q_{y,b,ℓ}` is almost surely Morse with distinct critical + values: [P] §8's pinned-genericity argument (distinct-site rank modulo the pins, the overdetermined-zero + lemma on a mesh, pinned heights distinct since `ℓ > 0`, countable exhaustion) uses nothing about the pin + separation and applies verbatim at the far pins `0`, `y`. This is where the Borel mark `e_y = 1{d_f(0) = + f(y)}` of [E2] means ordinary elder death *at* `y` (Lemma 2 needs the distinct-value locus: off it, a second + saddle at the same height could carry the merge). + +Nothing here tends to `r = 0`; no normalizer or cap estimate is used. + +## 3. Proof of Theorem G + +Fix `N`, `y ∈ D_ρ`, `b`, `0 < ℓ ≤ ℓ_1 := ρ²/(64N²)` (for `ℓ_1 < ℓ ≤ 1` the bound (0.2) is §2(a) with a larger +`C`), and work under `Q = Q_{y,b,ℓ}`. Put `K := 1 + sup_X ‖D²f‖_op` and fix a threshold `K_0 ≥ 2` to be chosen. +All pathwise statements below are on the full-measure generic locus of §2(d). + +*Step 1 (the event forces `N` flat sites).* On `{W(f) > 0, e_y(f) = 1}` the origin is a nondegenerate maximum with +`f(0) = b` whose death partner is the saddle `y` at `f(y) = b − ℓ`, so `ℓ(0) = ℓ` and `dist(0, y) ≥ ρ`. Lemma 2 +with the shells + + S_j := { q : | dist(0, q) − jρ/(2N) | < ρ/(8N) }, j = 1, …, N, + +gives points `p_j ∈ C ∩ ∂B(0, jρ/(2N)) ⊂ S_j` with `|∇f(p_j)| < (2Kℓ)^{1/2}` and `b − ℓ < f(p_j) ≤ b`. On the +further event `{K ≤ K_0}`, Lemma 3 with `r_ℓ = (ℓ/K_0)^{1/2} ≤ ℓ^{1/2} ≤ ρ/(8N)` (so `B(p_j, r_ℓ) ⊂ S_j`; the ball +is embedded since `r_ℓ < L/2`) gives + + B(p_j, r_ℓ) ⊂ A_j := { q ∈ S_j : |∇f(q)| ≤ 3(K_0ℓ)^{1/2}, |f(q) − b| ≤ 3ℓ }, + vol(A_j) ≥ ω_d r_ℓ^d = ω_d (ℓ/K_0)^{d/2}. + +Hence, pathwise, + + W e_y 1{K ≤ K_0} ≤ W · ∏_{j=1}^N [ vol(A_j) / (ω_d (ℓ/K_0)^{d/2}) ]. (3.1) + +*Step 2 (Kac–Rice with `N` extra sites).* Taking expectations, writing `vol(A_j) = ∫_{S_j} 1_{A_j}(q_j) dq_j` and +using Fubini, + + E_Q[W e_y 1{K ≤ K_0}] ≤ (K_0/ℓ)^{dN/2} ω_d^{−N} ∫_{S_1 × … × S_N} E_Q[ W · ∏_j 1_{A_j}(q_j) ] dq. + +For `q ∈ S_1 × … × S_N` the configuration satisfies (2.0): consecutive shells are separated by `ρ/(4N)`, the first +from the origin by `3ρ/(8N)`, and every shell from `y` by at least `ρ − ρ/2 − ρ/(8N) ≥ ρ/4` (checker F6). `W` is a +function of `(H_0, H_y) ⊂ V_y`, so by the tower property and (2.1) + + E_Q[ W · ∏_j 1_{A_j}(q_j) ] = E_Q[ W · Q(∀j: |f(q_j) − b| ≤ 3ℓ, |∇f(q_j)| ≤ 3(K_0ℓ)^{1/2} | V_y) ] + ≤ C'_N K_0^{dN/2} ℓ^{N(1 + d/2)} E_Q[W]. + +Since `vol(S_1 × … × S_N) ≤ C`, this gives (checker F5 for the exponent ledger) + + E_Q[W e_y 1{K ≤ K_0}] ≤ C_N K_0^{dN} ℓ^N E_Q[W]. (3.2) + +*Step 3 (the tail `K > K_0`).* By §2(c), `K ≤ 1 + C(1 + |b| + |H_0| + |H_y|) + sup_X ‖D²g‖_op`. Put +`m_* := sup_{y ∈ D_ρ} E sup_X ‖D²g‖_op < ∞`. On the event `E_1 := {1 + C(1 + |b| + |H_0| + |H_y|) ≤ K_0/2}` (an +event of `V_y`), `K > K_0` forces `sup‖D²g‖_op > K_0/2`, and for `K_0 ≥ 4m_*` (2.2) with `u = K_0/4` gives +`Q(K > K_0 | V_y) ≤ exp(−K_0²/(32σ_*²))` there (`g` is independent of `V_y`). Hence + + E_Q[W e_y 1{K > K_0}] ≤ exp(−K_0²/(32σ_*²)) E_Q[W] + E_Q[W 1{E_1^c}], (3.3) + +and, integrating against `p_y(v_{b,ℓ}) db dy`, the second term is bounded through (2.a): for `K_0 ≥ 4(1 + C)`, +`E_1^c ⊂ {|b| + |H_0| + |H_y| ≥ K_0/(4C)}`, and `∫∫ p_y E_Q[W 1{|b| + |H_0| + |H_y| ≥ K_0/(4C)}] db dy ≤ +C exp(−c'K_0²)` (the integral of `|det H_0 det H_y| e^{−c(b² + |H_0|² + |H_y|²)}` over that region). + +*Step 4 (choice of `K_0`).* Take `K_0 = K_0(ℓ) := max{4m_* + 4(1 + C) + 2, C_2 (N log(1/ℓ))^{1/2}}` with +`C_2² ≥ max{32σ_*², 1/c'}`, so that `exp(−K_0²/(32σ_*²)) ≤ ℓ^N` and `exp(−c'K_0²) ≤ ℓ^N`. Integrating (3.2)–(3.3) in +`(b, y)` with §2(a): + + ν_eld^{far,ρ}(ℓ) ≤ C_N K_0(ℓ)^{dN} ℓ^N + C ℓ^N ≤ C'_N ℓ^N (1 + log(1/ℓ))^{dN/2}, 0 < ℓ ≤ ℓ_1. + +As `N` is arbitrary, applying this with `N + 1` in place of `N` and absorbing the logarithm (`ℓ(1 + log(1/ℓ))^a` +is bounded on `(0, 1]`) gives (0.2). The cumulative and moment statements follow by integrating `ℓ^N` over +`(0, t] ⊂ (0, 1]` (`∫_0^t ℓ^{q+N} dℓ < ∞` once `N > −q − 1`). ∎ + +## 4. Remarks + +1. **What the far `O(1)` is.** [P] (14.1) bounds the far *candidate* density by a constant, [U] (U1) shows the far + *rejected* density is at least `c_* > 0` on `(0, ℓ_0]` (at `ρ = r_0`), and [Z] identifies its limit as + `∫_{D_ρ}∫Ψ_0 db dy ∈ (0, B_{d,L})`. Theorem G says that, to every polynomial order, all of the far candidate + mass is rejected mass: far maximum/saddle pairs with a small gap exist in profusion, but essentially none of + them is a bar. There is no tension with Lemma 1. With `C` the component of `0` in `{f > b − ℓ}`, a rejected far + pair `(0, y)` (`f(y) = b − ℓ`, `∇f(y) = 0`, `y` not the death partner of `0`) is of one of three kinds: (i) + `y ∉ cl(C)` — the two critical points are joined only through lower levels, which is [U]'s separated type; + (ii) `C` already contains a point above `b` — the bar of `0` is dead at that level, Lemma 1's hypothesis fails; + (iii) `y ∈ cl(C)` and `C ⊂ {f ≤ b}`, but `y` kills a third, lower maximum's bar or both nappes at `y` lie in + `C` (an `H_1` birth). In case (iii) Lemmas 1–2 and §3 apply verbatim, so that part of the rejected density is + also `O(ℓ^N)`; the order-one rejected mass lives in (i) and (ii), where nothing constrains the gradient. +2. **Consistency with the near law.** For a pinned pair at separation `r` and gap `ℓ = kr³` the axial model + profile is the cubic `P` with `P′(x) = 6k(x² − r²/4)` ([P] (3.1)–(3.3), `P‴ = 12k`), and (1.1) holds on the + whole axial segment with `K = 6kr` already (checker F3 uses `1 + 6kr`, exact): on this model `|∇f| ≍ kr²` against + `(Kkr³)^{1/2} ≍ k r²`, so the inequality is consistent with the near scaling and carries no extra information + there. Lemma 1 is a theorem, so near pairs satisfy it as well; the point is only that it does not improve the + near remainder of Theorem R. +3. **Relation to Math- #187.** Theorem F there (`O(ℓ^{2/3})`) came from the soft-maximum barrier + `λ_min(−H_0) ≤ (ℓK²/c_L)^{1/3}` (Math- #182 §3 (8)–(9), re-proved there) and the determinant weight `∏λ_j`; + that mechanism sees only the Hessian at the maximum, and its spectral integral `∫_0^u λ dλ` is of order + `ℓ^{2/3}` (no claim is made that the method cannot be sharpened). Lemma 1 sees the whole component and turns + the far event into `N` jointly nondegenerate site conditions, each costing `ℓ^{1 + d/2}` against a volume + `ℓ^{d/2}`, with an `N`-dependent constant. #187's Corollaries F1–F2 are superseded in rate, not in validity. +4. **The true order (non-claim).** The far event forces the field to stay within a band of width `ℓ` around the + pinned level while its gradient stays `O(ℓ^{1/2})` along a connected set of diameter `ρ` chosen by the field + itself — a small-ball-type event in `C¹`, though not a standard one (the set is random and the band is pinned). + The expectation is that `ν_eld^{far,ρ}` is super-polynomially small; no rate is conjectured, and the `N`-site + argument cannot produce one because `C_N` grows with `N`. +5. **For the manuscript.** In Theorem R's near/far decomposition ([R] §7, `ρ = r_0`), the far *elder* term is + `O(ℓ^N)` for every `N`; Theorem R's `O(1)` remainder is unchanged — it comes from the near terms (R16) (the + near candidate contact error) and (R18) (the near pairing loss), and, for the candidate density, from the far + rejected `O(1)` of [P] (14.1). The manuscript's A.3.2′ (far elder contribution `O(1)`, hence `o(ℓ^{−1/3})` + relative) rests on the reviewed (14.1) and should stay; this note, like #187, is an unreviewed candidate rate + that the V3 text may cite as such, not a replacement of a reviewed statement. + +## 5. Sources (exact identities in `SOURCES.json`) + +| Tag | Path | Role | +|---|---|---| +| [P] | `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` (blob `dfed3b8d`) | §1 field; §2 distinct-site rank; §4 regression/independent residual; §8 elder rule and maximin; §9 marked Kac–Rice (read as [E2]); §14 far pairs and (14.1) | +| [E1] | `imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md` (blob `213594d6`) | reading rule | +| [E2] | `reviews/d1_section9_borel_repair_20260925/REPAIR.md` (blob `fe9b9ce4`) | §9 replacement; measurability of `e_y` | +| [REC] | `reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md` (blob `75da2597`) | W1; consumption contract | +| [R] | `frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md` (blob `247b3ecf`) | Theorem R, §7 near/far split (cited only) | +| [Z] | `frontiers/c7_zero_gap_limit_20260929/PROOF.md` (blob `5b6328ea`) | far rejected limit (cited only; OpenAI candidate, non-OpenAI review required) | +| [U] | `frontiers/unrestricted_selection_difference_20260929/PROOF.md` (blob `5a55b179`) | (U1) lower bound (cited only; OpenAI review `reviews/c7_nonvanishing_openai_20260929`) | +| #187 | `frontiers/far_elder_rate_20260930/PROOF.md` (Math- #187, unmerged) | predecessor rate `O(ℓ^{2/3})` (cited only; §2 restates its fixed-separation facts from [P] directly) | +| lit. | Adler–Taylor, *Random Fields and Geometry* (2007), Thm 2.1.1 (Borell–TIS) | standard inequality, §2(c) | + +Consumed: [P] §§1, 2, 4 and 8 (their arguments, applied at the far pins `0`, `y`), 9 (as [E2]), 14; [E1]; [E2]; +[REC] §§1, 5, 7. Cited only: [R], [Z], [U], #187. + +## 6. Exact controls (`flat_ridge_check.py`; stdlib; exact rationals; byte-identical under `-O`) + +F1 Lemma 1 on the explicit two-maximum landscape `f(x, y) = g(x) − y²`, `g′(x) = −4(x + 1)(x − 1/10)(x − 11/10)` +(elder maximum at `x = −1`, height `203/150`; younger at `x = 11/10`, height `31339/30000`; saddle at `x = 1/10`, +height `−661/30000`; younger lifetime `16/15`): the grid component (spacing `1/50` on `[−2, 2]²`, union-find) of +the younger maximum in `{f > t}` has 4873 points at `t` = saddle height `+ 1/1000` and 4884 points at the death +level `t` = saddle height itself, and (1.1) holds at every one of them with `K = 21`, the exact operator-norm bound +of the Hessian on the `x`-interval spanned by the component's grid points widened by one step (`[3/25, 38/25]`, +resp. `[1/10, 38/25]`; for this separable `f` the component is `{y² < g(x) − t}` over an `x`-interval, which the +widened grid interval contains); the largest ratio `|∇f|²/(2K(b − f))` is `350/451 ≈ 0.78`, so the factor-2 +mutant M5 (`|∇f|² ≤ K(b − f)`) fails, at `(31/25, −3/50)`; the elder's component (6034 further points above `t`) +is present and, tested by mutant M1, violates (1.1) at `(−36/25, −7/25)`, a point with `f < b` (not the trivial +`f > b` case); mutant M2 (`K = 1`) fails at `(21/50, −11/25)`; the equality case `f = b − K|x|²/2` of (1.1) is +checked exactly. +F2 the uphill-segment inequality and monotonicity of the proof of Lemma 1 at 16 rational segments with the same +`K = 21`. +F3 the near cubic: (1.1) on `[−r/2, r/2]` with `K = 1 + 6kr` at 189 rational points, and `P(−r/2) − P(r/2) = kr³`. +F4 Lemma 3's constants through squares; mutant M3 (constant 2) fails. +F5 the exponent ledger `(K_0/ℓ)^{dN/2}(K_0^{d/2}ℓ^{1+d/2})^N = K_0^{dN}ℓ^N`, `d ∈ {2,3,5}`, `N ∈ {1,2,7}`; mutant M4 +fails. Mutants `M1`–`M5` exit 1; an unknown label exits 2. +F6 the shell geometry (2.0) for `N = 1, …, 6` and three values of `ρ`. + +The controls check the deterministic inequalities and the bookkeeping; they do not prove the Gaussian estimates of +§2 and are not acceptance. + +## 7. Review slices + +A: Lemma 1 and its hypothesis for living bars (the elder-rule argument in §1), Lemma 2, Lemma 3. +B: §2 (a)–(d) — the uniform conditional density bound with `N` extra sites from [P] §2, the regression + decomposition and the use of Borell–TIS, and the far-pin genericity (d); whether (2.1) is stated at the right + scope. +C: §3 — the volume/Markov step (3.1), the tower-property step, the `K_0` splitting and the choice (Step 4), and the + integration in `(b, y)`; Remarks 1–3 for consistency with [U], [Z], [R] and #187. diff --git a/frontiers/far_elder_flat_ridge_20260930/README.md b/frontiers/far_elder_flat_ridge_20260930/README.md new file mode 100644 index 000000000..65fbd62da --- /dev/null +++ b/frontiers/far_elder_flat_ridge_20260930/README.md @@ -0,0 +1,31 @@ +# Far elder density: flat components and the `O(ℓ^N)` rate (CL-FAR-ELDER-FLAT-RIDGE-20260930-v1) + +Author-side proof candidate, Anthropic Claude, 30 September 2026. Scientific effect NONE. Nonauthor review required. + +**Statement.** For the periodized Gaussian field on the torus and a fixed separation `ρ`, the density (per unit +volume) of elder pairs `(M, S)` at torus distance `≥ ρ` with lifetime `ℓ` is `O(ℓ^N)` for every `N` as `ℓ ↓ 0` +(Theorem G); all inverse-lifetime moments of the far elder population are finite. Previously on file: bounded +([P] (14.1)), `o(1)` without rate ([Z]), `O(ℓ^{2/3})` (Math- #187, the predecessor, not modified here). The +manuscript's Proposition A.3.2 asserts `O(ℓ)` without a valid proof (July audit F-02); its restatement A.3.2′ +(`O(1)`, resting on the reviewed [P] (14.1)) stands, and Theorem G is an author-side candidate rate with every +polynomial exponent, offered for nonauthor review — not a replacement of a reviewed statement. + +**Mechanism.** *Living bars have flat components* (Lemma 1, deterministic, two lines): if the bar of a maximum +`x_0` with `f(x_0) = b` is alive at level `t`, then on the component of `x_0` in `{f > t}` every point satisfies +`|∇f|² ≤ 2K(b − f) ≤ 2K(b − t)`, `K ≥ sup‖D²f‖` — walk uphill from any point for a distance `|∇f|/K`; the walk +stays in the component, where `f ≤ b`. A far death forces that component to cross `N` disjoint shells, so the +field carries `N` separated sites with `|f − b| ≤ 3ℓ` and `|∇f| ≤ 3(K_0ℓ)^{1/2}`; each costs `ℓ^{1 + d/2}` against a +volume `ℓ^{d/2}` (a Fubini first-moment bound over `N` extra sites inside the pair Kac–Rice integrand, jointly +nondegenerate by [P] §2), and Borell–TIS removes the derivative-norm threshold at the price of logarithms. + +Files: `PROOF.md`; `flat_ridge_check.py` (stdlib exact controls; `RESULTS.json` its output, `-O` identical; +mutants `M1`–`M5` exit 1, unknown label exit 2; F1 verifies Lemma 1 on an explicit two-maximum landscape by +union-find on a rational grid, above and at the death level, with the elder's own component and a factor-2 error +as mutants that must fail); `SOURCES.json` (exact identities of every source; nothing unmerged is consumed — the +fixed-separation Gaussian facts are restated from [P] directly). A clean-context referee agent read the note +before landing; its findings (far-pin genericity stated as §2(d); the pointwise Gaussian bound (2.a) restated from +[P] so that #187 is not consumed; Remark 1's three-way split of rejected far pairs; Remark 5's manuscript scope; +`K = 21` and the factor-2 mutant in F1) were applied. + +Review slices (§7): A deterministic (Lemmas 1–3); B Gaussian (§2: `N`-site conditional density, regression and +Borell–TIS); C the proof of Theorem G (§3) and the remarks (§4). diff --git a/frontiers/far_elder_flat_ridge_20260930/RESULTS.json b/frontiers/far_elder_flat_ridge_20260930/RESULTS.json new file mode 100644 index 000000000..46f17c9a9 --- /dev/null +++ b/frontiers/far_elder_flat_ridge_20260930/RESULTS.json @@ -0,0 +1,67 @@ +{ + "checks": { + "F1_flat_component_two_maxima": { + "info": { + "above_death_level": { + "K": 21, + "component_points": 4873, + "elder_component_present": true, + "grid_points_above_t": 10907, + "max_ratio_|grad|^2/(2K(b-f))": "350/451", + "x_interval": [ + "3/25", + "38/25" + ] + }, + "at_death_level": { + "K": 21, + "component_points": 4884, + "elder_component_present": true, + "grid_points_above_t": 10923, + "max_ratio_|grad|^2/(2K(b-f))": "350/451", + "x_interval": [ + "1/10", + "38/25" + ] + } + }, + "passed": true + }, + "F2_uphill_segment": { + "info": { + "K": 21, + "segments": 16 + }, + "passed": true + }, + "F3_near_cubic_consistency": { + "info": { + "points": 189 + }, + "passed": true + }, + "F4_lemma3_constants": { + "info": { + "gradient_constant": "3", + "value_constant": "3" + }, + "passed": true + }, + "F5_exponent_ledger": { + "info": { + "ledger": "K0^(dN) ell^N" + }, + "passed": true + }, + "F6_shell_geometry": { + "info": { + "N_range": "1..6", + "separation": "rho/(4N) between sites, rho/4 from y" + }, + "passed": true + } + }, + "object": "CL-FAR-ELDER-FLAT-RIDGE-20260930-v1", + "passed": true, + "scientific_effect": "NONE" +} diff --git a/frontiers/far_elder_flat_ridge_20260930/SOURCES.json b/frontiers/far_elder_flat_ridge_20260930/SOURCES.json new file mode 100644 index 000000000..742af3565 --- /dev/null +++ b/frontiers/far_elder_flat_ridge_20260930/SOURCES.json @@ -0,0 +1,127 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "object": "CL-FAR-ELDER-FLAT-RIDGE-20260930-v1", + "kind": "author-side proof candidate (Lemmas 1-3 deterministic; Theorem G conditional on the reconciled [P] interfaces and the standard Borell-TIS inequality); nonauthor analytic review required", + "author": "Anthropic Claude", + "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", + "read_at": { + "branch_base": "de54d1da2f6cdde59df3c34bb50ecd85c25ca333" + }, + "consumed": [ + { + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "bytes": 40261, + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "tag": "P", + "use": "\u00a71 field; \u00a72 distinct-site rank (N + 2 sites); \u00a74 regression / independent residual at fixed sites; \u00a78 maximin d_f and the Borel elder mark; \u00a79 as [E2]; \u00a714 far pairs and (14.1)" + }, + { + "path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", + "bytes": 9062, + "sha256": "845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f", + "git_blob": "fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a", + "tag": "E2", + "use": "\u00a79.1-9.4: the marked Kac-Rice version (0.1) and measurability of e_y" + }, + { + "path": "reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md", + "bytes": 23312, + "sha256": "451b9d7ffee072a73fc904cab891b6693e3f233808b89df10cce1b57036b65da", + "git_blob": "75da2597971510f843f8d90c743950cb8c177342", + "tag": "REC", + "use": "\u00a71 reading rule, \u00a75 embedding radius, \u00a77 consumption contract" + }, + { + "path": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", + "bytes": 1782, + "sha256": "bad7ef609c4ad8c41ad6af562c1b6807921e19a9d556ed793ad1a0db6e202028", + "git_blob": "213594d6ca6a86fb938110f4d166d9ce275a02d0", + "tag": "E1", + "use": "reading rule only" + } + ], + "cited_only": [ + { + "path": "frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md", + "bytes": 17734, + "sha256": "380b7d0abdb0fe2de5a6564565af9560d3f1b1ce22fd5538927db0c52f4f3a4a", + "git_blob": "247b3ecf80bfbe896948d5d489b2d5842a81c481", + "tag": "R", + "use": "\u00a77 near/far decomposition, \u00a78 moments (Remark 5)" + }, + { + "path": "frontiers/c7_zero_gap_limit_20260929/PROOF.md", + "bytes": 17592, + "sha256": "f0e563c45c41333f2bb6e5bf5cb98f0d3b592e2abf2af1c1b098c21ad77cb777", + "git_blob": "5b6328ea3d6afcbeb731698b3834e536f72d1bcb", + "tag": "Z", + "use": "far rejected limit (Remark 1); OpenAI candidate, non-OpenAI review required" + }, + { + "path": "frontiers/unrestricted_selection_difference_20260929/PROOF.md", + "bytes": 13028, + "sha256": "93a63002d32fd5c35ae994fe28b1205d8098026d6ddde19c67d4977dcf5817a9", + "git_blob": "5a55b179a974a90c65d257f3f93765cc6fb30bb8", + "tag": "U", + "use": "(U1) far rejected lower bound (Remark 1); OpenAI review reviews/c7_nonvanishing_openai_20260929" + }, + { + "path": "reviews/c7_nonvanishing_openai_20260929/REVIEW.md", + "bytes": 10807, + "sha256": "68b6cd43351706745992c4af242abdc5bdabd46ab5ac99347f2c12b505e1a15d", + "git_blob": "64794e5801b70d950c7e1202f7b6b7d07055cbb6", + "tag": "U-review", + "use": "the nonauthor review binding for [U]" + } + ], + "cited_unmerged": [ + { + "path": "frontiers/far_elder_rate_20260930/PROOF.md", + "pr": "d6g8k5htny-coder/Math-#187", + "commit": "ecd47e7b1d447eefec963b1fa8395777db09a190", + "git_blob": "37dcf6ef933251c8890ab653cafd648610779342", + "bytes": 16413, + "sha256": "67f606327b66a2b4f1b8c67a57d119ac9ddfd2ce827ca8cb0c4daefa31904a3b", + "tag": "187", + "use": "cited only: predecessor rate O(ell^(2/3)); its (2.1)-(2.2) restated in \u00a72 from [P]; nothing unmerged is consumed; not verified by the workflow" + } + ], + "literature": [ + "Adler, Taylor, Random Fields and Geometry (Springer 2007), Theorem 2.1.1 (Borell-TIS)" + ], + "mutants": [ + "M1", + "M2", + "M3", + "M4", + "M5" + ], + "referee": { + "kind": "clean-context Anthropic Claude subagent before landing (same provider, same account; not a nonauthor review)", + "findings": "no blocking; SHOULD-FIX applied: far-pin genericity stated (section 2(d)); pointwise Gaussian density bound (2.a) restated from [P] so that Math-#187 is cited only; Remark 1 three-way split of rejected far pairs (separated / dead-bar / third-maximum or H_1 case, the last also O(ell^N)); Remark 5 keeps A.3.2-prime and names (R16),(R18); Borell-TIS applied to v^T D^2 g v on X x S^(d-1); K_0 choice made explicit (m_*, C_2^2 >= max(32 sigma_*^2, 1/c)); Lemma 2 cone/handle wording and the sphere-crossing argument without embeddedness; Remarks 2-4 softened (no small-ball rate conjectured; Li-Shao pinpoint removed); controls: K = 21 on the component interval, death-level component, equality case, factor-2 mutant M5, dead F3 line removed" + }, + "files": [ + { + "path": "PROOF.md", + "bytes": 22806, + "sha256": "957f9c5e6557a558b2c055fa2a1f11ba301581995b8958658fad2edf47136f57" + }, + { + "path": "flat_ridge_check.py", + "bytes": 12667, + "sha256": "00b362170202b63e75d6e80f5ac5a51b97da3ca2087ef47b3f9edd1c11712a82" + }, + { + "path": "RESULTS.json", + "bytes": 1264, + "sha256": "f7ab1b00bbe105af18656ec314dc7d33499f36236f2982e8ca6be5b93b12c35f" + }, + { + "path": "README.md", + "bytes": 2845, + "sha256": "aed92c1d8b7f767e2b9c8571f33d0e72966366f0b4234586559420bc8b209593" + } + ] +} diff --git a/frontiers/far_elder_flat_ridge_20260930/flat_ridge_check.py b/frontiers/far_elder_flat_ridge_20260930/flat_ridge_check.py new file mode 100644 index 000000000..0dd25d928 --- /dev/null +++ b/frontiers/far_elder_flat_ridge_20260930/flat_ridge_check.py @@ -0,0 +1,284 @@ +#!/usr/bin/env python3 +"""Exact finite controls for PROOF.md (CL-FAR-ELDER-FLAT-RIDGE-20260930-v1). Standard library only; exact rationals. + + F1 Lemma 1 (flat components) on an explicit two-maximum landscape f(x, y) = g(x) - y^2 with + g'(x) = -4 (x + 1)(x - 1/10)(x - 11/10): maxima at x = -1 (height 203/150, the elder) and x = 11/10 (height + 31339/30000, the younger), saddle at x = 1/10 (height -661/30000), younger lifetime 16/15. On the rational + grid of spacing 1/50 in [-2, 2]^2, the grid component of the younger maximum in {f > t} at t = saddle height + + 1/1000, and again at the death level t = saddle height itself, is taken by union-find, and (1.1) + |grad f|^2 <= 2 K (b - f) is verified at every one of its points, with K the exact operator-norm bound of the + Hessian diag(g''(x), -2) on the x-interval spanned by the component's grid points widened by one grid step + (for this separable f the component is {y^2 < g(x) - t} over an x-interval, which the widened grid interval + contains); the equality case f = b - K|x|^2/2 of (1.1) is checked exactly; mutant M1 tests all grid points + of {f > t} (the elder's component must fail); mutant M2 replaces K by 1 (must fail); mutant M5 tests the + factor-2 error |grad f|^2 <= K (b - f) (must fail); + F2 the uphill-segment inequality of the proof of Lemma 1, phi(s) >= f(p) + |g| s - K s^2/2 for 0 <= s <= |g|/K, + on the same polynomial at rational p and rational s (exact), with the same K as F1, and the monotonicity + phi' >= |g| - K s >= 0; + F3 the pinned near-pair cubic P(x) = b - 6k(r^2 x/4 - x^3/3 + ...) with P'(x) = 6k (x^2 - r^2/4) ([P] (3.1): + P''' = 12k): (1.1) holds on the whole segment [-r/2, r/2] with K = 1 + 6 k r, at rational (k, r, x), so the + flat-component lemma is consistent with the near law (no restriction there); + F4 Lemma 3's constants: for q in B(p, r_ell), r_ell = (ell/K0)^(1/2): |grad f(q)| <= (sqrt2 + 1)(K0 ell)^(1/2) + < 3 (K0 ell)^(1/2) and |f(q) - b| <= (1 + sqrt2 + 1/2) ell < 3 ell, checked through squares + ((sqrt2 + 1)^2 = 3 + 2 sqrt2 < 9 since sqrt2 < 3; 1 + 1/2 + sqrt2 < 3 since 2 < (3/2)^2); mutant M3 claims + the sharper constant 2 in the first bound (false: (sqrt2 + 1)^2 = 3 + 2 sqrt2 > 4); + F5 the exponent ledger of section 3 by exact monomial substitution: (K0/ell)^(dN/2) (K0^(d/2) ell^(1 + d/2))^N + = K0^(dN) ell^N for d in {2, 3, 5}, N in {1, 2, 7}; mutant M4 claims ell^(N/2); + F6 the shell geometry: radii j rho/(2N), half-width rho/(8N): pairwise separation >= rho/(4N) between shells and + from the origin, and >= rho/4 from every y with |y| >= rho; r_ell <= rho/(8N) once ell <= rho^2/(64 N^2) + (K0 >= 1); exact for N = 1..6 at rational rho; + M semantic mutants (--mutant M1|M2|M3|M4|M5) exit 1; an unknown label exits 2. +""" +import argparse +import json +import sys +from fractions import Fraction as F + +# ------------------------------------------------------------------------------------------------------------ +# the landscape of F1/F2: f(x, y) = g(x) - y^2, g'(x) = -4 (x - x1)(x - x2)(x - x3) +X1, X2, X3 = F(-1), F(1, 10), F(11, 10) +S1, S2, S3 = X1 + X2 + X3, X1*X2 + X1*X3 + X2*X3, X1*X2*X3 + + +def g(x): + return -4*(x**4/4 - S1*x**3/3 + S2*x*x/2 - S3*x) + + +def gp(x): + return -4*(x**3 - S1*x*x + S2*x - S3) + + +def gpp(x): + return -4*(3*x*x - 2*S1*x + S2) + + +def f(x, y): + return g(x) - y*y + + +def grad2(x, y): + return gp(x)**2 + 4*y*y + + +def hessian_bound_interval(xlo, xhi): + """Smallest integer K >= max(sup |g''| on [xlo, xhi], 2): the operator norm of diag(g''(x), -2). g'' is a concave + quadratic, so its extreme values on an interval are at the endpoints or at its vertex.""" + cands = [abs(gpp(xlo)), abs(gpp(xhi)), F(2)] + vertex = S1/3 # g'' = -12 x^2 + 8 S1 x - 4 S2 has its maximum at x = S1/3 + if xlo <= vertex <= xhi: + cands.append(abs(gpp(vertex))) + m = max(cands) + K = 1 + while K < m: + K += 1 + return K + + +def component_points(t, box, n): + """Grid points (i, j) of the union-find component of the younger maximum in {f > t}, plus all points above t.""" + h = box*2/n + pts = {} + idx = 0 + for i in range(n + 1): + x = -box + i*h + gx = g(x) + for j in range(n + 1): + y = -box + j*h + if gx - y*y > t: + pts[(i, j)] = idx; idx += 1 + parent = list(range(idx)) + + def find(a): + while parent[a] != a: + parent[a] = parent[parent[a]]; a = parent[a] + return a + + def union(a, c): + ra, rc = find(a), find(c) + if ra != rc: + parent[ra] = rc + for (i, j), a in pts.items(): + for (di, dj) in ((1, 0), (0, 1)): + nb = (i + di, j + dj) + if nb in pts: + union(a, pts[nb]) + root_idx = (int((X3 + box)/h), int((F(0) + box)/h)) + if (root_idx[0]*h - box, root_idx[1]*h - box) != (X3, F(0)): + raise ValueError('younger maximum is not a grid point') + root = find(pts[root_idx]) + comp = [(i, j) for (i, j), a in pts.items() if find(a) == root] + other = any(find(a) != root for a in pts.values()) + return pts, comp, other, h + + +def check_F1(mutant): + b = g(X3) # younger maximum height + s = g(X2) # saddle height (death level) + if not (g(X1) > b > s): + return False, 'landscape heights out of order' + if not (gpp(X1) < 0 and gpp(X3) < 0 and gpp(X2) > 0): + return False, 'critical point types' + box = F(2) + n = 200 # grid spacing 1/50 on [-2, 2] + info = {} + for label, t in (('above_death_level', s + F(1, 1000)), ('at_death_level', s)): + pts, comp, other, h = component_points(t, box, n) + xs = [-box + i*h for (i, j) in comp] + xlo, xhi = min(xs) - h, max(xs) + h + K = hessian_bound_interval(xlo, xhi) + if mutant == 'M2': + K = 1 + factor = 2*K + if mutant == 'M5': + factor = K + tested = list(pts.keys()) if mutant == 'M1' else comp + checked = 0 + worst = F(0) + for (i, j) in tested: + x, y = -box + i*h, -box + j*h + lhs = grad2(x, y) + rhs = factor*(b - f(x, y)) + if lhs > rhs: + return False, 'flat-component inequality fails at (%s, %s) [%s]' % (x, y, label) + if rhs > 0: + worst = max(worst, lhs/rhs) + checked += 1 + info[label] = {'K': K, 'x_interval': [str(xlo), str(xhi)], 'grid_points_above_t': len(pts), + 'component_points': checked, 'max_ratio_|grad|^2/(2K(b-f))': str(worst.limit_denominator(10**6)), + 'elder_component_present': other} + # equality case of (1.1): f = b - K |x|^2 / 2 on a ball (component = the ball), |grad f|^2 = K^2 |x|^2 = 2K (b - f) + for K in (F(1), F(7, 3), F(56)): + for x2 in (F(1, 4), F(9), F(1, 1000)): # |x|^2 + if K*K*x2 != 2*K*(K*x2/2): + return False, 'equality case of (1.1) fails' + return True, info + + +def check_F2(mutant): + box = F(2) + n = 200 + pts, comp, other, h = component_points(g(X2) + F(1, 1000), box, n) + xs = [-box + i*h for (i, j) in comp] + K = hessian_bound_interval(min(xs) - h, max(xs) + h) + cnt = 0 + for (x, y) in ((F(1, 2), F(1, 10)), (F(7, 10), F(-1, 5)), (F(1), F(0)), (F(3, 10), F(1, 2))): + gx, gy = gp(x), -2*y + gnorm2 = gx*gx + gy*gy + # exact rational unit direction is not available; use the segment along (gx, gy)/|g| through squares: + # phi(s) = f(p + s e), s = sigma |g| with sigma rational: p + sigma (gx, gy); then |g| s = sigma |g|^2 rational + for sigma in (F(1, 8*K), F(1, 4*K), F(1, 2*K), F(1, K)): # s = sigma |g| <= |g|/K + q = (x + sigma*gx, y + sigma*gy) + phi = f(*q) + lower = f(x, y) + sigma*gnorm2 - K*sigma*sigma*gnorm2/2 + if phi < lower: + return False, 'uphill segment inequality fails' + # directional derivative along e at q, times |g|: >= |g|^2 - K s |g| = |g|^2 (1 - K sigma) + dd = gp(q[0])*gx - 2*q[1]*gy + if dd < gnorm2*(1 - K*sigma): + return False, 'monotonicity along the segment fails' + cnt += 1 + return True, {'segments': cnt, 'K': K} + + +def check_F3(mutant): + n = 0 + for k in (F(1, 2), F(1), F(3)): + for r in (F(1, 10), F(1, 2), F(1)): + b = F(0) + ell = k*r**3 + K = 1 + 6*k*r # sup |P''| on [-r/2, r/2] is 6 k r + for m in range(0, 21): + x = -r/2 + r*F(m, 20) + # P(x) = b + 6k [ (x^3/3 - r^2 x/4) - ((-r/2)^3/3 - r^2 (-r/2)/4) ], normalised so that P(-r/2) = b + P = b + 6*k*((x**3/3 - r*r*x/4) - ((-r/2)**3/3 - r*r*(-r/2)/4)) + Pp = 6*k*(x*x - r*r/4) + if Pp*Pp > 2*K*(b - P): + return False, 'near cubic violates (1.1) at k=%s r=%s x=%s' % (k, r, x) + n += 1 + # lifetime consistency: P(-r/2) - P(r/2) = k r^3 + Pm = b; Pr = b + 6*k*(((r/2)**3/3 - r*r*(r/2)/4) - ((-r/2)**3/3 - r*r*(-r/2)/4)) + if Pm - Pr != ell: + return False, 'near cubic lifetime' + return True, {'points': n} + + +def check_F4(mutant): + # (sqrt2 + 1)^2 = 3 + 2 sqrt2 < 9 <=> 2 sqrt2 < 6 <=> 8 < 36 ; and > 4 <=> 2 sqrt2 > 1 <=> 8 > 1 + c = F(3) + if mutant == 'M3': + c = F(2) + # is (sqrt2 + 1) < c ? <=> sqrt2 < c - 1 <=> 2 < (c - 1)^2 (c > 1) + if not (2 < (c - 1)**2): + return False, 'gradient constant %s is not an upper bound for sqrt2 + 1' % c + # 1 + 1/2 + sqrt2 < 3 <=> sqrt2 < 3/2 <=> 2 < 9/4 + if not (2 < F(9, 4)): + return False, 'value constant' + return True, {'gradient_constant': str(c), 'value_constant': '3'} + + +class Mono: + def __init__(self, ell=F(0), K=F(0)): + self.ell, self.K = F(ell), F(K) + def __mul__(self, o): + return Mono(self.ell + o.ell, self.K + o.K) + def __pow__(self, e): + e = F(e); return Mono(self.ell*e, self.K*e) + def key(self): + return (self.ell, self.K) + + +def check_F5(mutant): + for d in (2, 3, 5): + for N in (1, 2, 7): + ell, K0 = Mono(1, 0), Mono(0, 1) + lhs = (K0*ell**(-1))**F(d*N, 2) * ((K0**F(d, 2))*(ell**(1 + F(d, 2))))**N + want = (F(N), F(d*N)) + if mutant == 'M4': + want = (F(N, 2), F(d*N)) + if lhs.key() != want: + return False, 'exponent ledger fails for d=%d N=%d: %s' % (d, N, lhs.key()) + return True, {'ledger': 'K0^(dN) ell^N'} + + +def check_F6(mutant): + for rho in (F(1), F(1, 3), F(6)): + for N in range(1, 7): + radii = [F(j, 2*N)*rho for j in range(1, N + 1)] + hw = rho/(8*N) + # nearest approach between consecutive shells, and from the origin to the first shell + gaps = [radii[0] - hw] + [(radii[j + 1] - hw) - (radii[j] + hw) for j in range(N - 1)] + if min(gaps) < rho/(4*N): + return False, 'shell separation' + # from y with |y| >= rho: |y| - (radii[-1] + hw) >= rho/4 + if rho - (radii[-1] + hw) < rho/4: + return False, 'separation from y' + # r_ell^2 = ell/K0 <= ell <= rho^2/(64 N^2) = hw^2 + ell = rho*rho/(64*N*N) + if ell > hw*hw: + return False, 'ball radius exceeds the shell half-width' + return True, {'N_range': '1..6', 'separation': 'rho/(4N) between sites, rho/4 from y'} + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--mutant', default=None) + args = ap.parse_args() + mutant = args.mutant + if mutant is not None and mutant not in ('M1', 'M2', 'M3', 'M4', 'M5'): + sys.stderr.write('unknown mutant label\n'); sys.exit(2) + results = {} + ok_all = True + for name, fn in (('F1_flat_component_two_maxima', check_F1), ('F2_uphill_segment', check_F2), + ('F3_near_cubic_consistency', check_F3), ('F4_lemma3_constants', check_F4), + ('F5_exponent_ledger', check_F5), ('F6_shell_geometry', check_F6)): + ok, info = fn(mutant) + results[name] = {'passed': bool(ok), 'info': info} + ok_all = ok_all and ok + out = {'object': 'CL-FAR-ELDER-FLAT-RIDGE-20260930-v1', 'scientific_effect': 'NONE', 'passed': ok_all, + 'checks': results} + print(json.dumps(out, indent=1, sort_keys=True)) + sys.exit(0 if ok_all else 1) + + +if __name__ == '__main__': + main() From 85f0586a468c2b2f73af0e340d251e33a52caade Mon Sep 17 00:00:00 2001 From: "Claude Fable 5.1" Date: Wed, 30 Sep 2026 12:49:48 +0000 Subject: [PATCH 2/5] Far elder flat ridge: run the identity check when a bound source changes (workflow paths; Codex 4144690976) Scientific effect NONE; no packet bytes change. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .github/workflows/far-elder-flat-ridge.yml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/.github/workflows/far-elder-flat-ridge.yml b/.github/workflows/far-elder-flat-ridge.yml index c68ffb44e..73231247e 100644 --- a/.github/workflows/far-elder-flat-ridge.yml +++ b/.github/workflows/far-elder-flat-ridge.yml @@ -5,6 +5,15 @@ name: Far elder flat-ridge exact controls paths: - 'frontiers/far_elder_flat_ridge_20260930/**' - '.github/workflows/far-elder-flat-ridge.yml' + # bound sources (consumed and cited_only in SOURCES.json): a change to any of them must re-run the identity check + - '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/three_fronts_20260924/LIFETIME_REMAINDER.md' + - 'frontiers/c7_zero_gap_limit_20260929/PROOF.md' + - 'frontiers/unrestricted_selection_difference_20260929/PROOF.md' + - 'reviews/c7_nonvanishing_openai_20260929/REVIEW.md' workflow_dispatch: permissions: From 5e0b31c8304e3a6ef96a5ee28c8faab5f9fdf799 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 2 Oct 2026 16:58:17 +0000 Subject: [PATCH 3/5] Far elder flat ridge v1.1: merged context (#187, #191, #198, #220, #229); Remark 6 on the dependence on rho - #187 is merged (c2f1270; blob 07260114, a status-only change from the 37dcf6ef that v1 read); it moves to cited_only. - Remark 5 is rewritten for the merged expansions: the far elder density enters #220/#229 only at the fixed r_0^*, where #187's O(ell^(2/3)) is already below ell^(3/7). Theorem G changes no merged statement; it removes the far term as a limit on any future improvement. - Remark 6 records the two conditional consequences OpenAI Codex posted here (5938629116 diagonal cutoff and counterexample; 5940268333 moving contact tail, conditional on merged #198) and proves from the latter's (2.4) that any constant in (0.2) satisfies C(d, L, rho, N) >= c_N rho^(1-4N). - The workflow triggers on the new cited sources. Theorem G, sections 1-3, Remarks 1-4, flat_ridge_check.py and RESULTS.json are unchanged. Scientific effect NONE. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .github/workflows/far-elder-flat-ridge.yml | 5 + .../far_elder_flat_ridge_20260930/PROOF.md | 95 ++++++++++--- .../far_elder_flat_ridge_20260930/README.md | 17 ++- .../SOURCES.json | 126 +++++++++++++++--- 4 files changed, 210 insertions(+), 33 deletions(-) diff --git a/.github/workflows/far-elder-flat-ridge.yml b/.github/workflows/far-elder-flat-ridge.yml index 73231247e..32f9a40fb 100644 --- a/.github/workflows/far-elder-flat-ridge.yml +++ b/.github/workflows/far-elder-flat-ridge.yml @@ -14,6 +14,11 @@ name: Far elder flat-ridge exact controls - 'frontiers/c7_zero_gap_limit_20260929/PROOF.md' - 'frontiers/unrestricted_selection_difference_20260929/PROOF.md' - 'reviews/c7_nonvanishing_openai_20260929/REVIEW.md' + - 'frontiers/far_elder_rate_20260930/PROOF.md' + - 'frontiers/remainder_vanishing_20260930/PROOF.md' + - 'frontiers/remainder_rate_20260930/PROOF.md' + - 'frontiers/elder_third_order_20261001/PROOF.md' + - 'frontiers/third_order_rate_20261001/PROOF.md' workflow_dispatch: permissions: diff --git a/frontiers/far_elder_flat_ridge_20260930/PROOF.md b/frontiers/far_elder_flat_ridge_20260930/PROOF.md index 50cfbf4fc..0b089b894 100644 --- a/frontiers/far_elder_flat_ridge_20260930/PROOF.md +++ b/frontiers/far_elder_flat_ridge_20260930/PROOF.md @@ -1,11 +1,18 @@ # Living bars have flat components: the far elder density is `O(ℓ^N)` for every `N` -Object: CL-FAR-ELDER-FLAT-RIDGE-20260930-v1. -Author: Anthropic Claude (claude.ai session `session_01NMeKEismAyeqgdB4sy2NJU`), 30 September 2026. +Object: CL-FAR-ELDER-FLAT-RIDGE-20260930-v1.1. +- v1, `85f0586`. xAI read Slice A (5379778152), and a scoped check verified two control identities (5932225117). +- v1.1, 2 October 2026. It records what has changed around the note; Theorem G and its proof are unchanged. + - Math- #187 is merged at `c2f1270`, with a status-only change to its blob, now `07260114`. + - Remark 5 is rewritten for the merged expansions of the elder density: #191, #198, #220 and #229. + - The new Remark 6 records the two conditional consequences that OpenAI Codex posted on this PR (5938629116, + 5940268333). It proves from them that the constant in (0.2) must blow up at least like `ρ^{1−4N}` as `ρ ↓ 0`. + - §7 lists the changed bytes. +Author: Anthropic Claude (claude.ai session `session_01NMeKEismAyeqgdB4sy2NJU`), 30 September 2026 (v1.1: 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 claimed. Same GitHub account as every lane; zero organizational independence. Successor in rate to Math- #187 (`CL-FAR-ELDER-RATE-20260930-v1`, -`O(ℓ^{2/3})`), which it does not modify and whose barrier lemma it does not use. +`O(ℓ^{2/3})`; merged at `c2f1270`), which it does not modify and whose barrier lemma it does not use. ## 0. Statement @@ -23,7 +30,7 @@ and the far elder density per unit volume at lifetime `ℓ` (the canonical marke ν_eld^{far,ρ}(ℓ) = ∫_{dist(0,y) ≥ ρ} ∫_R p_y(v_{b,ℓ}) E_{Q_{y,b,ℓ}}[W(f) e_y(f)] db dy. (0.1) [P] §14's argument gives `ν_eld^{far,ρ}(ℓ) ≤ C` on `(0, 1]` ((14.1) is its case `ρ = r_0`); [Z] gives -`ν_eld^{far,ρ}(ℓ) → 0` with no rate; Math- #187 gives `O(ℓ^{2/3})`. The SIDE24 manuscript's Proposition A.3.2 / A.3.2′ asserts `O(ℓ)` without a valid proof (July audit +`ν_eld^{far,ρ}(ℓ) → 0` with no rate; Math- #187 (merged) gives `O(ℓ^{2/3})`. The SIDE24 manuscript's Proposition A.3.2 / A.3.2′ asserts `O(ℓ)` without a valid proof (July audit F-02). **Theorem G.** For every `ρ ∈ (0, L/4]` and every integer `N ≥ 1` there is `C = C(d, L, ρ, N) < ∞` such that @@ -56,8 +63,9 @@ the component `C_t` meets every sphere `∂B(x_0, r)`, `0 < r < ρ`, and on `C_t **What is not claimed.** No statement about the far *rejected* density (which stays of order one: [U] (U1) gives it the lower bound `c_* > 0` at `ρ = r_0`, and [Z] identifies its limit); no near-pair statement (Lemma 1 is consistent with the near law but adds nothing there, §4); no numerical `C`; no uniformity in `L`, `d`, `N` or -`ρ ↓ 0`; nothing about the true order of `ν_eld^{far,ρ}` beyond (0.2) (§4 records the expectation that it is -super-polynomially small; no rate is conjectured). +`ρ ↓ 0` (Remark 6: uniformity in `ρ` fails, conditionally on a posted estimate); nothing about the true order of +`ν_eld^{far,ρ}` beyond (0.2) (§4 records the expectation that it is super-polynomially small at fixed `ρ`; no rate is +conjectured). ## 1. Proofs of the deterministic lemmas @@ -232,12 +240,56 @@ is bounded on `(0, 1]`) gives (0.2). The cumulative and moment statements follow itself — a small-ball-type event in `C¹`, though not a standard one (the set is random and the band is pinned). The expectation is that `ν_eld^{far,ρ}` is super-polynomially small; no rate is conjectured, and the `N`-site argument cannot produce one because `C_N` grows with `N`. -5. **For the manuscript.** In Theorem R's near/far decomposition ([R] §7, `ρ = r_0`), the far *elder* term is - `O(ℓ^N)` for every `N`; Theorem R's `O(1)` remainder is unchanged — it comes from the near terms (R16) (the - near candidate contact error) and (R18) (the near pairing loss), and, for the candidate density, from the far - rejected `O(1)` of [P] (14.1). The manuscript's A.3.2′ (far elder contribution `O(1)`, hence `o(ℓ^{−1/3})` - relative) rests on the reviewed (14.1) and should stay; this note, like #187, is an unreviewed candidate rate - that the V3 text may cite as such, not a replacement of a reviewed statement. +5. **For the manuscript, and the merged expansions.** (Rewritten in v1.1.) Since v1 the elder density has been expanded on + `main`, each result at its packet's stated conditional scope: + - #191 (R+.2): `ν_eld = cℓ^{−1/3} + o(1)`; + - #198 Theorem R++: `ν_eld = cℓ^{−1/3} + O(ℓ^{1/4})`; + - #220 Theorem E3, and #229 Theorem E3⁺: + + ν_eld(ℓ) = cℓ^{−1/3} + c₁ℓ^{1/4} + c₂ℓ^{1/3} + ν_eld^{far,r_0^*}(ℓ) + O(ℓ^{3/7}) (#229 (E3⁺.0)). + + The far elder density enters these expansions only at the one fixed separation `r_0^* ≤ L/(4√2) < L/4` (#191 §0). + - #229 bounds that term by #187's Theorem F at `ρ = r_0^*`, which is `O(ℓ^{2/3})`. This is below `ℓ^{3/7}`, so the far + term does not limit the current remainder, and Theorem G changes no merged statement. + - What Theorem G adds is that the term is `O(ℓ^N)` for every `N`. By #229's equivalence, for `0 < θ ≤ 3/7`, + `ν_eld − cℓ^{−1/3} − c₁ℓ^{1/4} − c₂ℓ^{1/3} = O(ℓ^θ)` if and only if `ν_eld^{far,r_0^*} = O(ℓ^θ)`. So the far term + would not limit any future improvement of the near and intermediate estimates, whereas #187 alone stops at + `ℓ^{2/3}`. The same holds for the rejected density, #229 (R⁺.1). + - The manuscript's A.3.2′ (a far elder contribution `O(1)`, hence `o(ℓ^{−1/3})` relative) rests on the reviewed + (14.1) and should stay. This note is an unreviewed candidate rate that the V3 text may cite as such, not a + replacement of a reviewed statement. +6. **The dependence on `ρ`.** (New in v1.1.) Theorem G is a statement at a fixed separation, and its constant cannot be + uniform as `ρ ↓ 0`. Two results that OpenAI Codex posted on this PR make that precise. They are cited, not consumed, + and each is conditional on its stated sources; neither uses Theorem G as a premise except (a). + - (a) *A diagonal cutoff* (OA-FAR-DIAGONAL-CUTOFF-20261001-v1, comment 5938629116, conditional on (0.2)). There is a + deterministic cutoff `ρ(ℓ) → 0`, nondecreasing in `ℓ`, with `ρ(ℓ)/ℓ^a → ∞` for every `a > 0`, such that + `ν_eld^{far,ρ(ℓ)}(ℓ) = o(ℓ^n)` for every `n` (its Proposition D, with a cumulative form, D-cum). Its nonnegative + measure (D5) shows that (0.2) at each fixed `ρ`, by itself, implies nothing at an algebraic cutoff `ρ = Cℓ^a`. + - (b) *The moving contact tail* (OA-ELDER-MOVING-CONTACT-TAIL-20261001-v1, comment 5940268333). It is conditional on + merged #198 (Theorem R++, the proof of W.2, and W.3), with [P] and [R], and it does not use Theorem G. It retains + #198's contact tail and gives a uniform two-parameter estimate with an explicit `a_0 > 0` (its (2.1)): + + |ν_eld^{far,ρ}(ℓ) − (a_0/7)ℓ²ρ^{−7}| ≤ C_*[ℓ^{1/4} + ρ³ + ℓ⁴ρ^{−13}], 0 < ρ ≤ r_*, 0 < ℓ ≤ min(ℓ_*, ρ³) (its (2.4)). + + So `ν_eld^{far,ηℓ^a}(ℓ) ∼ (a_0/(7η⁷))ℓ^{2−7a}` for fixed `η > 0` and `1/4 < a < 1/3` (its (3.4)). At such cutoffs the + far elder density is not even `O(ℓ)`. + - (c) *Consequence for the constant in (0.2).* Suppose (b)'s (2.4) holds for the density (0.1). Then for every `N ≥ 1` + there are `c_N > 0` and `ρ_N > 0` such that every constant admissible in (0.2) satisfies + + C(d, L, ρ, N) ≥ c_N ρ^{1−4N}, 0 < ρ ≤ ρ_N. (R6.1) + + *Proof.* Fix `M ≥ 1` with `C_*M^{1/4} ≤ (a_0/14)M²`, and put `ℓ = Mρ⁴`. Take `ρ` so small that + `ρ ≤ min(r_*, 1/M, (ℓ_*/M)^{1/4})`, `Mρ⁴ ≤ 1` and `C_*(1 + M⁴)ρ² ≤ (a_0/28)M²`. Then `ℓ ≤ min(ℓ_*, ρ³)`, and (2.4) + applies: + - its main term is `(a_0/7)ℓ²ρ^{−7} = (a_0/7)M²ρ`; + - its error is at most `C_*M^{1/4}ρ + C_*(1 + M⁴)ρ³ ≤ (a_0/14 + a_0/28)M²ρ`. + + Hence `ν_eld^{far,ρ}(Mρ⁴) ≥ (a_0/28)M²ρ`, and (0.2) at `ℓ = Mρ⁴` gives `C(ρ, N) ≥ (a_0/28)M^{2−N}ρ^{1−4N}`. ∎ + - So the bound `C(ρ, N)ℓ^N ≥ c_Nρ(ℓ/ρ⁴)^N` of (0.2) can be informative only for `ℓ ≪ ρ⁴`, that is `ρ ≫ ℓ^{1/4}`. This + is the left end `a = 1/4` of the range in (b). + - Open: whether `ν_eld^{far,ρ}(ℓ) = O(ℓ^N)` for every `N` when `ρ ≥ ℓ^a` with `0 < a < 1/4`. Neither (0.2) nor (b) + decides it, since (2.4)'s error `ℓ^{1/4}` exceeds its main term there. A quantitative form of §2, tracking `ρ` in the + `N`-site conditional density bound (2.1) and in (2.a), is what the proof of Theorem G would need for it. ## 5. Sources (exact identities in `SOURCES.json`) @@ -250,11 +302,14 @@ is bounded on `(0, 1]`) gives (0.2). The cumulative and moment statements follow | [R] | `frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md` (blob `247b3ecf`) | Theorem R, §7 near/far split (cited only) | | [Z] | `frontiers/c7_zero_gap_limit_20260929/PROOF.md` (blob `5b6328ea`) | far rejected limit (cited only; OpenAI candidate, non-OpenAI review required) | | [U] | `frontiers/unrestricted_selection_difference_20260929/PROOF.md` (blob `5a55b179`) | (U1) lower bound (cited only; OpenAI review `reviews/c7_nonvanishing_openai_20260929`) | -| #187 | `frontiers/far_elder_rate_20260930/PROOF.md` (Math- #187, unmerged) | predecessor rate `O(ℓ^{2/3})` (cited only; §2 restates its fixed-separation facts from [P] directly) | +| #187 | `frontiers/far_elder_rate_20260930/PROOF.md` (Math- #187, merged at `c2f1270`; blob `07260114`, a status-only change from the `37dcf6ef` that v1 read) | predecessor rate `O(ℓ^{2/3})` (cited only; §2 restates its fixed-separation facts from [P] directly) | +| #191, #198 | `frontiers/remainder_vanishing_20260930/PROOF.md` (`441152df`), `frontiers/remainder_rate_20260930/PROOF.md` (`abfb98ae`), both merged | `r_0^*` (#191 §0); Theorem R++ (Remark 5); #198 is a premise of Remark 6(b), not of this note (cited only) | +| #220, #229 | `frontiers/elder_third_order_20261001/PROOF.md` (`c8767dde`), `frontiers/third_order_rate_20261001/PROOF.md` (`110ed33a`), both merged | (E3.0), (E3⁺.0), (E3⁺.1), (R⁺.1) and the equivalence after them (Remark 5; cited only) | +| OA-FD, OA-MT | Math- #188 comments 5938629116 (OA-FAR-DIAGONAL-CUTOFF-20261001-v1) and 5940268333 (OA-ELDER-MOVING-CONTACT-TAIL-20261001-v1), OpenAI Codex | Proposition D, D-cum and (D5); (2.1), (2.4), (3.4) (Remark 6; cited only, not verified by the workflow) | | lit. | Adler–Taylor, *Random Fields and Geometry* (2007), Thm 2.1.1 (Borell–TIS) | standard inequality, §2(c) | Consumed: [P] §§1, 2, 4 and 8 (their arguments, applied at the far pins `0`, `y`), 9 (as [E2]), 14; [E1]; [E2]; -[REC] §§1, 5, 7. Cited only: [R], [Z], [U], #187. +[REC] §§1, 5, 7. Cited only: [R], [Z], [U], #187, #191, #198, #220, #229, OA-FD, OA-MT. ## 6. Exact controls (`flat_ridge_check.py`; stdlib; exact rationals; byte-identical under `-O`) @@ -288,4 +343,14 @@ B: §2 (a)–(d) — the uniform conditional density bound with `N` extra sites decomposition and the use of Borell–TIS, and the far-pin genericity (d); whether (2.1) is stated at the right scope. C: §3 — the volume/Markov step (3.1), the tower-property step, the `K_0` splitting and the choice (Step 4), and the - integration in `(b, y)`; Remarks 1–3 for consistency with [U], [Z], [R] and #187. + integration in `(b, y)`; Remarks 1–3 for consistency with [U], [Z], [R] and #187; Remarks 5–6 (v1.1). + +**Changed bytes in v1.1** (for a delta check against v1, `85f0586`, blob `50cfbf4f`): +- *Header:* the object label and versions, the author line, the #187 merge in the Disposition paragraph. +- *§0:* "#187 (merged)", and the `ρ ↓ 0` clause of "What is not claimed". +- *§4:* Remark 5 (rewritten) and Remark 6 (new; its item (c) is the only new mathematics). +- *§5:* the #187 row, three new rows (#191/#198, #220/#229, OA-FD/OA-MT), and the cited-only list. +- *§7:* the Remarks 5–6 clause of Slice C, and this list. + +§§1–3 (Lemmas 1–3, §2 (a)–(d), the proof of Theorem G), Remarks 1–4, §6, `flat_ridge_check.py` and `RESULTS.json` +are unchanged. diff --git a/frontiers/far_elder_flat_ridge_20260930/README.md b/frontiers/far_elder_flat_ridge_20260930/README.md index 65fbd62da..4bec2ad81 100644 --- a/frontiers/far_elder_flat_ridge_20260930/README.md +++ b/frontiers/far_elder_flat_ridge_20260930/README.md @@ -1,15 +1,28 @@ -# Far elder density: flat components and the `O(ℓ^N)` rate (CL-FAR-ELDER-FLAT-RIDGE-20260930-v1) +# Far elder density: flat components and the `O(ℓ^N)` rate (CL-FAR-ELDER-FLAT-RIDGE-20260930-v1.1) Author-side proof candidate, Anthropic Claude, 30 September 2026. Scientific effect NONE. Nonauthor review required. **Statement.** For the periodized Gaussian field on the torus and a fixed separation `ρ`, the density (per unit volume) of elder pairs `(M, S)` at torus distance `≥ ρ` with lifetime `ℓ` is `O(ℓ^N)` for every `N` as `ℓ ↓ 0` (Theorem G); all inverse-lifetime moments of the far elder population are finite. Previously on file: bounded -([P] (14.1)), `o(1)` without rate ([Z]), `O(ℓ^{2/3})` (Math- #187, the predecessor, not modified here). The +([P] (14.1)), `o(1)` without rate ([Z]), `O(ℓ^{2/3})` (Math- #187, the predecessor, merged at `c2f1270`, not modified +here). The manuscript's Proposition A.3.2 asserts `O(ℓ)` without a valid proof (July audit F-02); its restatement A.3.2′ (`O(1)`, resting on the reviewed [P] (14.1)) stands, and Theorem G is an author-side candidate rate with every polynomial exponent, offered for nonauthor review — not a replacement of a reviewed statement. +**v1.1 (2 October 2026; Theorem G and its proof unchanged).** It records what has changed around the note. +- Remark 5 places Theorem G in the merged expansions of the elder density (#191, #198, #220, #229). There the far + density enters only at the fixed separation `r_0^*`, and #187's `O(ℓ^{2/3})` already lies below the current remainder + `ℓ^{3/7}`. So Theorem G changes no merged statement. It removes the far term as a limit on any future improvement. +- Remark 6 records two conditional consequences that OpenAI Codex posted on this PR: + - a diagonal cutoff `ρ(ℓ) → 0` with all-order far decay, and a measure showing that fixed-`ρ` flatness alone gives + nothing at an algebraic cutoff (5938629116); + - the moving contact tail `ν_eld^{far,ρ}(ℓ) ≈ (a_0/7)ℓ²ρ^{−7}` for `ℓ^{1/3} ≪ ρ ≪ ℓ^{1/4}`, conditional on merged #198 + (5940268333). +- From the second, Remark 6 proves that the constant of Theorem G must blow up at least like `ρ^{1−4N}` as `ρ ↓ 0`. So the + bound is informative only for `ρ ≫ ℓ^{1/4}`. Whether all-order decay holds for `ρ ≥ ℓ^a`, `a < 1/4`, is open. + **Mechanism.** *Living bars have flat components* (Lemma 1, deterministic, two lines): if the bar of a maximum `x_0` with `f(x_0) = b` is alive at level `t`, then on the component of `x_0` in `{f > t}` every point satisfies `|∇f|² ≤ 2K(b − f) ≤ 2K(b − t)`, `K ≥ sup‖D²f‖` — walk uphill from any point for a distance `|∇f|/K`; the walk diff --git a/frontiers/far_elder_flat_ridge_20260930/SOURCES.json b/frontiers/far_elder_flat_ridge_20260930/SOURCES.json index 742af3565..993f5cb48 100644 --- a/frontiers/far_elder_flat_ridge_20260930/SOURCES.json +++ b/frontiers/far_elder_flat_ridge_20260930/SOURCES.json @@ -1,12 +1,13 @@ { "schema": 1, "scientific_effect": "NONE", - "object": "CL-FAR-ELDER-FLAT-RIDGE-20260930-v1", - "kind": "author-side proof candidate (Lemmas 1-3 deterministic; Theorem G conditional on the reconciled [P] interfaces and the standard Borell-TIS inequality); nonauthor analytic review required", + "object": "CL-FAR-ELDER-FLAT-RIDGE-20260930-v1.1", + "kind": "author-side proof candidate (Lemmas 1-3 deterministic; Theorem G conditional on the reconciled [P] interfaces and the standard Borell-TIS inequality; v1.1: Remark 5 rewritten for the merged expansions #191/#198/#220/#229, Remark 6 records the posted Codex consequences and proves C(rho, N) >= c_N rho^(1-4N) conditionally on their (2.4); Theorem G and its proof unchanged); nonauthor analytic review required", "author": "Anthropic Claude", "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", "read_at": { - "branch_base": "de54d1da2f6cdde59df3c34bb50ecd85c25ca333" + "branch_base": "de54d1da2f6cdde59df3c34bb50ecd85c25ca333", + "main_merged_in_v1_1": "2d8616ef1b45c4d5bb0970dcc20453bb4126114d" }, "consumed": [ { @@ -74,18 +75,46 @@ "git_blob": "64794e5801b70d950c7e1202f7b6b7d07055cbb6", "tag": "U-review", "use": "the nonauthor review binding for [U]" - } - ], - "cited_unmerged": [ + }, { "path": "frontiers/far_elder_rate_20260930/PROOF.md", - "pr": "d6g8k5htny-coder/Math-#187", - "commit": "ecd47e7b1d447eefec963b1fa8395777db09a190", - "git_blob": "37dcf6ef933251c8890ab653cafd648610779342", - "bytes": 16413, - "sha256": "67f606327b66a2b4f1b8c67a57d119ac9ddfd2ce827ca8cb0c4daefa31904a3b", + "bytes": 16493, + "sha256": "ed908ed97348ed708c6fd06e5c09f6290ab0e8c47e6384b7bdded321452f523b", + "git_blob": "072601145601a1021037a2e91bf8826c1c971ecc", "tag": "187", - "use": "cited only: predecessor rate O(ell^(2/3)); its (2.1)-(2.2) restated in \u00a72 from [P]; nothing unmerged is consumed; not verified by the workflow" + "use": "cited only: predecessor rate O(ell^(2/3)) (Theorem F); merged at c2f1270 with blob 07260114, a status-only change from the 37dcf6ef that v1 read (#182 recorded as integrated); its (2.1)-(2.2) are restated in section 2 from [P]; nothing of it is consumed" + }, + { + "path": "frontiers/remainder_vanishing_20260930/PROOF.md", + "bytes": 25353, + "sha256": "0cb5b949261476f10e539677e2744e3288752474393af25ba787e67b1350f32a", + "git_blob": "441152dfc1d8d00cb268cebdb0394212a5bfacdb", + "tag": "191", + "use": "cited only (Remark 5): (R+.2) nu_eld = c ell^(-1/3) + o(1); section 0, the admissible radius r_0^* <= L/(4 sqrt 2)" + }, + { + "path": "frontiers/remainder_rate_20260930/PROOF.md", + "bytes": 33131, + "sha256": "0b690df6ac40707ca06783f5641d8b480277c716df75b1031d84ee53a0575f72", + "git_blob": "abfb98ae41d66a86d3cb094162db6547d0f29e7e", + "tag": "198", + "use": "cited only (Remark 5): Theorem R++, nu_eld = c ell^(-1/3) + O(ell^(1/4)); a premise of the cited Codex consequence OA-MT (Remark 6(b)), not of this note" + }, + { + "path": "frontiers/elder_third_order_20261001/PROOF.md", + "bytes": 70544, + "sha256": "74b5f031ba5be6f50b5e543636136df1d9b5fad0fcd2c8210320cfef02f80e37", + "git_blob": "c8767ddecf1041d234f685e95af582073a7be393", + "tag": "220", + "use": "cited only (Remark 5): Theorem E3, (E3.0) and (E3.3), the far elder density at the fixed separation r_0^*" + }, + { + "path": "frontiers/third_order_rate_20261001/PROOF.md", + "bytes": 37626, + "sha256": "5de5a6c7b942a71675c812000ade30c16766f02ee388e8dc3e1c51dde5297f7d", + "git_blob": "110ed33a57902bef11873807e722fde3888b59fb", + "tag": "229", + "use": "cited only (Remark 5): Theorem E3+ (E3+.0), (E3+.1), (R+.1) and the equivalence for 0 < theta <= 3/7" } ], "literature": [ @@ -105,8 +134,8 @@ "files": [ { "path": "PROOF.md", - "bytes": 22806, - "sha256": "957f9c5e6557a558b2c055fa2a1f11ba301581995b8958658fad2edf47136f57" + "bytes": 29110, + "sha256": "967148439e32e8e5d6c06a12df5cc7c1eb2475fe6828e4aeb3748c48817a4cba" }, { "path": "flat_ridge_check.py", @@ -120,8 +149,73 @@ }, { "path": "README.md", - "bytes": 2845, - "sha256": "aed92c1d8b7f767e2b9c8571f33d0e72966366f0b4234586559420bc8b209593" + "bytes": 3999, + "sha256": "4404bb60cfbe10d0ae677f8136330629797b97d374508efea02a4b6cb7a8c11b" + } + ], + "supersedes": { + "object": "CL-FAR-ELDER-FLAT-RIDGE-20260930-v1", + "head": "85f0586a468c2b2f73af0e340d251e33a52caade", + "proof_blob": "50cfbf4fcb9a3526f979eaedf885d42824a3c3a3" + }, + "cited_comments": [ + { + "tag": "OA-FD", + "object": "OA-FAR-DIAGONAL-CUTOFF-20261001-v1", + "where": "Math- #188 comment 5938629116", + "author": "OpenAI Codex root, under Dylan Roy's delegation (same GitHub account)", + "input": "this note at 85f0586, PROOF blob 50cfbf4f: (0.1) and Theorem G (0.2)", + "use": "Remark 6(a): Proposition D (a diagonal cutoff), D-cum, and the nonnegative measure (D5)", + "review": "fresh nonauthor OpenAI scoped PASS disclosed in the comment (organizational independence 0)" + }, + { + "tag": "OA-MT", + "object": "OA-ELDER-MOVING-CONTACT-TAIL-20261001-v1", + "where": "Math- #188 comment 5940268333", + "author": "OpenAI Codex /root/review_density_proof_gaps, under Dylan Roy's delegation (same GitHub account)", + "input": "merged #198 (blob abfb98ae: Theorem R++, the proof of W.2, W.3) with [P] and [R]; Theorem G is not a premise", + "use": "Remark 6(b)-(c): (2.1) a_0 > 0, (2.4) the uniform two-parameter estimate, (3.4); (R6.1) here is derived from (2.4)", + "review": "fresh nonauthor OpenAI conditional technical pass disclosed in the comment (organizational independence 0)" + } + ], + "nonauthor_reviews": [ + { + "slice": "A (note; not an acceptance)", + "reviewer": "xAI / Grok team (same GitHub account; organizational independence 0)", + "review": "pullrequestreview-5379778152", + "at": "85f0586", + "verdict": "NOT READY (Lemma 1 checked as the standard uphill bound with its sharp equality case; living-bar hypothesis, shell count and Kac-Rice insertion not checked; behind main)", + "findings": [] + }, + { + "slice": "scoped deterministic check (not a review of Theorem G)", + "reviewer": "same-account lane (unsigned in the comment; organizational independence 0)", + "comment": "5932225117", + "at": "85f0586", + "verdict": "two control identities exact: Lemma 1 sharpness on f = b - K|x|^2/2, and the younger lifetime 16/15 in F1", + "findings": [] + } + ], + "amendments": [ + { + "label": "v1.1", + "files_changed": [ + "PROOF.md", + "README.md", + "SOURCES.json", + ".github/workflows/far-elder-flat-ridge.yml" + ], + "unchanged": [ + "flat_ridge_check.py", + "RESULTS.json" + ], + "proof_parts_unchanged": [ + "sections 1-3", + "Theorem G", + "Remarks 1-4", + "section 6" + ], + "reason": "status of #187 (merged); Remark 5 for the merged #191/#198/#220/#229; Remark 6 records OA-FD and OA-MT and derives (R6.1); requested context: xAI 5379778152 and the scoped check 5932225117 note that #191 and #198 have merged" } ] } From 817aa26297380c3f23c4c5622d9e796434b98e93 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 13:14:23 +0000 Subject: [PATCH 4/5] Far elder packet v1.2: incorporate the reviewed C89 v1.1 extension (PROOF.md unchanged) Answers the incorporation request in #188 comment 5963266074 (pickup 5969476982). Additive only: PROOF.md ([G], blob 0b089b89, which C89 pins), flat_ridge_check.py and RESULTS.json are unchanged. Added, byte for byte from the public comments on this PR: - C89_V1_1_PROOF.md C89 v1.1, Theorem QSF (5963100306; 15039 B; 7d8d3063...), OpenAI/Codex root01a0bbb5 - C89_V1_PROOF.md historical v1 (5963042579; 14742 B; 74af6322...), AMEND retained - C89_V1_1_REVIEW.md full review, PASS_TECHNICAL_SCOPED (5963217842; 26692 B; d31e1aaf...) - c89_reviewer_controls.py and c89_reviewer_stdout.json: the reviewer's script (12190 B; 83982f11...) and stdout (1068 B; cee69d10...), extracted verbatim from that review Added (new): c89_replay.py, standard library only. It assembles the reviewer's --source-dir from the repository ([P], this PROOF.md as [G], the C89 copy), reruns the script under the current -O/-S flags, and requires the published stdout byte for byte; a one-byte change to the C89 copy must change the output. Locally the stdout is byte-identical under -B -S and -B -O -S. README.md gains an "Extension C89" section: the statement, its relation to Remark 6, and what C89 does not establish. SOURCES.json is now v1.2, with the six new files, an extensions record (exact identities, reviewer, verdict, consumed [G] parts) and an amendment entry. The workflow gains one step that runs the replay in both modes. Scientific effect: NONE. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .github/workflows/far-elder-flat-ridge.yml | 8 + .../C89_V1_1_PROOF.md | 307 ++++++++++++ .../C89_V1_1_REVIEW.md | 460 ++++++++++++++++++ .../C89_V1_PROOF.md | 303 ++++++++++++ .../far_elder_flat_ridge_20260930/README.md | 30 ++ .../SOURCES.json | 136 +++++- .../c89_replay.py | 96 ++++ .../c89_reviewer_controls.py | 335 +++++++++++++ .../c89_reviewer_stdout.json | 1 + 9 files changed, 1669 insertions(+), 7 deletions(-) create mode 100644 frontiers/far_elder_flat_ridge_20260930/C89_V1_1_PROOF.md create mode 100644 frontiers/far_elder_flat_ridge_20260930/C89_V1_1_REVIEW.md create mode 100644 frontiers/far_elder_flat_ridge_20260930/C89_V1_PROOF.md create mode 100644 frontiers/far_elder_flat_ridge_20260930/c89_replay.py create mode 100644 frontiers/far_elder_flat_ridge_20260930/c89_reviewer_controls.py create mode 100644 frontiers/far_elder_flat_ridge_20260930/c89_reviewer_stdout.json diff --git a/.github/workflows/far-elder-flat-ridge.yml b/.github/workflows/far-elder-flat-ridge.yml index 32f9a40fb..eff459afb 100644 --- a/.github/workflows/far-elder-flat-ridge.yml +++ b/.github/workflows/far-elder-flat-ridge.yml @@ -76,3 +76,11 @@ jobs: print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) PY git diff --exit-code + - name: Replay the published C89 v1.1 reviewer controls on the exact sources, both modes + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S frontiers/far_elder_flat_ridge_20260930/c89_replay.py + python -B -O -S frontiers/far_elder_flat_ridge_20260930/c89_replay.py + git diff --exit-code diff --git a/frontiers/far_elder_flat_ridge_20260930/C89_V1_1_PROOF.md b/frontiers/far_elder_flat_ridge_20260930/C89_V1_1_PROOF.md new file mode 100644 index 000000000..686122200 --- /dev/null +++ b/frontiers/far_elder_flat_ridge_20260930/C89_V1_1_PROOF.md @@ -0,0 +1,307 @@ +# Quantitative separated jets and a shrinking far-elder region + +Object: OA-QSF-20261002-C89-v1.1. Author: OpenAI / Codex, root01a0bbb5. +Dylan Roy — delegated AI work. Personal reading PENDING; organizational +independence 0; scientific effect NONE. This is an additive analytic candidate, +not a change to a scientific status register. Review disposition belongs in +REVIEW.md, separately from this author statement. + +## 0. Exact interface and result + +Fix d >= 2 and L > 0. Use the centered, variance-one periodized Gaussian field +on X = R^d/(L Z^d) of [P] §1, with Fourier weights + + a_n = exp(-2 pi^2 |n|^2/L^2) / sum_k exp(-2 pi^2 |k|^2/L^2) > 0. + +[P] is `source/P.md`, SHA256 +9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7, +40261 bytes. [G] is `source/G.md`, Math- PR188 head +5e0b31c8304e3a6ef96a5ee28c8faab5f9fdf799, blob +0b089b894960b0ee53fc2885e054d73ab73472bd, SHA256 +967148439e32e8e5d6c06a12df5cc7c1eb2475fe6828e4aeb3748c48817a4cba, +29110 bytes. Its complete source interface is preserved in +`source/G_SOURCES.json`. We consume [P] §§1–2 and [G]'s canonical marked +Kac–Rice definition (0.1), deterministic Lemmas 1–3, and conditional genericity +§2(d). We do not consume Remark 6 or the OA-FD/OA-MT consequences, the SIDE24 +coefficient, a finite-radius RN certificate, or a near-pair asymptotic. +The marked-measure construction retains [G]'s E2 repair and REC interpretation; +this note is not a new proof of those imported interfaces. + +Write O_y=(f(0),grad f(0),f(y),grad f(y)), v=(b,0,b-ell,0), Q for Gaussian +regression on O_y=v, H_0,H_y for the two Hessians, and + + W = |det H_0 det H_y| 1{H_0 negative definite, index H_y=d-1}. + +Let e_y be the ordinary global superlevel H_0 elder mark, not a branch-adjacency +mark. With p_y the density of O_y, define the canonical per-unit-spatial-volume +far-elder lifetime density + + F(ell,rho) = integral_{dist(0,y)>=rho} integral_R + p_y(v) E_Q[W e_y] db dy. (0.1) + +Let J=(d+1)(d+2)/2, the number of independent derivatives of orders 0,1,2 at +one site; a symmetric Hessian has d(d+1)/2 coordinates, not d^2. Put + + rho_* = min(1,L/4), + A_N = 24J + 12dN + 12N(N+1)(d+1). + +**Theorem QSF.** For every integer q>=1 set N=2(q+1). There is a finite constant +C_q=C(d,L,q), independent of ell,rho, such that + + F(ell,rho) <= C_q rho^(-A_N) ell^(q+1), (0.2) + +whenever 00, c>0, rho(ell)=c[log(e/ell)]^(-a), and every fixed +integer q>=1, F(ell,rho(ell))=O(ell^q) as ell decreases to zero. + +These are bounds on an actual elder-marked far population with a specified +moving spatial cutoff. They are not uniform in arbitrary shrinking cutoffs, +in L, d or q. They do not establish the contact-scale region, witness uniqueness, +the intermediate region inside rho(ell), or either direction of the full +canonical-witness/persistence correspondence. There is no weighted-Palm +normalizer Z_r in (0.1); dividing by one would change the statement. + +## 1. Constructive quantitative finite-jet rank + +**Lemma QJ.** Fix s>=1 distinct sites x_1,...,x_s with pairwise torus distance +at least delta, where 0= c(d,L,s) delta^[24(s-1)]. (1.1) + +The constant is strictly positive and finite. It can be constructed from +finitely many positive Fourier weights; no sampled-covariance inference occurs. + +Proof. Put omega=2pi/L and + + B_j(x)=sum_{k=1}^d [1-cos(omega(x_k-x_{j,k}))]. + +Choose coordinate differences in [-L/2,L/2]. The elementary inequality +sin t >= 2t/pi for 0<=t<=pi/2 gives + + B_j(x_i) >= 8 dist(x_i,x_j)^2/L^2 >= 8delta^2/L^2. + +The sum of absolute Fourier coefficients of B_j is at most 2d. For each i set + + Q_i(x)=product_{j!=i} [B_j(x)/B_j(x_i)]^2. + +It has value 1 at x_i, vanishes to order at least four at every other site, +has Fourier support |n|_infinity<=2(s-1), and has Fourier coefficient l1 norm +at most C delta^[-4(s-1)]. All its derivatives through order two at x_i have +the same bound, with a different C depending only on d,L,s. Here and below +C denotes a defined finite bound from the finite coefficient sum and its +frequency multipliers, never a constant allowed to depend on delta or the sites. + +For a multiindex alpha with |alpha|<=2 let R_{i,alpha}(h) be the Taylor polynomial +through total degree two of + + h^alpha / (alpha! Q_i(x_i+h)). + +The reciprocal is legitimate since Q_i(x_i)=1. If Q_i(x_i+h)=1+U_1(h)+U_2(h) ++O(|h|^3), its reciprocal through degree two is 1-U_1+U_1^2-U_2. Thus every +coefficient of R_{i,alpha} is bounded by C delta^[-8(s-1)]. Define the periodic +local coordinates z_k(x)=sin(omega(x_k-x_{i,k}))/omega and the trigonometric +polynomial + + P_{i,alpha}(x)=Q_i(x) R_{i,alpha}(z(x)). + +Since z(x_i+h)=h+O(|h|^3), its jets satisfy + + partial^gamma P_{i,alpha}(x_j) = 1{i=j,alpha=gamma}, |gamma|<=2. (1.2) + +At other sites the fourth-order zero of Q_i kills every derivative in question. +The Fourier support is |n|_infinity<=2s, and its coefficient l1 norm is bounded +by C_* delta^[-12(s-1)], uniformly over i,alpha and all separated configurations. +More precisely, choose C_Q to bound the coefficient l1 norm of Q_i after +factoring out delta^[-4(s-1)], and C_R to bound the sum of absolute monomial +coefficients of every R_{i,alpha} after factoring out delta^[-8(s-1)]. The +preceding derivative and reciprocal formulas construct both finite constants. +Each z-monomial of total degree at most two has Fourier coefficient l1 norm +at most C_Z=max(1,omega^(-2)). By the triangle and convolution inequalities, +the valid choice is C_*=C_Q C_R C_Z, a product of bounds, not their maximum. + +Let a_* = min_{|n|_infinity<=2s} a_n >0. For real coefficients t_{i,alpha} set +L_t=sum t_{i,alpha} partial^alpha|_{x_i}. Fourier expansion gives + + V_t=Var(L_t f)=sum_n a_n |L_t exp(i omega n.x)|^2. + +Writing P_{i,alpha}=sum p_n exp(i omega n.x), weighted Cauchy–Schwarz and (1.2) +give + + |t_{i,alpha}|^2 <= V_t sum |p_n|^2/a_n + <= V_t a_*^(-1) C_*^2 delta^[-24(s-1)]. + +Summing over sJ coordinates proves (1.1), with c=a_*/(sJ C_*^2). For s=1 +the empty product Q_i=1 supplies the same argument with exponent zero. +Every subvector has at least this covariance lower bound. If a subvector is +split into V,Z, its conditional covariance also has this lower bound: for z, +the Schur-complement variational formula minimizes Var(z.Z-a.V) over a, and +(1.1) bounds every such variance below by c delta^[24(s-1)] |z|^2. QED. + +This is deliberately conservative; it is a usable uniform power, not a sharp +collision exponent. The positivity of only the indicated finite cube suffices +for this rank estimate. The smooth field and moment arguments below additionally +use the summability of all Fourier modes of the stated Gaussian covariance. + +## 2. Two-pin weighted moments, with the separation tracked + +Let V_y=(O_y,H_0,H_y), with distinct symmetric Hessian coordinates. Its dimension +is 2J. Uniformly for dist(0,y)>=rho and 0= c rho^24, + lambda_max Sigma_y <= C. (2.1) + +The upper bound follows from the fixed finite derivative variances. Thus at +the slice v=(b,0,b-ell,0,H_0,H_y), 0=1, Gaussian regression gives + + E[K^p | V_y=v] <= C_p rho^(-12p) (1+|v|)^p. (2.3) + +Here is a direct uniform justification. Expand the real field into independent +standard-normal sine/cosine coefficients, with summable square-root spectral +amplitudes times (1+|n|)^2. For each standardized coefficient xi, its conditional +mean has absolute value at most sqrt(v^T Sigma_y^(-1)v), by covariance +Cauchy–Schwarz; its conditional centered variance is at most 1. Minkowski's +inequality, the spectral sum, and (2.1) bound the conditional L^p norm of K by +C_p(1+rho^(-12)|v|). The residual coefficients need not be independent of one +another. Infinite sums converge in conditional L^p(C^2) by the same summable +majorant. Gaussian regression, not conditioning on a positive-probability pin +event, defines these laws at every target v. + +Consequently, for p>=1 (and with the evident p=0 version), + + M_p(ell,rho) := integral_{dist(0,y)>=rho} integral_R + p_y(v) E_Q[W K^p] db dy + <= C_p rho^[-(24J+12p)]. (2.4) + +Indeed, disintegrate further onto the Hessians: p_y(v) times the conditional +Hessian density is exactly p_{V_y}(v,H_0,H_y). W is V_y-measurable and at most +|det H_0 det H_y|, a polynomially bounded function of degree 2d. Apply (2.2) +and (2.3), integrate the polynomial times the Gaussian in b,H_0,H_y, and bound +the y volume by L^d. This preserves the full determinant weight and integrates +over all birth heights. No unweighted-to-weighted probability substitution or +inverse random Hessian moment is used. + +## 3. N-site bound, retaining the weighted event + +Use exactly [G] §3's shells + + S_j={x: |dist(0,x)-j rho/(2N)|=rho, is separated by at +least delta=rho/(4N). Apply Lemma QJ with s=N+2 to the full two-jets, then take +the subvector (V_y,Z), where Z=(f(q_j),grad f(q_j))_{j=1}^N has m=N(d+1) +coordinates. Its conditional density given V_y, uniformly over all values, is +bounded by + + C_N rho^[-12N(N+1)(d+1)]. (3.1) + +Therefore the conditional probability of |f(q_j)-b|<=3ell and +|grad f(q_j)|<=3sqrt(K_0 ell) at all N sites is at most + + C_N rho^[-12N(N+1)(d+1)] K_0^(dN/2) ell^[N(1+d/2)]. (3.2) + +For 0=2, [G] Lemmas 1–3 force on the elder event +with K<=K_0 a near-critical ball of volume omega_d(ell/K_0)^(d/2) in every +shell. The pathwise product-volume bound [G](3.1), Tonelli, and (3.2) yield + + integral integral p_y E_Q[W e_y 1{K<=K_0}] + <= C_N rho^[-12N(N+1)(d+1)] K_0^(dN) ell^N M_0 + <= C_N rho^[-24J-12N(N+1)(d+1)] K_0^(dN) ell^N. (3.3) + +The shell product volume is at most L^(dN); this bound is independent of rho. +The tower step is valid because W is V_y-measurable, while (3.2) is uniform +in the conditioning values. No measurable choice of a point on each sphere +is needed: the forced lower volume is pathwise, and only measurable shell +integrals enter Tonelli. The conditional generic locus and the actual elder +topology are those explicitly imported from [G]; no claim that a local saddle +must be the elder saddle is introduced. + +For the complement, Markov's inequality and (2.4) give + + integral integral p_y E_Q[W e_y 1{K>K_0}] + <= K_0^(-p) M_p + <= C_p K_0^(-p) rho^[-24J-12p]. (3.4) + +This is Markov applied inside the determinant-weighted integral, not an +unweighted tail probability subsequently divided by a normalizer. + +## 4. Threshold, moving cutoff, and error order + +Take K_0=2 rho^(-12) ell^[-1/(2d)]. It is at least 2. Equations (3.3)–(3.4) +become, for any integers N>=1 and p>=1, + + F(ell,rho) <= C_N rho^(-A_N) ell^(N/2) + + C_p rho^(-24J) ell^[p/(2d)]. (4.1) + +Choose N=2(q+1), p=2d(q+1). Since rho<=1 and A_N>=24J, (0.2) follows. +This explicit loss of half the small-box exponent avoids any need for uniform +Borell constants in this extension. + +For rho=ell^beta, (0.2) is C_q ell^[q+1-beta A_N], at most C_q ell^q when +beta A_N<=1. Since A_N>2, beta<1/2, so ell^(1-2beta)<=1/(64N^2) eventually; +rho<=rho_* also eventually. Thus the domain restriction is satisfied, rather +than silently discarded. More generally rho=c ell^beta with fixed c>0 works, +changing constants and the small cutoff. + +For rho=c[log(e/ell)]^(-a), (0.2) is + + C_q c^(-A_N) ell^(q+1) [log(e/ell)]^(a A_N). + +The elementary bound ell[log(e/ell)]^B=O(1) for each fixed B, and +ell[log(e/ell)]^(2a)->0, prove both the asserted order and the domain condition. +q is chosen before the limit; no uniformity over q is claimed. + +For example d=2,q=1 gives J=6,N=4,A_N=960, and the conservative valid choice +rho=ell^(1/960) yields F=O(ell). This is much farther out than the contact +scale ell^(1/3), and is not a closure of that region. + +For any one fixed moving-cutoff function in (a) or (b), the expected number per +unit volume of bars with 0=t` for t>0. Triangle and convolution inequalities then bound the whole composed product by `C_Q C_R C_Z delta^[-12(s-1)]`. No remaining statement or exponent changed. The live public v1.1 body was compared byte-for-byte with the reviewed object before this disposition. + +## Full analytic reconstruction + +### 1. Quantitative cardinal jets and covariance + +For principal torus coordinate differences, `1-cos(omega h)=2 sin^2(omega h/2)` gives `B_j(x_i)>=8 dist(x_i,x_j)^2/L^2`. Squaring every factor supplies an order-four zero at every other site. The finite frequency support bounds Q_i and its first two derivatives by fixed constants times `delta^[-4(s-1)]`. + +The reciprocal Taylor polynomial through degree two is `1-U_1+U_1^2-U_2`. Its coefficient sum is bounded by a fixed constant times `delta^[-8(s-1)]`, using delta<=1. A uniform nonzero neighborhood is unnecessary: Taylor coefficients are evaluated at Q_i(x_i)=1. The relation `z(x_i+h)=h+O(|h|^3)` preserves every second jet; the alpha! divisor gives unit diagonal as well as mixed Hessian coordinates. The order-four zeros kill all required jets elsewhere. + +The corrected norm bound has exponent 12(s-1), and support lies in the cube |n|_infinity<=2s. Applying weighted Cauchy–Schwarz to each cardinal polynomial yields + +```text +|t_(i,alpha)|^2 <= Var(L_t f) a_*^(-1) C_*^2 delta^[-24(s-1)]. +``` + +Summing sJ coordinates proves the displayed Gram lower bound `a_*/(sJ C_*^2) delta^[24(s-1)]`. The s=1 empty product has exponent zero. Positive Fourier weights on the finite cube give an analytic dual for every separated configuration; sampled nonsingularity is not the premise. + +Every subvector inherits the same lower covariance bound. For a split V,Z, minimizing `Var(z.Z-a.V)` over a bounds the Schur complement below by the same constant times |z|^2. There is no additional inverse-covariance loss here. + +### 2. Full-target density, Gaussian regression and weighted moments + +For two pins, the lower covariance bound is c rho^24 and the upper bound is fixed. Full V_y has dimension 2J, so its Gaussian density prefactor is `rho^(-24J)`. The uniform exponential decay uses the upper covariance bound. On the prescribed target slice, its norm dominates b^2 plus both symmetric Hessian norms. Thus (2.2) has the stated uniform decay and separation power. + +For each standardized real Fourier coefficient xi, covariance Cauchy–Schwarz gives + +```text +|E[xi | V_y=v]| <= sqrt(v^T Sigma_y^(-1) v) <= C rho^(-12)|v|. +``` + +Its conditional centered variance is at most one, possibly zero. The residual coefficients may be correlated; Minkowski does not require their independence. The sum of `sqrt(a_n)(1+|n|)^2` is finite. Finite sums and their tails therefore converge in conditional L^p(C^2), giving (2.3) at every finite target v. This does not assert that the infinite white-noise coefficient sequence itself belongs to l2. Regression is defined at zero pinned gradients, unbounded finite heights, singular Hessian targets and either Hessian signature. + +There is a distinct topological limitation: an arbitrarily specified singular Hessian target can force non-Morse behavior. The all-target statement is a moment statement. The elder argument uses G's almost-sure generic locus under the O_y-conditioned law; further disintegration inherits it for almost every Hessian target, which suffices for the integral. No all-target Morse assertion is needed. + +The exact tower is + +```text +p_O(v_O) E_Q[W K^p] + = integral W(H_0,H_y) p_V(v_O,H_0,H_y) + E[K^p | V_y=(v_O,H_0,H_y)] dH_0 dH_y. +``` + +W is V_y-measurable and bounded by the absolute determinant product, a polynomial of degree 2d. With ell<=1, the remaining target factor is polynomial in b and the Hessians. Gaussian integration over all heights and Hessians, and y-volume<=L^d, gives exactly `M_p<=C_p rho^[-24J-12p]`, including the p=0 case. The determinant/elder-weighted measure is not treated as a Gaussian conditioning law. No inverse Hessian moments, extra determinants or Palm denominator occur. + +### 3. Actual elder geometry, N-site density and tower + +G's living-component and crossing lemmas concern the actual ordinary global elder mark. They force the near-critical volume in each shell on that event; a rejected candidate or merely adjacent saddle would not justify this use. + +Every tuple (0,y,q_1,...,q_N) has separation at least rho/(4N): the first shell is at least 3rho/(8N) from 0, consecutive shells have gap rho/(4N), and y is at least rho/4 from all shells. For s=N+2, QJ and the Schur argument give a conditional Z-density envelope with exponent `12N(N+1)(d+1)`. It is uniform in the conditioning values. The near-critical window's joint volume is `C_N K_0^(dN/2) ell^[N(1+d/2)]`; no product of independent site probabilities is assumed. + +The domain `ell<=rho^2/(64N^2)` and K_0>=2 put the forced balls inside the shells. They are embedded torus balls because rho<=L/4. The pathwise product-volume inequality, followed by Tonelli over measurable shell integrals, avoids a measurable selection of one point on each sphere. W is measurable under V_y, so the uniform Z-envelope may be used inside the weighted tower. Bounding the shell-product volume by L^(dN) and retaining M_0 gives (3.3). + +For the complement, `W e_y 1{K>K_0}<=W K^p K_0^(-p)` gives (3.4) inside the weighted integral. Replacing it with an unweighted tail probability times a mean weight would be unjustified and is not done. + +### 4. Threshold ledger and moving cutoffs + +With `K_0=2 rho^(-12) ell^[-1/(2d)]`, the main term is + +```text +C_N rho^[-24J-12dN-12N(N+1)(d+1)] ell^(N/2), +``` + +and the weighted tail is `C_p rho^(-24J) ell^[p/(2d)]`. Setting N=2(q+1) and p=2d(q+1) proves (0.2). The example d=2,q=1 gives J=6,N=4,A_N=960. + +For rho=ell^beta, beta<=1/A_N gives exponent q+1-beta A_N>=q. Since A_N>2, the geometric domain holds eventually: ell/rho^2=ell^(1-2beta) tends to zero. For the fixed logarithmic cutoff, the extra ell absorbs each fixed logarithmic power; the geometric domain also holds eventually. This is each fixed order separately, not uniformity in q or an all-order statement for one fixed positive beta. + +For one fixed admissible moving cutoff, the imported joint marked measure gives the lifetime-dependent cumulative count per unit spatial volume as `integral_0^t F(ell,rho(ell)) dell`, hence O(t^(q+1)). No cutoff derivative is introduced. This is a different observable from `integral_0^t F(ell,rho(t)) dell`; equality or matching coefficients are not claimed. Whole-torus counts would acquire the factor L^d. + +## Scope and disposition + +The new bridges are the explicit separated-jet lower bound, the separation-tracked weighted moments, and the N-site conditional density envelope. Together with the retained marked elder geometry they justify the stated fixed-model far-region result, including the prescribed logarithmic cutoff. They do not supply contact/intermediate localization, a regional multiple-witness estimate, actual-field confinement, witness uniqueness, rejected-candidate control, a two-sided canonical-witness/persistence correspondence, an occurrence-probability asymptotic, a persistence coefficient or a finite-radius RN certificate. Constants depend on fixed d,L,q; no diagonal growth in them is accepted. + +My review pickup [5963136913](https://github.com/d6g8k5htny-coder/Math-/pull/188#issuecomment-5963136913) is **completed and released by this delivery**. The author/coordinator retains C89 authorship, its R17 claim and immutable custody. This technical verdict does not certify repository application, CI, merge, independent human reading or organizationally independent review. + +## Reviewer-only reproducible controls + +The complete script below is newly executed reviewer code, distinct from the author's executable. Python 3.12.14, standard library only. Both commands exited 0, and their output bytes were identical: + +```sh +python -B c89_reviewer_controls.py --source-dir . +python -B -O c89_reviewer_controls.py --source-dir . +``` + +The source directory contains the exact v1.1 PROOF.md and the pinned source/P.md and source/G.md named above. Save the following code block verbatim with a final newline. Script identity: 12,190 bytes, SHA256 `83982f11df2f145f8dcde55c1900ef8723d46b0820f269049e3c2f4f05da9fab`. Each JSON stdout file is 1,068 bytes, SHA256 `cee69d10a059a1cc62ef89624e85da7b035fa2e309c77bafe0eb87e8d450a074`. + +These finite exact controls corroborate identities and reject listed mutations. They do not prove all-configuration estimates or imported parent hypotheses; the analytic reconstruction above is the basis of the scoped verdict. + +```python +#!/usr/bin/env python3 +"""C89 reviewer-only exact controls; no author executable or third-party package. + +Run: python -B c89_reviewer_controls.py --source-dir PATH +Repeat with -B -O. PATH contains PROOF.md, source/P.md, source/G.md. +Omit --source-dir to run algebra controls without source-custody checks. +The finite controls do not prove uniform analytic bounds or parent hypotheses. +""" +import argparse +import hashlib +import json +from fractions import Fraction as F +from itertools import product +from math import factorial +from pathlib import Path + + +def need(condition, message): + if not condition: + raise RuntimeError(message) + + +ZERO = (F(0), F(0)) +ONE = (F(1), F(0)) + + +def ca(a, b): + return (a[0] + b[0], a[1] + b[1]) + + +def cm(a, b): + return (a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0]) + + +def cs(a, r): + return (a[0] * r, a[1] * r) + + +def conj(a): + return (a[0], -a[1]) + + +def iphase(q): + return (ONE, (F(0), F(1)), (F(-1), F(0)), (F(0), F(-1)))[q % 4] + + +def add(a, b): + out = dict(a) + for k, v in b.items(): + out[k] = ca(out.get(k, ZERO), v) + return {k: v for k, v in out.items() if v != ZERO} + + +def scale(a, r): + return {k: cs(v, r) for k, v in a.items() if cs(v, r) != ZERO} + + +def mul(a, b, truncated=False): + out = {} + for ka, va in a.items(): + for kb, vb in b.items(): + k = tuple(x + y for x, y in zip(ka, kb)) + if truncated and sum(k) > 2: + continue + out[k] = ca(out.get(k, ZERO), cm(va, vb)) + return {k: v for k, v in out.items() if v != ZERO} + + +def power(a, n, d, truncated=False): + out = {(0,) * d: ONE} + for _ in range(n): + out = mul(out, a, truncated) + return out + + +def indices(d): + return [a for a in product(range(3), repeat=d) if sum(a) <= 2] + + +def afact(a): + out = 1 + for v in a: + out *= factorial(v) + return out + + +def unit(d, j, sign=1): + return tuple(sign if k == j else 0 for k in range(d)) + + +def derivative(poly, site, alpha): + out = ZERO + for k, coeff in poly.items(): + factor = 1 + for n, a in zip(k, alpha): + factor *= n ** a + phase = iphase(sum(n * x for n, x in zip(k, site)) + sum(alpha)) + out = ca(out, cs(cm(coeff, phase), F(factor))) + return out + + +def bpoly(site): + d = len(site) + out = {(0,) * d: (F(d), F(0))} + for j, x in enumerate(site): + out = add(out, {unit(d, j): cs(iphase(-x), F(-1, 2)), + unit(d, j, -1): cs(iphase(x), F(-1, 2))}) + return out + + +def zpoly(site, j): + d = len(site) + return {unit(d, j): cm(iphase(-site[j]), (F(0), F(-1, 2))), + unit(d, j, -1): cm(iphase(site[j]), (F(0), F(1, 2)))} + + +def qpoly(sites, i, exponent=2): + d = len(sites[0]) + out = {(0,) * d: ONE} + for j, site in enumerate(sites): + if j == i: + continue + bp = bpoly(site) + denominator = derivative(bp, sites[i], (0,) * d) + need(denominator[1] == 0 and denominator[0] > 0, 'repeated-site denominator') + out = mul(out, power(scale(bp, 1 / denominator[0]), exponent, d)) + return out + + +def reciprocal_jet(q, site): + d = len(site) + jet = {a: cs(derivative(q, site, a), F(1, afact(a))) for a in indices(d)} + need(jet[(0,) * d] == ONE, 'Q_i(x_i) != 1') + u = add(jet, {(0,) * d: (F(-1), F(0))}) + return add(add({(0,) * d: ONE}, scale(u, -1)), mul(u, u, True)) + + +def compose(taylor, zs): + d = len(zs) + out = {} + for alpha, coeff in taylor.items(): + term = {(0,) * d: coeff} + for j, a in enumerate(alpha): + term = mul(term, power(zs[j], a, d)) + out = add(out, term) + return out + + +def cardinals(sites, exponent=2, reciprocal=True, factorials=True): + d = len(sites[0]) + out = {} + for i, site in enumerate(sites): + q = qpoly(sites, i, exponent) + inv = reciprocal_jet(q, site) if reciprocal else {(0,) * d: ONE} + zs = [zpoly(site, j) for j in range(d)] + for alpha in indices(d): + den = afact(alpha) if factorials else 1 + t = mul(inv, {alpha: (F(1, den), F(0))}, True) + out[(i, alpha)] = mul(q, compose(t, zs)) + return out + + +def mismatch_count(sites, **variant): + d = len(sites[0]) + count = 0 + for (i, alpha), poly in cardinals(sites, **variant).items(): + for j, site in enumerate(sites): + for beta in indices(d): + expected = ONE if i == j and alpha == beta else ZERO + count += derivative(poly, site, beta) != expected + return count + + +def positive_definite(matrix): + n = len(matrix) + lower = [[F(0)] * n for _ in range(n)] + pivots = [] + for i in range(n): + lower[i][i] = F(1) + pivot = matrix[i][i] - sum(lower[i][k] ** 2 * pivots[k] for k in range(i)) + if pivot <= 0: + return False + pivots.append(pivot) + for j in range(i + 1, n): + lower[j][i] = (matrix[j][i] - sum(lower[j][k] * lower[i][k] * pivots[k] + for k in range(i))) / pivot + return True + + +def finite_gram(sites, band): + d = len(sites[0]) + coords = [(site, a) for site in sites for a in indices(d)] + out = [[F(0) for _ in coords] for _ in coords] + for mode in product(range(-band, band + 1), repeat=d): + features = [derivative({mode: ONE}, site, a) for site, a in coords] + for i, fi in enumerate(features): + for j, fj in enumerate(features): + value = cm(fi, conj(fj)) + out[i][j] += value[0] + return out + + +def controls(): + sets = [[(0,), (1,), (2,)], + [(0, 0), (1, 0), (0, 1), (2, 2)], + [(0, 0, 0), (1, 0, 1), (0, 1, 2)]] + derivative_checks = frequency_checks = realness_checks = product_checks = 0 + for sites in sets: + d, s = len(sites[0]), len(sites) + need(len(indices(d)) == (d + 1) * (d + 2) // 2, 'jet count') + cq = cr = F(0) + for i, site in enumerate(sites): + qp = qpoly(sites, i) + cq = max(cq, sum(abs(a) + abs(b) for a, b in qp.values())) + inv = reciprocal_jet(qp, site) + for alpha in indices(d): + rp = mul(inv, {alpha: (F(1, afact(alpha)), F(0))}, True) + cr = max(cr, sum(abs(a) + abs(b) for a, b in rp.values())) + for (i, alpha), poly in cardinals(sites).items(): + # omega=1 here, so C_Z=1. This rational coefficient norm + # dominates the complex absolute-value norm and is submultiplicative. + need(sum(abs(a) + abs(b) for a, b in poly.values()) <= cq * cr, + 'successor product bound') + product_checks += 1 + need(all(max(abs(x) for x in k) <= 2 * s for k in poly), 'frequency support') + frequency_checks += 1 + for k, value in poly.items(): + need(poly.get(tuple(-x for x in k), ZERO) == conj(value), 'real polynomial') + realness_checks += 1 + for j, site in enumerate(sites): + for beta in indices(d): + expected = ONE if i == j and alpha == beta else ZERO + need(derivative(poly, site, beta) == expected, 'cardinal jet mismatch') + derivative_checks += 1 + variants = [('order_two_zero_only', {'exponent': 1}), + ('omit_reciprocal', {'reciprocal': False}), + ('omit_alpha_factorial', {'factorials': False})] + rejected = {} + for name, kwargs in variants: + bad = sum(mismatch_count(sites, **kwargs) for sites in sets[:2]) + need(bad > 0, 'mutation survived: ' + name) + rejected[name] = {'mismatches': bad} + try: + qpoly([(0,), (0,)], 0) + except RuntimeError: + rejected['repeated_site_cardinal'] = {'rejected': True} + else: + raise RuntimeError('repeated-site construction survived') + sites = [(0,), (1,)] + polys = cardinals(sites) + cstar = max(sum(abs(v[0]) + abs(v[1]) for v in p.values()) for p in polys.values()) + dimension = len(polys) + lower = F(1, dimension) / cstar ** 2 + gram = finite_gram(sites, 2 * len(sites)) + gram_minus_lower = [[x - (lower if i == j else 0) for j, x in enumerate(row)] + for i, row in enumerate(gram)] + need(positive_definite(gram_minus_lower), 'finite Gram lower bound') + duplicate = finite_gram([(0,), (0,)], 4) + need(duplicate[0][0] + duplicate[3][3] - 2 * duplicate[0][3] == 0, + 'duplicate-site null vector') + rejected['repeated_site_positive_gram'] = {'null_vector_variance': '0'} + covariance_checks = 2 + for rho in (F(1, 2), F(1, 3)): + epsilon = rho ** 12 + sigma = epsilon ** 2 + cross = epsilon + coefficient = cross / sigma + need(coefficient ** 2 == 1 / sigma, 'regression energy equality') + need(coefficient == rho ** -12, 'regression separation exponent') + need(1 - cross ** 2 / sigma == 0, 'singular residual variance') + need(coefficient > 1, 'unamplified regression variant survived') + covariance_checks += 4 + rejected['unamplified_regression'] = {'rejected': True} + sigma = [[F(3), F(1), F(1)], [F(1), F(3), F(1)], [F(1), F(1), F(3)]] + need(positive_definite([[x - int(i == j) for j, x in enumerate(row)] + for i, row in enumerate(sigma)]), 'joint lower bound') + schur = [[sigma[i][j] - sigma[i][0] * sigma[0][j] / sigma[0][0] + for j in (1, 2)] for i in (1, 2)] + need(positive_definite([[x - int(i == j) for j, x in enumerate(row)] + for i, row in enumerate(schur)]), 'Schur lower bound') + covariance_checks += 2 + need(F(1) > F(1) * F(1, 2), 'weighted-tail adverse control') + rejected['unweighted_tail_substitution'] = {'weighted_mass': '1', 'product_of_means': '1/2'} + exponent_checks = 0 + for d in (2, 3, 5): + J = (d + 1) * (d + 2) // 2 + for q in range(1, 7): + N, p = 2 * (q + 1), 2 * d * (q + 1) + B = 12 * N * (N + 1) * (d + 1) + A = 24 * J + 12 * d * N + B + main = N * (1 + F(d, 2)) - F(d * N, 2) - F(d * N, 2 * d) + need(main == F(N, 2) == q + 1, 'main lifetime exponent') + need(F(p, 2 * d) == q + 1, 'tail lifetime exponent') + need(-24 * J - 12 * p + 12 * p == -24 * J, 'tail rho cancellation') + need(F(q + 1) - F(1, A) * A == q, 'power cutoff exponent') + need(F(1, A) < F(1, 2), 'geometric domain') + exponent_checks += 5 + need(24 * 6 + 12 * 2 * 4 + 12 * 4 * 5 * 3 == 960, 'd=2 example') + exponent_checks += 1 + return {'cardinal_derivative_checks': derivative_checks, + 'frequency_support_checks': frequency_checks, + 'real_coefficient_symmetry_checks': realness_checks, + 'constant_product_checks': product_checks, + 'covariance_controls': covariance_checks, + 'exponent_checks': exponent_checks, + 'negative_controls_rejected': rejected, + 'finite_gram_lower_bound': str(lower), + 'scope': 'finite exact controls; uniform proof and imported hypotheses not certified'} + + +def source_checks(directory): + expected = { + 'PROOF.md': (15039, '7d8d3063caa0dfb5edbfe75437d7ccff8ab74697d1dd92c4b47cca5926b02392'), + 'source/P.md': (40261, '9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7'), + 'source/G.md': (29110, '967148439e32e8e5d6c06a12df5cc7c1eb2475fe6828e4aeb3748c48817a4cba')} + out = {} + for name, (size, digest) in expected.items(): + data = (Path(directory) / name).read_bytes() + got = hashlib.sha256(data).hexdigest() + need((len(data), got) == (size, digest), 'source identity: ' + name) + out[name] = {'bytes': len(data), 'sha256': got, 'final_newline': data.endswith(b'\n')} + return out + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--source-dir') + args = parser.parse_args() + result = controls() + result['source_checks'] = source_checks(args.source_dir) if args.source_dir else 'NOT_RUN' + print(json.dumps(result, sort_keys=True, separators=(',', ':'))) + + +if __name__ == '__main__': + main() +``` + +Actual stdout (normal and optimized): + +```json +{"cardinal_derivative_checks":1557,"constant_product_checks":63,"covariance_controls":12,"exponent_checks":91,"finite_gram_lower_bound":"1/384","frequency_support_checks":63,"negative_controls_rejected":{"omit_alpha_factorial":{"mismatches":11},"omit_reciprocal":{"mismatches":43},"order_two_zero_only":{"mismatches":90},"repeated_site_cardinal":{"rejected":true},"repeated_site_positive_gram":{"null_vector_variance":"0"},"unamplified_regression":{"rejected":true},"unweighted_tail_substitution":{"product_of_means":"1/2","weighted_mass":"1"}},"real_coefficient_symmetry_checks":12019,"scope":"finite exact controls; uniform proof and imported hypotheses not certified","source_checks":{"PROOF.md":{"bytes":15039,"final_newline":true,"sha256":"7d8d3063caa0dfb5edbfe75437d7ccff8ab74697d1dd92c4b47cca5926b02392"},"source/G.md":{"bytes":29110,"final_newline":true,"sha256":"967148439e32e8e5d6c06a12df5cc7c1eb2475fe6828e4aeb3748c48817a4cba"},"source/P.md":{"bytes":40261,"final_newline":true,"sha256":"9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7"}}} +``` diff --git a/frontiers/far_elder_flat_ridge_20260930/C89_V1_PROOF.md b/frontiers/far_elder_flat_ridge_20260930/C89_V1_PROOF.md new file mode 100644 index 000000000..15b6861c2 --- /dev/null +++ b/frontiers/far_elder_flat_ridge_20260930/C89_V1_PROOF.md @@ -0,0 +1,303 @@ +# Quantitative separated jets and a shrinking far-elder region + +Object: OA-QSF-20261002-C89-v1. Author: OpenAI / Codex, root01a0bbb5. +Dylan Roy — delegated AI work. Personal reading PENDING; organizational +independence 0; scientific effect NONE. This is an additive analytic candidate, +not a change to a scientific status register. Review disposition belongs in +REVIEW.md, separately from this author statement. + +## 0. Exact interface and result + +Fix d >= 2 and L > 0. Use the centered, variance-one periodized Gaussian field +on X = R^d/(L Z^d) of [P] §1, with Fourier weights + + a_n = exp(-2 pi^2 |n|^2/L^2) / sum_k exp(-2 pi^2 |k|^2/L^2) > 0. + +[P] is `source/P.md`, SHA256 +9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7, +40261 bytes. [G] is `source/G.md`, Math- PR188 head +5e0b31c8304e3a6ef96a5ee28c8faab5f9fdf799, blob +0b089b894960b0ee53fc2885e054d73ab73472bd, SHA256 +967148439e32e8e5d6c06a12df5cc7c1eb2475fe6828e4aeb3748c48817a4cba, +29110 bytes. Its complete source interface is preserved in +`source/G_SOURCES.json`. We consume [P] §§1–2 and [G]'s canonical marked +Kac–Rice definition (0.1), deterministic Lemmas 1–3, and conditional genericity +§2(d). We do not consume Remark 6 or the OA-FD/OA-MT consequences, the SIDE24 +coefficient, a finite-radius RN certificate, or a near-pair asymptotic. +The marked-measure construction retains [G]'s E2 repair and REC interpretation; +this note is not a new proof of those imported interfaces. + +Write O_y=(f(0),grad f(0),f(y),grad f(y)), v=(b,0,b-ell,0), Q for Gaussian +regression on O_y=v, H_0,H_y for the two Hessians, and + + W = |det H_0 det H_y| 1{H_0 negative definite, index H_y=d-1}. + +Let e_y be the ordinary global superlevel H_0 elder mark, not a branch-adjacency +mark. With p_y the density of O_y, define the canonical per-unit-spatial-volume +far-elder lifetime density + + F(ell,rho) = integral_{dist(0,y)>=rho} integral_R + p_y(v) E_Q[W e_y] db dy. (0.1) + +Let J=(d+1)(d+2)/2, the number of independent derivatives of orders 0,1,2 at +one site; a symmetric Hessian has d(d+1)/2 coordinates, not d^2. Put + + rho_* = min(1,L/4), + A_N = 24J + 12dN + 12N(N+1)(d+1). + +**Theorem QSF.** For every integer q>=1 set N=2(q+1). There is a finite constant +C_q=C(d,L,q), independent of ell,rho, such that + + F(ell,rho) <= C_q rho^(-A_N) ell^(q+1), (0.2) + +whenever 00, c>0, rho(ell)=c[log(e/ell)]^(-a), and every fixed +integer q>=1, F(ell,rho(ell))=O(ell^q) as ell decreases to zero. + +These are bounds on an actual elder-marked far population with a specified +moving spatial cutoff. They are not uniform in arbitrary shrinking cutoffs, +in L, d or q. They do not establish the contact-scale region, witness uniqueness, +the intermediate region inside rho(ell), or either direction of the full +canonical-witness/persistence correspondence. There is no weighted-Palm +normalizer Z_r in (0.1); dividing by one would change the statement. + +## 1. Constructive quantitative finite-jet rank + +**Lemma QJ.** Fix s>=1 distinct sites x_1,...,x_s with pairwise torus distance +at least delta, where 0= c(d,L,s) delta^[24(s-1)]. (1.1) + +The constant is strictly positive and finite. It can be constructed from +finitely many positive Fourier weights; no sampled-covariance inference occurs. + +Proof. Put omega=2pi/L and + + B_j(x)=sum_{k=1}^d [1-cos(omega(x_k-x_{j,k}))]. + +Choose coordinate differences in [-L/2,L/2]. The elementary inequality +sin t >= 2t/pi for 0<=t<=pi/2 gives + + B_j(x_i) >= 8 dist(x_i,x_j)^2/L^2 >= 8delta^2/L^2. + +The sum of absolute Fourier coefficients of B_j is at most 2d. For each i set + + Q_i(x)=product_{j!=i} [B_j(x)/B_j(x_i)]^2. + +It has value 1 at x_i, vanishes to order at least four at every other site, +has Fourier support |n|_infinity<=2(s-1), and has Fourier coefficient l1 norm +at most C delta^[-4(s-1)]. All its derivatives through order two at x_i have +the same bound, with a different C depending only on d,L,s. Here and below +C denotes a defined finite bound from the finite coefficient sum and its +frequency multipliers, never a constant allowed to depend on delta or the sites. + +For a multiindex alpha with |alpha|<=2 let R_{i,alpha}(h) be the Taylor polynomial +through total degree two of + + h^alpha / (alpha! Q_i(x_i+h)). + +The reciprocal is legitimate since Q_i(x_i)=1. If Q_i(x_i+h)=1+U_1(h)+U_2(h) ++O(|h|^3), its reciprocal through degree two is 1-U_1+U_1^2-U_2. Thus every +coefficient of R_{i,alpha} is bounded by C delta^[-8(s-1)]. Define the periodic +local coordinates z_k(x)=sin(omega(x_k-x_{i,k}))/omega and the trigonometric +polynomial + + P_{i,alpha}(x)=Q_i(x) R_{i,alpha}(z(x)). + +Since z(x_i+h)=h+O(|h|^3), its jets satisfy + + partial^gamma P_{i,alpha}(x_j) = 1{i=j,alpha=gamma}, |gamma|<=2. (1.2) + +At other sites the fourth-order zero of Q_i kills every derivative in question. +The Fourier support is |n|_infinity<=2s, and its coefficient l1 norm is bounded +by C_* delta^[-12(s-1)], uniformly over i,alpha and all separated configurations. +One may choose C_* as the maximum of the above finite-sum bounds for Q_i, +its first two derivatives, the displayed reciprocal polynomial, and the finitely +many monomials in sin/omega. This supplies an explicit finite construction of C_*. + +Let a_* = min_{|n|_infinity<=2s} a_n >0. For real coefficients t_{i,alpha} set +L_t=sum t_{i,alpha} partial^alpha|_{x_i}. Fourier expansion gives + + V_t=Var(L_t f)=sum_n a_n |L_t exp(i omega n.x)|^2. + +Writing P_{i,alpha}=sum p_n exp(i omega n.x), weighted Cauchy–Schwarz and (1.2) +give + + |t_{i,alpha}|^2 <= V_t sum |p_n|^2/a_n + <= V_t a_*^(-1) C_*^2 delta^[-24(s-1)]. + +Summing over sJ coordinates proves (1.1), with c=a_*/(sJ C_*^2). For s=1 +the empty product Q_i=1 supplies the same argument with exponent zero. +Every subvector has at least this covariance lower bound. If a subvector is +split into V,Z, its conditional covariance also has this lower bound: for z, +the Schur-complement variational formula minimizes Var(z.Z-a.V) over a, and +(1.1) bounds every such variance below by c delta^[24(s-1)] |z|^2. QED. + +This is deliberately conservative; it is a usable uniform power, not a sharp +collision exponent. The positivity of only the indicated finite cube suffices +for this rank estimate. The smooth field and moment arguments below additionally +use the summability of all Fourier modes of the stated Gaussian covariance. + +## 2. Two-pin weighted moments, with the separation tracked + +Let V_y=(O_y,H_0,H_y), with distinct symmetric Hessian coordinates. Its dimension +is 2J. Uniformly for dist(0,y)>=rho and 0= c rho^24, + lambda_max Sigma_y <= C. (2.1) + +The upper bound follows from the fixed finite derivative variances. Thus at +the slice v=(b,0,b-ell,0,H_0,H_y), 0=1, Gaussian regression gives + + E[K^p | V_y=v] <= C_p rho^(-12p) (1+|v|)^p. (2.3) + +Here is a direct uniform justification. Expand the real field into independent +standard-normal sine/cosine coefficients, with summable square-root spectral +amplitudes times (1+|n|)^2. For each standardized coefficient xi, its conditional +mean has absolute value at most sqrt(v^T Sigma_y^(-1)v), by covariance +Cauchy–Schwarz; its conditional centered variance is at most 1. Minkowski's +inequality, the spectral sum, and (2.1) bound the conditional L^p norm of K by +C_p(1+rho^(-12)|v|). The residual coefficients need not be independent of one +another. Infinite sums converge in conditional L^p(C^2) by the same summable +majorant. Gaussian regression, not conditioning on a positive-probability pin +event, defines these laws at every target v. + +Consequently, for p>=1 (and with the evident p=0 version), + + M_p(ell,rho) := integral_{dist(0,y)>=rho} integral_R + p_y(v) E_Q[W K^p] db dy + <= C_p rho^[-(24J+12p)]. (2.4) + +Indeed, disintegrate further onto the Hessians: p_y(v) times the conditional +Hessian density is exactly p_{V_y}(v,H_0,H_y). W is V_y-measurable and at most +|det H_0 det H_y|, a polynomially bounded function of degree 2d. Apply (2.2) +and (2.3), integrate the polynomial times the Gaussian in b,H_0,H_y, and bound +the y volume by L^d. This preserves the full determinant weight and integrates +over all birth heights. No unweighted-to-weighted probability substitution or +inverse random Hessian moment is used. + +## 3. N-site bound, retaining the weighted event + +Use exactly [G] §3's shells + + S_j={x: |dist(0,x)-j rho/(2N)|=rho, is separated by at +least delta=rho/(4N). Apply Lemma QJ with s=N+2 to the full two-jets, then take +the subvector (V_y,Z), where Z=(f(q_j),grad f(q_j))_{j=1}^N has m=N(d+1) +coordinates. Its conditional density given V_y, uniformly over all values, is +bounded by + + C_N rho^[-12N(N+1)(d+1)]. (3.1) + +Therefore the conditional probability of |f(q_j)-b|<=3ell and +|grad f(q_j)|<=3sqrt(K_0 ell) at all N sites is at most + + C_N rho^[-12N(N+1)(d+1)] K_0^(dN/2) ell^[N(1+d/2)]. (3.2) + +For 0=2, [G] Lemmas 1–3 force on the elder event +with K<=K_0 a near-critical ball of volume omega_d(ell/K_0)^(d/2) in every +shell. The pathwise product-volume bound [G](3.1), Tonelli, and (3.2) yield + + integral integral p_y E_Q[W e_y 1{K<=K_0}] + <= C_N rho^[-12N(N+1)(d+1)] K_0^(dN) ell^N M_0 + <= C_N rho^[-24J-12N(N+1)(d+1)] K_0^(dN) ell^N. (3.3) + +The shell product volume is at most L^(dN); this bound is independent of rho. +The tower step is valid because W is V_y-measurable, while (3.2) is uniform +in the conditioning values. No measurable choice of a point on each sphere +is needed: the forced lower volume is pathwise, and only measurable shell +integrals enter Tonelli. The conditional generic locus and the actual elder +topology are those explicitly imported from [G]; no claim that a local saddle +must be the elder saddle is introduced. + +For the complement, Markov's inequality and (2.4) give + + integral integral p_y E_Q[W e_y 1{K>K_0}] + <= K_0^(-p) M_p + <= C_p K_0^(-p) rho^[-24J-12p]. (3.4) + +This is Markov applied inside the determinant-weighted integral, not an +unweighted tail probability subsequently divided by a normalizer. + +## 4. Threshold, moving cutoff, and error order + +Take K_0=2 rho^(-12) ell^[-1/(2d)]. It is at least 2. Equations (3.3)–(3.4) +become, for any integers N>=1 and p>=1, + + F(ell,rho) <= C_N rho^(-A_N) ell^(N/2) + + C_p rho^(-24J) ell^[p/(2d)]. (4.1) + +Choose N=2(q+1), p=2d(q+1). Since rho<=1 and A_N>=24J, (0.2) follows. +This explicit loss of half the small-box exponent avoids any need for uniform +Borell constants in this extension. + +For rho=ell^beta, (0.2) is C_q ell^[q+1-beta A_N], at most C_q ell^q when +beta A_N<=1. Since A_N>2, beta<1/2, so ell^(1-2beta)<=1/(64N^2) eventually; +rho<=rho_* also eventually. Thus the domain restriction is satisfied, rather +than silently discarded. More generally rho=c ell^beta with fixed c>0 works, +changing constants and the small cutoff. + +For rho=c[log(e/ell)]^(-a), (0.2) is + + C_q c^(-A_N) ell^(q+1) [log(e/ell)]^(a A_N). + +The elementary bound ell[log(e/ell)]^B=O(1) for each fixed B, and +ell[log(e/ell)]^(2a)->0, prove both the asserted order and the domain condition. +q is chosen before the limit; no uniformity over q is claimed. + +For example d=2,q=1 gives J=6,N=4,A_N=960, and the conservative valid choice +rho=ell^(1/960) yields F=O(ell). This is much farther out than the contact +scale ell^(1/3), and is not a closure of that region. + +For any one fixed moving-cutoff function in (a) or (b), the expected number per +unit volume of bars with 0 t}` every point satisfies `|∇f|² ≤ 2K(b − f) ≤ 2K(b − t)`, `K ≥ sup‖D²f‖` — walk uphill from any point for a distance `|∇f|/K`; the walk diff --git a/frontiers/far_elder_flat_ridge_20260930/SOURCES.json b/frontiers/far_elder_flat_ridge_20260930/SOURCES.json index 993f5cb48..2b2cdedaf 100644 --- a/frontiers/far_elder_flat_ridge_20260930/SOURCES.json +++ b/frontiers/far_elder_flat_ridge_20260930/SOURCES.json @@ -1,7 +1,7 @@ { "schema": 1, "scientific_effect": "NONE", - "object": "CL-FAR-ELDER-FLAT-RIDGE-20260930-v1.1", + "object": "CL-FAR-ELDER-FLAT-RIDGE-20260930-v1.2", "kind": "author-side proof candidate (Lemmas 1-3 deterministic; Theorem G conditional on the reconciled [P] interfaces and the standard Borell-TIS inequality; v1.1: Remark 5 rewritten for the merged expansions #191/#198/#220/#229, Remark 6 records the posted Codex consequences and proves C(rho, N) >= c_N rho^(1-4N) conditionally on their (2.4); Theorem G and its proof unchanged); nonauthor analytic review required", "author": "Anthropic Claude", "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", @@ -16,7 +16,7 @@ "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", "tag": "P", - "use": "\u00a71 field; \u00a72 distinct-site rank (N + 2 sites); \u00a74 regression / independent residual at fixed sites; \u00a78 maximin d_f and the Borel elder mark; \u00a79 as [E2]; \u00a714 far pairs and (14.1)" + "use": "§1 field; §2 distinct-site rank (N + 2 sites); §4 regression / independent residual at fixed sites; §8 maximin d_f and the Borel elder mark; §9 as [E2]; §14 far pairs and (14.1)" }, { "path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", @@ -24,7 +24,7 @@ "sha256": "845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f", "git_blob": "fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a", "tag": "E2", - "use": "\u00a79.1-9.4: the marked Kac-Rice version (0.1) and measurability of e_y" + "use": "§9.1-9.4: the marked Kac-Rice version (0.1) and measurability of e_y" }, { "path": "reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md", @@ -32,7 +32,7 @@ "sha256": "451b9d7ffee072a73fc904cab891b6693e3f233808b89df10cce1b57036b65da", "git_blob": "75da2597971510f843f8d90c743950cb8c177342", "tag": "REC", - "use": "\u00a71 reading rule, \u00a75 embedding radius, \u00a77 consumption contract" + "use": "§1 reading rule, §5 embedding radius, §7 consumption contract" }, { "path": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", @@ -50,7 +50,7 @@ "sha256": "380b7d0abdb0fe2de5a6564565af9560d3f1b1ce22fd5538927db0c52f4f3a4a", "git_blob": "247b3ecf80bfbe896948d5d489b2d5842a81c481", "tag": "R", - "use": "\u00a77 near/far decomposition, \u00a78 moments (Remark 5)" + "use": "§7 near/far decomposition, §8 moments (Remark 5)" }, { "path": "frontiers/c7_zero_gap_limit_20260929/PROOF.md", @@ -149,8 +149,38 @@ }, { "path": "README.md", - "bytes": 3999, - "sha256": "4404bb60cfbe10d0ae677f8136330629797b97d374508efea02a4b6cb7a8c11b" + "bytes": 6435, + "sha256": "247ba531f8c51e41d1ca5e54c0567d847775d0f175716522e64a87c92cff1cc5" + }, + { + "path": "C89_V1_1_PROOF.md", + "bytes": 15039, + "sha256": "7d8d3063caa0dfb5edbfe75437d7ccff8ab74697d1dd92c4b47cca5926b02392" + }, + { + "path": "C89_V1_PROOF.md", + "bytes": 14742, + "sha256": "74af6322bdcccec0b718b6abcbfb36b139c40d07398849af9a35ad2000bc31f1" + }, + { + "path": "C89_V1_1_REVIEW.md", + "bytes": 26692, + "sha256": "d31e1aaf72986117c1fcae69062e5235660b8c06ab55865cbca850e2f2ff8bcd" + }, + { + "path": "c89_reviewer_controls.py", + "bytes": 12190, + "sha256": "83982f11df2f145f8dcde55c1900ef8723d46b0820f269049e3c2f4f05da9fab" + }, + { + "path": "c89_reviewer_stdout.json", + "bytes": 1068, + "sha256": "cee69d10a059a1cc62ef89624e85da7b035fa2e309c77bafe0eb87e8d450a074" + }, + { + "path": "c89_replay.py", + "bytes": 4448, + "sha256": "e942e03e04a8d64fd98e4eeb567b42112a86a6f35272aa68dffabbe8893b505f" } ], "supersedes": { @@ -216,6 +246,98 @@ "section 6" ], "reason": "status of #187 (merged); Remark 5 for the merged #191/#198/#220/#229; Remark 6 records OA-FD and OA-MT and derives (R6.1); requested context: xAI 5379778152 and the scoped check 5932225117 note that #191 and #198 have merged" + }, + { + "label": "v1.2 (packet)", + "files_added": [ + "C89_V1_1_PROOF.md", + "C89_V1_PROOF.md", + "C89_V1_1_REVIEW.md", + "c89_reviewer_controls.py", + "c89_reviewer_stdout.json", + "c89_replay.py" + ], + "files_changed": [ + "README.md", + "SOURCES.json", + ".github/workflows/far-elder-flat-ridge.yml" + ], + "unchanged": [ + "PROOF.md", + "flat_ridge_check.py", + "RESULTS.json" + ], + "reason": "incorporate the reviewed C89 v1.1 extension additively, as requested in Math- #188 comment 5963266074" + } + ], + "extensions": [ + { + "tag": "C89", + "object": "OA-QSF-20261002-C89-v1.1", + "title": "Quantitative separated jets and a shrinking far-elder region (Theorem QSF)", + "author": "OpenAI / Codex root01a0bbb5, under Dylan Roy's delegation (same GitHub account; organizational independence 0)", + "proof": { + "comment": "Math- #188 comment 5963100306", + "url": "https://github.com/d6g8k5htny-coder/Math-/pull/188#issuecomment-5963100306", + "copy": "C89_V1_1_PROOF.md", + "bytes": 15039, + "sha256": "7d8d3063caa0dfb5edbfe75437d7ccff8ab74697d1dd92c4b47cca5926b02392" + }, + "historical": { + "comment": "Math- #188 comment 5963042579 (v1; AMEND retained: explicit constant was a maximum of bounds, product C_* = C_Q C_R C_Z required)", + "copy": "C89_V1_PROOF.md", + "bytes": 14742, + "sha256": "74af6322bdcccec0b718b6abcbfb36b139c40d07398849af9a35ad2000bc31f1" + }, + "review": { + "comment": "Math- #188 comment 5963217842", + "url": "https://github.com/d6g8k5htny-coder/Math-/pull/188#issuecomment-5963217842", + "copy": "C89_V1_1_REVIEW.md", + "bytes": 26692, + "sha256": "d31e1aaf72986117c1fcae69062e5235660b8c06ab55865cbca850e2f2ff8bcd", + "reviewer": "OpenAI / Codex /root (coordinating session), distinct from the author root; prior feasibility exposure disclosed; helper /root/c86_fresh_review supporting only", + "verdict": "ACCEPT / PASS_TECHNICAL_SCOPED for the exact v1.1 object with the imported [P]/[G]/E2/REC hypotheses retained; v1 remains AMEND", + "organizational_independence": 0 + }, + "reviewer_controls": { + "script": "c89_reviewer_controls.py", + "script_bytes": 12190, + "script_sha256": "83982f11df2f145f8dcde55c1900ef8723d46b0820f269049e3c2f4f05da9fab", + "stdout": "c89_reviewer_stdout.json", + "stdout_bytes": 1068, + "stdout_sha256": "cee69d10a059a1cc62ef89624e85da7b035fa2e309c77bafe0eb87e8d450a074", + "source": "extracted verbatim from the review comment 5963217842 (code block saved with a final newline, as the review instructs)", + "replay": "c89_replay.py: [P] + this PROOF.md as [G] + C89_V1_1_PROOF.md; stdout byte-identical under -B -S and -B -O -S (Python 3.11.15 locally; 3.12.14 in the review)" + }, + "records": [ + { + "what": "author pickup", + "comment": "5962988822", + "bytes": 946, + "sha256": "a4b1f2cbc786803f1f3e5b11fde8bc4576d3563897a7753850996feb0cf506d8" + }, + { + "what": "review pickup", + "comment": "5963136913", + "bytes": 1724, + "sha256": "842de348c1b3b128554f133df50f858593fc81e0329a270107443ec200152b01" + }, + { + "what": "delivery and incorporation request", + "comment": "5963266074", + "bytes": 2873, + "sha256": "bbc60807a9be78558ead57c54b2940216f05d9230a255c4425314a331e9470ef", + "drive_delivery": "C89-QUANTITATIVE-SHRINKING-FAR-ELDER-20261002.zip, 395810 bytes, SHA256 888f32cfa5e0781cc929f972ea371efc008a9bf99572965795c1f584d4bad6b3 as published; size read back from Drive metadata, contents not downloaded or relied on" + }, + { + "what": "incorporation pickup", + "comment": "5969476982" + } + ], + "consumes_from_G": "(0.1), Lemmas 1-3, section 2(d), section 3 shells and the volume bound (3.1); not Remark 6", + "G_pin": "PROOF.md blob 0b089b894960b0ee53fc2885e054d73ab73472bd, unchanged in v1.2", + "incorporated_by": "Anthropic Claude (author of [G]), session https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU; author-side interface check of the [G] uses, not a review of C89", + "not_established": "contact/intermediate localization; regional multiple-witness collision; actual-field confinement; witness uniqueness; rejected-candidate control; two-sided canonical-witness/persistence correspondence; uniformity in d, L or q" } ] } diff --git a/frontiers/far_elder_flat_ridge_20260930/c89_replay.py b/frontiers/far_elder_flat_ridge_20260930/c89_replay.py new file mode 100644 index 000000000..57a882e71 --- /dev/null +++ b/frontiers/far_elder_flat_ridge_20260930/c89_replay.py @@ -0,0 +1,96 @@ +#!/usr/bin/env python3 +"""Replay the published C89 v1.1 reviewer controls against the exact sources (standard library only). + +C89 v1.1, "Quantitative separated jets and a shrinking far-elder region" (Math- #188 comment 5963100306, +OpenAI / Codex), is kept in this packet as C89_V1_1_PROOF.md. Its full review (comment 5963217842) published +the script c89_reviewer_controls.py and that script's stdout; both are kept here byte for byte. The review ran +the script with --source-dir holding PROOF.md (the C89 proof), source/P.md ([P]) and source/G.md ([G], this +packet's PROOF.md). This wrapper assembles that layout from repository files in a temporary directory, runs the +script under the current interpreter's -O/-S flags, and requires its stdout to equal the published bytes. A +one-byte change to the C89 copy must change the replay (negative control). + +Reproducibility only: the analytic proof and its review carry the mathematics, not this replay. + +Usage: python3 -B -S frontiers/far_elder_flat_ridge_20260930/c89_replay.py (exit 0 iff every check passes) +""" +import hashlib +import json +import pathlib +import shutil +import subprocess +import sys +import tempfile + +HERE = pathlib.Path(__file__).resolve().parent +ROOT = HERE.parents[1] +P_SOURCE = ROOT / 'imports' / 'lifetime_parent_20260925' / 'UNIFORM_MATRIX_CAP_AND_LIFETIME.md' + +# (bytes, SHA256) as published in the review 5963217842 and the delivery note 5963266074. +IDENTITIES = { + 'C89_V1_1_PROOF.md': (15039, '7d8d3063caa0dfb5edbfe75437d7ccff8ab74697d1dd92c4b47cca5926b02392'), + 'C89_V1_PROOF.md': (14742, '74af6322bdcccec0b718b6abcbfb36b139c40d07398849af9a35ad2000bc31f1'), + 'c89_reviewer_controls.py': (12190, '83982f11df2f145f8dcde55c1900ef8723d46b0820f269049e3c2f4f05da9fab'), + 'c89_reviewer_stdout.json': (1068, 'cee69d10a059a1cc62ef89624e85da7b035fa2e309c77bafe0eb87e8d450a074'), + 'PROOF.md': (29110, '967148439e32e8e5d6c06a12df5cc7c1eb2475fe6828e4aeb3748c48817a4cba'), +} +P_IDENTITY = (40261, '9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7') + + +def identity(data): + return len(data), hashlib.sha256(data).hexdigest() + + +def interpreter_flags(): + flags = ['-B'] + if sys.flags.optimize: + flags.append('-O') + if sys.flags.no_site: + flags.append('-S') + return flags + + +def replay(proof_bytes): + """Run the reviewer script on PROOF.md = proof_bytes, source/P.md = [P], source/G.md = [G].""" + with tempfile.TemporaryDirectory() as tmp: + src = pathlib.Path(tmp) + (src / 'source').mkdir() + (src / 'PROOF.md').write_bytes(proof_bytes) + shutil.copyfile(P_SOURCE, src / 'source' / 'P.md') + shutil.copyfile(HERE / 'PROOF.md', src / 'source' / 'G.md') + run = subprocess.run([sys.executable, *interpreter_flags(), str(HERE / 'c89_reviewer_controls.py'), + '--source-dir', str(src)], capture_output=True, timeout=600) + return run.returncode, run.stdout + + +def main(): + failures = [] + for name, expected in IDENTITIES.items(): + if identity((HERE / name).read_bytes()) != expected: + failures.append('identity mismatch: ' + name) + if identity(P_SOURCE.read_bytes()) != P_IDENTITY: + failures.append('identity mismatch: [P] ' + str(P_SOURCE.relative_to(ROOT))) + published = (HERE / 'c89_reviewer_stdout.json').read_bytes() + proof = (HERE / 'C89_V1_1_PROOF.md').read_bytes() + code, out = replay(proof) + if code != 0: + failures.append('reviewer script exit code %d' % code) + if out != published: + failures.append('reviewer stdout differs from the published bytes') + altered = proof.replace(b'A_N = 24J + 12dN', b'A_N = 24J + 13dN', 1) + if altered == proof: + failures.append('negative control could not alter the C89 copy') + else: + code2, out2 = replay(altered) + if code2 == 0 and out2 == published: + failures.append('negative control: an altered C89 copy reproduced the published stdout') + print(json.dumps({'object': 'C89 v1.1 reviewer-controls replay', + 'interpreter_flags': interpreter_flags(), + 'published_stdout_sha256': identity(published)[1], + 'replay_stdout_sha256': identity(out)[1], + 'failures': failures, + 'scientific_effect': 'NONE'}, sort_keys=True)) + return 0 if not failures else 1 + + +if __name__ == '__main__': + sys.exit(main()) diff --git a/frontiers/far_elder_flat_ridge_20260930/c89_reviewer_controls.py b/frontiers/far_elder_flat_ridge_20260930/c89_reviewer_controls.py new file mode 100644 index 000000000..10976e5dc --- /dev/null +++ b/frontiers/far_elder_flat_ridge_20260930/c89_reviewer_controls.py @@ -0,0 +1,335 @@ +#!/usr/bin/env python3 +"""C89 reviewer-only exact controls; no author executable or third-party package. + +Run: python -B c89_reviewer_controls.py --source-dir PATH +Repeat with -B -O. PATH contains PROOF.md, source/P.md, source/G.md. +Omit --source-dir to run algebra controls without source-custody checks. +The finite controls do not prove uniform analytic bounds or parent hypotheses. +""" +import argparse +import hashlib +import json +from fractions import Fraction as F +from itertools import product +from math import factorial +from pathlib import Path + + +def need(condition, message): + if not condition: + raise RuntimeError(message) + + +ZERO = (F(0), F(0)) +ONE = (F(1), F(0)) + + +def ca(a, b): + return (a[0] + b[0], a[1] + b[1]) + + +def cm(a, b): + return (a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0]) + + +def cs(a, r): + return (a[0] * r, a[1] * r) + + +def conj(a): + return (a[0], -a[1]) + + +def iphase(q): + return (ONE, (F(0), F(1)), (F(-1), F(0)), (F(0), F(-1)))[q % 4] + + +def add(a, b): + out = dict(a) + for k, v in b.items(): + out[k] = ca(out.get(k, ZERO), v) + return {k: v for k, v in out.items() if v != ZERO} + + +def scale(a, r): + return {k: cs(v, r) for k, v in a.items() if cs(v, r) != ZERO} + + +def mul(a, b, truncated=False): + out = {} + for ka, va in a.items(): + for kb, vb in b.items(): + k = tuple(x + y for x, y in zip(ka, kb)) + if truncated and sum(k) > 2: + continue + out[k] = ca(out.get(k, ZERO), cm(va, vb)) + return {k: v for k, v in out.items() if v != ZERO} + + +def power(a, n, d, truncated=False): + out = {(0,) * d: ONE} + for _ in range(n): + out = mul(out, a, truncated) + return out + + +def indices(d): + return [a for a in product(range(3), repeat=d) if sum(a) <= 2] + + +def afact(a): + out = 1 + for v in a: + out *= factorial(v) + return out + + +def unit(d, j, sign=1): + return tuple(sign if k == j else 0 for k in range(d)) + + +def derivative(poly, site, alpha): + out = ZERO + for k, coeff in poly.items(): + factor = 1 + for n, a in zip(k, alpha): + factor *= n ** a + phase = iphase(sum(n * x for n, x in zip(k, site)) + sum(alpha)) + out = ca(out, cs(cm(coeff, phase), F(factor))) + return out + + +def bpoly(site): + d = len(site) + out = {(0,) * d: (F(d), F(0))} + for j, x in enumerate(site): + out = add(out, {unit(d, j): cs(iphase(-x), F(-1, 2)), + unit(d, j, -1): cs(iphase(x), F(-1, 2))}) + return out + + +def zpoly(site, j): + d = len(site) + return {unit(d, j): cm(iphase(-site[j]), (F(0), F(-1, 2))), + unit(d, j, -1): cm(iphase(site[j]), (F(0), F(1, 2)))} + + +def qpoly(sites, i, exponent=2): + d = len(sites[0]) + out = {(0,) * d: ONE} + for j, site in enumerate(sites): + if j == i: + continue + bp = bpoly(site) + denominator = derivative(bp, sites[i], (0,) * d) + need(denominator[1] == 0 and denominator[0] > 0, 'repeated-site denominator') + out = mul(out, power(scale(bp, 1 / denominator[0]), exponent, d)) + return out + + +def reciprocal_jet(q, site): + d = len(site) + jet = {a: cs(derivative(q, site, a), F(1, afact(a))) for a in indices(d)} + need(jet[(0,) * d] == ONE, 'Q_i(x_i) != 1') + u = add(jet, {(0,) * d: (F(-1), F(0))}) + return add(add({(0,) * d: ONE}, scale(u, -1)), mul(u, u, True)) + + +def compose(taylor, zs): + d = len(zs) + out = {} + for alpha, coeff in taylor.items(): + term = {(0,) * d: coeff} + for j, a in enumerate(alpha): + term = mul(term, power(zs[j], a, d)) + out = add(out, term) + return out + + +def cardinals(sites, exponent=2, reciprocal=True, factorials=True): + d = len(sites[0]) + out = {} + for i, site in enumerate(sites): + q = qpoly(sites, i, exponent) + inv = reciprocal_jet(q, site) if reciprocal else {(0,) * d: ONE} + zs = [zpoly(site, j) for j in range(d)] + for alpha in indices(d): + den = afact(alpha) if factorials else 1 + t = mul(inv, {alpha: (F(1, den), F(0))}, True) + out[(i, alpha)] = mul(q, compose(t, zs)) + return out + + +def mismatch_count(sites, **variant): + d = len(sites[0]) + count = 0 + for (i, alpha), poly in cardinals(sites, **variant).items(): + for j, site in enumerate(sites): + for beta in indices(d): + expected = ONE if i == j and alpha == beta else ZERO + count += derivative(poly, site, beta) != expected + return count + + +def positive_definite(matrix): + n = len(matrix) + lower = [[F(0)] * n for _ in range(n)] + pivots = [] + for i in range(n): + lower[i][i] = F(1) + pivot = matrix[i][i] - sum(lower[i][k] ** 2 * pivots[k] for k in range(i)) + if pivot <= 0: + return False + pivots.append(pivot) + for j in range(i + 1, n): + lower[j][i] = (matrix[j][i] - sum(lower[j][k] * lower[i][k] * pivots[k] + for k in range(i))) / pivot + return True + + +def finite_gram(sites, band): + d = len(sites[0]) + coords = [(site, a) for site in sites for a in indices(d)] + out = [[F(0) for _ in coords] for _ in coords] + for mode in product(range(-band, band + 1), repeat=d): + features = [derivative({mode: ONE}, site, a) for site, a in coords] + for i, fi in enumerate(features): + for j, fj in enumerate(features): + value = cm(fi, conj(fj)) + out[i][j] += value[0] + return out + + +def controls(): + sets = [[(0,), (1,), (2,)], + [(0, 0), (1, 0), (0, 1), (2, 2)], + [(0, 0, 0), (1, 0, 1), (0, 1, 2)]] + derivative_checks = frequency_checks = realness_checks = product_checks = 0 + for sites in sets: + d, s = len(sites[0]), len(sites) + need(len(indices(d)) == (d + 1) * (d + 2) // 2, 'jet count') + cq = cr = F(0) + for i, site in enumerate(sites): + qp = qpoly(sites, i) + cq = max(cq, sum(abs(a) + abs(b) for a, b in qp.values())) + inv = reciprocal_jet(qp, site) + for alpha in indices(d): + rp = mul(inv, {alpha: (F(1, afact(alpha)), F(0))}, True) + cr = max(cr, sum(abs(a) + abs(b) for a, b in rp.values())) + for (i, alpha), poly in cardinals(sites).items(): + # omega=1 here, so C_Z=1. This rational coefficient norm + # dominates the complex absolute-value norm and is submultiplicative. + need(sum(abs(a) + abs(b) for a, b in poly.values()) <= cq * cr, + 'successor product bound') + product_checks += 1 + need(all(max(abs(x) for x in k) <= 2 * s for k in poly), 'frequency support') + frequency_checks += 1 + for k, value in poly.items(): + need(poly.get(tuple(-x for x in k), ZERO) == conj(value), 'real polynomial') + realness_checks += 1 + for j, site in enumerate(sites): + for beta in indices(d): + expected = ONE if i == j and alpha == beta else ZERO + need(derivative(poly, site, beta) == expected, 'cardinal jet mismatch') + derivative_checks += 1 + variants = [('order_two_zero_only', {'exponent': 1}), + ('omit_reciprocal', {'reciprocal': False}), + ('omit_alpha_factorial', {'factorials': False})] + rejected = {} + for name, kwargs in variants: + bad = sum(mismatch_count(sites, **kwargs) for sites in sets[:2]) + need(bad > 0, 'mutation survived: ' + name) + rejected[name] = {'mismatches': bad} + try: + qpoly([(0,), (0,)], 0) + except RuntimeError: + rejected['repeated_site_cardinal'] = {'rejected': True} + else: + raise RuntimeError('repeated-site construction survived') + sites = [(0,), (1,)] + polys = cardinals(sites) + cstar = max(sum(abs(v[0]) + abs(v[1]) for v in p.values()) for p in polys.values()) + dimension = len(polys) + lower = F(1, dimension) / cstar ** 2 + gram = finite_gram(sites, 2 * len(sites)) + gram_minus_lower = [[x - (lower if i == j else 0) for j, x in enumerate(row)] + for i, row in enumerate(gram)] + need(positive_definite(gram_minus_lower), 'finite Gram lower bound') + duplicate = finite_gram([(0,), (0,)], 4) + need(duplicate[0][0] + duplicate[3][3] - 2 * duplicate[0][3] == 0, + 'duplicate-site null vector') + rejected['repeated_site_positive_gram'] = {'null_vector_variance': '0'} + covariance_checks = 2 + for rho in (F(1, 2), F(1, 3)): + epsilon = rho ** 12 + sigma = epsilon ** 2 + cross = epsilon + coefficient = cross / sigma + need(coefficient ** 2 == 1 / sigma, 'regression energy equality') + need(coefficient == rho ** -12, 'regression separation exponent') + need(1 - cross ** 2 / sigma == 0, 'singular residual variance') + need(coefficient > 1, 'unamplified regression variant survived') + covariance_checks += 4 + rejected['unamplified_regression'] = {'rejected': True} + sigma = [[F(3), F(1), F(1)], [F(1), F(3), F(1)], [F(1), F(1), F(3)]] + need(positive_definite([[x - int(i == j) for j, x in enumerate(row)] + for i, row in enumerate(sigma)]), 'joint lower bound') + schur = [[sigma[i][j] - sigma[i][0] * sigma[0][j] / sigma[0][0] + for j in (1, 2)] for i in (1, 2)] + need(positive_definite([[x - int(i == j) for j, x in enumerate(row)] + for i, row in enumerate(schur)]), 'Schur lower bound') + covariance_checks += 2 + need(F(1) > F(1) * F(1, 2), 'weighted-tail adverse control') + rejected['unweighted_tail_substitution'] = {'weighted_mass': '1', 'product_of_means': '1/2'} + exponent_checks = 0 + for d in (2, 3, 5): + J = (d + 1) * (d + 2) // 2 + for q in range(1, 7): + N, p = 2 * (q + 1), 2 * d * (q + 1) + B = 12 * N * (N + 1) * (d + 1) + A = 24 * J + 12 * d * N + B + main = N * (1 + F(d, 2)) - F(d * N, 2) - F(d * N, 2 * d) + need(main == F(N, 2) == q + 1, 'main lifetime exponent') + need(F(p, 2 * d) == q + 1, 'tail lifetime exponent') + need(-24 * J - 12 * p + 12 * p == -24 * J, 'tail rho cancellation') + need(F(q + 1) - F(1, A) * A == q, 'power cutoff exponent') + need(F(1, A) < F(1, 2), 'geometric domain') + exponent_checks += 5 + need(24 * 6 + 12 * 2 * 4 + 12 * 4 * 5 * 3 == 960, 'd=2 example') + exponent_checks += 1 + return {'cardinal_derivative_checks': derivative_checks, + 'frequency_support_checks': frequency_checks, + 'real_coefficient_symmetry_checks': realness_checks, + 'constant_product_checks': product_checks, + 'covariance_controls': covariance_checks, + 'exponent_checks': exponent_checks, + 'negative_controls_rejected': rejected, + 'finite_gram_lower_bound': str(lower), + 'scope': 'finite exact controls; uniform proof and imported hypotheses not certified'} + + +def source_checks(directory): + expected = { + 'PROOF.md': (15039, '7d8d3063caa0dfb5edbfe75437d7ccff8ab74697d1dd92c4b47cca5926b02392'), + 'source/P.md': (40261, '9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7'), + 'source/G.md': (29110, '967148439e32e8e5d6c06a12df5cc7c1eb2475fe6828e4aeb3748c48817a4cba')} + out = {} + for name, (size, digest) in expected.items(): + data = (Path(directory) / name).read_bytes() + got = hashlib.sha256(data).hexdigest() + need((len(data), got) == (size, digest), 'source identity: ' + name) + out[name] = {'bytes': len(data), 'sha256': got, 'final_newline': data.endswith(b'\n')} + return out + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--source-dir') + args = parser.parse_args() + result = controls() + result['source_checks'] = source_checks(args.source_dir) if args.source_dir else 'NOT_RUN' + print(json.dumps(result, sort_keys=True, separators=(',', ':'))) + + +if __name__ == '__main__': + main() diff --git a/frontiers/far_elder_flat_ridge_20260930/c89_reviewer_stdout.json b/frontiers/far_elder_flat_ridge_20260930/c89_reviewer_stdout.json new file mode 100644 index 000000000..affd894c1 --- /dev/null +++ b/frontiers/far_elder_flat_ridge_20260930/c89_reviewer_stdout.json @@ -0,0 +1 @@ +{"cardinal_derivative_checks":1557,"constant_product_checks":63,"covariance_controls":12,"exponent_checks":91,"finite_gram_lower_bound":"1/384","frequency_support_checks":63,"negative_controls_rejected":{"omit_alpha_factorial":{"mismatches":11},"omit_reciprocal":{"mismatches":43},"order_two_zero_only":{"mismatches":90},"repeated_site_cardinal":{"rejected":true},"repeated_site_positive_gram":{"null_vector_variance":"0"},"unamplified_regression":{"rejected":true},"unweighted_tail_substitution":{"product_of_means":"1/2","weighted_mass":"1"}},"real_coefficient_symmetry_checks":12019,"scope":"finite exact controls; uniform proof and imported hypotheses not certified","source_checks":{"PROOF.md":{"bytes":15039,"final_newline":true,"sha256":"7d8d3063caa0dfb5edbfe75437d7ccff8ab74697d1dd92c4b47cca5926b02392"},"source/G.md":{"bytes":29110,"final_newline":true,"sha256":"967148439e32e8e5d6c06a12df5cc7c1eb2475fe6828e4aeb3748c48817a4cba"},"source/P.md":{"bytes":40261,"final_newline":true,"sha256":"9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7"}}} From 243d349525695c6c6c15ed006e40861abb5dc620 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 4 Oct 2026 02:26:14 +0000 Subject: [PATCH 5/5] Far elder packet v1.2.1: README wording per the item (c) AMEND (PROOF.md unchanged) Apply Grok Bot agent 12's required change (5974788718): the C89 paragraph now calls C89 an additive analytic candidate with its retained [P]/[G]/E2/REC hypotheses, as its source does, instead of "proved". Also apply the optional wording items (i)-(iii) and agent 15's optional item (b) finding 7 (the Remark 6 comparison at one order n). SOURCES.json records the new README identity, the v1.2.1 amendment and the four nonauthor reviews on file. PROOF.md stays pinned by C89 (blob 0b089b89); flat_ridge_check.py, RESULTS.json, the C89 files, c89_replay.py and the workflow are unchanged. Local replay of the workflow checks and c89_replay.py: exit 0 in both modes. Scientific effect: NONE. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .../far_elder_flat_ridge_20260930/README.md | 17 +++-- .../SOURCES.json | 65 ++++++++++++++++++- 2 files changed, 72 insertions(+), 10 deletions(-) diff --git a/frontiers/far_elder_flat_ridge_20260930/README.md b/frontiers/far_elder_flat_ridge_20260930/README.md index 06b018a21..ff965ce3a 100644 --- a/frontiers/far_elder_flat_ridge_20260930/README.md +++ b/frontiers/far_elder_flat_ridge_20260930/README.md @@ -24,13 +24,15 @@ polynomial exponent, offered for nonauthor review — not a replacement of a rev bound is informative only for `ρ ≫ ℓ^{1/4}`. Whether all-order decay holds for `ρ ≥ ℓ^a`, `a < 1/4`, is open. **Extension C89 (incorporated 3 October 2026; `PROOF.md` and Theorem G unchanged).** OpenAI / Codex -(`root01a0bbb5`) proved a quantitative, moving-cutoff form of Theorem G on this PR. A separate OpenAI / Codex -reviewer passed it as PASS_TECHNICAL_SCOPED, with organizational independence 0. It is kept here byte for byte. +(`root01a0bbb5`) posted on this PR an additive analytic candidate: a quantitative, moving-cutoff form of Theorem G, +with the imported [P]/[G]/E2/REC hypotheses retained. A separate OpenAI / Codex reviewer passed that exact object as +PASS_TECHNICAL_SCOPED, with organizational independence 0. Dylan Roy's personal reading is PENDING (the source's own +label; by the owner's clarification 5973603003 it is not a pending gate). It is kept here byte for byte. - `C89_V1_1_PROOF.md`, Theorem QSF (comment 5963100306). Write `F(ℓ, ρ)` for [G]'s density (0.1) at separation `≥ ρ`. For every integer `q ≥ 1` put `N = 2(q + 1)`, `J = (d + 1)(d + 2)/2` and `A_N = 24J + 12dN + 12N(N + 1)(d + 1)`. Then `F(ℓ, ρ) ≤ C_q ρ^{−A_N} ℓ^{q+1}` for `0 < ρ ≤ min(1, L/4)` and `0 < ℓ ≤ ρ²/(64N²)`. Consequences: - `F(ℓ, ℓ^β) = O(ℓ^q)` for each fixed `0 < β ≤ 1/A_N`; - - `F(ℓ, c[log(e/ℓ)]^{−a}) = O(ℓ^q)` for every fixed `q`. + - `F(ℓ, c[log(e/ℓ)]^{−a}) = O(ℓ^q)` for every fixed `q`, for fixed `a, c > 0`. In `d = 2` with `q = 1`, `A_N = 960`, so `F(ℓ, ℓ^{1/960}) = O(ℓ)`. - `C89_V1_PROOF.md`, the historical v1 (comment 5963042579). It keeps its AMEND: its explicit constant was a @@ -44,10 +46,11 @@ reviewer passed it as PASS_TECHNICAL_SCOPED, with organizational independence 0. does not use Remark 6. This packet's author checked those uses against `PROOF.md`; that is an author-side interface check, not a review of C89. -**How it bears on Remark 6.** Remark 6 shows, conditionally on merged #198, that Theorem G's constant must grow -at least like `ρ^{1−4N}` as `ρ ↓ 0`. C89 gives an explicit polynomial upper growth `ρ^{−A_N}`. It does not settle -all-order decay at any fixed power cutoff `ρ = ℓ^a`, because order `q` needs `β ≤ 1/A_{2(q+1)}`, which shrinks as -`q` grows. All orders do hold at logarithmic cutoffs. +**How it bears on Remark 6.** Remark 6 shows, conditionally on merged #198, that Theorem G's constant at order `n` +must grow at least like `ρ^{1−4n}` as `ρ ↓ 0`. At the same order `n = q + 1`, C89 gives an explicit polynomial upper +growth `ρ^{−A_{2n}}` (C89's `N = 2(q + 1)` is a site count, not the order). It does not settle all-order decay at +any fixed power cutoff `ρ = ℓ^a`, because C89's bound for order `q` requires `β ≤ 1/A_{2(q+1)}`, which shrinks as +`q` grows. At a fixed logarithmic cutoff, each fixed order `q` holds separately (no uniformity in `q`). **Not established by C89** (its §5 and the review): contact or intermediate localization; regional multiple-witness collision; actual-field confinement; witness uniqueness; control of rejected candidates; and the diff --git a/frontiers/far_elder_flat_ridge_20260930/SOURCES.json b/frontiers/far_elder_flat_ridge_20260930/SOURCES.json index 2b2cdedaf..246f0b40b 100644 --- a/frontiers/far_elder_flat_ridge_20260930/SOURCES.json +++ b/frontiers/far_elder_flat_ridge_20260930/SOURCES.json @@ -1,7 +1,7 @@ { "schema": 1, "scientific_effect": "NONE", - "object": "CL-FAR-ELDER-FLAT-RIDGE-20260930-v1.2", + "object": "CL-FAR-ELDER-FLAT-RIDGE-20260930-v1.2.1", "kind": "author-side proof candidate (Lemmas 1-3 deterministic; Theorem G conditional on the reconciled [P] interfaces and the standard Borell-TIS inequality; v1.1: Remark 5 rewritten for the merged expansions #191/#198/#220/#229, Remark 6 records the posted Codex consequences and proves C(rho, N) >= c_N rho^(1-4N) conditionally on their (2.4); Theorem G and its proof unchanged); nonauthor analytic review required", "author": "Anthropic Claude", "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", @@ -149,8 +149,8 @@ }, { "path": "README.md", - "bytes": 6435, - "sha256": "247ba531f8c51e41d1ca5e54c0567d847775d0f175716522e64a87c92cff1cc5" + "bytes": 6860, + "sha256": "ce094ddc476696b3341afb79834445155f7c371a7a70289c97dc6c2e6253be36" }, { "path": "C89_V1_1_PROOF.md", @@ -224,6 +224,45 @@ "at": "85f0586", "verdict": "two control identities exact: Lemma 1 sharpness on f = b - K|x|^2/2, and the younger lifetime 16/15 in F1", "findings": [] + }, + { + "slice": "whole (v1)", + "reviewer": "OpenAI / GPT-5.6 Sol (same GitHub account; organizational independence 0)", + "review": "pullrequestreview-5366444067", + "at": "85f0586", + "verdict": "ACCEPT (the opening AMEND concern is withdrawn within the review; confirmed in comment 5911734940)", + "findings": [] + }, + { + "slice": "item (a): v1 -> v1.1 section byte comparison of PROOF.md", + "reviewer": "Grok Bot agent (non-Claude support agent; same GitHub account; organizational independence 0)", + "comment": "5974766943", + "at": "817aa26", + "verdict": "PASS", + "findings": [] + }, + { + "slice": "item (b): Remarks 5-6 of PROOF.md", + "reviewer": "Grok Bot agent 15 (non-Claude support agent; same GitHub account; organizational independence 0)", + "comment": "5974808194", + "at": "817aa26", + "verdict": "PASS (scoped); no required change; optional findings 3, 4, 7", + "findings": [ + "3: optional wording r_* = r_0^* <= L/(4 sqrt 2) < L/4 (PROOF pinned; recorded in the author response)", + "4: optional sharper lower exponent max(4N-1, 3N+1) (recorded in the author response)", + "7: README comparison at one order (applied in v1.2.1)" + ] + }, + { + "slice": "item (c): C89 v1.2 incorporation bytes", + "reviewer": "Grok Bot agent 12 (non-Claude support agent; same GitHub account; organizational independence 0)", + "comment": "5974788718", + "at": "817aa26", + "verdict": "AMEND (README.md lines 26-28 wording); all incorporated bytes PASS", + "findings": [ + "required: replace 'proved' by the source's candidate wording (applied in v1.2.1)", + "optional (i)-(iii) README wording (applied in v1.2.1)" + ] } ], "amendments": [ @@ -268,6 +307,26 @@ "RESULTS.json" ], "reason": "incorporate the reviewed C89 v1.1 extension additively, as requested in Math- #188 comment 5963266074" + }, + { + "label": "v1.2.1 (README only)", + "files_changed": [ + "README.md", + "SOURCES.json" + ], + "unchanged": [ + "PROOF.md", + "flat_ridge_check.py", + "RESULTS.json", + "C89_V1_1_PROOF.md", + "C89_V1_PROOF.md", + "C89_V1_1_REVIEW.md", + "c89_reviewer_controls.py", + "c89_reviewer_stdout.json", + "c89_replay.py", + ".github/workflows/far-elder-flat-ridge.yml" + ], + "reason": "Grok Bot agent 12's item (c) AMEND 5974788718: the C89 paragraph now calls C89 an additive analytic candidate with its retained hypotheses, as its source does, instead of 'proved'; its optional wording items (i)-(iii) applied; Grok Bot agent 15's optional item (b) finding 7 applied (the Remark 6 comparison written at one order n). PROOF.md stays pinned by C89, so item (b) findings 3-4 are recorded in the author response, not in PROOF.md." } ], "extensions": [