From ecd47e7b1d447eefec963b1fa8395777db09a190 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 11:37:59 +0000 Subject: [PATCH 1/2] Add far-elder-rate packet: short bars are born at soft maxima; far elder density O(ell^{2/3}) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit frontiers/far_elder_rate_20260930/ (CL-FAR-ELDER-RATE-20260930-v1): Lemma 1 (deterministic barrier: every finite bar of lifetime ell is born at a maximum with lambda_min(-D^2 f) <= (ell K^2/c_L)^{1/3}; the barrier of Math-#182 §3, re-proved) and Theorem F: the density of elder pairs at torus distance >= rho with lifetime ell is <= C ell^{2/3}, 0 < ell <= 1, by Kac-Rice with Markov conditional on the pins and both Hessians and a spectral integration that retains the determinant weight. Previously on file: bounded ([P] (14.1)) and o(1) without rate (Theorem Z). Corollaries: far elder bar count O(t^{5/3}), inverse-moment integrability up to 5/3 for the far population; a proven replacement for the manuscript's unproven O(ell) (Prop. A.3.2). Exact stdlib controls, four mutants, workflow gate; clean-context referee pass applied. Scientific effect NONE; will not merge. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .github/workflows/far-elder-rate.yml | 60 +++++ frontiers/far_elder_rate_20260930/PROOF.md | 217 ++++++++++++++++++ frontiers/far_elder_rate_20260930/README.md | 22 ++ .../far_elder_rate_20260930/RESULTS.json | 62 +++++ .../far_elder_rate_20260930/SOURCES.json | 117 ++++++++++ .../far_elder_check.py | 181 +++++++++++++++ 6 files changed, 659 insertions(+) create mode 100644 .github/workflows/far-elder-rate.yml create mode 100644 frontiers/far_elder_rate_20260930/PROOF.md create mode 100644 frontiers/far_elder_rate_20260930/README.md create mode 100644 frontiers/far_elder_rate_20260930/RESULTS.json create mode 100644 frontiers/far_elder_rate_20260930/SOURCES.json create mode 100644 frontiers/far_elder_rate_20260930/far_elder_check.py diff --git a/.github/workflows/far-elder-rate.yml b/.github/workflows/far-elder-rate.yml new file mode 100644 index 000000000..efe17c813 --- /dev/null +++ b/.github/workflows/far-elder-rate.yml @@ -0,0 +1,60 @@ +name: Far elder rate exact controls + +'on': + pull_request: + paths: + - 'frontiers/far_elder_rate_20260930/**' + - '.github/workflows/far-elder-rate.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_rate_20260930').resolve() + manifest = json.loads((root / 'SOURCES.json').read_text()) + 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 / 'far_elder_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 ('M1', 'M2', 'M3', 'M4'): + 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_rate_20260930/PROOF.md b/frontiers/far_elder_rate_20260930/PROOF.md new file mode 100644 index 000000000..37dcf6ef9 --- /dev/null +++ b/frontiers/far_elder_rate_20260930/PROOF.md @@ -0,0 +1,217 @@ +# Short bars are born at soft maxima: a rate for the far elder density + +Object: CL-FAR-ELDER-RATE-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. + +## 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/2]`. For `y ∈ X` with `dist(0, y) ≥ ρ` write, as in [P] §14 and [Z] §1, + + 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). + +The far elder density per unit volume at lifetime `ℓ` is the canonical marked Kac–Rice version ([P] §9 read as +[E2]; the height Jacobian is 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) + +The argument of [P] §14 gives `ν_eld^{far,ρ}(ℓ) ≤ C` for `0 < ℓ ≤ 1` ((14.1) is its case `ρ = r_0`); [Z] (Z11)–(Z12), +with the dominator of [Z] §4 on `D_ρ × R`, give `ν_eld^{far,ρ}(ℓ) → 0` as `ℓ ↓ 0` with no rate. The SIDE24 manuscript +(30 July 2026 revision, supplement Proposition A.3.2, restated as A.3.2′ in the 2026-08-01 amendment) asserts an +`O(ℓ)` bound for this quantity on `(0, ℓ_0]`; the July audit (F-02) found the supplement's proof of the rate invalid, +and no repository record proves it. + +**Theorem F.** There is `C = C(d, L, ρ) < ∞` such that + + ν_eld^{far,ρ}(ℓ) ≤ C ℓ^{2/3}, 0 < ℓ ≤ 1. (0.2) + +**Lemma 1 (deterministic; every short bar is born at a soft maximum).** Let `f ∈ C³(X)`, let `M` be a point +with `∇f(M) = 0` and `D²f(M) < 0`, put `λ = λ_min(−D²f(M)) > 0` and +`K = 1 + sup_X ‖D²f‖_op + sup_X ‖D³f‖_op`. With `a_L = min(1, L/4)` and `R = a_Lλ/K`, + + f(M + z) ≤ f(M) − (λ/3)|z|² for |z| ≤ R, (1.1) + ℓ(M) := f(M) − d_f(M) ≥ c_L λ³/K², c_L = a_L²/3, (1.2) + +where `d_f(M) = sup{min_t f(γ(t)) : γ(0) = M, f(γ(1)) > f(M)}` is the ordinary superlevel maximin of [P] §8 +(`d_f = −∞` for an essential maximum, and (1.2) then holds trivially). Equivalently: a finite `H_0` bar of +lifetime `ℓ` is born at a maximum with + + λ_min(−D²f(M)) ≤ (ℓK²/c_L)^{1/3}. (1.3) + +Lemma 1 is (8)–(9) of Math- #182 §3 (OpenAI, unmerged; accepted at Slice A by this author on 2026-09-30); its +five-line proof is repeated in §1 so that this note is self-contained and consumes nothing unmerged. + +**Corollary F1 (far bars).** For every `t ∈ (0, 1]`, `E N_eld^{far,ρ}(0, t] ≤ (3/5)C t^{5/3}` per unit volume, and +for every real `q > −5/3`, `E Σ_{far elder bars, ℓ_i ≤ t} ℓ_i^q ≤ C_q t^{q + 5/3}`. In particular the far elder +population has inverse-lifetime integrability at least up to `p < 5/3`, against the `p < 2/3` threshold of the +leading `ℓ^{−1/3}` density ([P] §12, [R] §8). + +**Corollary F2 (for the manuscript).** In the near/far decomposition of Theorem R ([R] §7, with `ρ = r_0`), +`ν_eld(ℓ) = ν_eld^{near}(ℓ) + O(ℓ^{2/3})` for `0 < ℓ ≤ 1`. This sharpens only the far term; Theorem R's absolute +`O(1)` remainder (R1) is dominated by its near terms (R16), (R18) and by the `O(1)` of [P] (14.1), and is +unchanged. What (0.2) supplies is a proven far-elder rate that may replace the manuscript's unproven `O(ℓ)` +(Proposition A.3.2 / A.3.2′) in the V3 text; the same proof gives `C(ℓ_0)ℓ^{2/3}` on any range `(0, ℓ_0]`. The +manuscript uses A.3.2 only to conclude that the far elder contribution is `o(ℓ^{−1/3})`, which boundedness already +gives. + +**What is not claimed.** No rate for the far *rejected* density (on `D_ρ` it tends to `∫_{D_ρ}∫Ψ_0 db dy ∈ +(0, B_{d,L})`, [Z] (Z5), and has the lower bound `c_*` of [U] (U1) at `ρ = r_0`); no near-pair statement beyond +(1.3); no numerical `C`; no uniformity in `L`, `d` or `ρ ↓ 0`; nothing about the true +order of `ν_eld^{far,ρ}` (§4 explains why it is expected to be far smaller than `ℓ^{2/3}`). + +## 1. Proof of Lemma 1 + +Since `K ≥ sup‖D²f‖_op ≥ λ`, `R = a_Lλ/K ≤ a_L ≤ L/4 < L/2`, so the ball `B(M, R)` is embedded in the torus. +For a unit vector `v` and `0 < t ≤ R`, Taylor's theorem with the global third-derivative bound gives + + f(M + tv) ≤ f(M) + (t²/2) vᵀD²f(M)v + (K/6)t³ ≤ f(M) − (λ/2)t² + (K/6)t³. + +For `t ≤ R ≤ λ/K` the cubic term is at most `(K/6)t²(λ/K) = (λ/6)t²`, which gives (1.1). Hence no point of +`B(M, R)` lies above `f(M)`, and every continuous path from `M` to a point above `f(M)` crosses the sphere +`|z − M| = R`, on which `f ≤ f(M) − λR²/3` by (1.1). Therefore `d_f(M) ≤ f(M) − λR²/3`, i.e. +`ℓ(M) ≥ λR²/3 = (a_L²/3)λ³/K²`, which is (1.2); (1.3) is (1.2) solved for `λ`. If no path to an older point +exists, `d_f = −∞` and (1.2) is trivial. ∎ + +The bound has the right exponent for the near law: for a pinned pair at separation `r` and gap `ℓ = kr³`, the +axial curvature at `M` satisfies `λ ≤ −f_xx(M) ≤ 6kr + r²M_4/2` ([P] (5.2)), and `K ≥ 1 + sup|f_xxx| ≥ 1 + 12k` +exactly, because the pinned row `U_3 = 12k` of [P] (3.1) is an average of `f_xxx` against a nonnegative kernel. +With `λ = 6kr`, `c_Lλ³/K² = 216c_Lk³r³/K² ≤ 216c_Lk²/(1 + 12k)² · ℓ < ℓ/2` for `c_L ≤ 1/3`. So for near pairs (1.3) +is satisfied automatically with the same exponent (`λ ≍ ℓ^{1/3}` on both sides), while for far pairs it is a +genuine restriction. + +## 2. Fixed-separation Gaussian facts (reconstructed; no contact limit) + +Let `D_ρ = {y ∈ X : dist(0, y) ≥ ρ}`, compact. Append to `O_y` the independent entries of `H_0 = D²f(0)` and +`H_y = D²f(y)`: + + V_y = (O_y, H_0, H_y) (2(d + 1) + d(d + 1) coordinates). + +All these functionals are distinct derivative evaluations at two distinct sites, so by [P] §2 their covariance +`Γ_y` is positive definite for each `y ≠ 0`; it is continuous in `y`, hence uniformly positive definite on the +compact `D_ρ` (this is the compactness argument of [P] §14, applied to the enlarged list). Consequently: + +(a) 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|²)]`, + and since `|v_{b,ℓ}|² ≥ b²`, + + p_y(v_{b,ℓ}) · density(H_0, H_y | O_y = v_{b,ℓ}) ≤ C exp[−c(b² + |H_0|² + |H_y|²)], (2.1) + + uniformly for `y ∈ D_ρ`, `b ∈ R` and every `ℓ` (`V_y` is centred; only the uniform eigenvalue bounds of `Γ_y` + enter); + +(b) regressing the whole field on `V_y` ([P] §4's argument at a fixed pair of sites) gives `f = m + g` with + `g` independent of `V_y`, `E‖g‖_{C³}^q ≤ C_q` uniformly on `D_ρ`, and `‖m‖_{C³} ≤ C(1 + |b| + |H_0| + |H_y|)` + for `ℓ ≤ 1` (the regression coefficients are fixed smooth covariance derivatives times the uniformly + bounded `Γ_y^{−1}`). Hence, with `K = 1 + sup‖D²f‖ + sup‖D³f‖`, for every `q ≥ 1` + + E[K^q | V_y = (v_{b,ℓ}, H_0, H_y)] ≤ C_q (1 + |b| + |H_0| + |H_y|)^q. (2.2) + + Under the regular conditional law the field is smooth almost surely ([E2] §9.1 constructs it on `C²`; the + same regression gives a `C^∞` version), so `K` is a.s. finite and (2.2) is a statement about that law. + +Nothing here tends to `r = 0`; no normalizer or cap estimate is used. + +## 3. Proof of Theorem F + +Fix `y ∈ D_ρ`, `b`, `0 < ℓ ≤ 1`, and work under `Q = Q_{y,b,ℓ}`. On the event `{W(f) > 0, e_y(f) = 1}` the point +`0` is a nondegenerate maximum with `f(0) = b`, and its death partner is the saddle at `y` with +`f(y) = b − ℓ`, so `d_f(0) = b − ℓ` and Lemma 1 gives, with `λ = λ_min(−H_0)`, + + ℓ ≥ c_L λ³/K², i.e. K ≥ (c_L λ³/ℓ)^{1/2}. + +Hence, pathwise, + + W(f) e_y(f) ≤ W(f) 1{K ≥ (c_Lλ³/ℓ)^{1/2}}. (3.1) + +`W` is a function of `(H_0, H_y)`, so conditioning on `V_y` and applying Markov's inequality with (2.2), + + E_Q[W e_y] ≤ E_Q[ W · min{1, C_q(1 + |b| + |H_0| + |H_y|)^q (ℓ/(c_Lλ³))^{q/2}} ]. (3.2) + +Multiply by `p_y(v_{b,ℓ})` and use (2.1); bound `(1 + |b| + |H_0| + |H_y|)^q ≤ (1 + |b|)^q(1 + |H_0|)^q(1 + |H_y|)^q`, +take the two Hessian factors outside the minimum (`min{1, xy} ≤ y·min{1, x}` for `y ≥ 1`), and integrate `H_y` +against `|det H_y|(1 + |H_y|)^q e^{−c|H_y|²}` (a constant). For `H_0` use the ordered spectral +coordinates of `−H_0 = O diag(λ_1 ≤ … ≤ λ_d) Oᵀ` on the cone `{H_0 < 0}` (Lebesgue Jacobian +`const · ∏_{i 2` (any `q > 4/3`; take `q = 2`) and `Aℓ^{q/2} = u^{3q/2}`, `u ≤ 1`. In every case the integral in (3.3) is at most +`Cu² = C A^{4/(3q)} ℓ^{2/3} = C (1 + |b|)^{4/3} ℓ^{2/3}`. Therefore + + p_y(v_{b,ℓ}) E_Q[W e_y] ≤ C (1 + |b|)^{4/3} e^{−cb²} ℓ^{2/3}, + +and integrating over `b ∈ R` and `y ∈ D_ρ` (volume at most `L^d`) in (0.1) proves (0.2). ∎ + +The proof retains the determinant weight throughout: the factor `λ_1` inside (3.3) is `|det H_0|`'s soft +eigenvalue, and it is what turns the barrier constraint `λ_1 ≲ ℓ^{1/3}` into the mass `ℓ^{2/3}`. Dropping the weight +(a raw Gaussian conditioning on the two types) would give only `ℓ^{1/3}`. + +## 4. What the rate does and does not say + +* (1.3) is deterministic and general: for any `C³` function on the torus, on the Morse distinct-critical-value + locus (where the bar born at `M` has lifetime `f(M) − d_f(M)`), every finite bar of lifetime `ℓ` is born at a + maximum whose weakest curvature is at most `(ℓK²/c_L)^{1/3}`; off that locus (1.1) still shows that the + component of `{f > f(M) − λR²/3}` containing `M` lies inside `B(M, R)` with `M` as its unique maximum. For the near population this is the + scaling `λ ≍ 6kr = 6(k²ℓ)^{1/3}` already built into [P]; for the far population it is a genuine restriction, + and (0.2) is its cost under the Kac–Rice weight. +* The bound is not expected to be sharp. For `y` to be the death saddle of `0` at gap `ℓ` with `dist(0, y) ≥ ρ`, + the superlevel component of `0` at level `b − ℓ` must reach `y` without meeting any point above `b`: the field + stays within a band of width `ℓ` along *some* curve of length `≥ ρ`. I expect the probability of such an + event to decay faster than any power of `ℓ` (for a fixed curve it is a small-ball event of a smooth Gaussian + process; here the curve is chosen by the field, and no such estimate is proved anywhere in the repository); + the barrier captures only its first factor, a soft maximum. Nothing beyond (0.2) is claimed. +* Corollary F1 follows from (0.2) by integrating `ℓ^{2/3}` (for the count) and `ℓ^{q + 2/3}` (for the moments, + finite at `0` iff `q > −5/3`). Corollary F2 is (0.2) inserted into [R] §7, where the far term entered only as + the `O(1)` of [P] (14.1). +* Consistency with [U] and [Z]: the far *rejected* density has the positive lower bound `c_*` ([U] (U1), at + `ρ = r_0`) and, on `D_ρ`, tends to the positive limit `∫_{D_ρ}∫Ψ_0 db dy` ([Z] (Z5)); (0.2) says the far *elder* + density is the vanishing part, at rate at least `ℓ^{2/3}`. Nothing in (0.2) bears on the rejected part. +* Method. The barrier–Markov–spectral route is that of Math- #182 §§2–4 (fixed-`r` pinned pair, upper bound of + its Theorem 1), including the remark that dropping the determinant weight would give `ℓ^{1/3}`. What is new + here is the transplant to a far saddle pinned at gap `ℓ`, the uniformity over the compact separation set + `D_ρ`, the `b`-growth bookkeeping and the `(b, y)` integration that turns it into a density rate. + +## 5. Sources (exact identities in `SOURCES.json`) + +| Tag | Source | Consumed | +|---|---|---| +| [P] | `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` (`dfed3b8d`) | §1 model; §2 distinct-site rank; §3 (3.1) row `U_3` and §5 (5.2) (only in the near-pair remark of §1); §4 regression argument (used at a fixed pair of sites); §7 spectral Lebesgue coordinates; §8 maximin definition and Borel elder mark; §9 marked Kac–Rice as [E2]; §14 far domain, uniform covariance, height Jacobian 1, (14.1). Read with [E1], [E2], [REC] §1. | +| [E1] | `imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md` (`213594d6`) | reading rule (not used in any step here). | +| [CAP] | `imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md` (`0633aca3`) | reading rule of [REC] §1 (not used in any step here). | +| [E2] | `reviews/d1_section9_borel_repair_20260925/REPAIR.md` (`fe9b9ce4`) | §9.1–9.4: regular conditional law on the field space, Borel weights on compact off-diagonal domains, the elder/type mark. | +| [REC] | `reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md` (`75da2597`) | §1 reading rule for [P]; §7 consumption contract (this note consumes only §§2, 4, 7–9, 14 conventions and (14.1)). | +| [Z] | `frontiers/c7_zero_gap_limit_20260929/PROOF.md` (`5b6328ea`) | cited only: (Z1) notation, Theorem Z, (Z11)–(Z12) as the `o(1)` predecessor. | +| [U] | `frontiers/unrestricted_selection_difference_20260929/PROOF.md` (`5a55b179`) | cited only: (U1). | +| [R] | `frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md` (`247b3ecf`) | cited only: §7 near/far decomposition, §8 moments. | +| [182] | Math- #182 `frontiers/fixed_r_inverse_lifetime_20260930/PROOF.md` (head `0f448f46`, blob `0d401877`) | cited only: §3 (8)–(9) is Lemma 1 and §§2, 4, 7 are the method (see §4); every step is re-proved here, nothing unmerged is consumed. | + +## 6. Finite controls + +`far_elder_check.py` (standard library, exact rationals): B1 the barrier inequality (1.1) on an explicit polynomial +at rational points of the ball; B2 the algebraic core of (1.1) (`Kt³/6 ≤ λt²/6` for `t ≤ λ/K`) and the constants +`a_L`, `c_L`; I1 the split integral of §3 in closed form and the inequality `∫_0^u λ dλ + ∫_u^1 λ(u/λ)^{3q/2} dλ ≤ +u²(1/2 + 1/(3q/2 − 2))` at rational `u, q`; I2 the exponent ledger (`u³ = A^{2/q}ℓ`, `u² ∝ ℓ^{2/3}`, the `5/3` +threshold and count exponent); N1 the near-pair consistency inequality `6(6c_L)^{1/2} < 12`; mutants `M1`–`M4` +exit 1, unknown label exits 2. These are algebra and calculus controls; they do not prove the Gaussian step. + +## 7. Review division + +* **Slice A (deterministic):** Lemma 1 and §1. Lemma 1 is OpenAI's (#182) and was accepted there by this author; + a provider distinct from both is xAI. +* **Slice B (Gaussian):** §2 and §3 — the uniform fixed-separation regression, the conditional Markov step (3.2), + the spectral integration (3.3) and the split. Best read by a lane not exposed to [P]'s authorship. +* **Slice C (consequences):** Corollaries F1–F2 and the honest §4. diff --git a/frontiers/far_elder_rate_20260930/README.md b/frontiers/far_elder_rate_20260930/README.md new file mode 100644 index 000000000..cdb2ba17e --- /dev/null +++ b/frontiers/far_elder_rate_20260930/README.md @@ -0,0 +1,22 @@ +# Far elder density rate (CL-FAR-ELDER-RATE-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(ℓ^{2/3})` as `ℓ ↓ 0` (Theorem F). +Previously on file: bounded ([P] (14.1)) and `o(1)` without rate ([Z]). The manuscript's Proposition A.3.2 asserts +`O(ℓ)` without a valid proof (July audit F-02); Theorem F is the proven replacement, with the weaker exponent. + +**Mechanism.** Every finite bar of lifetime `ℓ` is born at a maximum whose weakest curvature is at most +`(ℓK²/c_L)^{1/3}` (Lemma 1, deterministic; the barrier of Math- #182 §3, re-proved here). Under the Kac–Rice weight +`|det H_M|` the soft eigenvalue costs `∫_0^{u} λ dλ ≍ u²`, i.e. `ℓ^{2/3}`; Markov's inequality conditional on the +pins and both Hessians keeps the derivative norm inside the weighted integral (Math- #182 §§2–4's route, transplanted +to a far saddle pinned at gap `ℓ`, made uniform over the compact separation set). + +Files: `PROOF.md`; `far_elder_check.py` (stdlib exact controls; `RESULTS.json` its output, `-O` identical; mutants +`M1`–`M4` exit 1, unknown label exit 2); `SOURCES.json` (exact identities of every source; nothing unmerged is +consumed). A clean-context referee agent read the note before landing; its findings (F2 framing, the far rejected +limit on `D_ρ`, credit to #182's method, wording of the heuristic) were applied. + +Review slices (§7): A deterministic (Lemma 1; xAI is the provider distinct from both #182's author and this one); +B Gaussian (§§2–3); C consequences (Corollaries F1–F2, §4). diff --git a/frontiers/far_elder_rate_20260930/RESULTS.json b/frontiers/far_elder_rate_20260930/RESULTS.json new file mode 100644 index 000000000..07788c5ec --- /dev/null +++ b/frontiers/far_elder_rate_20260930/RESULTS.json @@ -0,0 +1,62 @@ +{ + "checks": { + "B1_barrier_polynomial": { + "info": { + "K": "22", + "R": "1/11", + "grid_points_in_ball": 1793, + "lambda": "2" + }, + "passed": true + }, + "B2_algebra_and_constants": { + "info": { + "L=1": { + "a_L": "1/4", + "c_L": "1/48" + }, + "L=2": { + "a_L": "1/2", + "c_L": "1/12" + }, + "L=24": { + "a_L": "1", + "c_L": "1/3" + }, + "L=4": { + "a_L": "1", + "c_L": "1/3" + } + }, + "passed": true + }, + "I1_split_integral": { + "info": { + "q=2,u=1/100": "149/1000000", + "q=2,u=1/4": "5/64", + "q=2,u=1/9": "25/1458", + "q=4,u=1/100": "299999999/4000000000000", + "q=4,u=1/4": "767/16384", + "q=4,u=1/9": "9841/1062882" + }, + "passed": true + }, + "I2_exponent_ledger": { + "info": { + "count exponent": "5/3", + "inverse moment threshold": "-5/3", + "u^2 exponent of ell": "2/3" + }, + "passed": true + }, + "N1_near_consistency": { + "info": { + "6*sqrt(6 c_L) < 12 for c_L <= 1/3": true + }, + "passed": true + } + }, + "object": "CL-FAR-ELDER-RATE-20260930-v1", + "passed": true, + "scientific_effect": "NONE" +} diff --git a/frontiers/far_elder_rate_20260930/SOURCES.json b/frontiers/far_elder_rate_20260930/SOURCES.json new file mode 100644 index 000000000..950c54f88 --- /dev/null +++ b/frontiers/far_elder_rate_20260930/SOURCES.json @@ -0,0 +1,117 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "object": "CL-FAR-ELDER-RATE-20260930-v1", + "kind": "author-side proof candidate (Lemma 1 deterministic; Theorem F conditional on the reconciled [P] interfaces); nonauthor analytic review required", + "author": "Anthropic Claude", + "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", + "read_at": { + "branch_base": "f430fdecbb1d8802d8af40419b701f12af87c039" + }, + "consumed": [ + { + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "bytes": 40261, + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "tag": "P", + "use": "§1, §2, §3 (3.1), §4 (argument at fixed sites), §5 (5.2), §7 (spectral coordinates), §8, §9 as [E2], §14" + }, + { + "path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", + "bytes": 9062, + "sha256": "845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f", + "git_blob": "fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a", + "tag": "E2", + "use": "§9.1-9.4" + }, + { + "path": "reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md", + "bytes": 23312, + "sha256": "451b9d7ffee072a73fc904cab891b6693e3f233808b89df10cce1b57036b65da", + "git_blob": "75da2597971510f843f8d90c743950cb8c177342", + "tag": "REC", + "use": "§1 reading rule, §7 consumption contract" + }, + { + "path": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", + "bytes": 1782, + "sha256": "bad7ef609c4ad8c41ad6af562c1b6807921e19a9d556ed793ad1a0db6e202028", + "git_blob": "213594d6ca6a86fb938110f4d166d9ce275a02d0", + "tag": "E1", + "use": "reading rule only" + }, + { + "path": "imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md", + "bytes": 15160, + "sha256": "0bf922b9203c29088b12388807aa0e2ecd020485eb0f6e919679841b5b2636fc", + "git_blob": "0633aca3c2a2882b0de4399da0a75d64c2e6b2e1", + "tag": "CAP", + "use": "reading rule only (not used in any step)" + } + ], + "cited_only": [ + { + "path": "frontiers/c7_zero_gap_limit_20260929/PROOF.md", + "bytes": 17592, + "sha256": "f0e563c45c41333f2bb6e5bf5cb98f0d3b592e2abf2af1c1b098c21ad77cb777", + "git_blob": "5b6328ea3d6afcbeb731698b3834e536f72d1bcb", + "tag": "Z", + "use": "(Z1), (Z5), Theorem Z, (Z11)-(Z12): the o(1) predecessor" + }, + { + "path": "frontiers/unrestricted_selection_difference_20260929/PROOF.md", + "bytes": 13028, + "sha256": "93a63002d32fd5c35ae994fe28b1205d8098026d6ddde19c67d4977dcf5817a9", + "git_blob": "5a55b179a974a90c65d257f3f93765cc6fb30bb8", + "tag": "U", + "use": "(U1)" + }, + { + "path": "frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md", + "bytes": 17734, + "sha256": "380b7d0abdb0fe2de5a6564565af9560d3f1b1ce22fd5538927db0c52f4f3a4a", + "git_blob": "247b3ecf80bfbe896948d5d489b2d5842a81c481", + "tag": "R", + "use": "§7 near/far decomposition, §8 moments" + } + ], + "cited_unmerged": [ + { + "path": "frontiers/fixed_r_inverse_lifetime_20260930/PROOF.md", + "pr": "d6g8k5htny-coder/Math-#182", + "commit": "0f448f469d391dee5f8a35cfb04b7cfa7709f947", + "git_blob": "0d4018777d13672c1de1696525512e80b23b7c3c", + "bytes": 17213, + "sha256": "5adef725c1c696adae9bc73a525efe0bfe09d5c07e95ee3f067db9e877283630", + "tag": "182", + "use": "cited only: §3 (8)-(9) is Lemma 1 (re-proved here); §§2, 4, 7 are the method; nothing unmerged is consumed; not verified by the workflow" + } + ], + "referee": { + "kind": "clean-context Anthropic Claude subagent before landing (same provider, same account; not a nonauthor review)", + "findings": "no blocking; amendments applied: Corollary F2 framing (Theorem R unchanged), far rejected limit restricted to D_rho, method credit to #182 sections 2/4/7, heuristic in section 4 stated as an expectation, generic-locus qualification of (1.3), implicit steps in (3.3), SOURCES.json added, script docstrings and the vacuous closed-form check repaired" + }, + "files": [ + { + "path": "PROOF.md", + "bytes": 16413, + "sha256": "67f606327b66a2b4f1b8c67a57d119ac9ddfd2ce827ca8cb0c4daefa31904a3b" + }, + { + "path": "far_elder_check.py", + "bytes": 8137, + "sha256": "38a8eea06941c5103b2bb2d1615e1cfe65f8f35d366d2e66f683f0c19b9abdb6" + }, + { + "path": "RESULTS.json", + "bytes": 1111, + "sha256": "6ef4152058bd186766c97aba47a8a3485f5b033943d3d1d134c427a6702c4947" + }, + { + "path": "README.md", + "bytes": 1808, + "sha256": "c1b9fbc8db38b8deab4c48c73d4f53f28e94f4e5ea92dff35bc3d8f5c2f316c7" + } + ] +} diff --git a/frontiers/far_elder_rate_20260930/far_elder_check.py b/frontiers/far_elder_rate_20260930/far_elder_check.py new file mode 100644 index 000000000..58ff10f85 --- /dev/null +++ b/frontiers/far_elder_rate_20260930/far_elder_check.py @@ -0,0 +1,181 @@ +#!/usr/bin/env python3 +"""Exact finite controls for PROOF.md (CL-FAR-ELDER-RATE-20260930-v1). Standard library only; exact rationals. + + B1 the barrier inequality (1.1) on an explicit polynomial f(z) = -z1^2 - 2 z2^2 + z1^3 + z1 z2^2 - z1^2 z2 on + R^2 (maximum at 0, lambda = 2): with K an explicit upper bound of 1 + sup||D^2 f|| + sup||D^3 f|| on the unit + ball (Frobenius bounds, which only enlarge K) and R = a_L lambda / K (L = 24, a_L = 1), f(z) <= -(lambda/3)|z|^2 + holds at every rational grid point with |z| <= R; + B2 the algebraic core of (1.1): (K/6) t^3 <= (lambda/6) t^2 for 0 <= t <= lambda/K, at rational (lambda, K, t); + and the constants a_L = min(1, L/4), c_L = a_L^2/3 for L in {1, 2, 4, 24}; + I1 the split integral of section 3: for rational 0 < u <= 1 and q with 3q/2 > 2, + int_0^u lambda dlambda + int_u^1 lambda (u/lambda)^(3q/2) dlambda = u^2/2 + (u^2 - u^(3q/2))/(3q/2 - 2), + evaluated exactly at u = 1/4, 1/9, 1/100 and q in {2, 4}, and bounded by u^2 (1/2 + 1/(3q/2 - 2)); + I2 the exponent ledger by exact monomial substitution: u^3 = A^(2/q) ell gives u^2 = A^(4/(3q)) ell^(2/3); + the cumulative count exponent 2/3 + 1 = 5/3; the inverse-moment threshold: q + 2/3 > -1 iff q > -5/3; + N1 near-pair consistency: c_L (6 k r)^3 / K^2 <= k r^3 iff K >= 6 sqrt(6 c_L) k; (6 sqrt(6 c_L))^2 = 216 c_L < 144 + checked exactly at c_L in {1/3, 1/12, 1/48}, and the constraint verified at K = 1 + 12k for a rational (k, r); + M semantic mutants (--mutant M1|M2|M3|M4) exit 1; an unknown label exits 2. +""" +import argparse +import json +import sys +from fractions import Fraction as F + + +def f_poly(z1, z2): + return -z1*z1 - 2*z2*z2 + z1**3 + z1*z2*z2 - z1*z1*z2 + + +def check_barrier_polynomial(mutant): + lam = F(2) # eigenvalues of -Hess f(0) = diag(2, 4) + # explicit bound of 1 + sup||D^2 f|| + sup||D^3 f|| on |z| <= 1 (Frobenius norms majorise operator norms): + # D^2 f = [[-2 + 6 z1 - 2 z2, 2 z2 - 2 z1], [2 z2 - 2 z1, -4 + 2 z1]]; on the unit ball the entries are + # bounded by 10, 4, 4, 6, so the Frobenius norm is <= sqrt(100 + 16 + 16 + 36) = sqrt(168) < 13; + # D^3 f entries: f111 = 6, f112 = f121 = f211 = -2, f122 = f212 = f221 = 2, f222 = 0 -> Frobenius sqrt(60) < 8 + K = F(1) + F(13) + F(8) + if mutant == 'M1': + K = F(1) # too small a K breaks the barrier radius + aL = F(1) # L = 24 -> a_L = min(1, 6) = 1 + R = aL*lam/K + checked = 0 + n = 24 + for i in range(-n, n+1): + for j in range(-n, n+1): + z1 = R*F(i, n); z2 = R*F(j, n) + if z1*z1 + z2*z2 > R*R: + continue + if f_poly(z1, z2) > -(lam/3)*(z1*z1 + z2*z2): + return False, 'barrier (1.1) fails at z=(%s,%s)' % (z1, z2) + checked += 1 + return True, {'grid_points_in_ball': checked, 'R': str(R), 'K': str(K), 'lambda': str(lam)} + + +def check_algebra(mutant): + for lam in (F(1, 3), F(2), F(7)): + for K in (lam, 2*lam, 10*lam + 1): + for t in [lam/K*F(n, 8) for n in range(0, 9)]: + cubic = (K/6)*t**3; quad = (lam/6)*t*t + if mutant == 'M2': + cubic = (K/6)*t**3*2 + if cubic > quad: + return False, 'core inequality fails at lam=%s K=%s t=%s' % (lam, K, t) + consts = {} + for L in (F(1), F(2), F(4), F(24)): + aL = min(F(1), L/4); cL = aL*aL/3 + consts['L=%s' % L] = {'a_L': str(aL), 'c_L': str(cL)} + if consts['L=24']['c_L'] != '1/3' or consts['L=1']['c_L'] != '1/48': + return False, 'constants a_L, c_L wrong' + return True, consts + + +def rational_pow(u, e): + """u^e for Fraction u and Fraction e when the result is rational (u a perfect power); else None.""" + num, den = u.numerator, u.denominator + p, q = e.numerator, e.denominator + def root(n, q): + r = round(n ** (1.0/q)) + for cand in (r-1, r, r+1): + if cand >= 0 and cand**q == n: + return cand + return None + rn, rd = root(num, q), root(den, q) + if rn is None or rd is None: + return None + base = F(rn, rd) + return base**p if p >= 0 else 1/(base**(-p)) + + +def check_split_integral(mutant): + rows = {} + for q in (F(2), F(4)): + e = 3*q/2 # exponent 3q/2 + for u in (F(1, 4), F(1, 9), F(1, 100)): + # int_0^u lambda dlambda = u^2/2 + first = u*u/2 + # int_u^1 lambda (u/lambda)^e dlambda = u^e int_u^1 lambda^(1-e) = u^e (1 - u^(2-e))/(2-e) = (u^2 - u^e)/(e-2) + ue = rational_pow(u, e) + if ue is None: + return False, 'non-rational power' + second = (u*u - ue)/(e-2) + total = first + second + bound = u*u*(F(1, 2) + 1/(e-2)) + if mutant == 'M3': + bound = u*u*F(1, 2) + if total > bound: + return False, 'split integral exceeds its bound at u=%s q=%s' % (u, q) + # independent evaluation of the second piece: u^e * [F(1) - F(u)] with F(x) = x^(2-e)/(2-e) + u2e = rational_pow(u, 2-e) + second_alt = ue*((F(1) - u2e)/(2-e)) + if second_alt != second: + return False, 'second piece: antiderivative evaluation disagrees with the closed form' + rows['q=%s,u=%s' % (q, u)] = str(total) + return True, rows + + +class Mono: + def __init__(self, ell=F(0), A=F(0)): + self.ell, self.A = F(ell), F(A) + def __mul__(self, o): + return Mono(self.ell+o.ell, self.A+o.A) + def __pow__(self, e): + e = F(e); return Mono(self.ell*e, self.A*e) + def key(self): + return (self.ell, self.A) + + +def check_exponents(mutant): + for q in (F(2), F(4), F(10)): + ell, A = Mono(1, 0), Mono(0, 1) + u3 = (A**(2/q))*ell # u^3 + u = u3**F(1, 3) + u2 = u**2 + want = (F(2, 3), 4/(3*q)) + if mutant == 'M4': + want = (F(1, 3), 4/(3*q)) + if u2.key() != want: + return False, 'u^2 monomial wrong for q=%s: %s' % (q, u2.key()) + if F(2, 3) + 1 != F(5, 3): + return False, 'count exponent' + # inverse moments: int_0^t ell^(q + 2/3) dell finite at 0 iff q + 2/3 > -1 iff q > -5/3 + for qq in (F(-5, 3) + F(1, 100), F(-1), F(0)): + if not (qq + F(2, 3) > -1): + return False, 'moment threshold' + if F(-5, 3) + F(2, 3) > -1: + return False, 'threshold endpoint' + return True, {'u^2 exponent of ell': '2/3', 'count exponent': '5/3', 'inverse moment threshold': '-5/3'} + + +def check_near_consistency(mutant): + # c_L (6kr)^3 / K^2 <= k r^3 <=> 216 c_L k^2 <= K^2 <=> K >= 6 sqrt(6 c_L) k ; and 36*6*c_L < 144 for c_L <= 1/3 + for cL in (F(1, 3), F(1, 48), F(1, 12)): + if not (36*6*cL < 144): + return False, 'near consistency fails for c_L=%s' % cL + k, r = F(2, 5), F(1, 7) + K = 12*k + 1 + if not (cL*(6*k*r)**3/(K*K) <= k*r**3): + return False, 'near-pair barrier constraint violated at K = 1 + 12k' + return True, {'6*sqrt(6 c_L) < 12 for c_L <= 1/3': True} + + +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'): + sys.stderr.write('unknown mutant label\n'); sys.exit(2) + results = {} + ok_all = True + for name, fn in (('B1_barrier_polynomial', check_barrier_polynomial), ('B2_algebra_and_constants', check_algebra), + ('I1_split_integral', check_split_integral), ('I2_exponent_ledger', check_exponents), + ('N1_near_consistency', check_near_consistency)): + ok, info = fn(mutant) + results[name] = {'passed': bool(ok), 'info': info} + ok_all = ok_all and ok + out = {'object': 'CL-FAR-ELDER-RATE-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 75c686cd1551a4a19a0f19fc6f6510b5ed5aa699 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 1 Oct 2026 13:22:27 +0000 Subject: [PATCH 2/2] =?UTF-8?q?Far=20elder=20rate:=20status=20repair=20?= =?UTF-8?q?=E2=80=94=20#182=20is=20integrated=20(2a10ed3);=20no=20mathemat?= =?UTF-8?q?ical=20change?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Requested before integration in comment 5930668450: §0 called Math- #182 unmerged. It was integrated into main on 2026-09-30 at 2a10ed3 with the cited blob 0d401877. PROOF.md's status sentence and source-table row now say so; SOURCES.json moves [182] from cited_unmerged to cited_only (the workflow now verifies it from the tree) and refreshes the packet fingerprints. Theorem F, Lemma 1 and every proof step are unchanged; RESULTS.json is unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- frontiers/far_elder_rate_20260930/PROOF.md | 7 +++--- .../far_elder_rate_20260930/SOURCES.json | 23 ++++++++----------- 2 files changed, 14 insertions(+), 16 deletions(-) diff --git a/frontiers/far_elder_rate_20260930/PROOF.md b/frontiers/far_elder_rate_20260930/PROOF.md index 37dcf6ef9..072601145 100644 --- a/frontiers/far_elder_rate_20260930/PROOF.md +++ b/frontiers/far_elder_rate_20260930/PROOF.md @@ -44,8 +44,9 @@ lifetime `ℓ` is born at a maximum with λ_min(−D²f(M)) ≤ (ℓK²/c_L)^{1/3}. (1.3) -Lemma 1 is (8)–(9) of Math- #182 §3 (OpenAI, unmerged; accepted at Slice A by this author on 2026-09-30); its -five-line proof is repeated in §1 so that this note is self-contained and consumes nothing unmerged. +Lemma 1 is (8)–(9) of Math- #182 §3 (OpenAI; integrated into `main` on 2026-09-30 at `2a10ed3`, blob `0d401877`; +accepted at Slice A by this author on 2026-09-30); its five-line proof is repeated in §1 so that this note is +self-contained and consumes nothing unmerged. **Corollary F1 (far bars).** For every `t ∈ (0, 1]`, `E N_eld^{far,ρ}(0, t] ≤ (3/5)C t^{5/3}` per unit volume, and for every real `q > −5/3`, `E Σ_{far elder bars, ℓ_i ≤ t} ℓ_i^q ≤ C_q t^{q + 5/3}`. In particular the far elder @@ -197,7 +198,7 @@ eigenvalue, and it is what turns the barrier constraint `λ_1 ≲ ℓ^{1/3}` int | [Z] | `frontiers/c7_zero_gap_limit_20260929/PROOF.md` (`5b6328ea`) | cited only: (Z1) notation, Theorem Z, (Z11)–(Z12) as the `o(1)` predecessor. | | [U] | `frontiers/unrestricted_selection_difference_20260929/PROOF.md` (`5a55b179`) | cited only: (U1). | | [R] | `frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md` (`247b3ecf`) | cited only: §7 near/far decomposition, §8 moments. | -| [182] | Math- #182 `frontiers/fixed_r_inverse_lifetime_20260930/PROOF.md` (head `0f448f46`, blob `0d401877`) | cited only: §3 (8)–(9) is Lemma 1 and §§2, 4, 7 are the method (see §4); every step is re-proved here, nothing unmerged is consumed. | +| [182] | Math- #182 `frontiers/fixed_r_inverse_lifetime_20260930/PROOF.md` (integrated at `2a10ed3` on 2026-09-30; blob `0d401877`) | cited only: §3 (8)–(9) is Lemma 1 and §§2, 4, 7 are the method (see §4); every step is re-proved here, nothing unmerged is consumed. | ## 6. Finite controls diff --git a/frontiers/far_elder_rate_20260930/SOURCES.json b/frontiers/far_elder_rate_20260930/SOURCES.json index 950c54f88..1ff213481 100644 --- a/frontiers/far_elder_rate_20260930/SOURCES.json +++ b/frontiers/far_elder_rate_20260930/SOURCES.json @@ -15,7 +15,7 @@ "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", "tag": "P", - "use": "§1, §2, §3 (3.1), §4 (argument at fixed sites), §5 (5.2), §7 (spectral coordinates), §8, §9 as [E2], §14" + "use": "\u00a71, \u00a72, \u00a73 (3.1), \u00a74 (argument at fixed sites), \u00a75 (5.2), \u00a77 (spectral coordinates), \u00a78, \u00a79 as [E2], \u00a714" }, { "path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", @@ -23,7 +23,7 @@ "sha256": "845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f", "git_blob": "fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a", "tag": "E2", - "use": "§9.1-9.4" + "use": "\u00a79.1-9.4" }, { "path": "reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md", @@ -31,7 +31,7 @@ "sha256": "451b9d7ffee072a73fc904cab891b6693e3f233808b89df10cce1b57036b65da", "git_blob": "75da2597971510f843f8d90c743950cb8c177342", "tag": "REC", - "use": "§1 reading rule, §7 consumption contract" + "use": "\u00a71 reading rule, \u00a77 consumption contract" }, { "path": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", @@ -73,21 +73,18 @@ "sha256": "380b7d0abdb0fe2de5a6564565af9560d3f1b1ce22fd5538927db0c52f4f3a4a", "git_blob": "247b3ecf80bfbe896948d5d489b2d5842a81c481", "tag": "R", - "use": "§7 near/far decomposition, §8 moments" - } - ], - "cited_unmerged": [ + "use": "\u00a77 near/far decomposition, \u00a78 moments" + }, { "path": "frontiers/fixed_r_inverse_lifetime_20260930/PROOF.md", - "pr": "d6g8k5htny-coder/Math-#182", - "commit": "0f448f469d391dee5f8a35cfb04b7cfa7709f947", - "git_blob": "0d4018777d13672c1de1696525512e80b23b7c3c", "bytes": 17213, "sha256": "5adef725c1c696adae9bc73a525efe0bfe09d5c07e95ee3f067db9e877283630", + "git_blob": "0d4018777d13672c1de1696525512e80b23b7c3c", "tag": "182", - "use": "cited only: §3 (8)-(9) is Lemma 1 (re-proved here); §§2, 4, 7 are the method; nothing unmerged is consumed; not verified by the workflow" + "use": "cited only (integrated into main at 2a10ed3 on 2026-09-30; previously cited unmerged at commit 0f448f46 with the same blob): \u00a73 (8)-(9) is Lemma 1 (re-proved here); \u00a7\u00a72, 4, 7 are the method; nothing unmerged is consumed" } ], + "cited_unmerged": [], "referee": { "kind": "clean-context Anthropic Claude subagent before landing (same provider, same account; not a nonauthor review)", "findings": "no blocking; amendments applied: Corollary F2 framing (Theorem R unchanged), far rejected limit restricted to D_rho, method credit to #182 sections 2/4/7, heuristic in section 4 stated as an expectation, generic-locus qualification of (1.3), implicit steps in (3.3), SOURCES.json added, script docstrings and the vacuous closed-form check repaired" @@ -95,8 +92,8 @@ "files": [ { "path": "PROOF.md", - "bytes": 16413, - "sha256": "67f606327b66a2b4f1b8c67a57d119ac9ddfd2ce827ca8cb0c4daefa31904a3b" + "bytes": 16493, + "sha256": "ed908ed97348ed708c6fd06e5c09f6290ab0e8c47e6384b7bdded321452f523b" }, { "path": "far_elder_check.py",