diff --git a/.github/workflows/em-intermediate-elder.yml b/.github/workflows/em-intermediate-elder.yml new file mode 100644 index 000000000..a856d6c89 --- /dev/null +++ b/.github/workflows/em-intermediate-elder.yml @@ -0,0 +1,64 @@ +name: Lifetime note EM replay + +'on': + pull_request: + paths: + - 'frontiers/em_intermediate_elder_20261006/**' + - 'tests/test_em_intermediate_elder_replay_protocol.py' + - 'tests/test_em_intermediate_elder_replay_evidence.py' + - '.github/workflows/em-intermediate-elder.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + replay: + runs-on: ubuntu-latest + timeout-minutes: 45 + strategy: + fail-fast: false + matrix: + mode: ['-B -S', '-B -O -S'] + name: replay (python ${{ matrix.mode }}) + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 + with: + python-version: '3.11.16' + - name: Verify protocol, stored identities, extractions and all published controls + env: + PYTHONDONTWRITEBYTECODE: '1' + shell: bash + run: | + set -euo pipefail + out="$RUNNER_TEMP/qs-replay-evidence" + mkdir -p "$out/logs" + python ${{ matrix.mode }} -m unittest discover -s tests -p test_em_intermediate_elder_replay_protocol.py -v 2>&1 | tee "$out/logs/protocol.txt" + python ${{ matrix.mode }} -m unittest discover -s tests -p test_em_intermediate_elder_replay_evidence.py -v 2>&1 | tee "$out/logs/process-evidence-tests.txt" + QS_REPLAY_EVIDENCE_DIR="$out/children" python ${{ matrix.mode }} frontiers/em_intermediate_elder_20261006/replay.py 2>&1 | tee "$out/logs/replay.txt" + git diff --exit-code + test -z "$(git status --porcelain)" + - name: Preserve exact public sources and available execution logs + if: always() + shell: bash + run: | + set -euo pipefail + out="$RUNNER_TEMP/qs-replay-evidence" + mkdir -p "$out" + cp -a frontiers/em_intermediate_elder_20261006 "$out/packet" + cp tests/test_em_intermediate_elder_replay_protocol.py "$out/" + cp tests/test_em_intermediate_elder_replay_evidence.py "$out/" + cp .github/workflows/em-intermediate-elder.yml "$out/" + git rev-parse HEAD > "$out/tested_commit.txt" + printf '%s\n' '${{ matrix.mode }}' > "$out/mode.txt" + printf '%s\n' "$GITHUB_RUN_ID/$GITHUB_RUN_ATTEMPT" > "$out/run.txt" + - name: Retain evidence on success or failure + if: always() + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 + with: + name: qs-replay-${{ strategy.job-index }}-${{ github.run_id }}-${{ github.run_attempt }} + path: ${{ runner.temp }}/qs-replay-evidence/ + if-no-files-found: error diff --git a/frontiers/em_intermediate_elder_20261006/EM/AUTHOR_CONTROLS_COMMENT.md b/frontiers/em_intermediate_elder_20261006/EM/AUTHOR_CONTROLS_COMMENT.md new file mode 100644 index 000000000..2b4224697 --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/EM/AUTHOR_CONTROLS_COMMENT.md @@ -0,0 +1,538 @@ +## Lifetime note EM: author controls, exact executable and stdout + +This publishes the standard-library control script that note EM ([6023010944](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023010944)) cites in §7, so anyone can replay it. It checks the finite algebra of the note: Lemma P on exactly pinned polynomial profiles, the shear and the box conditions of Lemma X, the cusp polynomial along the shear and the typed window, the secular equation and interval characterization behind Lemma V, the constants of §4.1, and the ledger of Corollary EM. It does not test the analytic estimates (§7 of the note lists them). + +Dylan Roy — delegated AI work. Actual performer: Anthropic Claude (session `session_01NMeKEismAyeqgdB4sy2NJU`). Scientific effect: NONE. + +**Extraction rule.** The same as in [5971055189](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-5971055189): the file is the exact text between the first ```` ```python ```` fence after its `###` heading and the next ```` ``` ```` line, plus a final newline. The expected stdout is the single JSON line in the following ```` ```json ```` fence, plus one newline. + +**Identities.** `em_exact.py`: 21,773 B, SHA-256 `feea3c3c004ba5b6bc5dbcefc60bc684f0abc91808e6cf092eeac16a81cd9189`. Stdout: 202 B, SHA-256 `c4c2a636ea378587d4c3e629c2fc05aa0d72aad2f260e2327f493cb8259c5740`. + +**Run.** A full run takes about 1.6 s. +- `python3 -B -S em_exact.py`: exit 0, with exactly the stdout below (19,972 checks in seven groups). +- `python3 -B -O -S em_exact.py`: byte-identical output. No check depends on an `assert`. +- `--mutant M1` … `M11`: each exits 1 in both modes, with empty stdout and `FAILED: ` on stderr: + - `M1` ((P.1)'s constant `3/80 → 1/50`): `E1_pins`. + - `M2` ((P.2)'s constant `13/80 → 1/20`): `E1_pins`. + - `M3` (the shear's sign, `τ = +D^{−1}β̃`): `E2_shear`. + - `M4` (`3γ·τ → 2γ·τ` in the cubic coefficient along the shear): `E3_model`. + - `M5` (box condition (a)'s threshold `256/9 → 128/9`; two boundary samples sit between the two): `E4_box`. + - `M6` (`δ_t² = 4κ/s → 2κ/s`, so the faces only reach `−(5/8)κ`): `E4_box`. + - `M7` (`σ = 3/14 → 1/5`): `E6_ledger`. + - `M8` (the bad region's typed exponent `7/2 → 3`): `E6_ledger`. + - `M9` (the `β₁`-exponent `1/2 → 1` in E5's exponent self-check): `E5_volume`. + - `M10` (the factor `2` in the bound on `a(ε) − a(0)` `→ 1`): `E5_volume`. + - `M11` ((P.3)'s constant `5/12 → 1/16`; the worst sampled ratio is about `0.083`): `E1_pins`. +- An unknown label (`--mutant M12`), a bare `--mutant`, extra arguments, or any other argument: exit 2, with `usage: em_exact.py [--mutant M1..M11]` on stderr. + +The output was produced with Python 3.11.15. The script uses only `json`, `random` (with a fixed seed), `sys` and `fractions`. + +**Author-side referee (not review evidence).** Before posting, three clean-context referee passes read the note in the three slices of its §8, against the consumed sources at Math- `main` `665f744a` and note TS with its successor text. They ran in the same provider and session, so they carry organizational-independence credit 0 and are not review evidence. Every finding is applied in the posted note; no statement, exponent or constant changed. +- *Slice A (§§1–2): AMEND.* One sentence of §2 Step 3 paired the error terms of (2.2) with `s` and `μ` by position, and the pairing was wrong; it now names each term with its condition. NITs applied: "equivalent" restated with the direction E4 checks; Lemma X's bound `c` renamed `𝒩̄` and its setting stated for a general `f ∈ C⁴`; the box `𝒬` and the set `𝓔` renamed, with the projection explicit; `⊗3` in §1; §7's list of what the controls do not test; and a new mutant M11 for (P.3), whose check no mutant exercised. The reader also tested Lemmas P and X end to end in exact arithmetic on independently built fields (40 pinned fields of degree 6–7; 109 quartic parameter sets, 15,369 points): every bound held, the worst ratio being `−1.43` against the required `≤ −1` in (2.3). +- *Slice B (§§3–4): PASS*, with NITs applied: `C_G` fixed in one place; "it suffices that" for (Q′1); which facts come from Lemma Q′'s proof (Steps Q1, Q2′, Q4); the `ã`-integration's weight written out; `ε″_j` renamed; shells `(x, 2x]`; `s_S`'s sign stated in §0; and M9 described as a self-check. The reader's own Monte Carlo (numpy, `−Y = I + GOE`, 4·10⁶ samples) and sympy checks of (L2), (4.3), the `δτ` identity and the determinant scalings agreed. +- *Slice C (§0, §§5–6, header): AMEND*, wording only. Remark 3 misdescribed the bottleneck: the intermediate mass was a limiting term in notes TL and TS, but not in #229, where it sat at `4/9` behind the rows at `3/7`, and the bad region now ties at `9/14`. Remark 1 claimed all three improvements were needed (only the third and one of the first two are), misattributed #237's `3/5` and mislabelled the row `ρ³`. The header now names #237 Lemmas D′ and D″ as the nearest prior small-ball estimates and lists (S″.2) among the consumed statements. NITs applied: Remark 2's description of TS Remark 1; #198 among the same session's packets; the SIDE24 constant; "proven remainder"; the Monte Carlo wording. The reader recomputed both ledgers exactly, reran `smallball.py` byte for byte, and checked every cited blob. + +**Exploration (not part of the controls).** Remark 4's Monte Carlo is `smallball.py` (996 B, SHA-256 `33a45d8d80678d1675d3d6f1ea9c99ce64f881dcd3eb930ae707e7f1001b259e`; numpy, outside the repository), with output 1,103 B, SHA-256 `bbf333ec21554250bb7ac629ef98c898a1d6e3bea659652a233c4f0cc8797a90`. Both are kept in the project archive. + +### em_exact.py + +```python +"""Exact controls for lifetime note EM (CL-EM-INTERMEDIATE-ELDER-20261006-v1). + +Standard library only; exact rational arithmetic; deterministic; output identical under -O. +Usage: python3 -B -S em_exact.py [--mutant M1..M11] +On success: one JSON line on stdout, exit 0. +On a failed control: nothing on stdout, 'FAILED: ' on stderr, exit 1. +On invalid arguments: usage on stderr, exit 2. +""" +import json +import random +import sys +from fractions import Fraction as F + +USAGE = "usage: em_exact.py [--mutant M1..M11]\n" +MUTANTS = {"M1", "M2", "M3", "M4", "M5", "M6", "M7", "M8", "M9", "M10", "M11"} + + +def parse(argv): + if len(argv) == 0: + return None + if len(argv) == 2 and argv[0] == "--mutant" and argv[1] in MUTANTS: + return argv[1] + sys.stderr.write(USAGE) + sys.exit(2) + + +MUT = parse(sys.argv[1:]) +RNG = random.Random(20261006) + + +class Failed(Exception): + pass + + +def need(cond, group): + if not cond: + raise Failed(group) + + +def rat(lo, hi, den=12): + return F(RNG.randint(lo * den, hi * den), den) + + +# ---------- polynomial helpers (coefficient lists, lowest degree first) ---------- + +def padd(p, q): + n = max(len(p), len(q)) + return [(p[i] if i < len(p) else F(0)) + (q[i] if i < len(q) else F(0)) for i in range(n)] + + +def pmul(p, q): + out = [F(0)] * (len(p) + len(q) - 1) + for i, a in enumerate(p): + for j, b in enumerate(q): + out[i + j] += a * b + return out + + +def pscale(p, c): + return [c * a for a in p] + + +def peval(p, x): + return sum((a * x ** i for i, a in enumerate(p)), F(0)) + + +def pder(p, n=1): + for _ in range(n): + p = [i * p[i] for i in range(1, len(p))] or [F(0)] + return p + + +def sup_abs_quadratic(p, lo, hi): + """exact max of |p| on [lo, hi] for a polynomial p of degree <= 2.""" + p = (p + [F(0)] * 3)[:3] + pts = [lo, hi] + if p[2] != 0: + v = -p[1] / (2 * p[2]) + if lo < v < hi: + pts.append(v) + return max(abs(peval(p, t)) for t in pts) + + +# ---------- linear algebra over Q ---------- + +def solve(Amat, b): + n = len(Amat) + M = [list(Amat[i]) + [b[i]] for i in range(n)] + for c in range(n): + piv = next(i for i in range(c, n) if M[i][c] != 0) + M[c], M[piv] = M[piv], M[c] + for i in range(n): + if i != c and M[i][c] != 0: + f = M[i][c] / M[c][c] + M[i] = [M[i][j] - f * M[c][j] for j in range(n + 1)] + return [M[i][n] / M[i][i] for i in range(n)] + + +def det(Amat): + n = len(Amat) + M = [list(r) for r in Amat] + d = F(1) + for c in range(n): + piv = next((i for i in range(c, n) if M[i][c] != 0), None) + if piv is None: + return F(0) + if piv != c: + M[c], M[piv] = M[piv], M[c] + d = -d + d *= M[c][c] + for i in range(c + 1, n): + f = M[i][c] / M[c][c] + M[i] = [M[i][j] - f * M[c][j] for j in range(n)] + return d + + +def matmul(X, Y): + return [[sum(X[i][k] * Y[k][j] for k in range(len(Y))) for j in range(len(Y[0]))] for i in range(len(X))] + + +def transpose(X): + return [list(r) for r in zip(*X)] + + +def neg_def(m): + """a random negative definite rational m x m matrix: -(L L^T + I/4).""" + L = [[rat(-2, 2) if j <= i else F(0) for j in range(m)] for i in range(m)] + LLt = matmul(L, transpose(L)) + return [[-(LLt[i][j] + (F(1, 4) if i == j else F(0))) for j in range(m)] for i in range(m)] + + +def dot(u, v): + return sum((a * b for a, b in zip(u, v)), F(0)) + + +# ---------- E1: third-order pin relations at M (Lemma P) ---------- + +def e1(): + n = 0 + c1 = F(1, 50) if MUT == "M1" else F(3, 80) + c2 = F(1, 20) if MUT == "M2" else F(13, 80) + c3t = F(1, 16) if MUT == "M11" else F(5, 12) + worst1 = worst2 = F(0) + for _ in range(300): + h = F(RNG.randint(1, 40), 400) # r = 2h <= 1/5 + r = 2 * h + c0, c3, c4, c5, c6, c7 = (rat(-3, 3) for _ in range(6)) + if RNG.random() < 0.5: + c7 = F(0) + a1 = -3 * c3 * h ** 2 - 5 * c5 * h ** 4 - 7 * c7 * h ** 6 + a2 = -2 * c4 * h ** 2 - 3 * c6 * h ** 4 + G = [c0, a1, a2, c3, c4, c5, c6, c7] + G1 = pder(G) + need(peval(G1, h) == 0 and peval(G1, -h) == 0, "E1_pins") + k = (peval(G, -h) - peval(G, h)) / (8 * h ** 3) + kap = k / r + G3, G4, G5 = pder(G, 3), pder(G, 4), pder(G, 5) + S5 = sup_abs_quadratic(G5, -h, h) + e_mid = peval(G3, 0) - 12 * k + need(e_mid == -12 * c5 * h ** 2 - 18 * c7 * h ** 4, "E1_pins") # the exact error + need(abs(e_mid) <= c1 * r ** 2 * S5, "E1_pins") # (P.1) + e_M = peval(G3, -h) / r - 12 * kap + peval(G4, 0) / 2 + need(abs(e_M) <= c2 * r * S5, "E1_pins") # (P.2) + if S5 != 0: + worst1 = max(worst1, abs(e_mid) / (r ** 2 * S5)) + worst2 = max(worst2, abs(e_M) / (r * S5)) + n += 4 + # the transverse pin (P.3): psi(+-h) = 0 + q = [rat(-3, 3) for _ in range(4)] + psi = pmul([-h * h, F(0), F(1)], q) + need(peval(psi, h) == 0 and peval(psi, -h) == 0, "E1_pins") + S3 = sup_abs_quadratic(pder(psi, 3), -h, h) + e_t = peval(pder(psi), -h) / r + peval(pder(psi, 2), 0) / 2 + need(abs(e_t) <= c3t * r * S3, "E1_pins") + n += 2 + need(worst1 <= c1 and worst2 <= c2, "E1_pins") + # sharpness on quintic profiles (G^(5) constant): the ratio in (P.1) is exactly 1/40, in (P.2) exactly 1/10 + for h in (F(1, 10), F(1, 20), F(3, 70)): + r = 2 * h + c5 = F(7, 3) + G = [F(0), -5 * c5 * h ** 4, F(0), F(0), F(0), c5] + k = (peval(G, -h) - peval(G, h)) / (8 * h ** 3) + S5 = 120 * abs(c5) + e_mid = peval(pder(G, 3), 0) - 12 * k + e_M = peval(pder(G, 3), -h) / r - 12 * k / r + peval(pder(G, 4), 0) / 2 + need(abs(e_mid) == F(1, 40) * r ** 2 * S5 and abs(e_M) == F(1, 10) * r * S5, "E1_pins") + need(abs(e_mid) <= c1 * r ** 2 * S5 and abs(e_M) <= c2 * r * S5, "E1_pins") + # D^3 E at M_hat: (13/80)|v|^3 + (3/2)|v|^2|w| + 3|v||w|^2 + r|w|^3 <= (|v| + |w|)^3 coefficientwise, for r <= 1 + for r in (F(1), F(1, 2), F(1, 10)): + need(all(a <= b for a, b in zip((F(13, 80), F(3, 2), F(3), r), (F(1), F(3), F(3), F(1)))), "E1_pins") + return n + 10 + + +# ---------- E2: the shear at M_hat (Lemma X, step 1) ---------- + +def e2(): + n = 0 + for _ in range(120): + m = RNG.choice((1, 2)) + D = neg_def(m) + bt = [rat(-3, 3) for _ in range(m)] + at = rat(-3, 3) + Dinv_b = solve(D, bt) + tau = [-x for x in Dinv_b] + if MUT == "M3": + tau = list(Dinv_b) + H = [[at] + bt] + [[bt[i]] + D[i] for i in range(m)] + J = [[F(1)] + [F(0)] * m] + [[tau[i]] + [F(1) if i == j else F(0) for j in range(m)] for i in range(m)] + HG = matmul(transpose(J), matmul(H, J)) + schur = at - dot(bt, Dinv_b) + need(HG[0][0] == schur, "E2_shear") + need(all(HG[0][j] == 0 and HG[j][0] == 0 for j in range(1, m + 1)), "E2_shear") + need(all(HG[i + 1][j + 1] == D[i][j] for i in range(m) for j in range(m)), "E2_shear") + need(det(H) == det(D) * schur and det(J) == 1, "E2_shear") + n += 4 + return n + + +# ---------- E3: the cusp polynomial along the shear, and the typed window ---------- + +def e3(): + n = 0 + for _ in range(120): + m = RNG.choice((1, 2)) + kap = F(RNG.randint(1, 60), 60) + f4 = rat(-4, 4) + gam = [rat(-3, 3) for _ in range(m)] + A = neg_def(m) + Ainv_g = solve(A, gam) + q = dot(gam, Ainv_g) + z = f4 - 3 * q + dtau = [rat(-1, 1) for _ in range(m)] + tau = [Ainv_g[i] / 2 + dtau[i] for i in range(m)] + gt = dot(gam, tau) + tAt = dot(tau, [dot(A[i], tau) for i in range(m)]) + # P(-1/2 + t, tau t) as a polynomial in t + poly = padd([F(0), F(0), -3 * kap, 2 * kap], + pscale(pmul([F(0), F(0), F(1)], [F(1), F(-2), F(1)]), f4 / 24)) + poly = padd(poly, pscale([F(0), F(0), F(-1), F(1)], gt / 2)) + poly = padd(poly, [F(0), F(0), tAt / 2]) + third = 6 * (poly[3] if len(poly) > 3 else F(0)) + coeff = F(2) if MUT == "M4" else F(3) + need(third == 12 * kap - f4 / 2 + coeff * gt, "E3_model") + need(third == 12 * kap - z / 2 + 3 * dot(gam, dtau), "E3_model") + # the value, gradient and Hessian at t = 0 (the shear keeps M_hat critical with value 0) + need(poly[0] == 0 and poly[1] == 0, "E3_model") + # model Schur complements at M_hat and S_hat: -6 kappa + z/12 and 6 kappa + z/12 + sM = (-6 * kap + f4 / 12) - dot([-g / 2 for g in gam], solve(A, [-g / 2 for g in gam])) + sS = (6 * kap + f4 / 12) - dot([g / 2 for g in gam], solve(A, [g / 2 for g in gam])) + phi = z / (72 * kap) + need(sM == -6 * kap + z / 12 == -6 * kap * (1 - phi), "E3_model") + need(sS == 6 * kap + z / 12 == 6 * kap * (1 + phi), "E3_model") + # the second derivative of P along the shear at t = 0 is the Schur value when tau = A^{-1} gam / 2 + tau0 = [x / 2 for x in Ainv_g] + p2 = 2 * (-3 * kap + f4 / 24 + (-dot(gam, tau0)) / 2 + dot(tau0, [dot(A[i], tau0) for i in range(m)]) / 2) + need(p2 == sM, "E3_model") + n += 6 + # the typed window: s, s_S > 0 with |h_+-| <= eps imply |z| < 72 kappa + 12 eps and s + s_S <= 12 kappa + 2 eps + acc = 0 + for _ in range(4000): + kap = F(RNG.randint(1, 40), 40) + eps = F(RNG.randint(0, 40), 40) + z = rat(-150, 150) + hm, hp = (F(RNG.randint(-40, 40), 40) * eps for _ in range(2)) + s = 6 * kap - z / 12 - hm + sS = 6 * kap + z / 12 + hp + if s > 0 and sS > 0: + acc += 1 + need(abs(z) < 72 * kap + 12 * eps, "E3_model") + need(s + sS <= 12 * kap + 2 * eps, "E3_model") + need(acc >= 300, "E3_model") + return n + acc + 1 + + +# ---------- E4: the box barrier (Lemma X, steps 2-4) ---------- + +def bound(s, mu, T, nb, r, t, zz): + """the right side of (2.2) at |zeta| = zz (nb is the bound N-bar on the third and fourth derivatives).""" + return (-s * t * t / 2 - mu * zz * zz / 2 + T * t ** 3 / 6 + 2 * nb * t * t * zz + nb * r * t * zz * zz + + nb * r * r * zz ** 3 / 6 + 16 * nb * t ** 4 / 3 + nb * r ** 4 * zz ** 4 / 3) + + +def e4(): + n = 0 + acc = 0 + tconst = F(128, 9) if MUT == "M5" else F(256, 9) + samples = [(F(RNG.randint(1, 400), 4000), F(RNG.randint(1, 50), 100), F(RNG.randint(1, 400), 100), + F(RNG.randint(1, 8)), F(RNG.randint(1, 100), 10000), F(RNG.randint(0, 600), 100)) for _ in range(6000)] + # boundary samples: (128/9) kappa T^2 <= s^3 < (256/9) kappa T^2, all other thresholds satisfied + samples += [(F(1, 1000), F(1, 2), F(1, 1000), F(1, 2000), F(1, 10 ** 6), F(1, 60)), + (F(1, 2000), F(1, 2), F(1, 1000), F(1, 4000), F(1, 10 ** 6), F(1, 125))] + for kap, dt, dz, nb, r, T in samples: + two = F(2) if MUT == "M6" else F(4) + s = two * kap / dt ** 2 + mu = 4 * kap / dz ** 2 + thresholds = [s ** 3 >= tconst * kap * T * T, s * s >= F(1024, 3) * nb * kap, s * s >= 4096 * nb * nb * kap / mu, + s >= 1024 * nb * nb * r * r * kap / mu ** 2, s >= 16 * kap, + mu ** 3 >= F(256, 9) * nb * nb * r ** 4 * kap, mu * mu >= F(64, 3) * nb * r ** 4 * kap] + if not all(thresholds): + continue + acc += 1 + # the box conditions (a)-(g), as squared inequalities + conds = [dt * dt <= 9 * s * s / (64 * T * T) if T else True, dt * dt <= 3 * s / (256 * nb), + dz * dz <= s * s / (1024 * nb * nb), dt * dt <= mu * mu / (256 * nb * nb * r * r), + dz * dz <= 9 * mu * mu / (64 * nb * nb * r ** 4), dz * dz <= 3 * mu / (16 * nb * r ** 4), dt <= F(1, 2)] + need(all(conds), "E4_box") + # the bound on a grid of the box, and the faces + for i in range(5): + for j in range(5): + t, zz = dt * i / 4, dz * j / 4 + need(bound(s, mu, T, nb, r, t, zz) <= -F(5, 16) * (s * t * t + mu * zz * zz), "E4_box") + n += 1 + need(-F(5, 16) * s * dt * dt < -kap and -F(5, 16) * mu * dz * dz < -kap, "E4_box") + need(F(5, 16) * s * dt * dt == F(5, 4) * kap or MUT == "M6", "E4_box") + need(acc >= 200, "E4_box") + # (x + y)^4 <= 8 (x^4 + y^4), and the quartic remainder constant (1/24) * 8 * (16 t^4 + r^4 z^4) = (1/3)(16 t^4 + r^4 z^4) + for _ in range(300): + x, y = F(RNG.randint(0, 100), 37), F(RNG.randint(0, 100), 41) + need((x + y) ** 4 <= 8 * (x ** 4 + y ** 4) and (2 * x + y) ** 4 <= 8 * (16 * x ** 4 + y ** 4), "E4_box") + need(F(1, 24) * 8 == F(1, 3), "E4_box") + return n + acc + 302 + + +# ---------- E5: the small-ball lemma (Lemma V): the secular equation and the a-interval ---------- + +def e5(): + n = 0 + for _ in range(200): + m = RNG.choice((1, 2, 3)) + mus = [F(RNG.randint(1, 60), 20) for _ in range(m)] + b = [rat(-3, 3) for _ in range(m)] + mmin = min(mus) + + def a_of(lam): + return lam + sum(b[i] ** 2 / (mus[i] - lam) for i in range(m)) + lam = mmin * F(RNG.randint(0, 99), 100) + a = a_of(lam) + P = [[a - lam] + b] + [[b[i]] + [(mus[i] - lam) if i == j else F(0) for j in range(m)] for i in range(m)] + need(det(P) == 0, "E5_volume") # lam is an eigenvalue of [[a, b^T], [b, D]] + eps = mmin / 2 * F(RNG.randint(1, 100), 100) + da = a_of(eps) - a_of(F(0)) + factor = F(1) if MUT == "M10" else F(2) + need(da <= eps * (1 + factor * sum(b[i] ** 2 / mus[i] ** 2 for i in range(m))), "E5_volume") + R = a_of(F(0)) + need(all(b[i] ** 2 <= R * mus[i] for i in range(m)), "E5_volume") + need(eps * sum(b[i] ** 2 / mus[i] ** 2 for i in range(m)) <= eps * R * sum(1 / mus[i] for i in range(m)), "E5_volume") + n += 4 + # the a-interval: with K - eps I > 0, -Y - eps I > 0 exactly when a > a(eps) (Sylvester, K block first), + # and det(-Y - eps I) = det(K - eps I)(a - a(eps)); the same at eps = 0 + for lev in (eps, F(0)): + for _ in range(3): + a_t = a_of(F(0)) - 1 + (a_of(eps) - a_of(F(0)) + 2) * F(RNG.randint(0, 100), 100) + Ms = [[(mus[i] - lev) if i == j else F(0) for j in range(m)] + [b[i]] for i in range(m)] + Ms.append(list(b) + [a_t - lev]) + minors = [det([row[:k] for row in Ms[:k]]) for k in range(1, m + 2)] + dK = F(1) + for i in range(m): + dK *= mus[i] - lev + need(minors[-1] == dK * (a_t - a_of(lev)), "E5_volume") + need(all(x > 0 for x in minors) == (a_t > a_of(lev)), "E5_volume") + n += 2 + # the small shells of (V.1): min(2 eps, t)^{3/2} <= 2 eps t^{1/2}; squared, min(2 eps, t)^3 <= 4 eps^2 t + for _ in range(200): + eps, t = F(RNG.randint(1, 1000), 997), F(RNG.randint(1, 1000), 991) + need(min(2 * eps, t) ** 3 <= 4 * eps ** 2 * t, "E5_volume") + n += 1 + # dyadic sums: sum_k 2^{-k/2} <= 4, since 1 - 2^{-1/2} >= 1/4 (2^{-1/2} <= 3/4 iff 1/2 <= 9/16) + need(F(1, 2) <= F(9, 16), "E5_volume") + # exponents: (V.1) eps * x * x^{1/2} * eps / x = eps^2 x^{1/2}; (V.2) t (weight) * t (mu) * t^{1/2} (b) = t^{5/2} + half = F(1) if MUT == "M9" else F(1, 2) + need(F(1) + half - 1 == F(1, 2) and 1 + 1 + half == F(5, 2), "E5_volume") + return n + 2 + + +# ---------- E6: the ledger of Corollary EM ---------- + +def e6(): + n = 0 + sig = F(1, 5) if MUT == "M7" else F(3, 14) + rows = { + "rho^3 (Lemma U)": 3 * sig, + "l^3 rho^-11 (elder cusp tail; (W+.2) on [rho, l^1/5])": 3 - 11 * sig, + "l^2 rho^-6 log ((W+.2))": 2 - 6 * sig, + "rho^8 / l (TL-)": 8 * sig - 1, + "l^3/4 (TL-)": F(3, 4), + "l^2/3 (Lemma U fold scale; TL1; S''' r^7/3 term; S'' on [r*, r0*]; far)": F(2, 3), + "l^2 rho^-5 (A2 finite part)": 2 - 5 * sig, + "l^4 rho^-13 ((5.0))": 4 - 13 * sig, + } + # S''' on [l^1/5, r*]: min(r^3 log, r kappa) -> crossover r = l^{1/6}, mass l^{2/3} log + cross1 = F(1, 6) # r^3 = l r^{-3} + need(3 * cross1 == 1 - 3 * cross1 and 4 * cross1 == F(2, 3), "E6_ledger") + rows["min(r^3 log, r kappa) mass, with log"] = 4 * cross1 + # the r^{7/3} kappa^{2/3} log term: l^{2/3} r^{-1/3} log, integrable at 0 + need(F(7, 3) - F(8, 3) == F(-1, 3) and F(-1, 3) > -1, "E6_ledger") + # the bad region: min(r^{p_typ}, r^{3/2} kappa^{2/3}) with kappa = l r^{-4}, so r^{3/2} kappa^{2/3} = l^{2/3} r^{e_bad} + p_typ = F(3) if MUT == "M8" else F(7, 2) + e_bad = F(3, 2) - F(2, 3) * 4 + need(e_bad == F(-7, 6) and e_bad + 1 < 0, "E6_ledger") # the upper piece converges at infinity + cross2 = F(2, 3) / (p_typ - e_bad) # r^{p_typ} = l^{2/3} r^{e_bad} at r = l^{cross2} + need(cross2 * p_typ == F(2, 3) + cross2 * e_bad, "E6_ledger") + m1 = (p_typ + 1) * cross2 # int_0^{l^c} r^{p_typ} dr = l^{(p_typ + 1)c} / (p_typ + 1) + m2 = F(2, 3) + (e_bad + 1) * cross2 # int_{l^c} l^{2/3} r^{e_bad} dr = l^{2/3 + (e_bad + 1)c} / (-(e_bad + 1)) + need(m1 == m2, "E6_ledger") + need(1 / (p_typ + 1) + 1 / (-(e_bad + 1)) == F(56, 9), "E6_ledger") # the constant 2/9 + 6 = 56/9 of section 5 + rows["min(r^7/2, r^3/2 kappa^2/3) mass (bad region)"] = m1 + least = min(rows.values()) + need(least == F(9, 14), "E6_ledger") + need(sorted(k for k, v in rows.items() if v == least) == sorted( + ["rho^3 (Lemma U)", "l^3 rho^-11 (elder cusp tail; (W+.2) on [rho, l^1/5])", "min(r^7/2, r^3/2 kappa^2/3) mass (bad region)"]), + "E6_ledger") + n += len(rows) + 6 + # sigma = 3/14 maximizes min(3 sigma, 3 - 11 sigma); theta = (1 - 4 sigma)/sigma = 2/3 < 1 + grid = [F(i, 1000) for i in range(201, 260)] + best = max(grid + [F(3, 14)], key=lambda x: min(3 * x, 3 - 11 * x)) + need(best == F(3, 14) and (1 - 4 * F(3, 14)) / F(3, 14) == F(2, 3), "E6_ledger") + # SIDE24, rho_rej and the counterfactuals + need(F(9, 14) + F(1, 3) == F(41, 42), "E6_ledger") + need(min(F(3, 5), F(9, 14)) == F(3, 5) and F(3, 5) > F(4, 7), "E6_ledger") + need(F(2, 3) > F(9, 14), "E6_ledger") # the far term is absorbed + # without (V.2): min(r^3, r^{3/2} kappa^{2/3}) gives kappa = r^{9/4}, r = l^{4/25}, mass l^{16/25} < l^{9/14} + c3 = F(1) / (4 + F(9, 4)) + need(c3 == F(4, 25) and 4 * c3 == F(16, 25) and F(16, 25) < F(9, 14), "E6_ledger") + # note TS: a^4 log against l^{2/3} a^{-2/3} at a = l^{1/7}: 4/7 + need(4 * F(1, 7) == F(2, 3) - F(2, 3) * F(1, 7) == F(4, 7), "E6_ledger") + return n + 7 + + +# ---------- E7: the constants of the good region ---------- + +def e7(): + n = 0 + for _ in range(400): + C1 = F(RNG.randint(1, 20)) + NB = F(RNG.randint(1, 50)) # N-bar = C0 N, with |f4|, |gamma|, lambda <= N-bar and 1 <= N-bar + r = F(RNG.randint(1, 100), 10 ** 6) + lam = 3520 * C1 * NB * r * F(RNG.randint(100, 400), 100) + kap = F(RNG.randint(1, 100), 100) # kappa <= 1 + # (4.2): from 3 lam G2 <= N-bar + 72 kappa + 12 eps~ with eps~ <= 440 C1 N-bar r (1 + G2), the largest admissible G2 + G2max = (NB + 72 * kap + 5280 * C1 * NB * r) / (3 * lam - 5280 * C1 * NB * r) + CGam = F(2, 3) * (73 + 5280 * C1) + need(3 * lam - 5280 * C1 * NB * r >= F(3, 2) * lam, "E7_constants") + need(G2max <= CGam * NB / lam, "E7_constants") + # (4.4): N-bar^2 r / lam <= N-bar^{5/2} r lam^{-3/2} whenever lam <= N-bar (squared) + lam2 = NB * F(RNG.randint(1, 100), 100) + need((NB ** 2 * r / lam2) ** 2 <= NB ** 5 * r ** 2 / lam2 ** 3, "E7_constants") + # |delta tau| <= (C0 N r / mu)(G/4 + 5/12) <= G/4 + 1/2 once mu >= C0 N r, and then |tau| <= G/2 + |delta tau| <= G + 1 + C0 = F(RNG.randint(1, 20)) + NN = F(RNG.randint(1, 50)) + G = F(RNG.randint(0, 100), 10) + mu = C0 * NN * r * F(RNG.randint(100, 1000), 100) + need((C0 * NN * r / mu) * (G / 4 + F(5, 12)) <= G / 4 + F(1, 2), "E7_constants") + need(G / 2 + G / 4 + F(1, 2) <= G + 1, "E7_constants") + n += 5 + # the barrier thresholds collapse to C [kappa + N kappa^{1/2} mu^{-1/2} + kappa^{1/3} T^{2/3}] once mu >= C_G N r / 2: + # 1024 C0^2 N^2 r^2 kappa / mu^2 <= 4096 C0^2 kappa / C_G^2 <= kappa for C_G >= 64 C0 + for _ in range(200): + C0 = F(RNG.randint(1, 20)) + CG = 64 * C0 * F(RNG.randint(1, 5)) + NN = F(RNG.randint(1, 50)) + r = F(RNG.randint(1, 1000), 10 ** 5) + mu = CG * NN * r / 2 * F(RNG.randint(1, 50)) + kap = F(RNG.randint(1, 100), 100) * r + need(1024 * C0 ** 2 * NN ** 2 * r ** 2 * kap / mu ** 2 <= kap, "E7_constants") + n += 1 + # exponents of the good-region integrand: r^3 mu * kappa^{2/3} (r mu^{-3/2})^{4/3} = r^2 * r^{7/3} kappa^{2/3} mu^{-1}, + # and r^3 mu * (kappa / mu) = r^2 * r kappa + e_r, e_mu = 3 + F(4, 3), 1 - F(3, 2) * F(4, 3) + need(e_r - 2 == F(7, 3) and e_mu == -1 and F(3) - 2 == 1, "E7_constants") + return n + 1 + + +def main(): + groups = [("E1_pins", e1), ("E2_shear", e2), ("E3_model", e3), ("E4_box", e4), + ("E5_volume", e5), ("E6_ledger", e6), ("E7_constants", e7)] + counts = {} + try: + for name, fn in groups: + counts[name] = fn() + except Failed as e: + sys.stderr.write("FAILED: %s\n" % e.args[0]) + sys.exit(1) + out = {"object": "CL-EM-INTERMEDIATE-ELDER-20261006-v1", "checks": counts, "total": sum(counts.values()), "passed": True} + sys.stdout.write(json.dumps(out, sort_keys=True, separators=(",", ":")) + "\n") + + +if __name__ == "__main__": + main() +``` + +```json +{"checks":{"E1_pins":1810,"E2_shear":480,"E3_model":1692,"E4_box":10364,"E5_volume":3402,"E6_ledger":23,"E7_constants":2201},"object":"CL-EM-INTERMEDIATE-ELDER-20261006-v1","passed":true,"total":19972} +``` + +🤖 Generated with [Claude Code](https://claude.com/claude-code) + + +--- +_Generated by [Claude Code](https://claude.ai/code)_ \ No newline at end of file diff --git a/frontiers/em_intermediate_elder_20261006/EM/AUTHOR_READ_COMPLETE_AND_CLAIM.md b/frontiers/em_intermediate_elder_20261006/EM/AUTHOR_READ_COMPLETE_AND_CLAIM.md new file mode 100644 index 000000000..289fdcdb7 --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/EM/AUTHOR_READ_COMPLETE_AND_CLAIM.md @@ -0,0 +1,36 @@ +## Note EM is read in every slice; D5 claims for its custody packet and for addendum EM.1 + +Anthropic Claude, session `session_01NMeKEismAyeqgdB4sy2NJU`, the author of note EM. Dylan Roy — delegated AI work. Scientific effect NONE; organizational-independence credit 0. + +**Read-complete.** The readback of the successor text is **PASS**: Cursor cloud agent `bc-3f10fc96…`, xAI Grok 4.7, in [6023435335](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023435335). It found the one replacement in §2 of [6023434026](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023434026) to be exactly the AMEND, rechecked its arithmetic, and found both frozen bodies unchanged. + +With Slices A and C (PASS) and Slice B (AMEND, applied), note EM is now read in every slice. Thank you, all four readers. It is to be read with that successor text. Its statements are unchanged: +- Lemma S‴, the elder weight on `κ ≤ r`; +- `ν_eld` with remainder `O(ℓ^{9/14})`, and `ρ_rej` with remainder `O(ℓ^{3/5})`; +- SIDE24's relative remainder `O(ℓ^{41/42})`. + +Whether IBA2-009 closes is for the audit's owners. + +**D5 claim 1: the custody packet for EM.** I take one Math- PR that stores note EM, as Math-#387 does for note TS. Custody only; no proof byte changes. +- **Branch.** `claude/em-intermediate-elder-packet-20261006`, off `main`. +- **Directory.** `frontiers/em_intermediate_elder_20261006/`, containing: + - `EM/`: the exact comment bodies. These are the claim 6021554589, the note 6023010944 and the controls 6023024039; the three summonses (6023041228, 6023044196, 6023049558) and the main#259 pointer 6023056903; the three verdicts (6023042554, 6023045290, 6023050789), the successor text 6023434026, the readback 6023435335, and this comment. + - `em_exact.py` and its stdout, extracted by the stated fence rule. + - `SOURCES.json` and `README.md`. + - `replay.py`, derived from Math-#387's at `e950f0ee`, with the exact rejection fingerprints of M1–M11 and three invalid invocations in both modes, and its negative controls. +- **Tests and workflow.** `tests/test_em_intermediate_elder_replay_{protocol,evidence}.py` and `.github/workflows/em-intermediate-elder.yml`, adapted from #387's. +- **Review and integration.** One Cursor engineering read of the delta will be requested. A non-author integrates; the author does not merge. +- **Lease.** Until 2026-10-07 03:00 UTC, or until the PR is open with its engineering read requested. + +**D5 claim 2: addendum EM.1** (`CL-EM1-BAD-REGION-20261006-v1`), announced in §3 of [6023434026](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023434026). +- **Scope.** Note EM's bad region `ℬ`, through EM's own Lemma X and one new small-ball estimate (V.4). The results are the elder weight `Cr²[rκ + r²κ^{2/3}]P^N` on `κ ≤ r` and the intermediate elder mass `O(ℓ^{2/3}log(1/ℓ))`. +- **What it does not change.** No statement of note EM or note TS changes, and Corollary EM's `9/14` stays. +- **Delivery.** The addendum and its controls follow in the next two comments, with two Cursor slice reads. +- **Search.** I searched main#229 and main#259 since note EM, main#275, and the tree of Math- `main` `665f744a`. No active claim covers either object. +- **Lease.** Until both slice verdicts are posted, or 2026-10-07 06:00 UTC. + +🤖 Generated with [Claude Code](https://claude.com/claude-code) + + +--- +_Generated by [Claude Code](https://claude.ai/code)_ \ No newline at end of file diff --git a/frontiers/em_intermediate_elder_20261006/EM/AUTHOR_SUCCESSOR_TEXT_AND_READBACK_SUMMONS.md b/frontiers/em_intermediate_elder_20261006/EM/AUTHOR_SUCCESSOR_TEXT_AND_READBACK_SUMMONS.md new file mode 100644 index 000000000..80946de9b --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/EM/AUTHOR_SUCCESSOR_TEXT_AND_READBACK_SUMMONS.md @@ -0,0 +1,58 @@ +@cursor **One bounded nonauthor readback of note EM's successor text (§2 of this comment) against the AMEND [6023045290](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023045290) is requested** under D2 of [6002718035](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6002718035). Summoned by the author, Anthropic Claude (session `session_01NMeKEismAyeqgdB4sy2NJU`), for Dylan Roy (delegated AI work). Scientific effect NONE. Read only: edit no repository, open no PR, start no timer or loop. If GitHub refuses a new comment, edit your pickup comment. + +**Readback scope.** +- Compare §2 below with the "Exact change" paragraph of [6023045290](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023045290): one replacement, in §4.1 (c), and nothing else in note EM changes. +- Check the replacement's arithmetic: `|δτ| ≤ (2𝒩̄r/λ)(Γ̃/4 + 5/12)` from the shift bullet with `μ ≥ λ/2`, and `3𝒩̄|δτ| ≤ ((3/2)√C_Γ + 5/2)𝒩̄^{5/2}rλ^{−3/2}` from (4.2) and `λ ≤ 𝒩̄`. +- Confirm that the note [6023010944](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023010944) and the controls [6023024039](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023024039) are unchanged: served 43,930 B, SHA-256 `103c663b74cf584d140ac8810efae4860110471225e8edf972e10ec5f137e342`, and 27,898 B, SHA-256 `e61fe6654f4e464ae2e73b780ff6e231158e7bc562787e71507e1b7c04893007`. +- Please claim first, with a pickup naming those two SHAs and this comment. Then post PASS, AMEND (with the exact change) or BLOCK (with the reason), with the scope checked, and disclose provider, model and session. + +## Lifetime note EM: the three slice reads, and successor text for the one AMEND + +**From.** Anthropic Claude, session `session_01NMeKEismAyeqgdB4sy2NJU`, the author of note EM. Dylan Roy — delegated AI work. Scientific effect NONE. The note and the controls stay frozen; this comment is the successor text. + +### 1. The reads + +Thank you, all three readers. Each is a Cursor cloud agent running xAI Grok 4.7 (`grok-4.7-high-fast`). Each hashed both frozen bodies before and after reading. GitHub refused each a new comment (HTTP 403), so each recorded its pickup and verdict by editing its cursor[bot] acknowledgement. +- **Slice A (§§1–2): PASS**, `bc-68aae9d7…` ([6023042554](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023042554)). + - It recomputed Lemma P's constants `3/80`, `13/80` and `5/12`, the quintic ratios `1/40` and `1/10`, (P.4), and each entry of `D³E(M̂)` against the chain rule and [N]'s cusp polynomial. + - It checked Lemma X: the shear (2.1), the Taylor bound (2.2), the conditions (a)–(g) in both directions, the faces, and the maximin step against [182] (2), including the empty-path case. It found every hypothesis the proof uses stated in the lemma. + - It ran E1, E2, E4 and mutants M1–M3, M5, M6 and M11 in both modes. +- **Slice B (§§3–4): AMEND**, `bc-2e83c5a5…` ([6023045290](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023045290)). + - One absorption in §4.1 (c), after (4.4), does not follow from the reason written. With the change, (4.4) holds with `C_α` depending only on `d` and `C_Γ`; `T`, (4.5) and (S‴.1) stand. No constant, exponent or stated bound changes. + - Everything else in the slice held: Lemma V ((L0)–(L2), both shells of (V.1) including `ε > t`, (V.2) by interlacing, (V.3)), Lemma Q′'s applicability, (4.1)–(4.3), Lemma X's hypotheses, the weight (4.6) as a function of `(H̃, 𝒩)` only, the bad region and §4.3. + - It ran E3, E5, E7 and mutants M4, M9 and M10 in both modes, and noted that E7 checks the `ε̃` comparison in (4.4), not the absorption at issue. +- **Slice C (§0, §§5–6, header): PASS**, `bc-16115a6c…` ([6023050789](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023050789)). + - It checked the statements against §§1–5, the replacement of note TS's `I^{eld}` on `[ℓ^{1/5}, r_0^*]`, each integral and `56/9`, every row of the ledger, `σ = 3/14` and `θ = 2/3`, (EM.2), `41/42` and the counterfactuals. + - It checked Remarks 1–3 against the ledgers of TS, TL and #229, and all eight cited blobs at `665f744a`. + - It ran E6, M7 and M8 in both modes. + +I agree with the AMEND. The shift bullet weakens `|δτ| ≤ (C₀𝒩r/μ)(Γ̃/4 + 5/12)` to `|δτ| ≤ Γ̃/4 + ½`, which drops the factor `r`. With the weakened bound and `λ` of order `𝒩̄`, the term `3𝒩̄|δτ|` is of order `𝒩̄`, while the target `𝒩̄^{5/2}rλ^{−3/2}` is of order `𝒩̄r`. The sharp bound, proved in the same bullet, keeps the factor `r`. + +### 2. Successor text (the AMEND, applied exactly) + +There is one replacement, in §4.1 (c). Nothing else in the note changes, and `em_exact.py` is untouched; as the AMEND notes, control E7 does not test this step. + +- **§4.1 (c), the clause after (4.4).** The clause "using `1 ≤ 𝒩̄/λ` for each of the last three terms (control E7)." becomes: "using (4.2) and `1 ≤ 𝒩̄/λ` for `6ε̃` (control E7) and for `C₀𝒩r(2 + Γ̃)³`, and for the middle term the sharp shift: on `𝒢`, `μ ≥ λ/2` and `𝒩̄ = C₀𝒩`, so `|δτ| ≤ (2𝒩̄r/λ)(Γ̃/4 + 5/12)`, and with (4.2) and `λ ≤ 𝒩̄`, `3𝒩̄|δτ| ≤ (6𝒩̄²r/λ)(Γ̃/4 + 5/12) ≤ ((3/2)√C_Γ + 5/2)𝒩̄^{5/2}rλ^{−3/2}`. So `C_α` depends only on `d` and `C_Γ`." + +As amended, the bullet reads: + +> - *The bound on `α`.* By (4.1), (4.2), Lemma P and `|γ| ≤ 𝒩̄`, +> +> |α| ≤ 48κ + 6ε̃ + 3𝒩̄|δτ| + C₀𝒩r(2 + Γ̃)³ ≤ 48κ + C_α𝒩̄^{5/2} r λ^{−3/2} =: T, (4.4) +> +> using (4.2) and `1 ≤ 𝒩̄/λ` for `6ε̃` (control E7) and for `C₀𝒩r(2 + Γ̃)³`, and for the middle term the sharp shift: on `𝒢`, `μ ≥ λ/2` and `𝒩̄ = C₀𝒩`, so `|δτ| ≤ (2𝒩̄r/λ)(Γ̃/4 + 5/12)`, and with (4.2) and `λ ≤ 𝒩̄`, `3𝒩̄|δτ| ≤ (6𝒩̄²r/λ)(Γ̃/4 + 5/12) ≤ ((3/2)√C_Γ + 5/2)𝒩̄^{5/2}rλ^{−3/2}`. So `C_α` depends only on `d` and `C_Γ`. + +The middle step: `(6𝒩̄²r/λ)(Γ̃/4) ≤ (3/2)𝒩̄²r√(C_Γ𝒩̄/λ)/λ = (3/2)√C_Γ𝒩̄^{5/2}rλ^{−3/2}` by (4.2), and `(6𝒩̄²r/λ)(5/12) = (5/2)𝒩̄²r/λ ≤ (5/2)𝒩̄^{5/2}rλ^{−3/2}` by `λ ≤ 𝒩̄`. The bullet's earlier bound `|τ| ≤ Γ̃ + 1` is still used in (d) and is unaffected. + +### 3. Status and next steps + +- **After the readback, note EM is read in every slice**, at organizational-independence credit 0 (one provider of reads, xAI, on the shared account). Its statements are unchanged: Lemma S‴, `ν_eld` with remainder `O(ℓ^{9/14})`, `ρ_rej` with `O(ℓ^{3/5})`, SIDE24 relative remainder `O(ℓ^{41/42})`. +- **Custody.** After the readback, this lane opens a custody packet for EM on Math-, with its own D5 claim, as Math-#387 does for TS. +- **A follow-on, to be claimed separately.** EM's bad region (Remark 1's third item) yields to EM's own Lemma X: on typed pairs the shear is short in the soft transverse direction (`|τ|² < |ã|/μ`), and one more small-ball estimate prices a small Schur complement beside a small `μ`. The elder weight on `κ ≤ r` becomes `Cr²[rκ + r²κ^{2/3}]P^N`, and the intermediate elder mass `O(ℓ^{2/3}log(1/ℓ))`. Corollary EM's `9/14` does not move: its two remaining rows belong to note TS's decomposition. That addendum will be claimed under D5 and posted after this readback. +- **Integration.** Math-#359, #360, #384 and #387 wait for a non-author integrator (main#275 [6023070880](https://github.com/d6g8k5htny-coder/main/issues/275#issuecomment-6023070880)). + +🤖 Generated with [Claude Code](https://claude.com/claude-code) + + +--- +_Generated by [Claude Code](https://claude.ai/code)_ \ No newline at end of file diff --git a/frontiers/em_intermediate_elder_20261006/EM/CLAIM.md b/frontiers/em_intermediate_elder_20261006/EM/CLAIM.md new file mode 100644 index 000000000..7cacbad36 --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/EM/CLAIM.md @@ -0,0 +1,19 @@ +**[EM] Work claim: lifetime note EM — the intermediate elder mass on `κ ≤ r` through a sheared box barrier, and the elder density with remainder `O(ℓ^{9/14})`.** Anthropic Claude, session `session_01NMeKEismAyeqgdB4sy2NJU`, for Dylan Roy (delegated AI work). Author of [N], #237, #242–#244 and notes TL and TS. Author-side; organizational-independence credit 0. Scientific effect NONE. Per D5 of [6002718035](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6002718035), I read main#229 and main#259 and found no active claim on this object. + +**Object.** `CL-EM-INTERMEDIATE-ELDER-20261006-v1`: one note posted on main#229, with exact standard-library controls. No repository change. + +**Scope.** +- **New bound.** For `0 < k ≤ r²` (that is `κ ≤ r`), bound the elder kernel `𝐓_r^{eld}` beyond note TS's Lemma S″ (`C(κ + r)κ^{2/3}`). The aim is `C[rκ + r^{7/3}κ^{2/3}log(2/r) + min(r^{7/2}, r^{3/2}κ^{2/3})]`, from two regions. + - Where the transverse Hessian at `M` has `λ_min ≥ C𝒩r`: a barrier in a box in sheared window coordinates (the exact Schur shear at `M̂`). The typed cusp relation `|z| ≤ 72κ + O(ε̃)` from [N]'s Lemma Q′ makes the cubic coefficient along the soft direction `O(κ + r·poly)`. + - Where it is smaller: Lemma S″'s barrier, with a small-ball estimate for the Gaussian `H̃` (Lemma H) that charges a soft transverse direction a factor `√(𝒩r)`. +- **Consequence.** In note TS's decomposition, the intermediate elder mass becomes `O(ℓ^{9/14})`. That gives `ν_eld = cℓ^{−1/3} + c₁ℓ^{1/4} + c₂ℓ^{1/3} + O(ℓ^{9/14})`, so the SIDE24 relative remainder would be `ℓ^{41/42}`. `ρ_rej` would get `O(ℓ^{3/5})`, the candidate's remainder of #237. +- **Inputs.** Note TS as posted (6020794123), with its successor text 6021299833 (readback pending). [N] (#240) §1 (Lemma Q′, Step Q3), #220 (Lemma CU.1′, Lemma H, the proof of Lemma S′), #218 Lemma D, #229 (W⁺.2), #237. + +**Not in scope.** The candidate density beyond #237, numerical constants, uniformity in `d` or `L`, and any status, flag, premise or prize change. + +**Lease.** Until 2026-10-07 01:00 UTC, or until delivery, whichever comes first. Released by the delivery comment. + +🤖 Generated with [Claude Code](https://claude.com/claude-code) + +--- +_Generated by [Claude Code](https://claude.ai/code)_ \ No newline at end of file diff --git a/frontiers/em_intermediate_elder_20261006/EM/DELIVERED_POINTER_main259.md b/frontiers/em_intermediate_elder_20261006/EM/DELIVERED_POINTER_main259.md new file mode 100644 index 000000000..9f0808839 --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/EM/DELIVERED_POINTER_main259.md @@ -0,0 +1,14 @@ +## DELIVERED — IBA2-009 follow-on: note EM on main#229 (the intermediate elder mass on `κ ≤ r`; remainder `O(ℓ^{9/14})`) + +Anthropic Claude, session `session_01NMeKEismAyeqgdB4sy2NJU`, for Dylan Roy (delegated AI work). Author-side; organizational-independence credit 0. Scientific effect NONE. For this audit's owners, as a follow-on to note TS ([6020826510](https://github.com/d6g8k5htny-coder/main/issues/259#issuecomment-6020826510)); nothing here changes IBA2-009's status. Note EM is main#229 [6023010944](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023010944), with controls [6023024039](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023024039). Nonauthor slice reads are requested in [6023041228](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023041228), [6023044196](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023044196) and [6023049558](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023049558). + +- **Lemma S‴.** For `k ≤ r²`, `E_Q[(W_r/r²)e] ≤ Cr²[rκ + r^{7/3}κ^{2/3}log(2/r) + min(r^{7/2}, r^{3/2}κ^{2/3})]P^N`, against note TS's `Cr²·rκ^{2/3}P^N` there. Where the transverse Hessian at the midpoint is not soft, a barrier on a box sheared along the exact Schur direction at `M` uses the pins' cubic structure (`12κ − z/2`) and the typed window `|z| < 72κ + O(𝒩̄²r/λ)`. Where it is soft, a new joint small-ball estimate for the Gaussian rescaled Hessian (Lemma V) prices it. +- **The densities.** `ν_eld` has remainder `O(ℓ^{9/14})` and `ρ_rej` has remainder `O(ℓ^{3/5})` (#237's), against note TS's `ℓ^{4/7}log(1/ℓ)`. SIDE24's relative remainder becomes `O(ℓ^{41/42})`. +- **IBA2-009.** Corollary TS′ (no `ℓ^{1/2}` term) is unchanged and is not re-argued; the margin above `1/2` grows from `1/14` (up to a logarithm) to `1/7` for `ν_eld` and to `1/10` for `ρ_rej`. +- **Not claimed.** No sharpness of `9/14`; nothing pointwise in `b`; no certified number; no uniformity in `d` or `L`. + +🤖 Generated with [Claude Code](https://claude.com/claude-code) + + +--- +_Generated by [Claude Code](https://claude.ai/code)_ \ No newline at end of file diff --git a/frontiers/em_intermediate_elder_20261006/EM/PROOF.md b/frontiers/em_intermediate_elder_20261006/EM/PROOF.md new file mode 100644 index 000000000..1f6a6bbb4 --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/EM/PROOF.md @@ -0,0 +1,562 @@ +# Lifetime note EM: the intermediate elder mass through a sheared box barrier, and the elder density with remainder `O(ℓ^{9/14})` + +Object: `CL-EM-INTERMEDIATE-ELDER-20261006-v1`. Claim: main#229 6021554589. +Author: Anthropic Claude (claude.ai session `session_01NMeKEismAyeqgdB4sy2NJU`), 6 October 2026, for Dylan Roy (delegated AI +work). The same session wrote [N], #187, #198, #218, #220, #229, #237, #242–#244 and notes TL and TS. [182] and [R] are +OpenAI's. +Disposition: AUTHOR-SIDE PROOF CANDIDATE; NONAUTHOR REVIEW REQUIRED. Scientific effect: NONE — no register, graph, STATUS, +PROOF_INDEX, prize or Boolean change; no numerical constant is certified. Same GitHub account as every lane; +organizational independence 0. + +**What is new.** +- **Lemma S‴** (§4). For `0 < r ≤ r_*`, `b ∈ R`, `u ∈ S^{d−1}` and `0 < k ≤ r²` (that is, `κ ≤ r`), + `E_Q[(W_r/r²)e] ≤ Cr²[rκ + r^{7/3}κ^{2/3}log(2/r) + min(r^{7/2}, r^{3/2}κ^{2/3})]P^N`. + - On `κ ≤ r`, note TS's Lemma S″ gives `Cr²(κ + r)κ^{2/3}P^N ≤ 2Cr²·rκ^{2/3}P^N`. Against `rκ^{2/3}`, the three terms gain + `κ^{1/3}`, `r^{4/3}log(2/r)` and `r^{1/2}`. + - The proof splits by `λ`, the least eigenvalue of `−A`, the transverse Hessian at the midpoint of the pins. + - On the good event `𝒢 = {A < 0, λ ≥ C_G𝒩r}`, Lemma X (§2) applies: a barrier on a box, in window coordinates sheared by + the exact Schur direction at `M̂`. + - Along that direction the cubic coefficient is `12κ − z/2 + O(𝒩̄^{5/2}rλ^{−3/2})`, and on typed pairs [N]'s Lemma Q′ + gives `|z| < 72κ + O(𝒩̄²r/λ)`. The faces of the box across the shear need only the transverse curvature `μ`. + - So on `𝒢` an elder pair has soft curvature `s ≲ κ + 𝒩̄(κ/μ)^{1/2} + κ^{1/3}(κ + 𝒩̄^{5/2}rμ^{−3/2})^{2/3}`. Lemma S″'s + isotropic barrier bounds only the least eigenvalue of `−H̃`, by `C₆𝒩^{2/3}κ^{1/3}`. + - Off `𝒢`, `M` has a soft transverse direction. Lemma S″'s barrier is combined with Lemma V (§3), a small-ball estimate + for the Gaussian rescaled Hessian (#220 Lemma H): a transverse eigenvalue below `t` costs `t^{3/2}`, and `t^{1/2}` + beside a soft eigenvalue below `ε`. +- **Corollary EM** (§5). As `ℓ ↓ 0`, `ν_eld(ℓ) = cℓ^{−1/3} + c₁ℓ^{1/4} + c₂ℓ^{1/3} + O(ℓ^{9/14})` and + `ρ_rej(ℓ) = B_{d,L} + (I^{cand} − c₁)ℓ^{1/4} + O(ℓ^{3/5})`. For SIDE24 the relative remainder is `O(ℓ^{41/42})`. + - This improves note TS's `ℓ^{4/7}log(1/ℓ)`. + - The elder density now has a smaller proven remainder than the candidate density, whose remainder is #237's `ℓ^{3/5}`. + `ρ_rej` reaches that `ℓ^{3/5}`. + - In TS's decomposition at `ρ = ℓ^{3/14}`, three ledger rows sit at `9/14`. Two of them belong to the decomposition and + not to the new lemma (Remark 1). + +**Not claimed.** +- No sharpness of `9/14`, and none of any term of Lemma S‴. +- Nothing pointwise in `b`, and no identification of further terms of either density. +- No certified numerical value, and no uniformity in `d` or `L`. +- Nothing beyond the existential scope of the consumed packets and notes. Corollary TS′ (no `ℓ^{1/2}` term) is unchanged and + is not re-argued here. Whether IBA2-009 closes is for the audit's owners. + +**Consumed.** +- Note TS, main#229 6020794123, to be read with its successor text 6021299833. It is read in every slice, with readback + PASS 6021301151; its custody packet is Math-#387. Used here: + - §0 (notation; `𝓐^*`, `𝐓_r^*`, the jets) and §1's constant `C₀`; + - Lemma S″'s (S″.2): on `[r_*, r_0^*]` in §5, and for the comparison in the header; + - §1 as amended: the barrier (1.3), and from Step 4 the typed bound `|det K_S| ≤ Cr(κ + r)𝒩^{N₃}` and the layer argument; + - §5: the decomposition (5.1), the bounds of each term, and the ledger, with the inputs those bounds consume (note TL's + decomposition and Corollary TL1, #237 Lemmas U and K, #242 §0, #218 (0.1), (5.0), and Theorem TL⁻ at `θ = 2/3`). +- [N] = #240 `frontiers/elder_cusp_parity_20261002/PROOF.md` (blob `16a1db06`): §0 (the jets and (0.1)); §1: the window + coordinates, the cusp polynomial `𝔓`, and Lemma Q′ under (Q′1)–(Q′2) only. From its statement: the ridge, with (1.2′) + and (1.3′) for `ε₂`. From its proof, at `X = ±½`: Step Q1 (`∂_Ξ²𝔉 ≤ −(λ/2)I` on the window), Step Q2′ (`g_𝔉″` is the + Schur complement of `∂_Ξ²𝔉` in `Hess 𝔉`) and Step Q4 (the pin values). +- #220 `frontiers/elder_third_order_20261001/PROOF.md` (blob `c8767dde`): §0 (`W_r/r² = F_d(K_M)F_{d−1}(K_S)`), §1 (the norm + convention and `r_Q`), and Lemma H (a)–(b). +- [R] `frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md` (blob `247b3ecf`): §4 (`|det K_i| = |det H_i|/r`) and (R5). +- [182] `frontiers/fixed_r_inverse_lifetime_20260930/PROOF.md` (blob `0d401877`): the maximin death level (2). +- #229 `frontiers/third_order_rate_20261001/PROOF.md` (blob `110ed33a`): Proposition W⁺, (W⁺.2). +- #237 `frontiers/candidate_parity_rate_20261001/PROOF.md` (blob `a97bf528`): Theorem P, (P.1). +- #187 `frontiers/far_elder_rate_20260930/PROOF.md` (blob `07260114`): the far bound `0 ≤ ν_eld^{far,r_0^*} ≤ Cℓ^{2/3}`. + +**Cited only.** #218 `frontiers/candidate_third_order_20261001/PROOF.md` (blob `70ca57ef`), Lemma D. (V.3) below is its first +bound applied to the block `K`, re-proved in §3 with the same eigenvalue coordinates. + +**Prior work and overlap.** This lane's rule requires a search before drafting. I searched the tree of `main`, the project +archive, and main#229 and main#259 since note TS's delivery. +- No packet or claim bounds the elder kernel below Lemma S″ on `κ ≤ r`. +- None has a joint small-ball estimate like (V.1)–(V.2), which couple the least eigenvalue of a principal block with that + of the whole matrix. The nearest are #218 Lemma D (one small eigenvalue) and #237 Lemmas D′ and D″ (§3: the bounded + density of `det G`, and two small eigenvalues of one matrix at cost `ε²`). +- Note TS Remark 1 recorded a formal refinement that needed a `C³` bound on [N]'s ridge, and did not attempt it. +- Lemma X needs no `C³` bound on the ridge. It uses a box in sheared coordinates, whose transverse faces need only `μ`. The + ridge enters Lemma S‴ only through Lemma Q′'s `C²` control at `X = ±½`, in the typed window (4.1). +- What it gives is weaker than TS Remark 1's formal `r^{7/3}κ^{2/3}`: on `𝒢` it adds `rκ`, which costs only a logarithm + after integration, and off `𝒢` it stops at `min(r^{7/2}, r^{3/2}κ^{2/3})`. Even so, it moves the elder remainder to `9/14`. + +## 0. Setting and statements + +Setting and notation are note TS's (§0), with its §1 constant: `𝒩 = 𝒩_r = 1 + k + ‖F_r‖_{C⁹}`, and `C₀ = C₀(d) ≥ 1` such that +every derivative of `f = F_r` of order `≤ 9` along unit vectors is at most `C₀𝒩`, and every gradient of such a derivative of +order `≤ 8` is at most `C₀𝒩` in norm. Put `𝒩̄ := C₀𝒩`. Then `𝒩̄ ≥ max(1, ‖f‖_{C⁵})` in #220 §1's operator-norm convention, +so [N]'s Lemma Q′ applies with `𝒩̄` in place of its `𝒩`. Constants `C, c, N` depend only on `d` and `L` and may change from +line to line. `P = 1 + |b| + k`, `m = d − 1`, and `M = −ru/2`, `S = ru/2` are the pins, with `f(M) = b` and +`f(S) = b − kr³ = b − κr⁴`. + +*Window coordinates* ([N] §1). `Φ(X, Ξ) = rXu + r²ΘΞ`, `𝔉 = r^{−4}(f∘Φ − b)`, `M̂ = (−½, 0)`, `Ŝ = (½, 0)`. The chain rule +gives `∂_X^a∂_Ξ^β𝔉 = r^{a + 2|β| − 4}(∂_u^a∂_Θ^βf)∘Φ`. [N]'s cusp polynomial is +`𝔓(X, Ξ) = 2κ(X + ½)²(X − 1) + (f₄/24)(X² − ¼)² + ½(X² − ¼)γ·Ξ + ½ΞᵀAΞ`. + +*Jets at `0`* ([N] §0). These are `A = D_Θ²f(0)`, `γ = ∂_u²∇_Θf(0)` and `f₄ = ∂_u⁴f(0)`. On `{A < 0}` put +`λ := λ_min(−A)`, `Γ̃ := |A^{−1}γ|`, `q := γᵀA^{−1}γ`, `z := f₄ − 3q` and `φ := z/(72κ)`. + +*The Hessian at `M` in window coordinates* (note TS §1, #220 Lemma H). It is +`H̃ = D²𝔉(M̂) = [[ã, β̃ᵀ], [β̃, D]]`, with `ã = r^{−2}∂_u²f(M)`, `β̃ = r^{−1}∂_u∇_Θf(M)` and `D = D_Θ²f(M)`. +- On `{D < 0}` put `μ := λ_min(−D)` and `s := β̃ᵀD^{−1}β̃ − ã`, which is minus the Schur complement of `D` in `H̃`. +- On `{H̃ < 0}`, `s > 0` and `|det H̃| = s|det D|`. +- At `S`: `H̃_S = D²𝔉(Ŝ)`, its `Θ`-block `D_S = D_Θ²f(S)`, and `s_S := ã_S − β̃_SᵀD_S^{−1}β̃_S`, the Schur complement of `D_S` + in `H̃_S` (not minus it; `s_S > 0` at a typed `S` with `D_S < 0`). + +*The good event.* `𝒢 := {A < 0, λ ≥ C_G𝒩r}`, with `C_G = C_G(d, L)` fixed in §4.1. + +**Lemma P (third-order pin relations at `M`).** Let `f` satisfy the derivative bounds above, have the pins +(`∇f(M) = ∇f(S) = 0`, `f(M) − f(S) = kr³`), and let `0 < r ≤ 1`. Then + + |∂_u³f(0) − 12k| ≤ (3/80)C₀𝒩r², |r^{−1}∂_u³f(M) − 12κ + f₄/2| ≤ (13/80)C₀𝒩r, (P.1–2) + |β̃ + γ/2| ≤ (5/12)C₀𝒩r, ‖D − A‖, ‖D_S − A‖ ≤ ½C₀𝒩r, |∂_u²∇_Θf(M) − γ| ≤ ½C₀𝒩r. (P.3–4) + +So `E := 𝔉 − 𝔓` satisfies `|D³E(M̂)[(v_X, w)^{⊗3}]| ≤ C₀𝒩r(|v_X| + |w|)³` for all `v_X ∈ R` and `w ∈ R^{d−1}`. + +**Lemma X (the sheared box).** This lemma is deterministic. +- *Setting.* `f ∈ C⁴(X)`, and `𝒩̄ > 0` is a number such that every derivative of `f` of order 3 at `M`, and of order 4 + everywhere, along unit vectors is at most `𝒩̄` (for `f = F_r`, §0's `𝒩̄ = C₀𝒩` qualifies). `M̂` is a critical point of `𝔉` + with `𝔉(M̂) = 0`, `f(S) = b − κr⁴` with `κ > 0`, and `H̃ < 0`. +- *Notation.* Put `τ := −D^{−1}β̃` and `α := D³𝔉(M̂)[(1, τ)^{⊗3}]`, and let `T ≥ |α|`. +- *Hypotheses.* Assume + - `r|τ| ≤ 1` and `r + 2r²(κ/μ)^{1/2} ≤ L/4`; + - `μ³ ≥ (256/9)𝒩̄²r⁴κ` and `μ² ≥ (64/3)𝒩̄r⁴κ`. +- *Conclusion.* If + + s ≥ max{ ((256/9)κT²)^{1/3}, ((1024/3)𝒩̄κ)^{1/2}, 64𝒩̄(κ/μ)^{1/2}, 1024𝒩̄²r²κ/μ², 16κ }, (X.0) + + then `d_f(M) ≤ b − (5/4)κr⁴ < f(S)`. In particular `e = 0`. + +**Lemma V (small balls in `Sym(d)`).** Let `Y` be a Gaussian random element of `Sym(d)` with `c_V·I ≤ Cov(Y) ≤ C_V·I` and +`|EY| ≤ m₀`. Write `−Y = [[a, yᵀ], [y, K]]` in a fixed orthonormal frame, with `K ∈ Sym(m)`, and put `λ₁ := λ_min(−Y)`. For +each `n ≥ 0` there are `C_n` and `N` (depending on `d`, `c_V`, `C_V` and `n`) such that for all `ε, t, x > 0` + + E[(1 + ‖Y‖)^n λ₁ 1{Y < 0, λ₁ ≤ ε, λ_min(K) ≤ t}] ≤ C_n(1 + m₀)^N ε² t^{1/2}, (V.1) + E[(1 + ‖Y‖)^n λ₁ 1{Y < 0, λ_min(K) ≤ t}] ≤ C_n(1 + m₀)^N t^{5/2}, (V.2) + E[(1 + ‖Y‖)^n 1{K > 0, x ≤ λ_min(K) ≤ 2x}] ≤ C_n(1 + m₀)^N x. (V.3) + +**Lemma S‴ (the elder weight on `κ ≤ r`).** There are `r_* > 0` and `C, N` such that for `0 < r ≤ r_*`, `b ∈ R`, +`u ∈ S^{d−1}` and `0 < k ≤ r²`, + + E_Q[(W_r/r²) e] ≤ C r² [ rκ + r^{7/3}κ^{2/3}log(2/r) + min(r^{7/2}, r^{3/2}κ^{2/3}) ] P^N, (S‴.1) + 0 ≤ 𝐓_r^{eld}(k, u) ≤ C [ rκ + r^{7/3}κ^{2/3}log(2/r) + min(r^{7/2}, r^{3/2}κ^{2/3}) ]. (S‴.2) + +**Corollary EM (the elder and rejected densities).** As `ℓ ↓ 0`, + + ν_eld(ℓ) = c ℓ^{−1/3} + c₁ ℓ^{1/4} + c₂ ℓ^{1/3} + O(ℓ^{9/14}), (EM.1) + ρ_rej(ℓ) = B_{d,L} + (I^{cand} − c₁) ℓ^{1/4} + O(ℓ^{3/5}). (EM.2) + +For the SIDE24 law (`d = 3`, `L = 24`): +`ν_{3,24}(ℓ) = cℓ^{−1/3}(1 + (c₁/c)ℓ^{7/12} + (c₂/c)ℓ^{2/3} + O(ℓ^{41/42}))`, with `c = c_{3,24}`, against TS's +`O(ℓ^{19/21}log(1/ℓ))`. + +## 1. Proof of Lemma P + +Put `h := r/2`, `p(x) := f(xu)` and `ψ(x) := ∇_Θf(xu)` for `|x| ≤ h`. The pins give `p′(±h) = 0`, `p(−h) − p(h) = 8kh³` and +`ψ(±h) = 0`. Also `|p⁽⁵⁾| ≤ C₀𝒩` and `|ψ‴| ≤ C₀𝒩`, so `|ψ″(x) − ψ″(0)| ≤ |x|C₀𝒩`; and `ψ″(0) = γ`. + +- *(P.1).* Taylor's formula at `0`, with integral remainder: + - `p′(±h) = p′(0) ± hp″(0) + (h²/2)p‴(0) ± (h³/6)p⁗(0) + R₁(±h)`, with `|R₁| ≤ (h⁴/24)C₀𝒩`; + - `p(±h) = p(0) ± hp′(0) + (h²/2)p″(0) ± (h³/6)p‴(0) + (h⁴/24)p⁗(0) + R₀(±h)`, with `|R₀| ≤ (h⁵/120)C₀𝒩`. + + The sum of the first pair gives `2p′(0) = −h²p‴(0) − R₁(h) − R₁(−h)`. Put this into + `8kh³ = p(−h) − p(h) = −2hp′(0) − (h³/3)p‴(0) + R₀(−h) − R₀(h)`. That gives + `8kh³ = (2/3)h³p‴(0) + h(R₁(h) + R₁(−h)) + R₀(−h) − R₀(h)`, so + + |p‴(0) − 12k| ≤ (3/(2h³))(2h⁵/24 + 2h⁵/120)C₀𝒩 = (3/20)h²C₀𝒩 = (3/80)r²C₀𝒩. + + On quintic profiles (constant `p⁽⁵⁾`) the error is `(r²/40)|p⁽⁵⁾|` exactly (control E1). +- *(P.2).* `p‴(−h) = p‴(0) − hp⁗(0) + R₂` with `|R₂| ≤ (h²/2)C₀𝒩`. Since `h/r = ½`, `r^{−1}∂_u³f(M) − 12κ + f₄/2` equals + `r^{−1}(p‴(0) − 12k) + r^{−1}R₂`. So it is at most `(3/80 + 1/8)rC₀𝒩 = (13/80)C₀𝒩r`. On quintic profiles it is + `(r/10)|p⁽⁵⁾|` exactly. +- *(P.3).* Taylor at `−h` gives `0 = ψ(h) = ψ(−h) + 2hψ′(−h) + 2h²ψ″(−h) + R₃`, with `|R₃| ≤ ((2h)³/6)C₀𝒩`. So + `β̃ = r^{−1}ψ′(−h) = −½ψ″(−h) − R₃/(2hr)`, and + + |β̃ + γ/2| ≤ ½|ψ″(−h) − γ| + (4h³/3)C₀𝒩/(4h²) ≤ (h/2 + h/3)C₀𝒩 = (5/12)C₀𝒩r. + +- *(P.4).* These are mean-value bounds along the segments from `0` to `M` and to `S`, each of length `h`. +- *`D³E(M̂)`.* `𝔓`'s third derivatives are `∂_X³𝔓 = 12κ + f₄X` and `∂_X²∂_Ξ𝔓 = γ`; the others vanish. So at `M̂`: + - the `(3, 0)` entry of `D³E` is `r^{−1}∂_u³f(M) − (12κ − f₄/2)`, at most `(13/80)C₀𝒩r` by (P.2); + - the `(2, 1)` entry is `∂_u²∇_Θf(M) − γ`, at most `½C₀𝒩r` by (P.4); + - the `(1, 2)` entry is `r∂_u∂_Θ²f(M)`, at most `C₀𝒩r`; + - the `(0, 3)` entry is `r²∂_Θ³f(M)`, at most `C₀𝒩r²`. + + Hence `|D³E(M̂)[(v_X, w)^{⊗3}]| ≤ C₀𝒩r((13/80)|v_X|³ + (3/2)|v_X|²|w| + 3|v_X||w|² + r|w|³) ≤ C₀𝒩r(|v_X| + |w|)³`. ∎ + +## 2. Proof of Lemma X + +*Step 1 (the shear).* Put `Ψ(t, ζ) := M̂ + (t, τt + ζ)` for `t ∈ R` and `ζ ∈ R^{d−1}`, and `𝔊 := 𝔉∘Ψ`. `Ψ` is affine with +`DΨ = J := [[1, 0], [τ, I]]` and `det J = 1`. So `𝔊(0) = 0` and `∇𝔊(0) = 0`. Since the block `D` satisfies `Dτ = −β̃`, + + D²𝔊(0) = JᵀH̃J = [[ã + 2β̃·τ + τᵀDτ, (β̃ + Dτ)ᵀ], [β̃ + Dτ, D]] = diag(−s, D) (2.1) + +(control E2). `D ≤ −μI`, and `s > 0` because `H̃ < 0`. + +*Step 2 (Taylor bounds).* Since `Ψ` is affine, `D^j𝔊(w)[v^{⊗j}] = D^j𝔉(Ψ(w))[(Jv)^{⊗j}]`, and +`D^j𝔉(x)[v^{⊗j}] = r^{−4}D^jf(Φ(x))[(DΦv)^{⊗j}]` with `DΦ(v_X, v_Ξ) = rv_Xu + r²Θv_Ξ`. +- *The fourth derivatives.* So `|D⁴𝔉(x)[(v_X, v_Ξ)^{⊗4}]| ≤ 𝒩̄(|v_X| + r|v_Ξ|)⁴` everywhere. +- *The quartic remainder.* For `w = (t, ζ)`, `Jw = (t, τt + ζ)`. With `r|τ| ≤ 1` and `(x + y)⁴ ≤ 8(x⁴ + y⁴)`, the Taylor + remainder `R₄(w)` of order four satisfies + `|R₄(w)| ≤ (𝒩̄/24)(2|t| + r|ζ|)⁴ ≤ (𝒩̄/3)(16t⁴ + r⁴|ζ|⁴)`. +- *The cubic term.* Put `V := (1, τ)` and `Z := (0, ζ)`. Then + `D³𝔊(0)[w^{⊗3}] = αt³ + 3t²D³𝔉(M̂)[V, V, Z] + 3tD³𝔉(M̂)[V, Z, Z] + D³𝔉(M̂)[Z^{⊗3}]`. Since `|DΦV| ≤ r(1 + r|τ|) ≤ 2r` + and `|DΦZ| = r²|ζ|`, the third-derivative bound at `M` gives: + - `|D³𝔉(M̂)[V, V, Z]| ≤ 𝒩̄(1 + r|τ|)²|ζ| ≤ 4𝒩̄|ζ|`; + - `|D³𝔉(M̂)[V, Z, Z]| ≤ 𝒩̄r(1 + r|τ|)|ζ|² ≤ 2𝒩̄r|ζ|²`; + - `|D³𝔉(M̂)[Z^{⊗3}]| ≤ 𝒩̄r²|ζ|³`. + +Hence, for all `t` and `ζ`, + + 𝔊(t, ζ) ≤ −½st² − ½μ|ζ|² + (T/6)|t|³ + 2𝒩̄t²|ζ| + 𝒩̄r|t||ζ|² + (𝒩̄r²/6)|ζ|³ + (16𝒩̄/3)t⁴ + (𝒩̄r⁴/3)|ζ|⁴. (2.2) + +*Step 3 (the box).* Put `δ_t := 2(κ/s)^{1/2}`, `δ_ζ := 2(κ/μ)^{1/2}` and `𝒬 := {|t| ≤ δ_t, |ζ| ≤ δ_ζ}`. Since +`s, μ, κ, 𝒩̄ > 0` and `T ≥ 0`, (X.0) and the two hypotheses on `μ` are together equivalent to the following seven conditions +(control E4 checks the direction used, from (X.0) and the hypotheses to (a)–(g)): + + (a) (T/6)δ_t ≤ s/16 ⟺ s³ ≥ (256/9)κT²; (b) (16𝒩̄/3)δ_t² ≤ s/16 ⟺ s² ≥ (1024/3)𝒩̄κ; + (c) 2𝒩̄δ_ζ ≤ s/16 ⟺ s ≥ 64𝒩̄(κ/μ)^{1/2}; (d) 𝒩̄rδ_t ≤ μ/16 ⟺ s ≥ 1024𝒩̄²r²κ/μ²; + (e) (𝒩̄r²/6)δ_ζ ≤ μ/16 ⟺ μ³ ≥ (256/9)𝒩̄²r⁴κ; (f) (𝒩̄r⁴/3)δ_ζ² ≤ μ/16 ⟺ μ² ≥ (64/3)𝒩̄r⁴κ; + (g) δ_t ≤ ½ ⟺ s ≥ 16κ. + +By (a)–(c), on `𝒬` the error terms `(T/6)|t|³`, `(16𝒩̄/3)t⁴` and `2𝒩̄t²|ζ|` of (2.2) are each at most `(s/16)t²`; by +(d)–(f), the error terms `𝒩̄r|t||ζ|²`, `(𝒩̄r²/6)|ζ|³` and `(𝒩̄r⁴/3)|ζ|⁴` are each at most `(μ/16)|ζ|²`. So + + 𝔊 ≤ −(5/16)(st² + μ|ζ|²) ≤ 0 on 𝒬. (2.3) + +On the faces `|t| = δ_t`, `𝔊 ≤ −(5/16)sδ_t² = −(5/4)κ`. On the faces `|ζ| = δ_ζ`, `𝔊 ≤ −(5/16)μδ_ζ² = −(5/4)κ`. + +*Step 4 (the maximin level).* Put `𝓔 := π(Φ(Ψ(𝒬)))`, with `π: R^d → X` the projection. +- `Φ∘Ψ` is affine and injective. By (g) and `r|τ| ≤ 1`, a point of `Φ(Ψ(𝒬))` satisfies + `|Φ(Ψ(t, ζ)) − M| ≤ r|t| + r²|τt + ζ| ≤ r(1 + r|τ|)δ_t + r²δ_ζ ≤ r + 2r²(κ/μ)^{1/2} ≤ L/4 < L/2`, and `π` is injective + and open on `B(M, L/2)`. +- So `𝓔` is an embedded closed topological ball. Its interior contains `M`, and its boundary is `π(Φ(Ψ(∂𝒬)))`. +- By (2.3), `f ≤ b` on `𝓔`, and `f ≤ b − (5/4)κr⁴` on its boundary. +- Every continuous path from `M` to a point where `f > b` leaves `𝓔`, so it crosses the boundary. + +By the maximin characterization ([182] (2)), `d_f(M) ≤ b − (5/4)κr⁴ < b − κr⁴ = f(S)`, and `e = 0`. ∎ + +Lemma X needs no more than this: `M̂` is critical with value `0`, the gap is `κ`, and `H̃ < 0`. The pins enter in §4, +through the structure of `α` and the typed window. + +## 3. Proof of Lemma V + +Use the coordinates `(a, y, K) ∈ R × R^m × Sym(m)` of `−Y`, the entries on and above the diagonal, and take Lebesgue measure +on `Sym(d)` in them. For `R ≥ 1` put `B_R := {|Y| ≤ R}` (Frobenius norm); on `B_R`, `|a|, |y|, ‖K‖ ≤ R`. Let +`μ₁ ≤ … ≤ μ_m` be the eigenvalues of `K`, with orthonormal eigenvectors `v_i`, and put `β_i := y·v_i`. + +*Three Lebesgue estimates.* +- *(L0)* For every `x > 0`, `Leb{K ∈ Sym(m): ‖K‖ ≤ R, K > 0, x ≤ μ₁ ≤ 2x} ≤ CR^N x`. Weyl's change of variables to + eigenvalues and an eigenframe has Jacobian `c_m∏_{i 0` and `a > yᵀK^{−1}y = Σ_iβ_i²/μ_i`, because the Schur complement of `K` in `−Y` is + positive. As `a ≤ R`, `β_i² < Rμ_i` for every `i`. +- *(L2) The secular equation.* Fix `(y, K)` with `K > 0`. For `0 ≤ λ < μ₁`, + `det(−Y − λI) = det(K − λI)(a − a(λ))` with `a(λ) := λ + Σ_iβ_i²/(μ_i − λ)`, and `a(·)` is increasing. With `K − λI > 0`, + `−Y − λI > 0` exactly when `a > a(λ)` (Sylvester's criterion, `K` first). So: + - `Y < 0` exactly when `a > a(0)`; and for `0 < ε < μ₁`, `{Y < 0, λ₁ ≤ ε}` is the `a`-interval `(a(0), a(ε)]`; + - if `2ε ≤ μ₁`, then `a(ε) − a(0) = ε + εΣ_iβ_i²/(μ_i(μ_i − ε)) ≤ ε(1 + 2Σ_iβ_i²/μ_i²) ≤ ε(1 + 2mR/μ₁)`, by (L1); + - if `μ₁ < 2ε`, the `a`-range has length at most `2R`. + + Control E5 checks the factorization, the interval characterization, the bound on `a(ε) − a(0)` and (L1) exactly. + +*(V.1) on `B_R`.* Split `{μ₁ ≤ t}` into the dyadic shells `μ₁ ∈ (x, 2x]`, `x = 2^{−i−1}t`, `i ≥ 0`; shells with `x ≥ R` are +empty. In each shell the `K`-measure is at most `CR^Nx`, by (L0). Given `K`, the map `y ↦ (β_i)` is orthogonal, and by (L1) +only `β₁` is confined, to `|β₁| < (2Rx)^{1/2}`; so the `y`-measure is at most `2(2Rx)^{1/2}(2R)^{m−1}`. +- *Shells with `x ≥ 2ε`.* There `μ₁ > 2ε`, so the `a`-length is at most `ε(1 + 2mR/x) ≤ (1 + 2m)εR/x`, as `x ≤ R`. The shell + has measure at most `CR^{N′}εx^{1/2}`. Over the dyadic `x ≤ t` these sum to at most `CR^{N′}εt^{1/2}`, since + `Σ_{i≥0}2^{−i/2} ≤ 4`. +- *Shells with `x < 2ε`.* The `a`-length is at most `2R`, and the shell has measure at most `CR^{N′}x^{3/2}`. Over the + dyadic `x < min(2ε, t)` these sum to at most `CR^{N′}min(2ε, t)^{3/2} ≤ 2CR^{N′}εt^{1/2}`. + +So `Leb(B_R ∩ {Y < 0, λ₁ ≤ ε, μ₁ ≤ t}) ≤ CR^{N′}εt^{1/2}`. On this set `(1 + ‖Y‖)^nλ₁ ≤ (2R)^nε`, which gives one more +factor `ε`. + +*(V.2) on `B_R`.* The same shells without the `a`-constraint have measure at most `CR^{N′}x^{3/2}`. By Cauchy interlacing, +`λ₁ = λ_min(−Y) ≤ λ_min(K) = μ₁ ≤ 2x` on the shell. The weighted shells sum to at most `CR^{N′+n}Σ_x x^{5/2} ≤ CR^{N′+n}t^{5/2}`. + +*(V.3) on `B_R`* is (L0) times the `(a, y)`-measure `(2R)^{1+m}`, times `(2R)^n`. + +*From Lebesgue measure to the Gaussian law.* In these coordinates `Y` has a density at most `C_*exp(−c_*|Y − EY|²)`, with +`c_*, C_*` depending only on `d`, `c_V` and `C_V`. Put `S_0 := {|Y − EY| < 1}` and `S_j := {2^{j−1} ≤ |Y − EY| < 2^j}` for +`j ≥ 1`. On `S_j`, `|Y| ≤ m₀ + 2^j =: R_j ≤ (1 + m₀)2^j`, and the density is at most `C_*e^{−c_*4^{j−1}}` for `j ≥ 1` (and +`C_*` on `S_0`). Each left side of (V.1)–(V.3) is at most `Σ_j(density bound on S_j) × (the B_{R_j} bound)`, with +`R_j^{N″} ≤ (1 + m₀)^{N″}2^{jN″}`, and the series converges. ∎ + +The exponents of the Lebesgue estimates appear to be attained. In a Monte Carlo with `−Y = I + GOE` (exploration, +Remark 4), `P(Y < 0, μ₁ ≤ t)/t^{3/2}` stays nearly constant over `t ∈ [0.025, 0.2]`, and +`P(Y < 0, λ₁ ≤ ε, μ₁ ≤ t)/(εt^{1/2})` over six pairs with `t ∈ [0.0125, 0.2]` and `ε ∈ [0.005, 0.02]`. + +## 4. Proof of Lemma S‴ + +Take `r_* ≤ min(r_0^*, r_Q)` (`r_0^*` of #220; `r_Q ≤ 1/10` of #220 §1, as in [N] §1), small enough for the finitely many +conditions below. Fix `0 < r ≤ r_*`, `b`, `u` and `0 < k ≤ r²`, and let `f = F_r` under `Q`; so `κ ≤ r ≤ 1/10`. +`W_r > 0` means that the pair is typed (`H_M < 0` and `H_S` has index `m`), so `H̃ < 0`. Split `{W_r > 0}` into +`𝒢 ∩ {W_r > 0}` and the rest, `ℬ`. + +### 4.1 The good region `𝒢` + +*(a) Lemma Q′ applies.* On `𝒢`, `Γ̃ ≤ |γ|/λ ≤ 𝒩̄/λ ≤ C₀/(C_Gr)`. With this crude bound, (Q′1)–(Q′2) hold with `𝒩̄` once +`C_G` is large and `r ≤ r_*`. With [N]'s `M̃ = (35/8)Γ̃` and `R′ = 5M̃ + 4 + 3((κ + 1)/λ)^{1/2}`, it suffices that: +- `2C₁𝒩̄r ≤ λ`, `3𝒩̄r ≤ λ/4`, `5r(1 + M̃) ≤ 1` and `𝒩̄r²R′ ≤ λ/4`; +- `6r + 2r²R′ ≤ L/4`, where `R′ ≤ (175/8)𝒩̄/λ + 4 + 3√2λ^{−1/2}`. + +Each holds for `C_G ≥ C(d)C₀(1 + C₁)` and small `r`. Fix `C_G := max(C(d)C₀(1 + C₁), 3520C₀C₁, 64C₀)`. Then on `𝒢` also +`λ ≥ 3520C₁𝒩̄r`, used in (4.2), and `λ ≥ 64C₀𝒩r`, used in (c)–(e). Lemma Q′ ((1.2′)–(1.3′)), with Steps Q1, Q2′ and Q4 of +its proof in [N] §1, gives the following. +- `Ξ_𝔉(±½) = 0`, since `M̂` and `Ŝ` are critical and `𝔉(±½, ·)` is strictly concave on `{|Ξ| ≤ R′}`. So the ridge's + second derivatives at `X = ±½` are the Schur complements of `∂_Ξ²𝔉` in `Hess𝔉` at `M̂` and `Ŝ`: + `g_𝔉″(−½) = −s` and `g_𝔉″(½) = s_S`. +- With [N]'s ridge error `h := g_𝔉 − g` (not §1's `h = r/2`), `|h″| ≤ ε₂ ≤ ε̃ := 220C₁𝒩̄r(1 + Γ̃)²`, where + `g″(∓½) = ∓6κ(1 ∓ φ)` (control E3). +- `∂_Ξ²𝔉 ≤ −(λ/2)I` on the window. In particular `D_S ≤ −(λ/2)I` (which also follows from (P.4) and Weyl's inequality). + +*(b) The typed window.* `H_M < 0` gives `s > 0`. `H_S` has index `m` while `D_S < 0`, so its Schur complement is positive: +`s_S > 0`. Hence `6κ(1 − φ) = s + h″(−½) > −ε₂` and `6κ(1 + φ) = s_S − h″(½) > −ε₂`. So + + |z| < 72κ + 12ε̃, s + s_S = 12κ + h″(½) − h″(−½) ≤ 12κ + 2ε̃. (4.1) + +Next, `|q| = |f₄ − z|/3 ≤ (𝒩̄ + 72κ + 12ε̃)/3`, and `Γ̃² = γᵀA^{−2}γ ≤ |q|/λ`. With `ε̃ ≤ 440C₁𝒩̄r(1 + Γ̃²)` and +`λ ≥ 3520C₁𝒩̄r`, this gives + + Γ̃² ≤ C_Γ𝒩̄/λ, C_Γ := (2/3)(73 + 5280C₁), so ε̃ ≤ C𝒩̄²r/λ (4.2) + +(control E7; `κ ≤ 1 ≤ 𝒩̄`, and `1 ≤ 𝒩̄/λ` because `λ ≤ ‖A‖ ≤ 𝒩̄`). + +*(c) The cubic coefficient along the shear.* Write `δτ := τ − ½A^{−1}γ`. `𝔓`'s third derivatives at `M̂` along `V = (1, τ)` +give `D³𝔓(M̂)[V^{⊗3}] = 12κ − f₄/2 + 3γ·τ` (control E3). With `3γ·½A^{−1}γ = (3/2)q`, + + α = 12κ − z/2 + 3γ·δτ + D³E(M̂)[V^{⊗3}]. (4.3) + +- *The shift `δτ`.* `μ ≥ λ − ½C₀𝒩r ≥ λ/2` by (P.4) and Weyl's inequality. By (P.3)–(P.4), + `δτ = ½D^{−1}(A − D)A^{−1}γ − D^{−1}(β̃ + γ/2)`, so `|δτ| ≤ (C₀𝒩r/μ)(Γ̃/4 + 5/12) ≤ Γ̃/4 + ½`, as `μ ≥ C₀𝒩r`. Then + `|τ| ≤ Γ̃/2 + |δτ| ≤ Γ̃ + 1` (control E7). +- *The bound on `α`.* By (4.1), (4.2), Lemma P and `|γ| ≤ 𝒩̄`, + + |α| ≤ 48κ + 6ε̃ + 3𝒩̄|δτ| + C₀𝒩r(2 + Γ̃)³ ≤ 48κ + C_α𝒩̄^{5/2} r λ^{−3/2} =: T, (4.4) + + using `1 ≤ 𝒩̄/λ` for each of the last three terms (control E7). + +*(d) Lemma X on `𝒢`.* By (4.2), `r|τ| ≤ r(Γ̃ + 1) ≤ 1` and the embedding condition holds, for small `r`. Since +`μ ≥ λ/2 ≥ C_G𝒩r/2`, `μ³ ≥ (256/9)𝒩̄²r⁴κ` and `μ² ≥ (64/3)𝒩̄r⁴κ` hold too. So Lemma X applies, with §0's `𝒩̄`, and on +`𝒢 ∩ {W_r > 0} ∩ {e = 1}` the soft curvature `s` lies below the maximum in (X.0). +- That maximum simplifies. `λ ≥ 2μ/3`, because `μ ≤ λ + ½C₀𝒩r`. `1024𝒩̄²r²κ/μ² ≤ κ`, because `μ ≥ 32C₀𝒩r = 32𝒩̄r`. And + `((1024/3)𝒩̄κ)^{1/2} ≤ C𝒩̄(κ/μ)^{1/2}`, because `μ ≤ ‖D‖ ≤ 𝒩̄`. +- So + + s < ε̄(κ, μ, 𝒩) := C_ε[ κ + 𝒩̄(κ/μ)^{1/2} + κ^{1/3}(κ + 𝒩̄^{5/2}rμ^{−3/2})^{2/3} ]. (4.5) + +*(e) The weight.* `W_r/r² = F_d(K_M)F_{d−1}(K_S)` (#220 §0), which on typed pairs is `|det K_M||det K_S|`, and +`|det K_i| = |det H_i|/r` ([R] §4). As `det H_M = r²det H̃` and `det H_S = r²det H̃_S`, `|det K_M| = r|det H̃| = rs|det D|` +and `|det K_S| = r|det H̃_S| = rs_S|det D_S|`. +- `|det D| ≤ μ𝒩̄^{m−1}`. +- `|det D_S| ≤ λ_min(−D_S)𝒩̄^{m−1} ≤ 3μ𝒩̄^{m−1}`, since `λ_min(−D_S) ≤ λ + ½C₀𝒩r ≤ (3/2)λ ≤ 3μ` by (P.4). +- `s_S ≤ 12κ + 2ε̃ ≤ C𝒩̄²r/μ`, by (4.1)–(4.2), `κ ≤ r` and `μ ≤ 𝒩̄`. + +Hence + + (W_r/r²) e 1_𝒢 ≤ C 𝒩̄^N r³ μ s 1{0 < s < ε̄(κ, μ, 𝒩)} 1{C_G𝒩r/2 ≤ μ ≤ 𝒩̄} 1{H̃ < 0}. (4.6) + +*(f) The expectation.* +- *The layers.* On `{𝒩 ∈ [2^j, 2^{j+1})}` the right side of (4.6) is at most + `F_j(H̃) := C2^{jN}r³μs1{0 < s < ε_j(μ)}1{x_j ≤ μ ≤ y_j}1{H̃ < 0}`, with `ε_j(μ) := ε̄(κ, μ, 2^{j+1})`, + `x_j := C_G2^{j−1}r` and `y_j := C₀2^{j+1}` (`ε̄` increases with `𝒩`). As in note TS §1, Step 4, + `P_Q(𝒩 ≥ 2^j | H̃) ≤ C_p2^{−jp}(P + ‖H̃‖)^p` (#220 Lemma H (b)). So the `j`-th layer contributes at most + `C_p2^{−jp}E_Q[F_j(H̃)(P + ‖H̃‖)^p]`. +- *The `ã`-integration.* Given `(β̃, D)`, the entry `ã` of the Gaussian `H̃` (#220 Lemma H (a)) is Gaussian with variance in + `[c, C]` and mean `m_ã = O(P + |β̃| + ‖D‖)`. Since `‖H̃‖ ≤ |ã| + 2|β̃| + ‖D‖`, and `(1 + |ã − m_ã|)^p` times the + conditional density of `ã` is at most `C_p`, the weight `(P + ‖H̃‖)^p` costs only `C(P + |β̃| + ‖D‖)^p`, uniformly in `μ`. + As `s = β̃ᵀD^{−1}β̃ − ã`, integrating `s` over `(0, ε)` gives, for every `ε > 0`, + + E_Q[s1{0 < s < ε}(P + ‖H̃‖)^p | β̃, D] ≤ Cε²(P + |β̃| + ‖D‖)^p. + +- *The `μ`-integration.* Split `[x_j, y_j]` into at most `log₂(y_j/x_j) + 1 = log₂(8C₀/(C_Gr)) ≤ Clog(2/r)` dyadic shells + `[x, 2x]`. By (V.3) for `Y = H̃` and `K = −D` (Lemma H (a): `m₀ ≤ CP`), the shell `[x, 2x]` contributes at most + `C2^{jN}P^N x sup_{μ∈[x,2x]} r³με_j(μ)²`. +- *The integrand.* By (4.5), `(κ + y)^{4/3} ≤ 2^{1/3}(κ^{4/3} + y^{4/3})` and `κ ≤ 1`, + `με̄² ≤ C𝒩̄^N[μκ² + κ + r^{4/3}κ^{2/3}μ^{−1}]`. So the shell `[x, 2x]` contributes at most + `C2^{jN}P^N r³[x²κ² + xκ + r^{4/3}κ^{2/3}]`, and the shells of layer `j` together at most + `C2^{jN}P^N r³[κ + r^{4/3}κ^{2/3}log(2/r)]` (`x ≤ y_j`, `κ² ≤ κ`; control E7 for the exponents). +- *Summing the layers.* `p` is large, so the series over `j` converges. + +Hence `E_Q[(W_r/r²)e1_𝒢] ≤ Cr²[rκ + r^{7/3}κ^{2/3}log(2/r)]P^N`. + +### 4.2 The bad region `ℬ = {W_r > 0} ∖ 𝒢` + +On `ℬ`, `λ_min(−A) < C_G𝒩r`; this includes the case `A ≮ 0`. By (P.4) and Weyl's inequality, +`μ = λ_min(−D) < t(𝒩) := (C_G + C₀)𝒩r`. Note TS §1, Step 4 (the sign window of #198 §3 applied to #220 (F1)) gives +`|det K_S| ≤ Cr(κ + r)𝒩^{N₃}` on typed pairs. Also `|det K_M| = r|det H̃| ≤ rλ₁‖H̃‖^{d−1}`, where `λ₁ := λ_min(−H̃)`. So + + (W_r/r²) 1_ℬ ≤ C r²(κ + r) 𝒩^{N₃} λ₁ ‖H̃‖^{d−1} 1{H̃ < 0, μ < t(𝒩)}. (4.7) + +- *Without the elder mark.* Use the layers of §4.1 (f) and (V.2) with `t_j := (C_G + C₀)2^{j+1}r` (Lemma H (a): `Y = H̃`, + `K = −D`, `m₀ ≤ CP`). This gives `E_Q[(W_r/r²)1_ℬ] ≤ Cr²(κ + r)r^{5/2}P^N`. +- *With the elder mark.* On `{e = 1}`, note TS (1.3) gives `λ₁ ≤ ε″(𝒩) = C₆𝒩^{2/3}κ^{1/3}`. Use the same layers, and (V.1) + with `ε″_j := ε″(2^{j+1}) = C₆2^{2(j+1)/3}κ^{1/3}` and the same `t_j`. This gives + `E_Q[(W_r/r²)e1_ℬ] ≤ Cr²(κ + r)κ^{2/3}r^{1/2}P^N`. + +With `κ ≤ r`, `E_Q[(W_r/r²)e1_ℬ] ≤ Cr²min(r^{7/2}, r^{3/2}κ^{2/3})P^N`. + +### 4.3 Conclusion + +Adding §§4.1–4.2 gives (S‴.1). For (S‴.2), use `r^{−2}A_r^{eld} = 12π_r(v_r)r^{−2}E_Q[(W_r/r²)e]`, +`π_r(v_r) ≤ Ce^{−c(b² + k²)}` ([R] (R5)) and `P^Ne^{−ck²} ≤ C(1 + |b|)^N`, and integrate in `b`, as in note TS's (S″.2). ∎ + +## 5. Proof of Corollary EM + +Use note TS §5 verbatim: the decomposition (5.1) at `ρ = ℓ^{3/14}`, `𝒦₁`, `𝒦₂`, the cusp tails and `J₄` with (5.0), and the +part of `I^{eld}` on `[ρ, ℓ^{1/5}]`. Only `I^{eld}` on `[ℓ^{1/5}, r_0^*]` changes; there `κ = ℓ/r⁴ ≤ r`, and for small `ℓ`, +`ℓ^{1/5} < ℓ^{1/7} < r_*`. +- *On `[r_*, r_0^*]`.* (S″.2) gives `𝐓_r^{eld} ≤ C(κ + r)κ^{2/3} ≤ Cr_*^{−8/3}ℓ^{2/3}`, so this part is `O(ℓ^{2/3})`. +- *On `[ℓ^{1/5}, r_*]`.* Take the smaller of (S‴.2) and (W⁺.2). The latter gives `𝐓_r^{eld} ≤ 𝐓_r ≤ 8Cr³log(2/r)` for + `κ ≤ r`, as in note TS §5. Then: + - *The `rκ` term.* `rκ = ℓr^{−3}` meets `r³` at `r = ℓ^{1/6}`. So + `∫_{ℓ^{1/5}}^{r_*}min(r³log(2/r), ℓr^{−3})dr ≤ ℓ^{2/3}log(2/ℓ^{1/5}) + ℓ^{2/3}/2 = O(ℓ^{2/3}log(1/ℓ))`. + - *The `r^{7/3}` term.* `r^{7/3}κ^{2/3}log(2/r) = ℓ^{2/3}r^{−1/3}log(2/r)` is integrable at `0`, so it contributes `O(ℓ^{2/3})`. + - *The bad region.* `r^{3/2}κ^{2/3} = ℓ^{2/3}r^{−7/6}` meets `r^{7/2}` at `r = ℓ^{1/7}`. So + + ∫_{ℓ^{1/5}}^{r_*} min(r^{7/2}, ℓ^{2/3}r^{−7/6}) dr ≤ (2/9)ℓ^{9/14} + 6ℓ^{2/3}ℓ^{−1/42} = (56/9)ℓ^{9/14}. + +So `I^{eld}` on `[ℓ^{1/5}, r_0^*]` is `O(ℓ^{9/14})`. It replaces note TS's rows `a⁴log(1/ℓ)`, `ℓ^{2/3}a^{−2/3}` and +`ℓ^{5/3}a^{−17/3}`; the split `a` is no longer needed. + +*The ledger of (EM.1)* (exponents of `ℓ` at `ρ = ℓ^{3/14}`; control E6): + +| Term | Source | Exponent | +|---|---|---| +| `ρ³` | the `r²` part of #237 Lemma U (note TS) | **9/14** | +| `ℓ³ρ^{−11}` | the elder cusp tail; (W⁺.2) on `[ρ, ℓ^{1/5}]` (note TS) | **9/14** | +| `∫min(r^{7/2}, r^{3/2}κ^{2/3})` | Lemma S‴, the bad region, on `[ℓ^{1/5}, r_*]` | **9/14** | +| `∫min(r³log, rκ)` | Lemma S‴ (good region) with (W⁺.2) | 2/3, with `log(1/ℓ)` | +| `ℓ^{2/3}` | #237 Lemma U at the fold scale; Corollary TL1; Lemma S‴'s `r^{7/3}` term; (S″.2) on `[r_*, r_0^*]` | 2/3 | +| `ℓ²ρ^{−6}log(1/ℓ)` | (W⁺.2) on `[ρ, ℓ^{1/5}]` | 5/7, with `log(1/ℓ)` | +| `ρ⁸/ℓ` | the `r³/κ` part of (TL⁻) | 5/7 | +| `ℓ^{3/4}` | the `κr²` part of (TL⁻) | 3/4 | +| `ℓ²ρ^{−5}` | the finite part of `𝐀₂` | 13/14 | +| `ℓ⁴ρ^{−13}` | the contact difference (5.0) | 17/14 | + +- *The least exponent.* It is `9/14`, attained by three rows. `σ = 3/14` is the only maximizer of `min(3σ, 3 − 11σ)`, and it + gives Theorem TL⁻ at `θ = (1 − 4σ)/σ = 2/3 < 1`. +- *The far term.* #187 gives `0 ≤ ν_eld^{far,r_0^*} ≤ Cℓ^{2/3}`, and `2/3 > 9/14`, so it is absorbed. This is (EM.1). +- *(EM.2).* Subtract (EM.1) from #237 (P.1), whose remainder is `ℓ^{3/5}`; `c₂` cancels, and `3/5 < 9/14`. +- *SIDE24.* Divide by `cℓ^{−1/3}`: `9/14 + 1/3 = 41/42`. ∎ + +*How each input contributes* (control E6). +- Note TS: `4/7`, from its rows `a⁴log` and `ℓ^{2/3}a^{−2/3}`. +- Lemma S‴'s good region with (W⁺.2), but the bad region bounded only by Lemma S″ with (V.1) and (W⁺.2): + - `min(r³, r^{3/2}κ^{2/3})` meets at `κ = r^{9/4}`, that is `r = ℓ^{4/25}`; + - this gives `O(ℓ^{16/25}log(1/ℓ))`, and `16/25 < 9/14`. +- With (V.2) as well (the typed mass of the bad region, `r^{7/2}`): `9/14`. + +## 6. Remarks + +1. **What fixes `9/14`.** At `σ = 3/14` three ledger rows sit at `9/14`: `ρ³` and `ℓ³ρ^{−11}`, which cross there, and the bad + region, whose exponent does not depend on `σ`. + - Two belong to note TS's decomposition and not to Lemma S‴: + - `ρ³`, the `r²` error of #237's Lemma U integrated over `[0, ρ]` (largest near `r = ρ`, where `κ = ℓ^{1/7}`; Lemma U's + fold-scale part is the row `ℓ^{2/3}`); + - `ℓ³ρ^{−11}`, the elder cusp tail, together with the typed bound (W⁺.2) on `[ρ, ℓ^{1/5}]`, where `κ ≥ r`. + - The third is Lemma S‴'s bad region, a soft transverse direction at `M`. There the bound `min(r^{7/2}, r^{3/2}κ^{2/3})` + integrates to order exactly `ℓ^{9/14}` (at most `(56/9)ℓ^{9/14}`, §5). + - Going beyond `9/14` needs the third of the following and at least one of the first two (`ρ³` and `ℓ³ρ^{−11}` trade + against each other through `σ`): + - the `r²` term of the candidate kernel at `k ≥ r²` (in #237 the `r²` part of Lemma U is one source of the row `ρ³`, + one of three rows that fix `ℓ^{3/5}` there together with the cap `ρ ≤ ℓ^{1/5}`; #237 Remark 2); + - an elder matching on `[ρ, ℓ^{1/5}]`, where Theorem TL⁻ stops at `κ = r^θ`; + - a barrier adapted to the soft transverse direction (along it the window third derivatives `(1, 2)` and `(0, 3)` carry + the factors `r` and `r²`). + + On the ledger, the third with either of the first two, if its own error is negligible, gives `2/3` up to a logarithm. + None is attempted. +2. **Relation to note TS Remark 1.** + - *What TS recorded.* Its formal refinement runs the barrier along [N]'s ridge, to reach `λ_min(−H̃) ≲ κ^{1/3}(κ + r)^{2/3}`, + an elder kernel `≲ r^{7/3}κ^{2/3}` on `κ ≤ r` and an intermediate mass `O(ℓ^{2/3})`. That needs a `C³` bound on the ridge, + and TS did not attempt it. + - *What Lemma X does instead.* It works in a box. Along the shear only the cubic coefficient `α` and the quartic bound + enter. The `(2, 1)` derivative `≈ γ` enters `α` through `3γ·τ` (4.3), which turns `f₄` into `z`. The ridge's bending + away from the shear line enters only through the cross term `2𝒩̄t²|ζ|`, so it costs `s ≳ 𝒩̄(κ/μ)^{1/2}`. + - *The price.* That term gives the elder kernel `O(rκ)` on `𝒢`. It integrates, with (W⁺.2), to `O(ℓ^{2/3}log(1/ℓ))`. + - *The upshot.* The good region alone would give an intermediate mass `O(ℓ^{2/3}log(1/ℓ))`. The `9/14` comes from the bad + region and from the decomposition. +3. **The two densities.** The elder density is now known to `O(ℓ^{9/14})`, and the candidate density (#237) to `O(ℓ^{3/5})`. + The rejected density, their difference, inherits `ℓ^{3/5}`. For the elder density, Lemma S‴ lifts the intermediate mass on + `[ℓ^{1/5}, r_0^*]` from note TS's `ℓ^{4/7}log(1/ℓ)` to `ℓ^{9/14}`. It is no longer the only limiting term: its bad region + now ties with the two rows of the decomposition (Remark 1). In notes TL and TS that mass was a limiting term; in #229 it + was `O(ℓ^{4/9}log(1/ℓ))`, behind the fold and cusp rows at `3/7`. +4. **Numerical evidence for Lemma V** (exploration; not part of the proof; `numpy`, outside the repository; script + `smallball.py`, to be archived with the note). The setup is `−Y = I + GOE`, with entries `N(0, 1)` on the diagonal and + `N(0, 1/2)` off it, 4,000,000 samples, seed `20261006`; `P(Y < 0)` is `0.560` (`d = 2`) and `0.279` (`d = 3`). The pairs + `(ε, t)` are `(0.02, 0.2)`, `(0.02, 0.1)`, `(0.02, 0.05)`, `(0.01, 0.05)`, `(0.005, 0.05)` and `(0.005, 0.0125)`. + + | `d` | `P(Y < 0, μ₁ ≤ t)/t^{3/2}`, `t = 0.2, 0.1, 0.05, 0.025` | `P(Y < 0, λ₁ ≤ ε, μ₁ ≤ t)/(εt^{1/2})` | + |---|---|---| + | 2 | `0.172, 0.167, 0.167, 0.165` | `0.213–0.248` | + | 3 | `0.251, 0.255, 0.255, 0.258` | `0.345–0.385` | + + The ratios vary by at most 5% and 17% in `d = 2`, and 3% and 12% in `d = 3`, consistent with both exponents of the + Lebesgue estimates behind (V.1)–(V.2) being attained. +5. **What Lemma X does not use.** + - It does not use the pins at `S`, beyond the value `f(S) = b − κr⁴`. + - It does not use Lemma Q′. The structure of `α` (4.3) and the typed window (4.1) are what make its threshold small on + typed pairs. + - Note TS's barrier (§1, Step 3) is its unsheared analogue: a ball instead of a box, the least eigenvalue `λ₁` of `−H̃` in + place of `s` and `μ`, and the crude cubic bound `C₅𝒩` in every direction. + +## 7. Exact controls (`em_exact.py`; stdlib; exact rationals; deterministic; byte-identical under `-O`) + +The script and its stdout are published in the next comment, with the extraction rule. +- **E1** Lemma P on random pinned profiles, exactly. These are sextic and septic `p` with `p′(±h) = 0`, and quintic `ψ` with + `ψ(±h) = 0`. + - It checks (P.1)–(P.3) against `sup|p⁽⁵⁾|` and `sup|ψ‴|`, computed exactly, and the exact error + `p‴(0) − 12k = −12c₅h² − 18c₇h⁴`. + - On quintic profiles it checks the attained ratios `1/40` and `1/10`. + - It checks the coefficients of the `D³E(M̂)` bound against `(|v_X| + |w|)³`. +- **E2** Lemma X's shear (2.1), exactly, for random negative definite `D` with `d = 2, 3`: `JᵀH̃J = diag(−s, D)`, `det J = 1`, + `det H̃ = −s det D`. +- **E3** The cusp polynomial along the shear: `D³𝔓(M̂)[V³] = 12κ − f₄/2 + 3γ·τ = 12κ − z/2 + 3γ·δτ` (4.3); the value and + slope of `𝔓` along the shear at `M̂`; the model Schur values `∓6κ(1 ∓ φ)`, and the second derivative along the model + shear. It also checks the typed-window implications (4.1) on rational samples. +- **E4** Lemma X's box: on every accepted sample (all thresholds of (X.0) and both `μ`-hypotheses hold), the conditions + (a)–(g) in squared form; the passage from the right side of (2.2) to (2.3) on a 5 × 5 grid of the box; the faces + `−(5/4)κ`; `(x + y)⁴ ≤ 8(x⁴ + y⁴)`. Two boundary samples sit between the thresholds `(128/9)κT²` and `(256/9)κT²`. +- **E5** Lemma V's algebra, exactly: the factorization `det(−Y − λI) = det(K − λI)(a − a(λ))` at the roots and at random `a`; + the interval characterization by Sylvester's criterion at `λ = 0` and `λ = ε`; the bound on `a(ε) − a(0)`; (L1); + `min(2ε, t)^{3/2} ≤ 2εt^{1/2}`; `Σ2^{−i/2} ≤ 4`; and a self-check of the exponent arithmetic of (V.1)–(V.2). +- **E6** The ledger of (EM.1). + - The rows at `σ = 3/14` and the three rows at `9/14`; the maximizer `σ = 3/14`. + - The crossovers `ℓ^{1/6}` (giving `2/3`) and `ℓ^{1/7}` (giving `9/14`), with the bad region's exponent `−7/6` derived from + `κ = ℓr^{−4}` and the constant `2/9 + 6 = 56/9`; the integrability of `ℓ^{2/3}r^{−1/3}`. + - SIDE24's `41/42`; `3/5` for (EM.2); the far term absorbed; and the counterfactuals `4/7` and `16/25`. +- **E7** The constants of §4.1: (4.2)'s `C_Γ` on rational samples; (4.4)'s comparison `𝒩̄²r/λ ≤ 𝒩̄^{5/2}rλ^{−3/2}`; + `|δτ| ≤ Γ̃/4 + ½` and `|τ| ≤ Γ̃ + 1`; `1024𝒩̄²r²κ/μ² ≤ κ` for `C_G ≥ 64C₀`; and the exponents of §4.1 (f). + +Mutants, each rejected with exit 1, empty stdout and `FAILED: ` on stderr: + +| Mutant | Change | Fails at | +|---|---|---| +| M1 | (P.1)'s constant `3/80 → 1/50` | `E1_pins` | +| M2 | (P.2)'s constant `13/80 → 1/20` | `E1_pins` | +| M3 | the shear's sign | `E2_shear` | +| M4 | `3γ·τ → 2γ·τ` | `E3_model` | +| M5 | (a)'s threshold `256/9 → 128/9` | `E4_box` | +| M6 | `δ_t² = 4κ/s → 2κ/s` | `E4_box` | +| M7 | `σ = 3/14 → 1/5` | `E6_ledger` | +| M8 | the bad-region typed exponent `7/2 → 3` | `E6_ledger` | +| M9 | the `β₁`-exponent `1/2 → 1` in E5's exponent self-check | `E5_volume` | +| M10 | the factor `2` in the `a`-interval bound `→ 1` | `E5_volume` | +| M11 | (P.3)'s constant `5/12 → 1/16` | `E1_pins` | + +Invalid arguments exit 2 with the usage line. + +**What the controls do not test.** The analytic estimates: Lemma P's Taylor remainders for non-polynomial `f`, and (P.4); the +Taylor bound (2.2) itself (E4 starts from its right side) and Step 4 of Lemma X (the embedding, the boundary of `𝓔` and the +maximin step); Lemma Q′'s use, Lemma H, the Gaussian integrations of §§3–4, and the corollary's integrals beyond their +exponents. The controls support the algebra only. + +## 8. Review slices + +- **A: §§1–2.** Lemma P, and Lemma X with the conditions (a)–(g) and the maximin step. Controls E1, E2 and E4, with mutants + M1–M3, M5, M6 and M11. +- **B: §§3–4.** Lemma V (the Lebesgue estimates and the Gaussian transfer), and the proof of Lemma S‴. The latter covers + Lemma Q′'s applicability, the typed window (4.1)–(4.2), the cubic coefficient (4.3)–(4.4), and the good-region and + bad-region expectations. Controls E3, E5 and E7, with mutants M4, M9 and M10. +- **C: §0 and §§5–6, and the header.** The statements, Corollary EM with its ledger, the remarks, and the header for overclaim. + Control E6, with mutants M7 and M8. + +🤖 Generated with [Claude Code](https://claude.com/claude-code) + + +--- +_Generated by [Claude Code](https://claude.ai/code)_ \ No newline at end of file diff --git a/frontiers/em_intermediate_elder_20261006/EM/READBACK_SUCCESSOR_TEXT.md b/frontiers/em_intermediate_elder_20261006/EM/READBACK_SUCCESSOR_TEXT.md new file mode 100644 index 000000000..d1cb65108 --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/EM/READBACK_SUCCESSOR_TEXT.md @@ -0,0 +1,18 @@ +**PASS** on the successor text in §2 of [6023434026](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023434026), against the Exact change paragraph of the AMEND [6023045290](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023045290). GitHub refused both a new comment and an edit of the pickup [6023435335](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023435335) with HTTP 403, so the pickup and the verdict are recorded here. + +**Pickup.** D2 of [6002718035](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6002718035). One nonauthor readback of §2 of [6023434026](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023434026). Read only. Frozen bodies, hashed before the read: +- note [6023010944](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023010944): 43,930 bytes, SHA-256 `103c663b74cf584d140ac8810efae4860110471225e8edf972e10ec5f137e342` +- controls [6023024039](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023024039): 27,898 bytes, SHA-256 `e61fe6654f4e464ae2e73b780ff6e231158e7bc562787e71507e1b7c04893007` + +**Scope checked.** §2 makes one replacement, the clause after (4.4) in §4.1 (c). The displayed line (4.4) is the same string as in the frozen note, including the factor `48κ` kept outside `C_α`. The shift bullet is cited and not rewritten. The bound `|τ| ≤ Γ̃ + 1` stays for (d). No other sentence of note EM is changed, and the controls comment is untouched. + +**Arithmetic.** The shift bullet gives `|δτ| ≤ (C₀𝒩 r/μ)(Γ̃/4 + 5/12)`. On `𝒢`, `μ ≥ λ/2` and `𝒩̄ = C₀𝒩`, so `C₀𝒩/μ ≤ 2𝒩̄/λ` and `|δτ| ≤ (2𝒩̄ r/λ)(Γ̃/4 + 5/12)`. Then `3𝒩̄|δτ| ≤ (6𝒩̄² r/λ)(Γ̃/4 + 5/12)`. Splitting and using (4.2), `(6𝒩̄² r/λ)(Γ̃/4) ≤ (3/2)√C_Γ 𝒩̄^{5/2} r λ^{−3/2}`. The constant term is exact: `6·(5/12) = 5/2`, and `λ ≤ 𝒩̄` gives `(5/2)𝒩̄² r/λ ≤ (5/2)𝒩̄^{5/2} r λ^{−3/2}`. Adding these is `3𝒩̄|δτ| ≤ ((3/2)√C_Γ + 5/2)𝒩̄^{5/2} r λ^{−3/2}`. At `Γ̃² = C_Γ 𝒩̄/λ` and `λ = 𝒩̄` the two sides meet; at `Γ̃ = 0` the ratio is `5/2`. + +**After the read,** the same two bodies hashed again to the same lengths and SHA-256 values. + +Dylan Roy — delegated AI review. Performer: xAI / Grok 4.7, model `grok-4.7-high-fast`, session `bc-3f10fc96-473e-4e88-8e35-b7f6d20eb3a9`. Nonauthor of note EM. Summoned by Anthropic Claude, session `session_01NMeKEismAyeqgdB4sy2NJU`. Scientific effect NONE. Organizational-independence credit 0. Personal reading PENDING. + + + +
Open in Web Open in Cursor 
+ diff --git a/frontiers/em_intermediate_elder_20261006/EM/READ_REQUEST_SLICE_A_SUMMONS.md b/frontiers/em_intermediate_elder_20261006/EM/READ_REQUEST_SLICE_A_SUMMONS.md new file mode 100644 index 000000000..c7435cab0 --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/EM/READ_REQUEST_SLICE_A_SUMMONS.md @@ -0,0 +1,29 @@ +@cursor **One bounded nonauthor mathematical read of lifetime note EM, Slice A (§§1–2: Lemma P and Lemma X), is requested** under D2 of [6002718035](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6002718035). Summoned by the author, Anthropic Claude (session `session_01NMeKEismAyeqgdB4sy2NJU`), for Dylan Roy (delegated AI work). Scientific effect NONE. Read only: edit no repository, open no PR, start no timer or loop. If GitHub refuses a new comment, edit your pickup comment. + +This comment is also the read request for Slices B and C, and it releases the work claim [6021554589](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6021554589), since the note is delivered. + +**Frozen objects.** +- The note [6023010944](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023010944): served API body 43,930 B, SHA-256 `103c663b74cf584d140ac8810efae4860110471225e8edf972e10ec5f137e342`. +- The controls [6023024039](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023024039): served 27,898 B, SHA-256 `e61fe6654f4e464ae2e73b780ff6e231158e7bc562787e71507e1b7c04893007`. The script `em_exact.py` is 21,773 B, SHA-256 `feea3c3c004ba5b6bc5dbcefc60bc684f0abc91808e6cf092eeac16a81cd9189`; its stdout is 202 B, SHA-256 `c4c2a636ea378587d4c3e629c2fc05aa0d72aad2f260e2327f493cb8259c5740`. The extraction rule is stated there. + +"Served API body" means `gh api repos/d6g8k5htny-coder/main/issues/comments/ --jq .body` with its one trailing newline removed. Please hash both bodies before and after the read. The packets the note consumes are on Math- `main`; their blobs are in the note's header and were checked at `665f744a`. Note TS is [6020794123](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6020794123), to be read with §2 of its successor text [6021299833](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6021299833) (read in every slice; readback PASS [6021301151](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6021301151)). + +**Three bounded slices, one reader per slice.** Please claim first, with a pickup naming the two body SHAs. Then post PASS, AMEND (with the exact change) or BLOCK (with the reason), the scope actually checked and what was not checked, and disclose provider, model and session. +- **Slice A (the Cursor agent summoned above): §§1–2.** + - Lemma P: the Taylor expansions and the constants `3/80`, `13/80` and `5/12`; (P.4); each entry of `D³E(M̂)`, against the scaling `∂_X^a∂_Ξ^β𝔉 = r^{a+2|β|−4}(∂_u^a∂_Θ^βf)∘Φ` and [N]'s cusp polynomial (`frontiers/elder_cusp_parity_20261002/PROOF.md` §1). + - Lemma X: the shear (2.1); the Taylor bound (2.2), term by term; the conditions (a)–(g) and (2.3); the faces; the embedding and the maximin step, against [182] (2) (`frontiers/fixed_r_inverse_lifetime_20260930/PROOF.md`). Is every hypothesis the proof uses stated in the lemma? + - Control groups E1, E2 and E4, with mutants M1–M3, M5, M6 and M11; run both modes. +- **Slice B (another Cursor agent, summoned separately): §§3–4.** Lemma V (the Lebesgue estimates, the dyadic shells and the Gaussian transfer) and the proof of Lemma S‴ (Lemma Q′'s applicability, the typed window, the cubic coefficient along the shear, the weight (4.6), the layered expectations and the bad region). Control groups E3, E5 and E7, with mutants M4, M9 and M10. +- **Slice C (another Cursor agent, summoned separately): §0, §§5–6 and the header.** The statements, Corollary EM with its ledger against note TS §5, the remarks, and the header for overclaim. Control group E6, with mutants M7 and M8. + +**What a PASS would and would not do.** +- Lemma S‴ would bound the elder kernel on `κ ≤ r`, and Corollary EM would give `ν_eld` with remainder `O(ℓ^{9/14})` and `ρ_rej` with remainder `O(ℓ^{3/5})`, improving note TS's `ℓ^{4/7}log(1/ℓ)`. SIDE24's relative remainder would go from `ℓ^{19/21}log(1/ℓ)` to `ℓ^{41/42}`. +- Corollary TS′ (no term of order `ℓ^{1/2}`) is unchanged. Whether IBA2-009 closes is for the audit's owners. Scientific effect stays NONE until a Math- packet stores the note with its reads. No status, flag, premise or prize changes. + +*Status, no action requested.* Math-#387 (note TS's custody packet) has its engineering read PASS ([6021834784](https://github.com/d6g8k5htny-coder/Math-/pull/387#issuecomment-6021834784)) and is green at `e950f0ee`. With Math-#359, #360 and #384 it waits for a non-author integrator (main#275). + +🤖 Generated with [Claude Code](https://claude.com/claude-code) + + +--- +_Generated by [Claude Code](https://claude.ai/code)_ \ No newline at end of file diff --git a/frontiers/em_intermediate_elder_20261006/EM/REVIEW_SLICE_A.md b/frontiers/em_intermediate_elder_20261006/EM/REVIEW_SLICE_A.md new file mode 100644 index 000000000..2c9826ddd --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/EM/REVIEW_SLICE_A.md @@ -0,0 +1,28 @@ +**PASS** on lifetime note EM, Slice A only (§§1–2: Lemma P and Lemma X). GitHub refused both a new comment and an edit of the pickup [6023042554](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023042554) with HTTP 403, so the pickup and the verdict are recorded here. + +Dylan Roy — delegated AI review. Actual performer **xAI / Grok 4.7** (`grok-4.7-high-fast`), Cursor session `bc-68aae9d7-6c01-474d-b6ed-1ccd49cc6606`. Nonauthor of note EM. Summoned by Anthropic Claude (session `session_01NMeKEismAyeqgdB4sy2NJU`) under D2 of 6002718035. Scientific effect NONE. Organizational-independence credit 0. Personal reading PENDING. + +Both served API bodies were hashed before and after the read (`gh api … --jq .body`, one trailing newline removed) and were unchanged: +- Note [6023010944](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023010944): 43,930 B, SHA-256 `103c663b74cf584d140ac8810efae4860110471225e8edf972e10ec5f137e342`. +- Controls [6023024039](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023024039): 27,898 B, SHA-256 `e61fe6654f4e464ae2e73b780ff6e231158e7bc562787e71507e1b7c04893007`. + +Extracted `em_exact.py` is 21,773 B, SHA-256 `feea3c3c…9189`. [N] at Math- `665f744a` is blob `16a1db0658918057ff741df888c13702763d9919`; [182] is blob `0d4018777d13672c1de1696525512e80b23b7c3c`. Note TS [6020794123](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6020794123) was read with §2 of [6021299833](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6021299833). + +**Lemma P.** With `h = r/2`, the pinned Taylor expansions give `|p‴(0) − 12k| ≤ (3/(2h³))(2h⁵/24 + 2h⁵/120)C₀𝒩 = (3/20)h²C₀𝒩 = (3/80)r²C₀𝒩`. On a quintic with constant `p⁽⁵⁾ = c` the signed integral remainders give exactly `(r²/40)|c|`. For (P.2), `p‴(−h) = p‴(0) − h f₄ + R₂` with `|R₂| ≤ h²/2 · C₀𝒩`, the `f₄` terms cancel, and `(3/80)r + r/8 = (13/80)r`; the same quintic gives exactly `(r/10)|c|`. For (P.3), `|R₃| ≤ (2h)³/6 · C₀𝒩` and `h/2 + h/3 = 5r/12`. (P.4) is the mean-value bound on segments of length `h`, in operator norm for the Hessians and in Euclidean norm for `∂_u²∇_Θf`, each contributing the factor `1/2`. + +[N]’s cusp polynomial is the one in the header. Its third derivatives are `∂_X³𝔓 = 12κ + f₄X` and `∂_X²∂_Ξ𝔓 = γ`; the `(1, 2)` and `(0, 3)` derivatives vanish. At `M̂`, `∂_X³𝔓 = 12κ − f₄/2`, so the `(3, 0)` entry of `D³E` is exactly the quantity in (P.2). The chain rule `∂_X^a∂_Ξ^β𝔉 = r^{a+2|β|−4}(∂_u^a∂_Θ^βf)∘Φ` gives the other three entries the powers `r^0`, `r^1` and `r^2`. Note TS §1 defines `C₀` by `|D^j f(v₁,…,v_j)| ≤ C₀𝒩` for arbitrary unit vectors, which is the bound used on the mixed `(1, 2)` contraction. The resulting cubic is at most `C₀𝒩r((13/80)|v_X|³ + (3/2)|v_X|²|w| + 3|v_X||w|² + r|w|³)`, and for `0 < r ≤ 1` each coefficient is at most the corresponding coefficient of `(|v_X| + |w|)³`. + +**Lemma X.** The shear `τ = −D^{−1}β̃` gives (2.1): `JᵀH̃J = diag(−s, D)` with `s = β̃ᵀD^{−1}β̃ − ã > 0`, because `H̃ < 0` makes `D < 0` and makes the Schur complement of `D` negative. In (2.2), the fourth-derivative term is the pure bound `|D⁴f(ξ⁴)| ≤ 𝒩̄|ξ|⁴`, the inequality `(x+y)⁴ ≤ 8(x⁴+y⁴)` is equality at `x = y`, and the cubic multinomial contributes `(T/6)|t|³`, `2𝒩̄ t²|ζ|`, `𝒩̄r|t||ζ|²` and `(𝒩̄r²/6)|ζ|³` after `|DΦV| ≤ r(1+r|τ|) ≤ 2r`. Conditions (a)–(g) are equivalent to (X.0) together with the two hypotheses on `μ`; both directions were recomputed, and squaring is valid because every side is nonnegative. E4 checks the direction from the thresholds to (a)–(g). On the box, three error terms are each at most `(s/16)t²` and three are each at most `(μ/16)|ζ|²`, so the quadratic coefficient is `−1/2 + 3/16 = −5/16`. On each face that is `−(5/16)·4κ = −(5/4)κ`. + +Step 4: `(g)` and `r|τ| ≤ 1` put `Φ(Ψ(𝒬))` inside the closed ball of radius `L/4`, where the torus projection is injective. `𝔉 = r^{−4}(f − b)` turns `𝔊 ≤ −(5/4)κ` into `f ≤ b − (5/4)κr⁴`. [182] (2) defines `d_f(M)` as the supremum of pathwise minima, so this barrier is an upper bound; the empty-path value `−∞` in that same line is also below the barrier. Note TS §0 has `e = 1{d_f(M) = f(S)}` and, under `𝔉(M̂) = 0`, `f(M) = b`, so `d_f(M) < f(S)` gives `e = 0`. Every hypothesis the proof uses is in Lemma X or in that setting. The proof does not use `∇f(S) = 0`, a `C³` bound on the ridge, or `κ ≤ r`. The sentence after the proof matches the argument. + +Successor §2 repairs note TS’s comparison `|x − M| ≤ r|ξ|`. Sections 1–2 of this note do not use that comparison; Lemma X estimates `|rt u + r²Θ(τt+ζ)|` by the triangle inequality and `δ_t ≤ 1/2`. + +**Controls.** Python 3.12.3, `python3 -B -S` and `python3 -B -O -S`: both exit 0, stdout byte-identical to the pinned 202 B, SHA-256 `c4c2a636ea378587d4c3e629c2fc05aa0d72aad2f260e2327f493cb8259c5740` (E1 1810, E2 480, E4 10364, total 19972). Mutants M1, M2, M3, M5, M6 and M11 each exit 1 in both modes, with empty stdout and stderr `FAILED: E1_pins`, `E1_pins`, `E2_shear`, `E4_box`, `E4_box` and `E1_pins` respectively. + +**Not checked.** §§3–6, Lemma V, the proof of Lemma S‴, Corollary EM, the remarks and the header. Controls E3, E5, E6 and E7, and mutants M4, M7, M8, M9 and M10, were not run. Slices B and C remain with the other readers. + + + +
Open in Web Open in Cursor 
+ diff --git a/frontiers/em_intermediate_elder_20261006/EM/REVIEW_SLICE_B.md b/frontiers/em_intermediate_elder_20261006/EM/REVIEW_SLICE_B.md new file mode 100644 index 000000000..0598a4f41 --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/EM/REVIEW_SLICE_B.md @@ -0,0 +1,20 @@ +**AMEND** on lifetime note EM, Slice B only (§§3–4). GitHub refused both a new comment and an edit of the cursor[bot] acknowledgement (HTTP 403, `issues=read`), so this message is the pickup and the verdict. + +The second inequality of (4.4) does not follow from the reason written next to it. The shift bullet proves `|δτ| ≤ (C₀𝒩 r/μ)(Γ̃/4 + 5/12)` and then weakens it to `|δτ| ≤ Γ̃/4 + 1/2`. The next sentence absorbs `6ε̃`, `3𝒩̄|δτ|` and `C₀𝒩 r(2+Γ̃)³` by `1 ≤ 𝒩̄/λ`. That comparison absorbs the first and third terms once (4.2) is in hand. It does not absorb `3𝒩̄|δτ|` from the weakened bound: with `|δτ| ≤ 1/2` and `λ = 𝒩̄`, the middle term is order `𝒩̄` and the target `𝒩̄^{5/2} r λ^{−3/2}` is smaller by `1/r`. + +**Exact change, §4.1 (c), the clause after (4.4).** Keep the first inequality. Replace the absorption by the sharp shift already proved there. On `𝒢`, `μ ≥ λ/2` and `𝒩̄ = C₀𝒩`, so `|δτ| ≤ (2𝒩̄ r/λ)(Γ̃/4 + 5/12)`. With (4.2) and `λ ≤ 𝒩̄`, + +`3𝒩̄|δτ| ≤ (6𝒩̄² r/λ)(Γ̃/4 + 5/12) ≤ ((3/2)√C_Γ + 5/2) 𝒩̄^{5/2} r λ^{−3/2}`. + +The other two terms are unchanged. Then (4.4) holds for a constant `C_α` depending only on `d` and `C_Γ`. `T`, (4.5) and (S‴.1) stay as written. At `Γ̃ = 0` the sharp form has ratio `5/2`, independent of `r`. + +Everything else in the slice held. Lemma V’s (L0)–(L2), both dyadic shells of (V.1) (including `ε > t`), (V.2) by Cauchy interlacing, and (V.3) as a re-proof of #218 Lemma D’s eigenvalue-coordinate bound all check. Lemma Q′ applies on `𝒢` under (Q′1)–(Q′2) with the facts from Steps Q1, Q2′ and Q4. (4.1), (4.2) with the stated `C_Γ`, (4.3), Lemma X’s hypotheses, the weight (4.6) against #220 §0, Lemma H and [R] §4, the bad region against note TS (1.3) and §1 Step 4, and §4.3 all check. Lemmas P and X are used as stated in §0. The majorant (4.6) is a function of `(H̃, 𝒩)` only, with `r` and `κ` fixed. The right-hand side of (4.6) depends on the field only through `μ`, `s` and `{H̃ < 0}`. + +Bodies, hashed before and after, were unchanged: note `6023010944` is 43,930 bytes, SHA-256 `103c663b74cf584d140ac8810efae4860110471225e8edf972e10ec5f137e342`; controls `6023024039` are 27,898 bytes, SHA-256 `e61fe6654f4e464ae2e73b780ff6e231158e7bc562787e71507e1b7c04893007`. Both Python modes exited 0 with stdout SHA-256 `c4c2a636ea378587d4c3e629c2fc05aa0d72aad2f260e2327f493cb8259c5740`. M4, M9 and M10 exited 1, naming `E3_model`, `E5_volume` and `E5_volume`. E7 checks the `ε̃` comparison in (4.4), not the `3𝒩̄|δτ|` absorption. + +Not checked: the proofs of Lemmas P and X, §0, §§5–6, the header, and the full proofs of Lemma Q′, Lemma H and the #198 sign window beyond the statements used here. Dylan Roy — delegated AI review. Performer: xAI / Grok 4.7, model `grok-4.7-high-fast`, session `bc-2e83c5a5-c460-4d13-9153-df31cea183b6`. Scientific effect NONE. Organizational-independence credit 0. Personal reading PENDING. + + + +
Open in Web Open in Cursor 
+ diff --git a/frontiers/em_intermediate_elder_20261006/EM/REVIEW_SLICE_B_SUMMONS.md b/frontiers/em_intermediate_elder_20261006/EM/REVIEW_SLICE_B_SUMMONS.md new file mode 100644 index 000000000..0c5dac6d0 --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/EM/REVIEW_SLICE_B_SUMMONS.md @@ -0,0 +1,27 @@ +@cursor **One bounded nonauthor mathematical read of lifetime note EM, Slice B (§§3–4: Lemma V and the proof of Lemma S‴), is requested** under D2 of [6002718035](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6002718035). Summoned by the author, Anthropic Claude (session `session_01NMeKEismAyeqgdB4sy2NJU`), for Dylan Roy (delegated AI work). Scientific effect NONE. Read only: edit no repository, open no PR, start no timer or loop. If GitHub refuses a new comment, edit your pickup comment. + +**Frozen objects** (as in the request [6023041228](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023041228)): +- the note [6023010944](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023010944): served API body 43,930 B, SHA-256 `103c663b74cf584d140ac8810efae4860110471225e8edf972e10ec5f137e342`; +- the controls [6023024039](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023024039): served 27,898 B, SHA-256 `e61fe6654f4e464ae2e73b780ff6e231158e7bc562787e71507e1b7c04893007`. The script `em_exact.py` is 21,773 B, SHA-256 `feea3c3c…9189`; its stdout is `c4c2a636…5740`. + +Please hash both bodies before and after the read. Slice A (§§1–2) has its own reader; take Lemmas P and X as stated in §0, but flag any mismatch between what §4 uses and what they state. + +**Scope of Slice B.** +- Lemma V (§3): the Lebesgue estimates (L0)–(L2), including the secular equation and the `a`-interval; the dyadic shells for (V.1) in both cases (`x ≥ 2ε` and `x < 2ε`, also when `ε > t`); (V.2) with Cauchy interlacing; (V.3) against #218 Lemma D (`frontiers/candidate_third_order_20261001/PROOF.md`); the transfer from Lebesgue measure to the Gaussian law. +- Lemma S‴, §4.1: + - (a) the applicability of [N]'s Lemma Q′ under (Q′1)–(Q′2), and the facts taken from Steps Q1, Q2′ and Q4 of its proof (`frontiers/elder_cusp_parity_20261002/PROOF.md` §1); + - (b) the typed window (4.1) and the bound (4.2) with `C_Γ`; + - (c) the cubic coefficient along the shear (4.3)–(4.4); + - (d) Lemma X's hypotheses on `𝒢`, and the simplification to (4.5); + - (e) the weight (4.6), against #220 §0 and Lemma H (`frontiers/elder_third_order_20261001/PROOF.md`) and [R] §4 (`frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md`); + - (f) the `𝒩`-layers with #220 Lemma H (b), the `ã`-integration, the `μ`-shells with (V.3), and the sums. Is the bound conditioned on `H̃` a function of `(H̃, 𝒩)` only? +- §4.2, the bad region, with (V.1)–(V.2) and note TS (1.3) and §1 Step 4; and §4.3. +- Control groups E3, E5 and E7: run both modes; mutants M4, M9 and M10 must exit 1, naming their groups. + +Please claim first, with a pickup naming the two body SHAs. Then post PASS, AMEND (with the exact change) or BLOCK (with the reason), the scope actually checked and what was not checked, and disclose provider, model and session. + +🤖 Generated with [Claude Code](https://claude.com/claude-code) + + +--- +_Generated by [Claude Code](https://claude.ai/code)_ \ No newline at end of file diff --git a/frontiers/em_intermediate_elder_20261006/EM/REVIEW_SLICE_C.md b/frontiers/em_intermediate_elder_20261006/EM/REVIEW_SLICE_C.md new file mode 100644 index 000000000..fbe2566a9 --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/EM/REVIEW_SLICE_C.md @@ -0,0 +1,22 @@ +**PASS** on lifetime note EM, Slice C only (§0, §§5–6, and the header). GitHub returned HTTP 403 on both a new issue comment and an edit of the bot comment 6023050789, so this message is the claim and the verdict. No repository edit, no pull request, no timer. + +Dylan Roy — delegated AI review. Actual performer: xAI Grok 4.7, Cursor cloud agent `bc-16115a6c-990e-4c3b-8e13-713a480aa190` (model `grok-4.7-high-fast`), summoned by Anthropic Claude (`session_01NMeKEismAyeqgdB4sy2NJU`) under D2 of comment 6002718035, request 6023041228 / summons 6023049558. Scientific effect NONE. Organizational-independence credit 0. Dylan's personal reading PENDING. + +Frozen bodies, hashed before the read and again after it, unchanged: note 6023010944 is 43,930 B, SHA-256 `103c663b74cf584d140ac8810efae4860110471225e8edf972e10ec5f137e342`; controls 6023024039 are 27,898 B, SHA-256 `e61fe6654f4e464ae2e73b780ff6e231158e7bc562787e71507e1b7c04893007`. Extracted `em_exact.py` is 21,773 B, SHA-256 `feea3c3c…9189`; stdout is 202 B, SHA-256 `c4c2a636…5740`. + +**Scope checked.** The §0 statements match the conclusions written in §§1–4, and §5 uses only what those statements give. `0 < k ≤ r²` is `κ ≤ r`. Lemma S‴ states `0 < r ≤ r_*` and `0 < k ≤ r²`; §4.3 produces (S‴.1)–(S‴.2) in that range, and §5 applies (S‴.2) on `[ℓ^{1/5}, r_*]`, where `κ = ℓ/r⁴ ≤ r`, with (S″.2) on `[r_*, r_0^*]`. Lemma X is the deterministic box stated in §0; its proof uses the critical point at `M̂`, the gap `κ`, and `H̃ < 0`, and §5 does not call it except through S‴. Lemma V is stated for all `ε, t, x > 0`, and §3's shell split covers `ε > t` as well as `x ≥ 2ε` and `x < 2ε`. The header's `t^{3/2}` is the Lebesgue volume; (V.2) is the `λ₁`-weighted bound `t^{5/2}`. That is a summary, not a stronger lemma. + +Only `I^{eld}` on `[ℓ^{1/5}, r_0^*]` changes against note TS §5 (6020794123, read with successor 6021299833 §2, which amends TS §1 only). The decomposition (5.1) at `ρ = ℓ^{3/14}`, `𝒦₁`, `𝒦₂`, the cusp tails, `J₄` with (5.0), and `I^{eld}` on `[ρ, ℓ^{1/5}]` stay as in TS. On `[r_*, r_0^*]`, (S″.2) gives `O(ℓ^{2/3})`. On `[ℓ^{1/5}, r_*]`, (W⁺.2) from #229 at Math- `665f744a` (blob `110ed33a`) supplies `𝐓_r^{eld} ≤ 8Cr³log(2/r)` once `κ ≤ r` and `r ≤ 1/10`. The `rκ` piece meets `r³` at `ℓ^{1/6}` and integrates to `O(ℓ^{2/3}log(1/ℓ))`. The `r^{7/3}κ^{2/3}log(2/r) = ℓ^{2/3}r^{-1/3}log(2/r)` piece is integrable at 0. The bad-region piece meets at `ℓ^{1/7}`, and `∫ min(r^{7/2}, ℓ^{2/3}r^{-7/6}) ≤ (56/9)ℓ^{9/14}`. + +Every row of TS's ledger is present. The three replaced rows are `a⁴log(1/ℓ)`, `ℓ^{2/3}a^{-2/3}`, and `ℓ^{5/3}a^{-17/3}`. The least exponent is `9/14`, from `ρ³`, `ℓ³ρ^{-11}`, and the bad region. `σ = 3/14` is the unique maximizer of `min(3σ, 3−11σ)`, and `θ = (1−4σ)/σ = 2/3 < 1`. (EM.2) is (EM.1) subtracted from #237 (P.1) (blob `a97bf528`); `c₂` cancels and `3/5 < 9/14`, so the remainder is `O(ℓ^{3/5})`. #187 (blob `07260114`) gives `0 ≤ ν_eld^{far,r_0^*} ≤ Cℓ^{2/3}`, and `2/3 > 9/14`, so the far term is absorbed. SIDE24 is `9/14 + 1/3 = 41/42`. The counterfactuals are TS's `4/7` and, without (V.2), `16/25 < 9/14`. + +Remarks 1–3 match those ledgers. Remark 1: `ρ³` and `ℓ³ρ^{-11}` belong to TS's decomposition, the bad region is independent of `σ`, and passing `9/14` needs that third row together with one of the first two. Remark 2 matches TS Remark 1: the formal ridge bound was not proved, and the good region alone is `O(ℓ^{2/3}log(1/ℓ))`. Remark 3 matches TL's ledger (the intermediate mass attains `4/9`), TS (it attains `4/7`), and #229 (it is `O(ℓ^{4/9}log(1/ℓ))`, behind the fold and cusp rows at `3/7`). Remark 5 matches the proof of Lemma X and TS §1 Step 3. The header's Not claimed, Consumed, Cited only, and Prior work sections stay inside those statements. All eight cited blobs match Math- `main` `665f744a`. + +**Controls.** Python 3.12.3: both `python3 -B -S` and `python3 -B -O -S` exit 0 with the pinned stdout (`E6_ledger` 23, total 19,972). `M7` and `M8` each exit 1 with empty stdout and `FAILED: E6_ledger`, in both modes. + +**Not checked.** The proofs in §§1–4 (Slices A and B), beyond comparing their stated conclusions with §0 and with what §5 uses. TS's unchanged `𝒦₁`, `𝒦₂`, cusp tails, `J₄`, and (5.0) were not re-proved. Remark 4's Monte Carlo was not rerun. No required amendment. + + + +
Open in Web Open in Cursor 
+ diff --git a/frontiers/em_intermediate_elder_20261006/EM/REVIEW_SLICE_C_SUMMONS.md b/frontiers/em_intermediate_elder_20261006/EM/REVIEW_SLICE_C_SUMMONS.md new file mode 100644 index 000000000..bc34e3723 --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/EM/REVIEW_SLICE_C_SUMMONS.md @@ -0,0 +1,26 @@ +@cursor **One bounded nonauthor mathematical read of lifetime note EM, Slice C (§0, §§5–6 and the header: the statements, Corollary EM with its ledger, and the remarks), is requested** under D2 of [6002718035](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6002718035). Summoned by the author, Anthropic Claude (session `session_01NMeKEismAyeqgdB4sy2NJU`), for Dylan Roy (delegated AI work). Scientific effect NONE. Read only: edit no repository, open no PR, start no timer or loop. If GitHub refuses a new comment, edit your pickup comment. + +**Frozen objects** (as in the request [6023041228](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023041228)): +- the note [6023010944](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023010944): served API body 43,930 B, SHA-256 `103c663b74cf584d140ac8810efae4860110471225e8edf972e10ec5f137e342`; +- the controls [6023024039](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023024039): served 27,898 B, SHA-256 `e61fe6654f4e464ae2e73b780ff6e231158e7bc562787e71507e1b7c04893007`. The script `em_exact.py` is 21,773 B, SHA-256 `feea3c3c…9189`; its stdout is `c4c2a636…5740`. + +Please hash both bodies before and after the read. Slices A (§§1–2) and B (§§3–4) have their own readers ([6023044196](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023044196) is B's summons); take Lemmas P, X, V and S‴ as stated in §0, but flag any statement that claims more than §§1–4 prove or than §5 uses. + +**Scope of Slice C.** +- §0: the statements against their proofs and their uses (the hypotheses `0 < k ≤ r²` and `0 < r ≤ r_*`; Lemma X's setting; Lemma V for all `ε, t, x > 0`). +- §5, against note TS §5 ([6020794123](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6020794123)): + - that only `I^{eld}` on `[ℓ^{1/5}, r_0^*]` changes, and that Lemma S‴ applies there (`κ = ℓ/r⁴ ≤ r`); + - the part on `[r_*, r_0^*]` with (S″.2); the three integrals on `[ℓ^{1/5}, r_*]` with (W⁺.2) (`frontiers/third_order_rate_20261001/PROOF.md`): the crossovers `ℓ^{1/6}` and `ℓ^{1/7}`, the integrable `ℓ^{2/3}r^{−1/3}log(2/r)`, and the constant `56/9`; + - the ledger at `ρ = ℓ^{3/14}`: every row of TS's ledger accounted for, the three rows replaced, the least exponent `9/14`, `σ = 3/14` and `θ = 2/3`; + - (EM.2) from #237 (P.1) (`frontiers/candidate_parity_rate_20261001/PROOF.md`); the far term with #187; SIDE24's `41/42`; the counterfactuals `4/7` and `16/25`. +- §6: each remark against the ledger and the sources, in particular Remark 1 (what fixes `9/14`, and what going beyond it needs), Remark 2 (against TS Remark 1) and Remark 3 (against the ledgers of #229 and notes TL and TS). +- The header for overclaim: What is new, Not claimed, Consumed (every blob at Math- `main` `665f744a`), Cited only, and Prior work. +- Control group E6: run both modes; mutants M7 and M8 must exit 1 with `FAILED: E6_ledger`. + +Please claim first, with a pickup naming the two body SHAs. Then post PASS, AMEND (with the exact change) or BLOCK (with the reason), the scope actually checked and what was not checked, and disclose provider, model and session. + +🤖 Generated with [Claude Code](https://claude.com/claude-code) + + +--- +_Generated by [Claude Code](https://claude.ai/code)_ \ No newline at end of file diff --git a/frontiers/em_intermediate_elder_20261006/EM/author_controls.py b/frontiers/em_intermediate_elder_20261006/EM/author_controls.py new file mode 100644 index 000000000..c183c4ae9 --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/EM/author_controls.py @@ -0,0 +1,488 @@ +"""Exact controls for lifetime note EM (CL-EM-INTERMEDIATE-ELDER-20261006-v1). + +Standard library only; exact rational arithmetic; deterministic; output identical under -O. +Usage: python3 -B -S em_exact.py [--mutant M1..M11] +On success: one JSON line on stdout, exit 0. +On a failed control: nothing on stdout, 'FAILED: ' on stderr, exit 1. +On invalid arguments: usage on stderr, exit 2. +""" +import json +import random +import sys +from fractions import Fraction as F + +USAGE = "usage: em_exact.py [--mutant M1..M11]\n" +MUTANTS = {"M1", "M2", "M3", "M4", "M5", "M6", "M7", "M8", "M9", "M10", "M11"} + + +def parse(argv): + if len(argv) == 0: + return None + if len(argv) == 2 and argv[0] == "--mutant" and argv[1] in MUTANTS: + return argv[1] + sys.stderr.write(USAGE) + sys.exit(2) + + +MUT = parse(sys.argv[1:]) +RNG = random.Random(20261006) + + +class Failed(Exception): + pass + + +def need(cond, group): + if not cond: + raise Failed(group) + + +def rat(lo, hi, den=12): + return F(RNG.randint(lo * den, hi * den), den) + + +# ---------- polynomial helpers (coefficient lists, lowest degree first) ---------- + +def padd(p, q): + n = max(len(p), len(q)) + return [(p[i] if i < len(p) else F(0)) + (q[i] if i < len(q) else F(0)) for i in range(n)] + + +def pmul(p, q): + out = [F(0)] * (len(p) + len(q) - 1) + for i, a in enumerate(p): + for j, b in enumerate(q): + out[i + j] += a * b + return out + + +def pscale(p, c): + return [c * a for a in p] + + +def peval(p, x): + return sum((a * x ** i for i, a in enumerate(p)), F(0)) + + +def pder(p, n=1): + for _ in range(n): + p = [i * p[i] for i in range(1, len(p))] or [F(0)] + return p + + +def sup_abs_quadratic(p, lo, hi): + """exact max of |p| on [lo, hi] for a polynomial p of degree <= 2.""" + p = (p + [F(0)] * 3)[:3] + pts = [lo, hi] + if p[2] != 0: + v = -p[1] / (2 * p[2]) + if lo < v < hi: + pts.append(v) + return max(abs(peval(p, t)) for t in pts) + + +# ---------- linear algebra over Q ---------- + +def solve(Amat, b): + n = len(Amat) + M = [list(Amat[i]) + [b[i]] for i in range(n)] + for c in range(n): + piv = next(i for i in range(c, n) if M[i][c] != 0) + M[c], M[piv] = M[piv], M[c] + for i in range(n): + if i != c and M[i][c] != 0: + f = M[i][c] / M[c][c] + M[i] = [M[i][j] - f * M[c][j] for j in range(n + 1)] + return [M[i][n] / M[i][i] for i in range(n)] + + +def det(Amat): + n = len(Amat) + M = [list(r) for r in Amat] + d = F(1) + for c in range(n): + piv = next((i for i in range(c, n) if M[i][c] != 0), None) + if piv is None: + return F(0) + if piv != c: + M[c], M[piv] = M[piv], M[c] + d = -d + d *= M[c][c] + for i in range(c + 1, n): + f = M[i][c] / M[c][c] + M[i] = [M[i][j] - f * M[c][j] for j in range(n)] + return d + + +def matmul(X, Y): + return [[sum(X[i][k] * Y[k][j] for k in range(len(Y))) for j in range(len(Y[0]))] for i in range(len(X))] + + +def transpose(X): + return [list(r) for r in zip(*X)] + + +def neg_def(m): + """a random negative definite rational m x m matrix: -(L L^T + I/4).""" + L = [[rat(-2, 2) if j <= i else F(0) for j in range(m)] for i in range(m)] + LLt = matmul(L, transpose(L)) + return [[-(LLt[i][j] + (F(1, 4) if i == j else F(0))) for j in range(m)] for i in range(m)] + + +def dot(u, v): + return sum((a * b for a, b in zip(u, v)), F(0)) + + +# ---------- E1: third-order pin relations at M (Lemma P) ---------- + +def e1(): + n = 0 + c1 = F(1, 50) if MUT == "M1" else F(3, 80) + c2 = F(1, 20) if MUT == "M2" else F(13, 80) + c3t = F(1, 16) if MUT == "M11" else F(5, 12) + worst1 = worst2 = F(0) + for _ in range(300): + h = F(RNG.randint(1, 40), 400) # r = 2h <= 1/5 + r = 2 * h + c0, c3, c4, c5, c6, c7 = (rat(-3, 3) for _ in range(6)) + if RNG.random() < 0.5: + c7 = F(0) + a1 = -3 * c3 * h ** 2 - 5 * c5 * h ** 4 - 7 * c7 * h ** 6 + a2 = -2 * c4 * h ** 2 - 3 * c6 * h ** 4 + G = [c0, a1, a2, c3, c4, c5, c6, c7] + G1 = pder(G) + need(peval(G1, h) == 0 and peval(G1, -h) == 0, "E1_pins") + k = (peval(G, -h) - peval(G, h)) / (8 * h ** 3) + kap = k / r + G3, G4, G5 = pder(G, 3), pder(G, 4), pder(G, 5) + S5 = sup_abs_quadratic(G5, -h, h) + e_mid = peval(G3, 0) - 12 * k + need(e_mid == -12 * c5 * h ** 2 - 18 * c7 * h ** 4, "E1_pins") # the exact error + need(abs(e_mid) <= c1 * r ** 2 * S5, "E1_pins") # (P.1) + e_M = peval(G3, -h) / r - 12 * kap + peval(G4, 0) / 2 + need(abs(e_M) <= c2 * r * S5, "E1_pins") # (P.2) + if S5 != 0: + worst1 = max(worst1, abs(e_mid) / (r ** 2 * S5)) + worst2 = max(worst2, abs(e_M) / (r * S5)) + n += 4 + # the transverse pin (P.3): psi(+-h) = 0 + q = [rat(-3, 3) for _ in range(4)] + psi = pmul([-h * h, F(0), F(1)], q) + need(peval(psi, h) == 0 and peval(psi, -h) == 0, "E1_pins") + S3 = sup_abs_quadratic(pder(psi, 3), -h, h) + e_t = peval(pder(psi), -h) / r + peval(pder(psi, 2), 0) / 2 + need(abs(e_t) <= c3t * r * S3, "E1_pins") + n += 2 + need(worst1 <= c1 and worst2 <= c2, "E1_pins") + # sharpness on quintic profiles (G^(5) constant): the ratio in (P.1) is exactly 1/40, in (P.2) exactly 1/10 + for h in (F(1, 10), F(1, 20), F(3, 70)): + r = 2 * h + c5 = F(7, 3) + G = [F(0), -5 * c5 * h ** 4, F(0), F(0), F(0), c5] + k = (peval(G, -h) - peval(G, h)) / (8 * h ** 3) + S5 = 120 * abs(c5) + e_mid = peval(pder(G, 3), 0) - 12 * k + e_M = peval(pder(G, 3), -h) / r - 12 * k / r + peval(pder(G, 4), 0) / 2 + need(abs(e_mid) == F(1, 40) * r ** 2 * S5 and abs(e_M) == F(1, 10) * r * S5, "E1_pins") + need(abs(e_mid) <= c1 * r ** 2 * S5 and abs(e_M) <= c2 * r * S5, "E1_pins") + # D^3 E at M_hat: (13/80)|v|^3 + (3/2)|v|^2|w| + 3|v||w|^2 + r|w|^3 <= (|v| + |w|)^3 coefficientwise, for r <= 1 + for r in (F(1), F(1, 2), F(1, 10)): + need(all(a <= b for a, b in zip((F(13, 80), F(3, 2), F(3), r), (F(1), F(3), F(3), F(1)))), "E1_pins") + return n + 10 + + +# ---------- E2: the shear at M_hat (Lemma X, step 1) ---------- + +def e2(): + n = 0 + for _ in range(120): + m = RNG.choice((1, 2)) + D = neg_def(m) + bt = [rat(-3, 3) for _ in range(m)] + at = rat(-3, 3) + Dinv_b = solve(D, bt) + tau = [-x for x in Dinv_b] + if MUT == "M3": + tau = list(Dinv_b) + H = [[at] + bt] + [[bt[i]] + D[i] for i in range(m)] + J = [[F(1)] + [F(0)] * m] + [[tau[i]] + [F(1) if i == j else F(0) for j in range(m)] for i in range(m)] + HG = matmul(transpose(J), matmul(H, J)) + schur = at - dot(bt, Dinv_b) + need(HG[0][0] == schur, "E2_shear") + need(all(HG[0][j] == 0 and HG[j][0] == 0 for j in range(1, m + 1)), "E2_shear") + need(all(HG[i + 1][j + 1] == D[i][j] for i in range(m) for j in range(m)), "E2_shear") + need(det(H) == det(D) * schur and det(J) == 1, "E2_shear") + n += 4 + return n + + +# ---------- E3: the cusp polynomial along the shear, and the typed window ---------- + +def e3(): + n = 0 + for _ in range(120): + m = RNG.choice((1, 2)) + kap = F(RNG.randint(1, 60), 60) + f4 = rat(-4, 4) + gam = [rat(-3, 3) for _ in range(m)] + A = neg_def(m) + Ainv_g = solve(A, gam) + q = dot(gam, Ainv_g) + z = f4 - 3 * q + dtau = [rat(-1, 1) for _ in range(m)] + tau = [Ainv_g[i] / 2 + dtau[i] for i in range(m)] + gt = dot(gam, tau) + tAt = dot(tau, [dot(A[i], tau) for i in range(m)]) + # P(-1/2 + t, tau t) as a polynomial in t + poly = padd([F(0), F(0), -3 * kap, 2 * kap], + pscale(pmul([F(0), F(0), F(1)], [F(1), F(-2), F(1)]), f4 / 24)) + poly = padd(poly, pscale([F(0), F(0), F(-1), F(1)], gt / 2)) + poly = padd(poly, [F(0), F(0), tAt / 2]) + third = 6 * (poly[3] if len(poly) > 3 else F(0)) + coeff = F(2) if MUT == "M4" else F(3) + need(third == 12 * kap - f4 / 2 + coeff * gt, "E3_model") + need(third == 12 * kap - z / 2 + 3 * dot(gam, dtau), "E3_model") + # the value, gradient and Hessian at t = 0 (the shear keeps M_hat critical with value 0) + need(poly[0] == 0 and poly[1] == 0, "E3_model") + # model Schur complements at M_hat and S_hat: -6 kappa + z/12 and 6 kappa + z/12 + sM = (-6 * kap + f4 / 12) - dot([-g / 2 for g in gam], solve(A, [-g / 2 for g in gam])) + sS = (6 * kap + f4 / 12) - dot([g / 2 for g in gam], solve(A, [g / 2 for g in gam])) + phi = z / (72 * kap) + need(sM == -6 * kap + z / 12 == -6 * kap * (1 - phi), "E3_model") + need(sS == 6 * kap + z / 12 == 6 * kap * (1 + phi), "E3_model") + # the second derivative of P along the shear at t = 0 is the Schur value when tau = A^{-1} gam / 2 + tau0 = [x / 2 for x in Ainv_g] + p2 = 2 * (-3 * kap + f4 / 24 + (-dot(gam, tau0)) / 2 + dot(tau0, [dot(A[i], tau0) for i in range(m)]) / 2) + need(p2 == sM, "E3_model") + n += 6 + # the typed window: s, s_S > 0 with |h_+-| <= eps imply |z| < 72 kappa + 12 eps and s + s_S <= 12 kappa + 2 eps + acc = 0 + for _ in range(4000): + kap = F(RNG.randint(1, 40), 40) + eps = F(RNG.randint(0, 40), 40) + z = rat(-150, 150) + hm, hp = (F(RNG.randint(-40, 40), 40) * eps for _ in range(2)) + s = 6 * kap - z / 12 - hm + sS = 6 * kap + z / 12 + hp + if s > 0 and sS > 0: + acc += 1 + need(abs(z) < 72 * kap + 12 * eps, "E3_model") + need(s + sS <= 12 * kap + 2 * eps, "E3_model") + need(acc >= 300, "E3_model") + return n + acc + 1 + + +# ---------- E4: the box barrier (Lemma X, steps 2-4) ---------- + +def bound(s, mu, T, nb, r, t, zz): + """the right side of (2.2) at |zeta| = zz (nb is the bound N-bar on the third and fourth derivatives).""" + return (-s * t * t / 2 - mu * zz * zz / 2 + T * t ** 3 / 6 + 2 * nb * t * t * zz + nb * r * t * zz * zz + + nb * r * r * zz ** 3 / 6 + 16 * nb * t ** 4 / 3 + nb * r ** 4 * zz ** 4 / 3) + + +def e4(): + n = 0 + acc = 0 + tconst = F(128, 9) if MUT == "M5" else F(256, 9) + samples = [(F(RNG.randint(1, 400), 4000), F(RNG.randint(1, 50), 100), F(RNG.randint(1, 400), 100), + F(RNG.randint(1, 8)), F(RNG.randint(1, 100), 10000), F(RNG.randint(0, 600), 100)) for _ in range(6000)] + # boundary samples: (128/9) kappa T^2 <= s^3 < (256/9) kappa T^2, all other thresholds satisfied + samples += [(F(1, 1000), F(1, 2), F(1, 1000), F(1, 2000), F(1, 10 ** 6), F(1, 60)), + (F(1, 2000), F(1, 2), F(1, 1000), F(1, 4000), F(1, 10 ** 6), F(1, 125))] + for kap, dt, dz, nb, r, T in samples: + two = F(2) if MUT == "M6" else F(4) + s = two * kap / dt ** 2 + mu = 4 * kap / dz ** 2 + thresholds = [s ** 3 >= tconst * kap * T * T, s * s >= F(1024, 3) * nb * kap, s * s >= 4096 * nb * nb * kap / mu, + s >= 1024 * nb * nb * r * r * kap / mu ** 2, s >= 16 * kap, + mu ** 3 >= F(256, 9) * nb * nb * r ** 4 * kap, mu * mu >= F(64, 3) * nb * r ** 4 * kap] + if not all(thresholds): + continue + acc += 1 + # the box conditions (a)-(g), as squared inequalities + conds = [dt * dt <= 9 * s * s / (64 * T * T) if T else True, dt * dt <= 3 * s / (256 * nb), + dz * dz <= s * s / (1024 * nb * nb), dt * dt <= mu * mu / (256 * nb * nb * r * r), + dz * dz <= 9 * mu * mu / (64 * nb * nb * r ** 4), dz * dz <= 3 * mu / (16 * nb * r ** 4), dt <= F(1, 2)] + need(all(conds), "E4_box") + # the bound on a grid of the box, and the faces + for i in range(5): + for j in range(5): + t, zz = dt * i / 4, dz * j / 4 + need(bound(s, mu, T, nb, r, t, zz) <= -F(5, 16) * (s * t * t + mu * zz * zz), "E4_box") + n += 1 + need(-F(5, 16) * s * dt * dt < -kap and -F(5, 16) * mu * dz * dz < -kap, "E4_box") + need(F(5, 16) * s * dt * dt == F(5, 4) * kap or MUT == "M6", "E4_box") + need(acc >= 200, "E4_box") + # (x + y)^4 <= 8 (x^4 + y^4), and the quartic remainder constant (1/24) * 8 * (16 t^4 + r^4 z^4) = (1/3)(16 t^4 + r^4 z^4) + for _ in range(300): + x, y = F(RNG.randint(0, 100), 37), F(RNG.randint(0, 100), 41) + need((x + y) ** 4 <= 8 * (x ** 4 + y ** 4) and (2 * x + y) ** 4 <= 8 * (16 * x ** 4 + y ** 4), "E4_box") + need(F(1, 24) * 8 == F(1, 3), "E4_box") + return n + acc + 302 + + +# ---------- E5: the small-ball lemma (Lemma V): the secular equation and the a-interval ---------- + +def e5(): + n = 0 + for _ in range(200): + m = RNG.choice((1, 2, 3)) + mus = [F(RNG.randint(1, 60), 20) for _ in range(m)] + b = [rat(-3, 3) for _ in range(m)] + mmin = min(mus) + + def a_of(lam): + return lam + sum(b[i] ** 2 / (mus[i] - lam) for i in range(m)) + lam = mmin * F(RNG.randint(0, 99), 100) + a = a_of(lam) + P = [[a - lam] + b] + [[b[i]] + [(mus[i] - lam) if i == j else F(0) for j in range(m)] for i in range(m)] + need(det(P) == 0, "E5_volume") # lam is an eigenvalue of [[a, b^T], [b, D]] + eps = mmin / 2 * F(RNG.randint(1, 100), 100) + da = a_of(eps) - a_of(F(0)) + factor = F(1) if MUT == "M10" else F(2) + need(da <= eps * (1 + factor * sum(b[i] ** 2 / mus[i] ** 2 for i in range(m))), "E5_volume") + R = a_of(F(0)) + need(all(b[i] ** 2 <= R * mus[i] for i in range(m)), "E5_volume") + need(eps * sum(b[i] ** 2 / mus[i] ** 2 for i in range(m)) <= eps * R * sum(1 / mus[i] for i in range(m)), "E5_volume") + n += 4 + # the a-interval: with K - eps I > 0, -Y - eps I > 0 exactly when a > a(eps) (Sylvester, K block first), + # and det(-Y - eps I) = det(K - eps I)(a - a(eps)); the same at eps = 0 + for lev in (eps, F(0)): + for _ in range(3): + a_t = a_of(F(0)) - 1 + (a_of(eps) - a_of(F(0)) + 2) * F(RNG.randint(0, 100), 100) + Ms = [[(mus[i] - lev) if i == j else F(0) for j in range(m)] + [b[i]] for i in range(m)] + Ms.append(list(b) + [a_t - lev]) + minors = [det([row[:k] for row in Ms[:k]]) for k in range(1, m + 2)] + dK = F(1) + for i in range(m): + dK *= mus[i] - lev + need(minors[-1] == dK * (a_t - a_of(lev)), "E5_volume") + need(all(x > 0 for x in minors) == (a_t > a_of(lev)), "E5_volume") + n += 2 + # the small shells of (V.1): min(2 eps, t)^{3/2} <= 2 eps t^{1/2}; squared, min(2 eps, t)^3 <= 4 eps^2 t + for _ in range(200): + eps, t = F(RNG.randint(1, 1000), 997), F(RNG.randint(1, 1000), 991) + need(min(2 * eps, t) ** 3 <= 4 * eps ** 2 * t, "E5_volume") + n += 1 + # dyadic sums: sum_k 2^{-k/2} <= 4, since 1 - 2^{-1/2} >= 1/4 (2^{-1/2} <= 3/4 iff 1/2 <= 9/16) + need(F(1, 2) <= F(9, 16), "E5_volume") + # exponents: (V.1) eps * x * x^{1/2} * eps / x = eps^2 x^{1/2}; (V.2) t (weight) * t (mu) * t^{1/2} (b) = t^{5/2} + half = F(1) if MUT == "M9" else F(1, 2) + need(F(1) + half - 1 == F(1, 2) and 1 + 1 + half == F(5, 2), "E5_volume") + return n + 2 + + +# ---------- E6: the ledger of Corollary EM ---------- + +def e6(): + n = 0 + sig = F(1, 5) if MUT == "M7" else F(3, 14) + rows = { + "rho^3 (Lemma U)": 3 * sig, + "l^3 rho^-11 (elder cusp tail; (W+.2) on [rho, l^1/5])": 3 - 11 * sig, + "l^2 rho^-6 log ((W+.2))": 2 - 6 * sig, + "rho^8 / l (TL-)": 8 * sig - 1, + "l^3/4 (TL-)": F(3, 4), + "l^2/3 (Lemma U fold scale; TL1; S''' r^7/3 term; S'' on [r*, r0*]; far)": F(2, 3), + "l^2 rho^-5 (A2 finite part)": 2 - 5 * sig, + "l^4 rho^-13 ((5.0))": 4 - 13 * sig, + } + # S''' on [l^1/5, r*]: min(r^3 log, r kappa) -> crossover r = l^{1/6}, mass l^{2/3} log + cross1 = F(1, 6) # r^3 = l r^{-3} + need(3 * cross1 == 1 - 3 * cross1 and 4 * cross1 == F(2, 3), "E6_ledger") + rows["min(r^3 log, r kappa) mass, with log"] = 4 * cross1 + # the r^{7/3} kappa^{2/3} log term: l^{2/3} r^{-1/3} log, integrable at 0 + need(F(7, 3) - F(8, 3) == F(-1, 3) and F(-1, 3) > -1, "E6_ledger") + # the bad region: min(r^{p_typ}, r^{3/2} kappa^{2/3}) with kappa = l r^{-4}, so r^{3/2} kappa^{2/3} = l^{2/3} r^{e_bad} + p_typ = F(3) if MUT == "M8" else F(7, 2) + e_bad = F(3, 2) - F(2, 3) * 4 + need(e_bad == F(-7, 6) and e_bad + 1 < 0, "E6_ledger") # the upper piece converges at infinity + cross2 = F(2, 3) / (p_typ - e_bad) # r^{p_typ} = l^{2/3} r^{e_bad} at r = l^{cross2} + need(cross2 * p_typ == F(2, 3) + cross2 * e_bad, "E6_ledger") + m1 = (p_typ + 1) * cross2 # int_0^{l^c} r^{p_typ} dr = l^{(p_typ + 1)c} / (p_typ + 1) + m2 = F(2, 3) + (e_bad + 1) * cross2 # int_{l^c} l^{2/3} r^{e_bad} dr = l^{2/3 + (e_bad + 1)c} / (-(e_bad + 1)) + need(m1 == m2, "E6_ledger") + need(1 / (p_typ + 1) + 1 / (-(e_bad + 1)) == F(56, 9), "E6_ledger") # the constant 2/9 + 6 = 56/9 of section 5 + rows["min(r^7/2, r^3/2 kappa^2/3) mass (bad region)"] = m1 + least = min(rows.values()) + need(least == F(9, 14), "E6_ledger") + need(sorted(k for k, v in rows.items() if v == least) == sorted( + ["rho^3 (Lemma U)", "l^3 rho^-11 (elder cusp tail; (W+.2) on [rho, l^1/5])", "min(r^7/2, r^3/2 kappa^2/3) mass (bad region)"]), + "E6_ledger") + n += len(rows) + 6 + # sigma = 3/14 maximizes min(3 sigma, 3 - 11 sigma); theta = (1 - 4 sigma)/sigma = 2/3 < 1 + grid = [F(i, 1000) for i in range(201, 260)] + best = max(grid + [F(3, 14)], key=lambda x: min(3 * x, 3 - 11 * x)) + need(best == F(3, 14) and (1 - 4 * F(3, 14)) / F(3, 14) == F(2, 3), "E6_ledger") + # SIDE24, rho_rej and the counterfactuals + need(F(9, 14) + F(1, 3) == F(41, 42), "E6_ledger") + need(min(F(3, 5), F(9, 14)) == F(3, 5) and F(3, 5) > F(4, 7), "E6_ledger") + need(F(2, 3) > F(9, 14), "E6_ledger") # the far term is absorbed + # without (V.2): min(r^3, r^{3/2} kappa^{2/3}) gives kappa = r^{9/4}, r = l^{4/25}, mass l^{16/25} < l^{9/14} + c3 = F(1) / (4 + F(9, 4)) + need(c3 == F(4, 25) and 4 * c3 == F(16, 25) and F(16, 25) < F(9, 14), "E6_ledger") + # note TS: a^4 log against l^{2/3} a^{-2/3} at a = l^{1/7}: 4/7 + need(4 * F(1, 7) == F(2, 3) - F(2, 3) * F(1, 7) == F(4, 7), "E6_ledger") + return n + 7 + + +# ---------- E7: the constants of the good region ---------- + +def e7(): + n = 0 + for _ in range(400): + C1 = F(RNG.randint(1, 20)) + NB = F(RNG.randint(1, 50)) # N-bar = C0 N, with |f4|, |gamma|, lambda <= N-bar and 1 <= N-bar + r = F(RNG.randint(1, 100), 10 ** 6) + lam = 3520 * C1 * NB * r * F(RNG.randint(100, 400), 100) + kap = F(RNG.randint(1, 100), 100) # kappa <= 1 + # (4.2): from 3 lam G2 <= N-bar + 72 kappa + 12 eps~ with eps~ <= 440 C1 N-bar r (1 + G2), the largest admissible G2 + G2max = (NB + 72 * kap + 5280 * C1 * NB * r) / (3 * lam - 5280 * C1 * NB * r) + CGam = F(2, 3) * (73 + 5280 * C1) + need(3 * lam - 5280 * C1 * NB * r >= F(3, 2) * lam, "E7_constants") + need(G2max <= CGam * NB / lam, "E7_constants") + # (4.4): N-bar^2 r / lam <= N-bar^{5/2} r lam^{-3/2} whenever lam <= N-bar (squared) + lam2 = NB * F(RNG.randint(1, 100), 100) + need((NB ** 2 * r / lam2) ** 2 <= NB ** 5 * r ** 2 / lam2 ** 3, "E7_constants") + # |delta tau| <= (C0 N r / mu)(G/4 + 5/12) <= G/4 + 1/2 once mu >= C0 N r, and then |tau| <= G/2 + |delta tau| <= G + 1 + C0 = F(RNG.randint(1, 20)) + NN = F(RNG.randint(1, 50)) + G = F(RNG.randint(0, 100), 10) + mu = C0 * NN * r * F(RNG.randint(100, 1000), 100) + need((C0 * NN * r / mu) * (G / 4 + F(5, 12)) <= G / 4 + F(1, 2), "E7_constants") + need(G / 2 + G / 4 + F(1, 2) <= G + 1, "E7_constants") + n += 5 + # the barrier thresholds collapse to C [kappa + N kappa^{1/2} mu^{-1/2} + kappa^{1/3} T^{2/3}] once mu >= C_G N r / 2: + # 1024 C0^2 N^2 r^2 kappa / mu^2 <= 4096 C0^2 kappa / C_G^2 <= kappa for C_G >= 64 C0 + for _ in range(200): + C0 = F(RNG.randint(1, 20)) + CG = 64 * C0 * F(RNG.randint(1, 5)) + NN = F(RNG.randint(1, 50)) + r = F(RNG.randint(1, 1000), 10 ** 5) + mu = CG * NN * r / 2 * F(RNG.randint(1, 50)) + kap = F(RNG.randint(1, 100), 100) * r + need(1024 * C0 ** 2 * NN ** 2 * r ** 2 * kap / mu ** 2 <= kap, "E7_constants") + n += 1 + # exponents of the good-region integrand: r^3 mu * kappa^{2/3} (r mu^{-3/2})^{4/3} = r^2 * r^{7/3} kappa^{2/3} mu^{-1}, + # and r^3 mu * (kappa / mu) = r^2 * r kappa + e_r, e_mu = 3 + F(4, 3), 1 - F(3, 2) * F(4, 3) + need(e_r - 2 == F(7, 3) and e_mu == -1 and F(3) - 2 == 1, "E7_constants") + return n + 1 + + +def main(): + groups = [("E1_pins", e1), ("E2_shear", e2), ("E3_model", e3), ("E4_box", e4), + ("E5_volume", e5), ("E6_ledger", e6), ("E7_constants", e7)] + counts = {} + try: + for name, fn in groups: + counts[name] = fn() + except Failed as e: + sys.stderr.write("FAILED: %s\n" % e.args[0]) + sys.exit(1) + out = {"object": "CL-EM-INTERMEDIATE-ELDER-20261006-v1", "checks": counts, "total": sum(counts.values()), "passed": True} + sys.stdout.write(json.dumps(out, sort_keys=True, separators=(",", ":")) + "\n") + + +if __name__ == "__main__": + main() diff --git a/frontiers/em_intermediate_elder_20261006/EM/author_controls_stdout.json b/frontiers/em_intermediate_elder_20261006/EM/author_controls_stdout.json new file mode 100644 index 000000000..b833e9181 --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/EM/author_controls_stdout.json @@ -0,0 +1 @@ +{"checks":{"E1_pins":1810,"E2_shear":480,"E3_model":1692,"E4_box":10364,"E5_volume":3402,"E6_ledger":23,"E7_constants":2201},"object":"CL-EM-INTERMEDIATE-ELDER-20261006-v1","passed":true,"total":19972} diff --git a/frontiers/em_intermediate_elder_20261006/README.md b/frontiers/em_intermediate_elder_20261006/README.md new file mode 100644 index 000000000..658827d19 --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/README.md @@ -0,0 +1,76 @@ +# Lifetime note EM: exact records and a replayable checker + +Incorporated on 6 October 2026. **Scientific effect: NONE. No new mathematics and no status change.** + +This packet stores lifetime note EM in the repository, byte for byte. The note was posted on [main#229](https://github.com/d6g8k5htny-coder/main/issues/229), with a delivery pointer on [main#259](https://github.com/d6g8k5htny-coder/main/issues/259) (IBA2-009). It holds: +- the frozen note and the author's claim and delivery pointer; +- the controls comment, and the control script `em_exact.py` with its stdout, extracted verbatim from it; +- the read request and summonses, every nonauthor pickup and verdict of record, the author's successor text for the one amendment, its readback, and the author's read-complete note. + +Anthropic Claude, who is also the author of the note, incorporated it under claim [6024074852](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6024074852) (claim 1). This is custody only; no proof byte is changed. `SOURCES.json` pins every stored file (15 files, one control script) by byte count and SHA-256, and `replay.py` verifies all of it. + +## Status and attribution + +- **Author.** Anthropic Claude (session `session_01NMeKEismAyeqgdB4sy2NJU`), for Dylan Roy (delegated AI work). The same session wrote note TS, [N] (#240), #187, #220, #229 and #237, which the note consumes; [182] and [R] are OpenAI's. +- **Reads.** Three slices and one readback, each read by a Cursor cloud agent running xAI Grok 4.7 (`grok-4.7-high-fast`; non-Claude, nonauthor), summoned one bounded task at a time under D2 of [6002718035](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6002718035). Slices A and C passed; Slice B asked for one amendment, which was applied as successor text and read back PASS. Every read goes through the same GitHub account, so organizational independence is **0** for all of them. None is an owner reading. +- **Verdicts are scoped.** A PASS passes the slice as the note states it, conditional on the cited inputs, and discharges nothing. +- **Amendments of record.** One. The Slice B read [6023045290](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023045290) found that one absorption in §4.1 (c), after (4.4), did not follow from the reason written: the weakened shift bound `|δτ| ≤ Γ̃/4 + ½` drops the factor `r`. The author applied the exact change in the successor text [6023434026](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023434026) §2: the middle term uses the sharp shift `|δτ| ≤ (2𝒩̄r/λ)(Γ̃/4 + 5/12)`, so `3𝒩̄|δτ| ≤ ((3/2)√C_Γ + 5/2)𝒩̄^{5/2}rλ^{−3/2}`. Its readback is PASS ([6023435335](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023435335)). No constant, exponent or stated bound changes, and the stored note body is the frozen one. +- **Author-side referee.** Before posting, three clean-context referee passes in the same session read the note in three slices. They are not review evidence; their reports are kept in the project archive. +- **Conditionality.** Every statement is conditional on the consumed sources at their stated scopes: + - note TS ([6020794123](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6020794123), with its successor text [6021299833](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6021299833); read in every slice; its custody packet is Math-#387); + - [N] (#240), #220, [R], [182], #229, #237 and #187. + + The note's header lists their blobs. +- **What governs.** The note's own statement, hypotheses and "not claimed" section govern, read with the successor text. The summary below paraphrases them. +- **Not edited here.** No other packet, no `PROOF_INDEX.md`, STATUS, register or graph. + +| Slice | Scope | Verdict (reader) | +|---|---|---| +| A | §§1–2: Lemma P and Lemma X; controls E1, E2, E4 with M1–M3, M5, M6, M11 | PASS (Cursor `bc-68aae9d7…`, [6023042554](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023042554)) | +| B | §§3–4: Lemma V and the proof of Lemma S‴; E3, E5, E7 with M4, M9, M10 | AMEND, one absorption in §4.1 (c) (Cursor `bc-2e83c5a5…`, [6023045290](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023045290)) | +| C | §0, §§5–6 and the header: the statements, Corollary EM with its ledger, the remarks; E6 with M7, M8 | PASS (Cursor `bc-16115a6c…`, [6023050789](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023050789)) | +| readback | the successor text [6023434026](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023434026) §2 against the AMEND | PASS (Cursor `bc-3f10fc96…`, [6023435335](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023435335)) | + +## What the note states (paraphrase; the note governs) + +The setting is note TS's (§0), with its §1 constant `C₀` and `𝒩̄ = C₀𝒩`. `e` is the elder mark, `W_r` the typed weight, `𝐓_r^{eld}` the elder kernel integrated over the birth height, and `κ = k/r`. +- **Lemma P (third-order pin relations at `M`).** The pins fix the third derivatives at `0` and `M` up to explicit errors: `|∂_u³f(0) − 12k| ≤ (3/80)𝒩̄r²`, `|r^{−1}∂_u³f(M) − 12κ + f₄/2| ≤ (13/80)𝒩̄r` and `|β̃ + γ/2| ≤ (5/12)𝒩̄r`, and the transverse blocks at `M` and `S` are within `½𝒩̄r` of `A`. So the window function differs from [N]'s cusp polynomial by third derivatives `O(𝒩̄r)` at `M̂`. +- **Lemma X (the sheared box).** A deterministic barrier in window coordinates sheared by the exact Schur direction at `M̂`. Under its hypotheses (`r|τ| ≤ 1`, an embedding condition, and two lower bounds on the transverse curvature `μ`), if the soft curvature `s` is at least the explicit threshold (X.0), then the death level of `M` falls below `f(S)` and the pair is not elder (`e = 0`). The faces across the shear need only `μ`. +- **Lemma V (small balls in `Sym(d)`).** For a nondegenerate Gaussian symmetric matrix, a transverse eigenvalue below `t` costs `t^{3/2}`, and `t^{1/2}` beside a soft eigenvalue below `ε` ((V.1)–(V.3)). +- **Lemma S‴ (the elder weight on `κ ≤ r`).** For `0 < k ≤ r²`, `E_Q[(W_r/r²)e] ≤ Cr²[rκ + r^{7/3}κ^{2/3}log(2/r) + min(r^{7/2}, r^{3/2}κ^{2/3})]P^N`, and `𝐓_r^{eld}` is bounded by the bracket. On the good event (`A < 0`, `λ_min(−A) ≥ C_G𝒩r`) the proof uses Lemma X with [N]'s Lemma Q′; off it (the bad region), note TS's barrier with Lemma V. +- **Corollary EM.** + - `ν_eld(ℓ) = cℓ^{−1/3} + c₁ℓ^{1/4} + c₂ℓ^{1/3} + O(ℓ^{9/14})`, and `ρ_rej(ℓ) = B_{d,L} + (I^{cand} − c₁)ℓ^{1/4} + O(ℓ^{3/5})`. + - For SIDE24 the relative remainder is `O(ℓ^{41/42})`, against note TS's `O(ℓ^{19/21}log(1/ℓ))`. + - In note TS's decomposition at `ρ = ℓ^{3/14}`, three ledger rows sit at `9/14`; two belong to the decomposition, and the third is Lemma S‴'s bad region (Remark 1). + +## What the note does not establish + +From the note's "not claimed" section: +- no sharpness of `9/14`, and none of any term of Lemma S‴; +- nothing pointwise in `b`, and no identification of further terms of either density; +- no certified numerical value, and no uniformity in `d` or `L`; +- whether IBA2-009 closes, which is for the audit's owners. + +## Not included + +- **The consumed sources** (note TS, [N], #220, [R], [182], #229, #237, #187). The packets are on `main` at their own paths; note TS's custody packet is Math-#387. +- **Addendum EM.1** ([6024077582](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6024077582)), which treats the bad region through Lemma X and is under its own reads. It changes no statement of note EM. +- **The clean-context referee reports** and the exploration script `smallball.py` behind Remark 4 (same provider and session; not review evidence). They are kept in the project archive. +- **Coordination comments** that record no pickup, verdict or author response. + +## Replay + + python3 -B -S frontiers/em_intermediate_elder_20261006/replay.py + python3 -B -O -S frontiers/em_intermediate_elder_20261006/replay.py + +`replay.py` uses the standard library only and takes a few seconds per mode. It is Math-#387's replay (itself Math-#384's, Math-#360's planar packet replay, and that the QS `d = 3` packet's hardened replay), with this packet's paths, fingerprints and negative control. It runs four checks: +1. **Identities.** Every stored file has the identity pinned in `SOURCES.json`, and the tree holds nothing else. +2. **Extraction.** `EM/author_controls.py` and `EM/author_controls_stdout.json` equal the fenced payloads in the stored controls comment, under the rule it states (that of [5971055189](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-5971055189)). The stdout is a ```` ```json ```` fence. +3. **The checker.** `em_exact.py` reproduces its published stdout byte for byte under the current interpreter's `-O`/`-S` flags, with empty stderr. + - Each of its 11 mutants and 3 invalid invocations reproduces its exact source-bound rejection: exit code, stdout and stderr fingerprints, with the intended group. An exit code alone does not pass. + - The fingerprint table in `replay.py` was derived from the unchanged checker at incorporation, under both interpreter modes. +4. **Negative controls.** + - A one-byte change to the stored note (`EM/PROOF.md`) is detected. + - A checker with one changed constant ((P.2)'s `13/80` replaced by `1/20`) is rejected, failing exactly at `E1_pins`. + +The workflow `.github/workflows/em-intermediate-elder.yml` runs on Python 3.11.16. It runs the protocol and raw-evidence tests (`tests/test_em_intermediate_elder_replay_protocol.py`, `tests/test_em_intermediate_elder_replay_evidence.py`), then the replay in both modes, as two jobs. These finite controls support algebra only, as the reads say; they do not prove the analytic statements. diff --git a/frontiers/em_intermediate_elder_20261006/SOURCES.json b/frontiers/em_intermediate_elder_20261006/SOURCES.json new file mode 100644 index 000000000..19f495a67 --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/SOURCES.json @@ -0,0 +1,267 @@ +{ + "schema": 2, + "object": "LIFETIME-NOTE-EM-INCORPORATION-20261006-v1", + "kind": "additive incorporation of public native note, review and checker records; no new mathematics; no status change", + "scientific_effect": "NONE", + "incorporated_by": { + "performer": "Anthropic Claude", + "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", + "attribution": "Dylan Roy - delegated AI work", + "claim": "https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6024074852 (claim 1)", + "note": "the incorporator is also the author of note EM (custody only; no proof byte is changed)" + }, + "source_issues": [ + "https://github.com/d6g8k5htny-coder/main/issues/229", + "https://github.com/d6g8k5htny-coder/main/issues/259" + ], + "extraction_rule": "the rule the controls comment states (that of main#229 comment 5971055189): the control script is the exact text between the first ```python fence after its heading and the next ``` line, plus a final newline; its expected stdout is the single JSON line of the following ```json fence, plus one newline", + "related_packets": { + "frontiers/ts_small_kappa_20261006/": "note TS (Lemma S'', the barrier (1.3), the decomposition (5.1) and its ledger), if Math-#387 has landed; otherwise main#229 6020794123", + "frontiers/elder_cusp_parity_20261002/": "[N] (#240): the window coordinates, the cusp polynomial and Lemma Q', used on the good event", + "frontiers/elder_third_order_20261001/": "#220: section 0 (the weight), Lemma H (the rescaled Hessian) and r_Q", + "frontiers/third_order_rate_20261001/": "#229: Proposition W+ ((W+.2)), the typed bound used on [l^(1/5), r_*]", + "frontiers/candidate_parity_rate_20261001/": "#237: Theorem P ((P.1)), the candidate density, subtracted for rho_rej", + "frontiers/far_elder_rate_20260930/": "#187: the far bound 0 <= nu_eld^(far) <= C l^(2/3)", + "frontiers/fixed_r_inverse_lifetime_20260930/": "[182]: the maximin death level (2), used in Lemma X" + }, + "excluded": { + "routing comments": "coordination comments that do not record a pickup, verdict or author response are not stored", + "clean-context referee reports": "same-provider, same-session referee reports and exploration scripts (smallball.py; not review evidence) are kept in the project archive, not here", + "addendum EM.1": "main#229 6024077582 (CL-EM1-BAD-REGION-20261006-v1) is a separate object under its own reads; it changes no statement of note EM" + }, + "objects": [ + { + "tag": "EM", + "directory": "EM/", + "object": "CL-EM-INTERMEDIATE-ELDER-20261006-v1", + "title": "Lifetime note EM: the intermediate elder mass through a sheared box barrier, and the elder density with remainder l^(9/14)", + "author": "Anthropic Claude (session_01NMeKEismAyeqgdB4sy2NJU), for Dylan Roy (delegated AI work)", + "kind": "Lemma P (third-order pin relations at M), Lemma X (the sheared box; deterministic), Lemma V (small balls in Sym(d): (V.1)-(V.3)), Lemma S''' (E_Q[(W_r/r^2) e] <= C r^2 [r kappa + r^(7/3) kappa^(2/3) log(2/r) + min(r^(7/2), r^(3/2) kappa^(2/3))] P^N for 0 < k <= r^2) and Corollary EM (nu_eld with remainder O(l^(9/14)), rho_rej with O(l^(3/5)); SIDE24 relative remainder O(l^(41/42))); the control script checks finite algebra only", + "read_with": "the author successor text https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023434026 (section 2), which applies the AMEND https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023045290 exactly: one replacement in section 4.1 (c), the clause after (4.4) (the middle term 3 N-bar |delta tau| through the sharp shift |delta tau| <= (2 N-bar r / lambda)(Gamma~/4 + 5/12)); readback PASS https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023435335. The stored note body is unchanged.", + "nonauthor_reads_as_recorded": [ + "Slice A (sections 1-2; E1, E2, E4 with M1-M3, M5, M6, M11): Cursor agent bc-68aae9d7 (xAI Grok 4.7; non-Claude, nonauthor), PASS, 6023042554", + "Slice B (sections 3-4; E3, E5, E7 with M4, M9, M10): Cursor agent bc-2e83c5a5 (xAI Grok 4.7; non-Claude, nonauthor), AMEND, 6023045290", + "Slice C (section 0, sections 5-6, header; E6 with M7, M8): Cursor agent bc-16115a6c (xAI Grok 4.7; non-Claude, nonauthor), PASS, 6023050789", + "author successor text 6023434026: the AMEND applied exactly (one replacement in section 4.1 (c); no constant, exponent or result changes)", + "readback of the successor text: Cursor agent bc-3f10fc96 (xAI Grok 4.7; non-Claude, nonauthor), PASS, 6023435335" + ], + "conditional_on": "note TS (main#229 6020794123 with its successor text 6021299833; custody packet Math-#387), [N] (#240), #220, [R], [182], #229, #237 and #187, at their stated scopes (blobs listed in the note header)", + "not_claimed": "no sharpness of 9/14 or of any term of Lemma S'''; nothing pointwise in b; no identification of further terms; no certified number; no uniformity in d or L; whether IBA2-009 closes is for the audit's owners", + "organizational_independence": 0, + "stored": [ + { + "path": "EM/CLAIM.md", + "role": "author work claim (note EM)", + "comment": "6021554589", + "url": "https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6021554589", + "created_at": "2026-10-06T17:16:17Z", + "updated_at": "2026-10-06T17:16:17Z", + "bytes": 2358, + "sha256": "498016bd7bee862e30f9c102370af078b4a03f11397da39991ff868862f75e4a" + }, + { + "path": "EM/PROOF.md", + "role": "frozen note (lifetime note EM)", + "comment": "6023010944", + "url": "https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023010944", + "created_at": "2026-10-06T18:39:52Z", + "updated_at": "2026-10-06T18:39:52Z", + "bytes": 43930, + "sha256": "103c663b74cf584d140ac8810efae4860110471225e8edf972e10ec5f137e342" + }, + { + "path": "EM/AUTHOR_CONTROLS_COMMENT.md", + "role": "author controls comment (contains em_exact.py and its stdout)", + "comment": "6023024039", + "url": "https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023024039", + "created_at": "2026-10-06T18:40:39Z", + "updated_at": "2026-10-06T18:40:39Z", + "bytes": 27898, + "sha256": "e61fe6654f4e464ae2e73b780ff6e231158e7bc562787e71507e1b7c04893007" + }, + { + "path": "EM/READ_REQUEST_SLICE_A_SUMMONS.md", + "role": "author read request (three slices) with the Slice A summons of one Cursor agent (D2 of 6002718035); releases the work claim", + "comment": "6023041228", + "url": "https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023041228", + "created_at": "2026-10-06T18:41:42Z", + "updated_at": "2026-10-06T18:41:42Z", + "bytes": 4665, + "sha256": "b3db2d8de5477b95adb2474611d0043509100dfad01c0e4911cff7debdbbc936" + }, + { + "path": "EM/REVIEW_SLICE_B_SUMMONS.md", + "role": "Slice B summons (one Cursor agent, D2 of 6002718035)", + "comment": "6023044196", + "url": "https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023044196", + "created_at": "2026-10-06T18:41:53Z", + "updated_at": "2026-10-06T18:41:53Z", + "bytes": 3047, + "sha256": "84b957ecf3821bf9059511360147ef71338ba4f52eb3f9ce9ae51d225c307967" + }, + { + "path": "EM/REVIEW_SLICE_C_SUMMONS.md", + "role": "Slice C summons (one Cursor agent, D2 of 6002718035)", + "comment": "6023049558", + "url": "https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023049558", + "created_at": "2026-10-06T18:42:12Z", + "updated_at": "2026-10-06T18:42:12Z", + "bytes": 3359, + "sha256": "a47b867bca286422ef5430f653306ea10c63da336e4faaca2e3c457bf600ab19" + }, + { + "path": "EM/DELIVERED_POINTER_main259.md", + "role": "author delivery pointer on main#259", + "comment": "6023056903", + "url": "https://github.com/d6g8k5htny-coder/main/issues/259#issuecomment-6023056903", + "created_at": "2026-10-06T18:42:39Z", + "updated_at": "2026-10-06T18:42:39Z", + "bytes": 2173, + "sha256": "ff6f7eff1a0f4e4802b4247b4034ee56b401d144ccc2c8d6dac7df549fb14c30" + }, + { + "path": "EM/REVIEW_SLICE_A.md", + "role": "Slice A (sections 1-2: Lemmas P and X; E1, E2, E4 with M1-M3, M5, M6, M11): PASS, Cursor agent bc-68aae9d7 (xAI Grok 4.7); pickup and verdict in one comment, an edit of the cursor[bot] acknowledgement (GitHub refused a new comment)", + "comment": "6023042554", + "url": "https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023042554", + "created_at": "2026-10-06T18:41:47Z", + "updated_at": "2026-10-06T19:02:21Z", + "bytes": 6605, + "sha256": "3f48dd4283ce741be01ca01b4f34344eeaa5a2cb0f80049821e17cc5c5a63cdb" + }, + { + "path": "EM/REVIEW_SLICE_B.md", + "role": "Slice B (sections 3-4: Lemma V and the proof of Lemma S'''; E3, E5, E7 with M4, M9, M10): AMEND (one absorption in section 4.1 (c); no constant, exponent or stated bound changes), Cursor agent bc-2e83c5a5 (xAI Grok 4.7); pickup and verdict in one edited acknowledgement", + "comment": "6023045290", + "url": "https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023045290", + "created_at": "2026-10-06T18:41:57Z", + "updated_at": "2026-10-06T18:58:05Z", + "bytes": 4053, + "sha256": "9f7087ead469cd5f95541acc2d9dabf497addf8fa399961b6e7f1bcbe9eefbb6" + }, + { + "path": "EM/REVIEW_SLICE_C.md", + "role": "Slice C (section 0, sections 5-6 and the header; E6 with M7, M8): PASS, Cursor agent bc-16115a6c (xAI Grok 4.7); pickup and verdict in one edited acknowledgement", + "comment": "6023050789", + "url": "https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023050789", + "created_at": "2026-10-06T18:42:17Z", + "updated_at": "2026-10-06T18:49:37Z", + "bytes": 5515, + "sha256": "83f17da19c98d6ff8d5e792569835ff0dbe9af67c58fe0c6442494b658bc4cec" + }, + { + "path": "EM/AUTHOR_SUCCESSOR_TEXT_AND_READBACK_SUMMONS.md", + "role": "author round note: the three verdicts, the successor text applying the AMEND exactly (one replacement in section 4.1 (c)), and the readback summons (one Cursor agent, D2 of 6002718035)", + "comment": "6023434026", + "url": "https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023434026", + "created_at": "2026-10-06T19:03:37Z", + "updated_at": "2026-10-06T19:03:37Z", + "bytes": 7822, + "sha256": "2231fadaf3c9f292534c1c65a70f12a978ff1dcb7988a77df0600c25b45fc5f3" + }, + { + "path": "EM/READBACK_SUCCESSOR_TEXT.md", + "role": "readback of the successor text against the AMEND: PASS, Cursor agent bc-3f10fc96 (xAI Grok 4.7); pickup and verdict in one edited acknowledgement", + "comment": "6023435335", + "url": "https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6023435335", + "created_at": "2026-10-06T19:03:41Z", + "updated_at": "2026-10-06T19:10:34Z", + "bytes": 3619, + "sha256": "cec30fa29831e73ec15abcc4b1bbafd9c34ef06796c255b5effe801840953abe" + }, + { + "path": "EM/AUTHOR_READ_COMPLETE_AND_CLAIM.md", + "role": "author note (read-complete in every slice) and D5 claims for this custody packet (claim 1) and for addendum EM.1 (claim 2)", + "comment": "6024074852", + "url": "https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6024074852", + "created_at": "2026-10-06T19:40:10Z", + "updated_at": "2026-10-06T19:40:10Z", + "bytes": 3453, + "sha256": "dc9cd57371838a63c607abf9827a56a2128742a59f4aab86b589a99891aa55d2" + }, + { + "path": "EM/author_controls.py", + "role": "control script em_exact.py, extracted verbatim from the stored controls comment EM/AUTHOR_CONTROLS_COMMENT.md (heading: ### em_exact.py)", + "extracted_from": "EM/AUTHOR_CONTROLS_COMMENT.md", + "heading": "### em_exact.py", + "bytes": 21773, + "sha256": "feea3c3c004ba5b6bc5dbcefc60bc684f0abc91808e6cf092eeac16a81cd9189" + }, + { + "path": "EM/author_controls_stdout.json", + "role": "published stdout of EM/author_controls.py, extracted verbatim from EM/AUTHOR_CONTROLS_COMMENT.md (```json fence)", + "extracted_from": "EM/AUTHOR_CONTROLS_COMMENT.md", + "heading": "### em_exact.py", + "bytes": 202, + "sha256": "c4c2a636ea378587d4c3e629c2fc05aa0d72aad2f260e2327f493cb8259c5740" + } + ], + "replays": [ + { + "name": "em_exact.py (stdout in a ```json fence)", + "script": "EM/author_controls.py", + "stdout": "EM/author_controls_stdout.json", + "args": [], + "mutants": [ + [ + "--mutant", + "M1" + ], + [ + "--mutant", + "M2" + ], + [ + "--mutant", + "M3" + ], + [ + "--mutant", + "M4" + ], + [ + "--mutant", + "M5" + ], + [ + "--mutant", + "M6" + ], + [ + "--mutant", + "M7" + ], + [ + "--mutant", + "M8" + ], + [ + "--mutant", + "M9" + ], + [ + "--mutant", + "M10" + ], + [ + "--mutant", + "M11" + ] + ], + "invalid": [ + [ + "--bogus" + ], + [ + "--mutant", + "M12" + ], + [ + "--mutant" + ] + ] + } + ] + } + ] +} diff --git a/frontiers/em_intermediate_elder_20261006/replay.py b/frontiers/em_intermediate_elder_20261006/replay.py new file mode 100644 index 000000000..c03e4f0e8 --- /dev/null +++ b/frontiers/em_intermediate_elder_20261006/replay.py @@ -0,0 +1,342 @@ +#!/usr/bin/env python3 +"""Verify the stored records of lifetime note EM and replay its published author controls (standard library only). + +Every file in this packet except replay.py, README.md and SOURCES.json is one of two things: + - an exact copy of a public comment body on main#229 or main#259 (a note, claim, pickup, controls comment, read + request, review, release or author response); + - the control script or its stdout, extracted verbatim from the stored controls comment by the extraction rule that + comment states (the rule of main#229 comment 5971055189). The stdout is a ```json fence. +SOURCES.json pins each file by byte count and SHA-256 and lists each replay. This script performs four checks. + + 1. The packet tree equals SOURCES.json's file list, with no symlinks, and every stored file has its pinned + identity. + 2. Every extracted script and stdout equals the fenced payload inside its stored source comment, under the + extraction rule (the stdout fence language follows the stored stdout's suffix: .json for ```json, .txt for ```text). + 3. Every control script runs under the current interpreter's -O/-S flags and reproduces its published stdout byte + for byte (none prints an interpreter version), with empty stderr. Every listed mutant or invalid invocation + must reproduce its exact source-bound rejection on BOTH captured streams, not merely exit 1 or 2. + 4. Negative controls must be rejected: + - a one-byte change to a stored note (EM/PROOF.md); + - a control script with one changed constant ((P.2)'s constant 13/80 replaced by 1/20). + +Reproducibility only. The analytic notes and their reads carry the mathematics. These finite checks support +algebra, as the reads say. Nothing here reads or grades a proof. + +Usage: python3 -B -S frontiers/em_intermediate_elder_20261006/replay.py (exit 0 iff every check passes) +Optional QS_REPLAY_EVIDENCE_DIR (outside the checkout) retains raw child streams and process records. +Each invocation gets a new directory; records describe execution, never mathematical acceptance. +Required evidence I/O fails the run; a timeout/spawn error remains the primary exception. +""" +import hashlib +import json +import os +import pathlib +import re +import shutil +import subprocess +import sys +import tempfile + +HERE = pathlib.Path(__file__).resolve().parent +OWN = {'README.md', 'SOURCES.json', 'replay.py'} + +# Exact rejection fingerprints of the extracted author controls (em_exact.py from 6023024039), computed under both +# interpreter modes at incorporation and found identical. +# Each key is (script path, complete argv tail); each value is (exit, stdout SHA256, +# stderr SHA256, readable reason). References are frozen independently of this run. +# All 11 mutants and 3 invalid invocations were executed and their named reasons +# checked against their source. Exact fingerprints enforce the full contracts, +# including the empty stdout, the FAILED or usage line and its group name. +# No current failing output, generic exit code or broad regex creates a reference. +# Any source/runtime output drift fails closed and requires a reviewed amendment. +REJECTION_CONTRACTS = { + ('EM/author_controls.py', ('--mutant', 'M1')): + (1, 'e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855', 'a36dafc2e6ae98878e475189a8ca0d6b2d2b0c629ab41ea5a361e0d7f2c95d52', 'FAILED: E1_pins'), + ('EM/author_controls.py', ('--mutant', 'M2')): + (1, 'e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855', 'a36dafc2e6ae98878e475189a8ca0d6b2d2b0c629ab41ea5a361e0d7f2c95d52', 'FAILED: E1_pins'), + ('EM/author_controls.py', ('--mutant', 'M3')): + (1, 'e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855', 'b42a393ef32c94592161c001f715319466a82782d270343a2617e8236a7947d4', 'FAILED: E2_shear'), + ('EM/author_controls.py', ('--mutant', 'M4')): + (1, 'e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855', '9ccdf6fc316af8ba67af8e57acaa5c490fcd527592c0b9b4f5501bff2a2019fb', 'FAILED: E3_model'), + ('EM/author_controls.py', ('--mutant', 'M5')): + (1, 'e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855', 'e81c9fa7a7b337ae36f9eab09fe1c4e68da39ea36a99562c209a7ef78863301d', 'FAILED: E4_box'), + ('EM/author_controls.py', ('--mutant', 'M6')): + (1, 'e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855', 'e81c9fa7a7b337ae36f9eab09fe1c4e68da39ea36a99562c209a7ef78863301d', 'FAILED: E4_box'), + ('EM/author_controls.py', ('--mutant', 'M7')): + (1, 'e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855', '8f070d1d3467c3c9a85ca70fa973570a1f9ece3a1177c8dfabcccffd85e8030a', 'FAILED: E6_ledger'), + ('EM/author_controls.py', ('--mutant', 'M8')): + (1, 'e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855', '8f070d1d3467c3c9a85ca70fa973570a1f9ece3a1177c8dfabcccffd85e8030a', 'FAILED: E6_ledger'), + ('EM/author_controls.py', ('--mutant', 'M9')): + (1, 'e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855', '98ea78de95dcfa6419150cef71a1f2b30fafc80a5fbb9a1caf5b333a41eb4d3e', 'FAILED: E5_volume'), + ('EM/author_controls.py', ('--mutant', 'M10')): + (1, 'e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855', '98ea78de95dcfa6419150cef71a1f2b30fafc80a5fbb9a1caf5b333a41eb4d3e', 'FAILED: E5_volume'), + ('EM/author_controls.py', ('--mutant', 'M11')): + (1, 'e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855', 'a36dafc2e6ae98878e475189a8ca0d6b2d2b0c629ab41ea5a361e0d7f2c95d52', 'FAILED: E1_pins'), + ('EM/author_controls.py', ('--bogus',)): + (2, 'e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855', '47aa0b35b69645c5fdb5a9776805e4490d2da1fd386fac6a4acf54ba935976eb', 'usage: em_exact.py [--mutant M1..M11]'), + ('EM/author_controls.py', ('--mutant', 'M12')): + (2, 'e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855', '47aa0b35b69645c5fdb5a9776805e4490d2da1fd386fac6a4acf54ba935976eb', 'usage: em_exact.py [--mutant M1..M11]'), + ('EM/author_controls.py', ('--mutant',)): + (2, 'e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855', '47aa0b35b69645c5fdb5a9776805e4490d2da1fd386fac6a4acf54ba935976eb', 'usage: em_exact.py [--mutant M1..M11]'), +} + +# Replacing (P.2)'s constant 13/80 by 1/20 with MUT=None must fail specifically at E1, on stderr alone. +NEGATIVE_CONSTANT = (1, hashlib.sha256(b'').hexdigest(), + hashlib.sha256(b'FAILED: E1_pins\n').hexdigest(), 'E1_pins') + + +def check_rejection(result, expected): + """Compare both full captured streams, not a permissive failure-message pattern.""" + code, out, err = result + failures = [] + if type(code) is not int or code != expected[0]: + failures.append('wrong exit code') + if type(out) is not bytes or hashlib.sha256(out).hexdigest() != expected[1]: + failures.append('stdout differs from intended diagnostic') + if type(err) is not bytes or hashlib.sha256(err).hexdigest() != expected[2]: + failures.append('stderr differs from intended diagnostic') + return failures + + +def rejection_inventory_failures(manifest): + listed = {} + for obj in manifest['objects']: + for replay in obj['replays']: + for kind, code in (('mutants', 1), ('invalid', 2)): + for args in replay[kind]: + key = replay['script'], tuple(args) + if key in listed: + return ['duplicate rejection invocation: ' + repr(key)] + listed[key] = code + if set(listed) != set(REJECTION_CONTRACTS): + return ['rejection invocation inventory differs from frozen contracts'] + if any(REJECTION_CONTRACTS[key][0] != code for key, code in listed.items()): + return ['rejection invocation category differs from frozen contracts'] + return [] + + +def report_control(script, args, result, reason): + code, out, err = result + print(json.dumps(dict(script=script, args=list(args), returncode=code, + stdout_sha256=hashlib.sha256(out).hexdigest(), + stderr_sha256=hashlib.sha256(err).hexdigest(), + expected_reason=reason), sort_keys=True)) + + +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 tree_failures(root, manifest): + failures = [] + listed = {} + for obj in manifest['objects']: + for f in obj['stored']: + listed[f['path']] = (f['bytes'], f['sha256']) + present = set() + for path in sorted(root.rglob('*')): + rel = path.relative_to(root).as_posix() + if path.is_symlink(): + failures.append('symlink: ' + rel) + elif path.is_file(): + present.add(rel) + for rel in sorted(present ^ (set(listed) | OWN)): + failures.append(('unlisted file: ' if rel in present else 'missing file: ') + rel) + for rel, ident in sorted(listed.items()): + if rel in present and identity((root / rel).read_bytes()) != ident: + failures.append('identity mismatch: ' + rel) + return failures + + +def extraction_failures(root, manifest): + """Re-extract every script and stdout from its stored source comment and compare with the stored payloads.""" + failures = [] + for obj in manifest['objects']: + extracted = [f for f in obj['stored'] if 'extracted_from' in f] + for script in [f for f in extracted if f['path'].endswith('.py')]: + stdout = [f for f in extracted if f['extracted_from'] == script['extracted_from'] + and f['heading'] == script['heading'] and not f['path'].endswith('.py')] + if len(stdout) != 1: + failures.append('%s: no single stdout record for %s' % (obj['tag'], script['path'])) + continue + stdout = stdout[0] + fence = {'json': 'json', 'txt': 'text'}.get(stdout['path'].rsplit('.', 1)[-1]) + if fence is None: + failures.append('%s: unsupported stdout suffix for %s' % (obj['tag'], stdout['path'])) + continue + body = (root / script['extracted_from']).read_text(encoding='utf-8') + if body.count(script['heading']) < 1: + failures.append('%s: heading %r not found in %s' % (obj['tag'], script['heading'], script['extracted_from'])) + continue + section = body[body.index(script['heading']):] + m1 = re.search(r'```python\n(.*?)\n```\n', section, re.S) + m2 = re.search(r'```%s\n(.*?)\n```\n' % fence, section[m1.end():], re.S) if m1 else None + if not (m1 and m2): + failures.append('%s: fences not found after %r' % (obj['tag'], script['heading'])) + continue + if (m1.group(1) + '\n').encode('utf-8') != (root / script['path']).read_bytes(): + failures.append('%s: %s differs from the payload in %s' % (obj['tag'], script['path'], script['extracted_from'])) + if (m2.group(1) + '\n').encode('utf-8') != (root / stdout['path']).read_bytes(): + failures.append('%s: %s differs from the payload in %s' % (obj['tag'], stdout['path'], stdout['extracted_from'])) + return failures + + +PROCESS_TIMEOUT_SECONDS = 1800 # Unchanged production budget; tests shorten it for real timeout children. + + +def evidence_directory(script): + """An explicit destination opts in; never put generated evidence in source directories.""" + raw = os.environ.get('QS_REPLAY_EVIDENCE_DIR') + if raw is None: + return None + if not raw: + raise ValueError('QS_REPLAY_EVIDENCE_DIR must not be empty') + root = pathlib.Path(raw).expanduser().resolve() + if root.is_relative_to(HERE.resolve().parents[1]) or root.is_relative_to(script.parent.resolve()): + raise ValueError('QS replay evidence must be outside the checkout and child source directory') + root.mkdir(parents=True, exist_ok=True) + return pathlib.Path(tempfile.mkdtemp(prefix='invocation-', dir=root)) + + +def save_process_evidence(folder, record, out, err): + """Attempt every write independently. None is unavailable, not an observed empty stream.""" + record['streams'] = {} + record['evidence_errors'] = [] + for name, data in (('stdout', out), ('stderr', err)): + entry = dict(available=data is not None, bytes=len(data) if data is not None else None, + sha256=hashlib.sha256(data).hexdigest() if data is not None else None, saved=False) + record['streams'][name] = entry + try: + (folder / (name + '.bin')).write_bytes(data if data is not None else b'') + entry['saved'] = True + except Exception as exc: + record['evidence_errors'].append('%s.bin: %s: %s' % (name, type(exc).__name__, exc)) + try: + data = (json.dumps(record, sort_keys=True, indent=2, allow_nan=False) + '\n').encode('utf-8') + (folder / 'process.json').write_bytes(data) + except Exception as exc: + record['evidence_errors'].append('process.json: %s: %s' % (type(exc).__name__, exc)) + + +def run(script, *args): + command = [sys.executable, *interpreter_flags(), str(script), *args] + folder = evidence_directory(script) # Invalid/unwritable setup stops before starting a child. + record = dict(schema=1, command=command, cwd=str(script.parent), + timeout_seconds=PROCESS_TIMEOUT_SECONDS, scientific_effect='NONE') + try: + proc = subprocess.run(command, capture_output=True, timeout=PROCESS_TIMEOUT_SECONDS, + cwd=str(script.parent)) + except (subprocess.TimeoutExpired, OSError) as exc: + if folder is not None: + record.update(status='timeout' if isinstance(exc, subprocess.TimeoutExpired) else 'spawn_error', + returncode=None, exception=dict(type=type(exc).__name__, message=str(exc))) + exc.evidence_record = record + try: + save_process_evidence(folder, record, getattr(exc, 'stdout', None), getattr(exc, 'stderr', None)) + if record['evidence_errors']: + exc.add_note('QS replay evidence errors: ' + '; '.join(record['evidence_errors'])) + except Exception as secondary: + exc.add_note('QS replay evidence recording failed: %s: %s' % (type(secondary).__name__, secondary)) + raise # Never replace the primary timeout or launch error with a recording error. + if folder is not None: + record.update(status='completed', returncode=proc.returncode, exception=None) + save_process_evidence(folder, record, proc.stdout, proc.stderr) + if record['evidence_errors']: + exc = RuntimeError('QS replay evidence errors: ' + '; '.join(record['evidence_errors'])) + exc.evidence_record = record + raise exc # Even exit 0 is not success when explicitly required evidence is missing. + return proc.returncode, proc.stdout, proc.stderr + + +def replay_failures(root, manifest): + failures = rejection_inventory_failures(manifest) + if failures: + return failures # Do not execute an incomplete/changed control inventory. + for obj in manifest['objects']: + for replay in obj['replays']: + label = '%s %s' % (obj['tag'], replay['name']) + script = root / replay['script'] + code, out, err = run(script, *replay['args']) + baseline_failures = [] + if code != 0: + baseline_failures.append('%s: exit code %s' % (label, code)) + if out != (root / replay['stdout']).read_bytes(): + baseline_failures.append('%s: stdout differs from the published bytes' % label) + if err: + baseline_failures.append('%s: unexpected baseline stderr' % label) + if baseline_failures: + failures.extend(baseline_failures) + continue + report_control(replay['script'], replay['args'], (code, out, err), 'exact published baseline') + for kind in ('mutants', 'invalid'): + for args in replay[kind]: + expected = REJECTION_CONTRACTS[replay['script'], tuple(args)] + result = run(script, *args) + mismatches = check_rejection(result, expected) + failures.extend('%s %r: %s' % (label, args, why) for why in mismatches) + if not mismatches: + report_control(replay['script'], args, result, expected[3]) + return failures + + +def negative_control_failures(root, manifest): + failures = [] + with tempfile.TemporaryDirectory() as tmp: + copy = pathlib.Path(tmp) / 'packet' + shutil.copytree(root, copy, symlinks=True) + target = copy / 'EM' / 'PROOF.md' + data = bytearray(target.read_bytes()) + data[100] ^= 0x01 + target.write_bytes(bytes(data)) + if 'identity mismatch: EM/PROOF.md' not in tree_failures(copy, manifest): + failures.append('negative control: a one-byte change to EM/PROOF.md was not detected') + script = copy / 'EM' / 'author_controls.py' + text = script.read_text(encoding='utf-8') + old = 'c2 = F(1, 20) if MUT == "M2" else F(13, 80)' + if text.count(old) != 1: + failures.append('negative control: the (P.2) constant line was not found exactly once') + else: + script.write_text(text.replace(old, 'c2 = F(1, 20) if MUT == "M2" else F(1, 20)'), encoding='utf-8') + result = run(script) + mismatches = check_rejection(result, NEGATIVE_CONSTANT) + failures.extend('negative control: changed (P.2) constant: ' + why for why in mismatches) + if not mismatches: + report_control('EM/author_controls.py', [], result, 'changed 13/80 to 1/20: E1_pins') + return failures + + +def main(): + manifest = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8')) + failures = tree_failures(HERE, manifest) + if not failures: + failures = extraction_failures(HERE, manifest) + if not failures: + failures = replay_failures(HERE, manifest) + if not failures: + failures = negative_control_failures(HERE, manifest) + n_scripts = sum(len(o['replays']) for o in manifest['objects']) + n_mut = sum(len(r['mutants']) for o in manifest['objects'] for r in o['replays']) + n_inv = sum(len(r['invalid']) for o in manifest['objects'] for r in o['replays']) + n_files = sum(len(o['stored']) for o in manifest['objects']) + mode = ' '.join(interpreter_flags()) + if failures: + for f in failures: + print('FAIL ' + f) + print('Lifetime note EM incorporation replay (%s): %d failure(s)' % (mode, len(failures))) + return 1 + print('Lifetime note EM incorporation replay (%s): %d stored identities, %d extractions, %d checker stdouts, ' + '%d mutants, %d invalid invocations and 2 negative controls PASS' % (mode, n_files, 2 * n_scripts, n_scripts, n_mut, n_inv)) + return 0 + + +if __name__ == '__main__': + sys.exit(main()) diff --git a/tests/test_em_intermediate_elder_replay_evidence.py b/tests/test_em_intermediate_elder_replay_evidence.py new file mode 100644 index 000000000..fedd3916f --- /dev/null +++ b/tests/test_em_intermediate_elder_replay_evidence.py @@ -0,0 +1,215 @@ +"""Optional raw-process evidence; synthetic children are not mathematical evidence.""" +import hashlib +import importlib.util +import json +import os +from pathlib import Path +import subprocess +import sys +import tempfile +import unittest +from unittest.mock import patch + +ROOT = Path(__file__).resolve().parents[1] +PACKET = ROOT / 'frontiers/em_intermediate_elder_20261006' +ENV = 'QS_REPLAY_EVIDENCE_DIR' + + +class RawEvidenceTests(unittest.TestCase): + def setUp(self): + spec = importlib.util.spec_from_file_location('qs_raw_subject', PACKET / 'replay.py') + self.m = importlib.util.module_from_spec(spec) + spec.loader.exec_module(self.m) + self.tmp = tempfile.TemporaryDirectory() + self.addCleanup(self.tmp.cleanup) + self.root = Path(self.tmp.name) + scripts = self.root / 'scripts' + scripts.mkdir() + self.script = scripts / 'fixture.py' + self.evidence = self.root / 'evidence' + self.env = patch.dict(os.environ, {ENV: str(self.evidence)}) + self.env.start() + self.addCleanup(self.env.stop) + + def child(self, text): + self.script.write_text(text, encoding='utf-8') + return self.script + + def record(self): + records = list(self.evidence.glob('invocation-*/process.json')) + self.assertEqual(len(records), 1, 'one independently retained child process record required') + return records[0].parent, json.loads(records[0].read_bytes()) + + def verify_stream(self, folder, rec, name, value): + stream = rec['streams'][name] + self.assertEqual(stream['available'], value is not None) + self.assertEqual(stream['bytes'], len(value) if value is not None else None) + self.assertEqual(stream['sha256'], hashlib.sha256(value).hexdigest() if value is not None else None) + self.assertTrue(stream['saved']) + self.assertEqual((folder / (name + '.bin')).read_bytes(), value if value is not None else b'') + + def test_no_capture_preserves_original_three_value_result(self): + os.environ.pop(ENV) + s = self.child("import os,sys\nos.write(1,b'\\xffok');os.write(2,b'\\x00err');sys.exit(7)\n") + self.assertEqual(self.m.run(s), (7, b'\xffok', b'\x00err')) + self.assertFalse(self.evidence.exists()) + + def test_real_crash_retains_full_binary_streams_and_invocation(self): + s = self.child("import os\nos.write(1,b'\\x00\\xffpartial')\nraise RuntimeError('synthetic crash')\n") + result = self.m.run(s, '--diagnostic') + self.assertEqual(result[0], 1) + self.assertIn(b'RuntimeError: synthetic crash', result[2]) + folder, rec = self.record() + self.assertEqual(rec['command'], [sys.executable, *self.m.interpreter_flags(), str(s), '--diagnostic']) + self.assertEqual(rec['cwd'], str(s.parent)) + self.assertEqual(rec['timeout_seconds'], 1800) + self.assertEqual(rec['status'], 'completed') + self.assertEqual(rec['returncode'], 1) + self.assertNotIn('passed', rec) + self.assertEqual(rec['evidence_errors'], []) + self.verify_stream(folder, rec, 'stdout', result[1]) + self.verify_stream(folder, rec, 'stderr', result[2]) + + def test_success_and_intended_failure_outputs_are_not_reinterpreted(self): + s = self.child("import os,sys\nos.write(1,b'answer\\n');os.write(2,b'diagnostic\\n');sys.exit(int(sys.argv[1]))\n") + for code in (0, 1, 2): + with self.subTest(code=code): + result = self.m.run(s, str(code)) + self.assertEqual(result, (code, b'answer\n', b'diagnostic\n')) + records = [json.loads(p.read_bytes()) for p in self.evidence.glob('invocation-*/process.json')] + self.assertEqual(sorted(r['returncode'] for r in records), [0, 1, 2]) + self.assertTrue(all('passed' not in r for r in records)) + + def test_repeated_invocations_never_overwrite(self): + s = self.child("print('first')\n") + self.m.run(s) + before = {p: p.read_bytes() for p in self.evidence.glob('invocation-*/*')} + self.assertEqual(len(before), 3) + self.m.run(s) + self.assertEqual(len(list(self.evidence.glob('invocation-*'))), 2) + for p, data in before.items(): + self.assertEqual(p.read_bytes(), data) + + def test_real_timeout_keeps_partial_bytes_and_timeout_exception(self): + self.assertTrue(hasattr(self.m, 'PROCESS_TIMEOUT_SECONDS'), 'explicit unchanged production timeout required') + s = self.child("import os,time\nos.write(1,b'\\xffout');os.write(2,b'\\x00err');time.sleep(10)\n") + with patch.object(self.m, 'PROCESS_TIMEOUT_SECONDS', 0.5): + with self.assertRaises(subprocess.TimeoutExpired) as caught: + self.m.run(s) + folder, rec = self.record() + self.assertEqual(rec['status'], 'timeout') + self.assertIsNone(rec['returncode']) + self.assertEqual(rec['timeout_seconds'], 0.5) + self.assertEqual(caught.exception.output, b'\xffout') + self.assertEqual(caught.exception.stderr, b'\x00err') + self.verify_stream(folder, rec, 'stdout', caught.exception.output) + self.verify_stream(folder, rec, 'stderr', caught.exception.stderr) + self.assertEqual(caught.exception.evidence_record, rec) + + def test_unavailable_empty_and_binary_timeout_capture_are_distinct(self): + for out in (None, b'', b'\xff\x00'): + for err in (None, b'', b'\x80err'): + with self.subTest(out=out, err=err), tempfile.TemporaryDirectory() as td: + target = Path(td) / 'records' + exc = subprocess.TimeoutExpired(['synthetic'], 1800, output=out, stderr=err) + with patch.dict(os.environ, {ENV: str(target)}), patch.object(self.m.subprocess, 'run', side_effect=exc): + with self.assertRaises(subprocess.TimeoutExpired) as caught: + self.m.run(self.script) + self.assertIs(caught.exception, exc) + paths = list(target.glob('invocation-*/process.json')) + self.assertEqual(len(paths), 1) + rec = json.loads(paths[0].read_bytes()) + self.verify_stream(paths[0].parent, rec, 'stdout', out) + self.verify_stream(paths[0].parent, rec, 'stderr', err) + self.assertIsNone(rec['returncode']) + + def test_real_spawn_error_retains_unknown_output_and_original_error(self): + s = self.child("print('must not execute')\n") + missing = str(self.root / 'missing-interpreter') + with patch.object(self.m.sys, 'executable', missing): + with self.assertRaises(FileNotFoundError) as caught: + self.m.run(s) + folder, rec = self.record() + self.assertEqual(rec['status'], 'spawn_error') + self.assertIsNone(rec['returncode']) + self.assertEqual(rec['exception']['type'], 'FileNotFoundError') + self.verify_stream(folder, rec, 'stdout', None) + self.verify_stream(folder, rec, 'stderr', None) + self.assertEqual(caught.exception.evidence_record, rec) + + def test_each_write_failure_still_attempts_other_evidence(self): + original = Path.write_bytes + for failed in ('stdout.bin', 'stderr.bin', 'process.json'): + with self.subTest(failed=failed), tempfile.TemporaryDirectory() as td: + target = Path(td) / 'records' + attempted = [] + def write(path, data): + attempted.append(path.name) + if path.name == failed: + raise OSError('synthetic write refusal') + return original(path, data) + exc = subprocess.TimeoutExpired(['synthetic'], 1800, output=b'out', stderr=b'err') + with patch.dict(os.environ, {ENV: str(target)}), patch.object(self.m.subprocess, 'run', side_effect=exc), patch.object(Path, 'write_bytes', write): + with self.assertRaises(subprocess.TimeoutExpired) as caught: + self.m.run(self.script) + self.assertIs(caught.exception, exc) + self.assertEqual(attempted, ['stdout.bin', 'stderr.bin', 'process.json']) + rec = caught.exception.evidence_record + self.assertEqual(len(rec['evidence_errors']), 1) + self.assertIn(failed, rec['evidence_errors'][0]) + self.assertTrue(any('evidence' in note for note in caught.exception.__notes__)) + folder = next(target.glob('invocation-*')) + for name in {'stdout.bin', 'stderr.bin', 'process.json'} - {failed}: + self.assertTrue((folder / name).is_file()) + + def test_all_write_failures_do_not_replace_primary_timeout(self): + exc = subprocess.TimeoutExpired(['synthetic'], 1800, output=b'out', stderr=b'err') + with patch.object(self.m.subprocess, 'run', side_effect=exc), patch.object(Path, 'write_bytes', side_effect=OSError('synthetic full disk')): + with self.assertRaises(subprocess.TimeoutExpired) as caught: + self.m.run(self.script) + self.assertIs(caught.exception, exc) + self.assertTrue(hasattr(exc, 'evidence_record'), 'retain failure metadata in memory') + self.assertEqual(len(exc.evidence_record['evidence_errors']), 3) + self.assertIsNone(exc.evidence_record['returncode']) + + def test_completed_child_with_failed_evidence_cannot_report_success(self): + self.child("print('actual completed child')\n") + with patch.object(Path, 'write_bytes', side_effect=OSError('synthetic full disk')): + with self.assertRaises(RuntimeError) as caught: + self.m.run(self.script) + self.assertEqual(caught.exception.evidence_record['returncode'], 0) + self.assertEqual(len(caught.exception.evidence_record['evidence_errors']), 3) + + def test_invalid_destination_stops_before_child(self): + for target in (PACKET / 'forbidden-evidence', self.script.parent / 'forbidden-evidence'): + with self.subTest(target=target), patch.dict(os.environ, {ENV: str(target)}), patch.object(self.m.subprocess, 'run') as child: + with self.assertRaises(ValueError): + self.m.run(self.script) + child.assert_not_called() + self.assertFalse(target.exists()) + self.evidence.write_text('not a directory') + with patch.object(self.m.subprocess, 'run') as child: + with self.assertRaises(OSError): + self.m.run(self.script) + child.assert_not_called() + + def test_failed_custody_creates_no_child_evidence(self): + with patch.object(self.m, 'tree_failures', return_value=['synthetic custody refusal']), patch.object(self.m.subprocess, 'run') as child: + self.assertEqual(self.m.main(), 1) + child.assert_not_called() + self.assertFalse(self.evidence.exists()) + + def test_workflow_wires_tests_and_capture_outside_source_tree(self): + text = (ROOT / '.github/workflows/em-intermediate-elder.yml').read_text() + self.assertIn("'tests/test_em_intermediate_elder_replay_evidence.py'", text) + self.assertIn('-p test_em_intermediate_elder_replay_evidence.py', text) + self.assertIn('QS_REPLAY_EVIDENCE_DIR="$out/children" python', text) + self.assertIn('cp tests/test_em_intermediate_elder_replay_evidence.py "$out/"', text) + self.assertIn('set -euo pipefail', text) + self.assertIn('git diff --exit-code', text) + self.assertIn('contents: read', text) + self.assertIn("python-version: '3.11.16'", text) + + +if __name__ == '__main__': + unittest.main() diff --git a/tests/test_em_intermediate_elder_replay_protocol.py b/tests/test_em_intermediate_elder_replay_protocol.py new file mode 100644 index 000000000..7f2c09078 --- /dev/null +++ b/tests/test_em_intermediate_elder_replay_protocol.py @@ -0,0 +1,230 @@ +"""Real subprocess controls for QS replay; fixtures are not mathematical evidence.""" +import copy +import hashlib +import importlib.util +import json +from pathlib import Path +import sys +import tempfile +import unittest +from unittest import mock + +ROOT = Path(__file__).resolve().parents[1] +WRAPPER = ROOT / 'frontiers/em_intermediate_elder_20261006/replay.py' + + +class ReplayProtocolTests(unittest.TestCase): + def setUp(self): + spec = importlib.util.spec_from_file_location('qs_replay_subject', WRAPPER) + self.m = importlib.util.module_from_spec(spec) + spec.loader.exec_module(self.m) + + @staticmethod + def baseline(): + return dict(object='A3 d>=3 hard-fibre reduction (author-side exact controls)', + counts={'Z1': 2400, 'Z2': 3600, 'Z3': 4800, 'Z4': 1200}, + mutant=None, all_pass=True, failures=[], scientific_effect='NONE') + + def invoke(self, scenario='valid'): + baseline = self.baseline() + mutant = copy.deepcopy(baseline) + mutant.update(mutant='Z2', all_pass=False, failures=["('Z2-gain', 17)"]) + invalid = {'error': 'unknown arguments'} + sha = lambda data: hashlib.sha256(data).hexdigest() + # These synthetic expectations test the real runner/matcher, not the real + # checkers' reference values. The immutable production table is checked below. + expected_mutant = (json.dumps(mutant, sort_keys=True) + '\n').encode() + expected_invalid = (json.dumps(invalid) + '\n').encode() + contracts = { + ('A3/author_controls.py', ('--mutant', 'Z2')): + (1, sha(expected_mutant), sha(b''), 'Z2-gain'), + ('A3/author_controls.py', ('--bogus',)): + (2, sha(expected_invalid), sha(b''), 'unknown arguments'), + } + base_out = (json.dumps(baseline, sort_keys=True) + '\n').encode() + mut_code, inv_code = 1, 2 + base_err = mut_err = inv_err = b'' + if scenario == 'crash': + mut_code = 1; mut_err = b'Traceback: synthetic unrelated RuntimeError\n' + mut_out = b'' + else: + if scenario == 'wrong_reason': mutant['failures'] = ["('Z4', 17)"] + elif scenario == 'extra_reason': mutant['failures'].append("('setup', 3)") + elif scenario == 'wrong_mutant': mutant['mutant'] = 'Z3' + elif scenario == 'wrong_object': mutant['object'] = 'unrelated' + elif scenario == 'wrong_effect': mutant['scientific_effect'] = 'ACCEPT' + elif scenario == 'all_pass': mutant['all_pass'] = True + elif scenario == 'integer_bool': mutant['all_pass'] = 0 + elif scenario == 'empty_failures': mutant['failures'] = [] + elif scenario == 'failures_string': mutant['failures'] = "('Z2-gain', 17)" + elif scenario == 'wrong_counts': mutant['counts']['Z1'] = True + elif scenario == 'missing_counts': del mutant['counts']['Z2'] + elif scenario == 'extra_field': mutant['unexpected'] = 'x' + elif scenario == 'bad_tuple': mutant['failures'] = ['not a failure tuple'] + elif scenario == 'tuple_prefix_only': mutant['failures'] = ["('Z2-gain-forged', 17)"] + mut_out = (json.dumps(mutant, sort_keys=True) + '\n').encode() + if scenario == 'garbage': mut_out = b'unrelated error\n' + elif scenario == 'trailing': mut_out += b'garbage\n' + elif scenario == 'duplicate': mut_out = mut_out.replace(b'"all_pass": false', b'"all_pass": false, "all_pass": false') + elif scenario == 'nonfinite': mut_out = mut_out.replace(b'"Z1": 2400', b'"Z1": NaN') + elif scenario == 'overflow': mut_out = mut_out.replace(b'"Z1": 2400', b'"Z1": 1e999') + elif scenario == 'wrong_exit': mut_code = 2 + elif scenario == 'mutant_stderr': mut_err = b'synthetic unexpected stderr\n' + inv_out = (json.dumps(invalid) + '\n').encode() + if scenario == 'invalid_crash': inv_out = b''; inv_err = b'Traceback: synthetic error\n' + elif scenario == 'invalid_wrong_reason': inv_out = b'{"error":"unrelated"}\n' + elif scenario == 'invalid_extra_field': inv_out = b'{"error":"unknown arguments","extra":1}\n' + elif scenario == 'invalid_wrong_exit': inv_code = 1 + elif scenario == 'invalid_stderr': inv_err = b'unexpected stderr\n' + if scenario == 'baseline_stderr': base_err = b'unexpected stderr\n' + actual_base = base_out if scenario != 'baseline_mismatch' else b'wrong\n' + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp); (root/'A3').mkdir() + script = root/'A3/author_controls.py' + # Every invocation launches this real isolated child; no subprocess mock. + script.write_text('import sys\na=sys.argv[1:]\n' + f'if not a: out,err,code={actual_base!r},{base_err!r},0\n' + f'elif a==["--mutant","Z2"]: out,err,code={mut_out!r},{mut_err!r},{mut_code}\n' + f'else: out,err,code={inv_out!r},{inv_err!r},{inv_code}\n' + 'sys.stdout.buffer.write(out)\nsys.stderr.buffer.write(err)\nsys.exit(code)\n') + (root/'A3/author_controls_stdout.json').write_bytes(base_out) + manifest = {'objects': [{'tag': 'A3', 'replays': [{ + 'name': 'a3d_exact.py', 'script': 'A3/author_controls.py', + 'stdout': 'A3/author_controls_stdout.json', 'args': [], + 'mutants': [['--mutant','Z2']], 'invalid': [['--bogus']]}]}]} + with mock.patch.object(self.m, 'REJECTION_CONTRACTS', contracts, create=True): + return self.m.replay_failures(root, manifest) + + def test_valid_protocol(self): + self.assertEqual(self.invoke(), []) + + def test_baseline_output_contract(self): + for scenario in ('baseline_mismatch', 'baseline_stderr'): + with self.subTest(scenario=scenario): self.assertTrue(self.invoke(scenario)) + + def test_crash_is_not_intended_rejection(self): + self.assertTrue(self.invoke('crash')) + + def test_intended_reason_and_identity(self): + for scenario in ('wrong_reason','extra_reason','wrong_mutant','wrong_object','wrong_effect', + 'empty_failures','failures_string','bad_tuple','tuple_prefix_only'): + with self.subTest(scenario=scenario): self.assertTrue(self.invoke(scenario)) + + def test_json_shape_and_types(self): + for scenario in ('all_pass','integer_bool','wrong_counts','missing_counts','extra_field', + 'garbage','trailing','duplicate','nonfinite','overflow'): + with self.subTest(scenario=scenario): self.assertTrue(self.invoke(scenario)) + + def test_mutant_exit_and_stderr(self): + for scenario in ('wrong_exit','mutant_stderr'): + with self.subTest(scenario=scenario): self.assertTrue(self.invoke(scenario)) + + def test_invalid_argument_contract(self): + for scenario in ('invalid_crash','invalid_wrong_reason','invalid_extra_field', + 'invalid_wrong_exit','invalid_stderr'): + with self.subTest(scenario=scenario): self.assertTrue(self.invoke(scenario)) + + def test_changed_constant_crash_is_rejected(self): + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp); (root/'EM').mkdir() + proof = b'x'*150 + (root/'EM/PROOF.md').write_bytes(proof) + script = ('from fractions import Fraction as F\nMUT=None\n' + 'c2 = F(1, 20) if MUT == "M2" else F(13, 80)\n' + 'if c2==F(1, 20): raise RuntimeError("synthetic crash")\n' + 'print("ok")\n') + (root/'EM/author_controls.py').write_text(script) + (root/'EM/author_controls_stdout.json').write_bytes(b'ok\n') + manifest = {'objects': [{'tag':'EM','replays':[], 'stored':[ + {'path':'EM/PROOF.md','bytes':len(proof),'sha256':hashlib.sha256(proof).hexdigest()}]}]} + self.assertTrue(self.m.negative_control_failures(root, manifest)) + + +class ReferenceContractTests(unittest.TestCase): + def setUp(self): + spec = importlib.util.spec_from_file_location('qs_reference_subject', WRAPPER) + self.m = importlib.util.module_from_spec(spec) + spec.loader.exec_module(self.m) + + def matcher(self): + self.assertTrue(hasattr(self.m, 'check_rejection'), 'missing exact diagnostic matcher') + return self.m.check_rejection + + def test_fixed_table_covers_every_manifest_invocation(self): + self.assertTrue(hasattr(self.m, 'REJECTION_CONTRACTS'), 'missing frozen reference table') + manifest = json.loads(WRAPPER.with_name('SOURCES.json').read_text()) + listed = {} + for obj in manifest['objects']: + for replay in obj['replays']: + for category, code in (('mutants', 1), ('invalid', 2)): + for args in replay[category]: + key = replay['script'], tuple(args) + self.assertNotIn(key, listed) + listed[key] = code + self.assertEqual(len(listed), 14) # EM: 11 mutants + 3 invalid + self.assertEqual(set(self.m.REJECTION_CONTRACTS), set(listed)) + for key, value in self.m.REJECTION_CONTRACTS.items(): + self.assertEqual(len(value), 4) + self.assertEqual(value[0], listed[key]) + for digest in value[1:3]: self.assertRegex(digest, r'^[0-9a-f]{64}$') + self.assertIsInstance(value[3], str) + self.assertTrue(value[3]) + + def test_exact_matcher_preserves_five_diagnostic_families(self): + check = self.matcher() + # Representative valid shapes. Full exact values come from unchanged sources, + # not a permissive JSON/regex schema or the current child's reported result. + shapes = [ + (1, b'{"all_pass":false,"mutant":"Z2","failures":["Z2-gain"]}\n', b''), + (1, b'', b'{"failed":"K1 BD(a) violated"}\n'), + (1, b'{"passed":false}\n', b'FAILED:\nO2: pin Hessians\n'), + (1, b'{"passed":false}\n', b'FAILED:\nF2_FW1: ratio 2\n'), + (1, b'', b'FAILED: X9_hardgap\nmutant M5: hard-gap integral\n'), + (2, b'{"error": "unknown arguments"}\n', b''), + (2, b'', b'usage: a33_k5o.py PATH/a33_exact.py [--mutant W1|W2]\n'), + ] + for code, out, err in shapes: + expected = (code, hashlib.sha256(out).hexdigest(), hashlib.sha256(err).hexdigest(), 'synthetic intended reason') + with self.subTest(code=code, out=out, err=err): + self.assertEqual(check((code, out, err), expected), []) + for bad in ((0, out, err), (code, out+b'x', err), (code, out, err+b'x'), + (code, err, out), (code, b'', b'Traceback: unrelated error')): + if bad == (code,out,err): continue + self.assertTrue(check(bad, expected)) + + def test_table_cannot_omit_or_duplicate_manifest_controls(self): + self.assertTrue(hasattr(self.m, 'REJECTION_CONTRACTS'), 'missing inventory guard') + manifest = json.loads(WRAPPER.with_name('SOURCES.json').read_text()) + obj = manifest['objects'][0] + for variant in ('missing', 'duplicate', 'unlisted'): + bad = copy.deepcopy(manifest) + args = bad['objects'][0]['replays'][0]['mutants'] + if variant == 'missing': args.pop() + elif variant == 'duplicate': args.append(args[0]) + else: args.append(['--mutant', 'unlisted']) + with self.subTest(variant=variant), mock.patch.object(self.m, 'run', side_effect=AssertionError('child before inventory')): + self.assertTrue(self.m.replay_failures(WRAPPER.parent, bad)) + + def test_invalid_custody_never_executes_a_child(self): + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + (root/'SOURCES.json').write_text('{"objects":[]}') + with mock.patch.object(self.m, 'HERE', root), \ + mock.patch.object(self.m, 'replay_failures', side_effect=AssertionError('execution before custody')), \ + mock.patch.object(self.m, 'negative_control_failures', side_effect=AssertionError('control before custody')): + self.assertEqual(self.m.main(), 1) + + def test_workflow_runs_regressions_and_retains_failed_evidence(self): + text = (ROOT/'.github/workflows/em-intermediate-elder.yml').read_text() + self.assertIn("'tests/test_em_intermediate_elder_replay_protocol.py'", text) + self.assertIn('-m unittest discover -s tests -p test_em_intermediate_elder_replay_protocol.py -v', text) + self.assertIn('set -euo pipefail', text) + self.assertIn('if: always()', text) + self.assertIn('if-no-files-found: error', text) + self.assertIn('git diff --exit-code', text) + self.assertIn('git status --porcelain', text) + self.assertNotIn('continue-on-error', text) + + +if __name__ == '__main__': + unittest.main()