From 4b1ae3522a0db60ede0f859f52c70bff3deefa5c Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 1 Oct 2026 21:59:15 +0000 Subject: [PATCH 1/3] Theorem D1+: the one-dimensional lifetime and crest-to-trough laws with remainder O(h^(3/4)) Author-side proof candidate (Anthropic Claude); scientific effect NONE; nonauthor review required. Consumes Math- #214 (open; head cf162b1, PROOF blob 873532b9) and improves its remainders O(h^(1/2)) to O(h^(3/4)): Lemma E (the E2-correction is O(v2 min(1, s))), Proposition 2.2+ (the model kernel fold - cusp is O(h^3 t^-12) beyond t_*), Lemma Phi (regression of the even part on E1), Lemma W (the elder set is an interval in phi_G whose edges move by -eta(-+3/2)/12 + O(eps^2); the even part cancels from the window length), Proposition M (the misclassified mass is O(h^(3/4))). Stdlib controls d1p_check.py (C1-C7, mutants M1-M7); drift-gated SOURCES.json; workflow. Two clean-context same-family referees: ACCEPT WITH MINOR FIXES, then ACCEPT on the delta. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .github/workflows/d1-sharp-remainder.yml | 156 +++++ .../d1_sharp_remainder_20261001/PROOF.md | 560 ++++++++++++++++++ .../d1_sharp_remainder_20261001/README.md | 153 +++++ .../d1_sharp_remainder_20261001/RESULTS.json | 233 ++++++++ .../d1_sharp_remainder_20261001/SOURCES.json | 141 +++++ .../d1_sharp_remainder_20261001/d1p_check.py | 516 ++++++++++++++++ 6 files changed, 1759 insertions(+) create mode 100644 .github/workflows/d1-sharp-remainder.yml create mode 100644 frontiers/d1_sharp_remainder_20261001/PROOF.md create mode 100644 frontiers/d1_sharp_remainder_20261001/README.md create mode 100644 frontiers/d1_sharp_remainder_20261001/RESULTS.json create mode 100644 frontiers/d1_sharp_remainder_20261001/SOURCES.json create mode 100644 frontiers/d1_sharp_remainder_20261001/d1p_check.py diff --git a/.github/workflows/d1-sharp-remainder.yml b/.github/workflows/d1-sharp-remainder.yml new file mode 100644 index 00000000..4208c851 --- /dev/null +++ b/.github/workflows/d1-sharp-remainder.yml @@ -0,0 +1,156 @@ +name: D1 sharp remainder 3/4 exact controls + +'on': + pull_request: + paths: + - 'frontiers/d1_sharp_remainder_20261001/**' + - '.github/workflows/d1-sharp-remainder.yml' + # bound merged sources (cited in SOURCES.json) and the pinned unmerged sources + - 'frontiers/cusp_second_order_20261001/PROOF.md' + - 'frontiers/d1_third_order_law_20261001/PROOF.md' + - 'frontiers/candidate_parity_rate_20261001/PROOF.md' + - 'frontiers/elder_third_order_20261001/PROOF.md' + - 'frontiers/third_order_rate_20261001/PROOF.md' + workflow_dispatch: + +permissions: + contents: read + pull-requests: read + +jobs: + exact-controls: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + GH_TOKEN: ${{ github.token }} + GH_REPOSITORY: ${{ github.repository }} + run: | + set -euo pipefail + python -B -S - <<'PY' + import base64, hashlib, json, os, pathlib, subprocess, sys, urllib.parse, urllib.request + root = pathlib.Path('frontiers/d1_sharp_remainder_20261001').resolve() + manifest = json.loads((root / 'SOURCES.json').read_text()) + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest['files']] + ['SOURCES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest['files']: + path = root / entry['path'] + if path.is_symlink(): + raise ValueError('symlink: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('packet file identity mismatch: ' + entry['path']) + def same(data, entry): + framed = b'blob ' + str(len(data)).encode() + b'\0' + data + return len(data) == entry['bytes'] and hashlib.sha256(data).hexdigest() == entry['sha256'] and hashlib.sha1(framed).hexdigest() == entry['git_blob'] + def tree_entry(path): + # the checked-out commit's tree entry for path: (mode, type, blob) or None; symlinks have mode 120000 + out = subprocess.run(['git', 'ls-tree', '-z', 'HEAD', '--', path], check=True, capture_output=True).stdout + if not out: + return None + meta, name = out.rstrip(b'\0').split(b'\t', 1) + if name.decode() != path: + raise ValueError('unexpected tree entry for ' + path) + mode, kind, sha = meta.decode().split() + return mode, kind, sha + def tree_bytes(entry): + # a source read from the checkout must be a regular file whose tree blob is the recorded one + te = tree_entry(entry['path']) + if te is None: + return None + mode, kind, sha = te + if mode != '100644' or kind != 'blob' or sha != entry['git_blob']: + raise ValueError('tree entry is not the recorded regular-file blob (mode/type/blob ' + ' '.join(te) + '): ' + entry['path']) + path = pathlib.Path(entry['path']) + if path.is_symlink() or not path.is_file(): + raise ValueError('checkout path is not a regular file: ' + entry['path']) + return path.read_bytes() + for entry in manifest['consumed'] + manifest['cited_only']: + data = tree_bytes(entry) + if data is None or not same(data, entry): + raise ValueError('merged source drifted or absent: ' + entry['path']) + # unmerged sources are bound to their recorded commit, path and blob through the repository API: the head must + # resolve, the path in that head's tree must be a file with the recorded blob id and size, and the bytes must have + # the recorded sha256; a consumed dependency that has landed is instead read from the tree and must be identical + # to the pinned version (else this packet needs rebinding) + api = 'https://api.github.com/repos/' + os.environ['GH_REPOSITORY'] + def get_json(url): + req = urllib.request.Request(url, headers={'Authorization': 'Bearer ' + os.environ['GH_TOKEN'], + 'Accept': 'application/vnd.github+json'}) + with urllib.request.urlopen(req, timeout=60) as resp: + return json.load(resp) + def bound(entry): + commit = get_json(api + '/commits/' + entry['head']) + if commit.get('sha') != entry['head']: + raise ValueError('recorded head does not resolve: ' + entry['head']) + node = get_json(api + '/contents/' + urllib.parse.quote(entry['path']) + '?ref=' + entry['head']) + if (node.get('type') != 'file' or node.get('path') != entry['path'] or node.get('sha') != entry['git_blob'] + or node.get('size') != entry['bytes']): + raise ValueError('recorded head/path does not map to the recorded blob: ' + entry['path']) + blob = get_json(api + '/git/blobs/' + entry['git_blob']) + if blob.get('encoding') != 'base64': + raise ValueError('unexpected blob encoding for ' + entry['path']) + return base64.b64decode(blob['content']) + def current(entry): + # drift gate (as on #220, after Copilot's review there): the recorded head keeps resolving after a dependency PR advances, so + # also resolve the dependency PR now. Open: the file at its current head must be the pinned blob. Merged: + # the file at its merge commit must be the pinned blob. Closed unmerged: rebinding is required. + pr = get_json(api + '/pulls/' + entry['pr'].split('#', 1)[1]) + if pr.get('merged'): + ref = pr.get('merge_commit_sha') + elif pr.get('state') == 'open': + ref = pr['head']['sha'] + else: + raise ValueError('dependency ' + entry['pr'] + ' closed without merge: rebind required') + node = get_json(api + '/contents/' + urllib.parse.quote(entry['path']) + '?ref=' + ref) + if node.get('type') != 'file' or node.get('sha') != entry['git_blob'] or node.get('size') != entry['bytes']: + raise ValueError('dependency ' + entry['pr'] + ' advanced: ' + entry['path'] + ' at ' + ref + + ' is not the pinned blob (rebind required)') + return ref + for kind in ('consumed_unmerged', 'cited_unmerged'): + for entry in manifest.get(kind, []): + # a landed consumed dependency must be the recorded regular-file blob in this tree (symlinks and any + # other mode are rejected by tree_bytes); otherwise the source is bound through the API + landed = tree_bytes(entry) if kind == 'consumed_unmerged' else None + if landed is not None: + data, where = landed, 'tree' + else: + if os.path.lexists(entry['path']) and kind == 'consumed_unmerged': + raise ValueError('path present in the checkout but not as a tracked blob: ' + entry['path']) + data, where = bound(entry), 'head/path/blob api' + if not same(data, entry): + raise ValueError(kind + ' source differs from its pinned blob (rebind required): ' + entry['path'] + ' via ' + where) + now = current(entry) if kind == 'consumed_unmerged' else None + print(json.dumps({kind + '_bound': entry['path'], 'git_blob': entry['git_blob'], 'head': entry['head'], + 'via': where, 'current_ref_checked': now})) + script = str(root / 'd1p_check.py') + expected = (root / 'RESULTS.json').read_bytes() + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], check=True, capture_output=True, timeout=600).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + # each mutant must exit 1 and fail in its own control (the 'failed' message starts with the control label) + for m, control in sorted(manifest['mutants'].items()): + proc = subprocess.run([sys.executable, *flags, script, '--mutant', m], capture_output=True, timeout=600) + if proc.returncode != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + failed = json.loads(proc.stderr.decode().strip().splitlines()[-1])['failed'] + if not failed.startswith(control + ' '): + raise RuntimeError('mutant ' + m + ' failed outside ' + control + ': ' + failed) + for bad in (['--mutant', 'M99'], ['--mutant']): + rc = subprocess.run([sys.executable, *flags, script, *bad], capture_output=True, timeout=600).returncode + if rc != 2: + raise RuntimeError('bad mutant argument ' + repr(bad) + ' not rejected with exit 2') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/frontiers/d1_sharp_remainder_20261001/PROOF.md b/frontiers/d1_sharp_remainder_20261001/PROOF.md new file mode 100644 index 00000000..a5d8da20 --- /dev/null +++ b/frontiers/d1_sharp_remainder_20261001/PROOF.md @@ -0,0 +1,560 @@ +# The one-dimensional lifetime and crest-to-trough laws with remainder `O(h^{3/4})` + +Object: CL-D1-SHARP-REMAINDER-20261001-v1. +Author: Anthropic Claude (claude.ai session `session_01NMeKEismAyeqgdB4sy2NJU`), 1 October 2026. +Disposition: AUTHOR-SIDE PROOF CANDIDATE; NONAUTHOR REVIEW REQUIRED. Scientific effect: NONE — no register, graph, +STATUS, PROOF_INDEX, prize or Boolean change. Same GitHub account as every lane; zero organizational independence. +**Consumes** Math- #214 (open, unmerged; head `cf162b1c69…`, `frontiers/d1_third_order_law_20261001/PROOF.md` blob +`873532b9`, v1.1), cited below as [D1]. Its nonauthor analytic review (OpenAI Codex, comment 5933752065, "Slices A–D and +Theorem D1 ACCEPTED at the stated circle scope") was given on head `f4a58df`; the refresh to `cf162b1` merged `main` and +left the packet's bytes unchanged. Used from [D1]: §§0–5 as stated, and also the intermediate estimates in the proof of +[D1] Prop. 2.2 (c)–(d). §2 reruns those estimates on a longer range. The expansions among them follow from [D1] Lemma +1.3, the bounds on `ζ_θ` are properties of `ζ_θ` alone, and none of them uses `t ≤ t_*` (Prop. 2.2⁺ (c)). Nothing else +is consumed. + +## 0. Statement + +Setting, notation and constants are those of [D1] §0–§1: +- the circle `T = R/LZ` and the hypothesis (H); +- the canonical two-point densities `ν₊` (crest-to-trough amplitude) and `ν` (persistence lifetime); +- the pair at `±τ`, with separation `t = 2τ`, gap `h`, `α = 12h/t³` and `κ = h/t⁴`; +- the pinned law `Q = Q_{t,α}` and the pair variables `E₁, E₂, m = c(t)α, v₁, v₂`; +- the constants `C₀, C₁, I = (3^{1/4}/2)C₁, B₂`. + +Throughout, `‖u‖_{C²} := max(sup|u|, sup|u'|, sup|u''|)` on `[−2, 2]`. + +**Theorem D1⁺.** Under (H), as `h ↓ 0` and `ℓ ↓ 0`, + + ν₊(h) = (C₀/2) h^{−1/3} + (I/2) h^{1/4} + B₂ h^{1/3} + O(h^{3/4}), (D1⁺.1) + ν(ℓ) = C₀ ℓ^{−1/3} + C₁ ℓ^{1/4} + 2B₂ ℓ^{1/3} + O(ℓ^{3/4}). (D1⁺.2) + +In particular `2ν₊(ℓ) − ν(ℓ) = (I − C₁)ℓ^{1/4} + O(ℓ^{3/4})`. [D1] §0 reads `2ν₊ − ν` as the density of adjacent +max/min pairs that are not elder pairs. + +[D1] proved the same expansions with `O(h^{1/2})`; its proof gives `O(h^{0.57})` for (D1.1). The exponent `3/4` is the +order of the first correction to the cusp term (§5.1). No claim is made that its coefficient is nonzero. + +**What limited [D1], and what replaces it.** + +| | [D1] | limit | here | +|---|---|---|---| +| `E₂`-correction | Prop. 2.2 (a): kernel `≤ Ct²` on `t ≤ t_*` | `O(t_*³) = O(h^{0.61})` | Lemma E: kernel `≤ Ct² min(1, s)`, `s = m v₁^{−1/2} ≍ κ`, so `O(h^{3/4})` | +| tails at `t_*` | Prop. 2.2 (c), (d): fold and cusp cut at `t_*` separately | `O(h²t_*^{−7}) = O(h^{0.57})` | Prop. 2.2⁺ (b): their difference, the model kernel, is `O(h³t^{−12})` beyond `t_*`, so both are integrated to a fixed `t₀` | +| elder misclassification | §5: window perturbation of relative size `t/κ`, bounded in absolute value | `O(h^{1/2})` | Lemmas Φ, W and Prop. M: given all but `φ_G = E₁/m`, the elder set is an interval `(φ₋, φ₊)` independent of `φ_G`. The misclassified mass is first order in the mean of the first-order part of `φ₊ − φ₋ − 2/3`, which is `O(t²)`, and second order in its fluctuation, `O((t/κ)²)`. | + +**Mechanism.** +- *Splitting and regression.* Under `Q` the field splits into independent even and odd parts ([D1] Remark 1.4). + Regressing the even part on `E₁` makes the rescaled field affine in `φ_G := E₁/m` (Lemma Φ). The profile is + `≈ 3(X² − ¼)²`, and the remainder is independent of `φ_G`. +- *The elder set is an interval.* The elder rule is monotone in `φ_G` near the window edges `±1/3`. So, given the + remainder, the elder set is an interval `(φ₋, φ₊)`. To first order its edges move by the values of the perturbation at + `∓3/2`, where `∂_φ` of the competing critical value is `12` (Lemma W). +- *What moves the edges.* The even remainder `B` moves both edges the same way. A translation of the window costs + nothing to first order, because the weight and the density of `φ_G` are even. The odd part changes the window length + by `O(3/2)/6`, and the deterministic even profile `φÊ` changes it by `−Ê(3/2)/18`. +- *Why the mean is `O(t²)`.* The mean of this first-order part is `O(t²)`: the pins see the odd jets only through + `α ≍ κt`, and `Ê = O(t²)`. +- *Second order.* The fluctuations, of relative size `t/κ`, enter at second order, and through the correlation + `2m Cov(E₂, O(3/2))` of `O` with the weight. + +Both orders are relative `O(t² + (t/κ)²)` of the edge mass, which integrates to `O(h^{3/4})` (Proposition M). + +**Not claimed.** The `h^{3/4}` coefficient or its sign; sharpness of `3/4`; uniformity in the covariance; anything on `R` +([D1] §6.4). + +## 1. The `E₂`-correction + +As in [D1] §2, let `E₁ ~ N(0, v₁)` and `E₂ ~ N(0, v₂)` be independent, `m > 0` and `s := m v₁^{−1/2}`. Put + + w := ((m + E₂)² − E₁²)⁺1{m + E₂ > 0}, G₁ := E w, G_{1/3} := E[w 1{|E₁| < m/3}], + g_θ := E[(m² − E₁²)⁺1{|E₁| < θm}] for θ ∈ {1, 1/3}. + +**Lemma E.** For `θ ∈ {1, 1/3}`, with an absolute constant `C`, + + 0 ≤ G_θ − g_θ ≤ C [ v₂ min(1, s) + (v₂ + m²) e^{−m²/(8v₂)} ]. (1.1) + +*Proof.* For `a ≥ 0` put `q_a(e) := (m + e)² − a²` and `χ_a(e) := q_a(e)1{m + e > a} = ((m + e)² − a²)⁺1{m + e > 0}`. +`χ_a` is convex: it is zero for `e ≤ a − m`, equal to `q_a` beyond, and `q_a'(a − m) = 2a ≥ 0`. So +`Ψ(a) := Eχ_a(E₂) − χ_a(0) ≥ 0`. By independence, `G₁ − g₁ = EΨ(|E₁|)` and +`G_{1/3} − g_{1/3} = E[Ψ(|E₁|)1{|E₁| < m/3}]`, which gives the lower bound. + +If `m² < 64v₂`, the upper bound is trivial: `G_θ − g_θ ≤ G₁ ≤ E(m + E₂)² = m² + v₂ ≤ e⁸(v₂ + m²)e^{−m²/(8v₂)}`. So assume +`m² ≥ 64v₂`, and put `T(x) := E[E₂²1{|E₂| > x}] ≤ C(v₂ + x²)e^{−x²/(2v₂)}`. + +(i) `a ≤ m/2`. On `{|E₂| ≤ m/2}`, `χ_a(E₂) = χ_a(0) + 2mE₂ + E₂²`, and `E[E₂1{|E₂| ≤ m/2}] = 0`. On `{|E₂| > m/2}`, +`χ_a(E₂) ≤ (m + |E₂|)² ≤ 9E₂²`. So `Ψ(a) ≤ v₂ + 9T(m/2)`. + +(ii) `m/2 < a ≤ 2m`, with `b := |a − m|`. +- If `a < m`, then `χ_a = q_a − q_a1{E₂ ≤ −b}`. On `{E₂ ≤ −b}`, + `−q_a(E₂) = (|E₂| − b)(m + a − |E₂|) ≤ 3m(|E₂| − b)⁺`. Since `Eq_a(E₂) − q_a(0) = v₂`, `Ψ(a) ≤ v₂ + 3mE(|E₂| − b)⁺`. +- If `a ≥ m`, then `χ_a(0) = 0` and `χ_a(e) = (e − b)⁺(e − b + 2a) ≤ (|e| − b)⁺(|e| + 4m)`. + +In both cases `Ψ(a) ≤ v₂ + E[(|E₂| − |a − m|)⁺(|E₂| + 4m)]`. + +(iii) `a > 2m`, with `b := a − m > m`. For `e > b`, `χ_a(e) ≤ e(e + b + 2m) ≤ 4e²`, so `Ψ(a) ≤ 4T(m)`. + +For `θ = 1/3` only (i) occurs, and `P(|E₁| < m/3) ≤ min(1, s)`. For `θ = 1`, + + EΨ(|E₁|) ≤ (v₂ + 9T(m/2))P(|E₁| ≤ 2m) + E[(|E₂| + 4m)∫_{m/2}^{2m}(|E₂| − |a − m|)⁺p_{|E₁|}(a)da] + 4T(m). + +Fix `E₂ = e`. If `|e| ≤ m/2`, the integrand lives on `|a − m| < |e|`, where `p_{|E₁|}(a) ≤ 2(2πv₁)^{−1/2}e^{−s²/8}`, +and `∫(|e| − |a − m|)⁺da = e²`. If `|e| > m/2`, the integral is at most `|e|`. So the middle term is at most + + 2(2πv₁)^{−1/2}e^{−s²/8}E[(|E₂| + 4m)E₂²] + 9T(m/2) ≤ C(m + v₂^{1/2})v₂v₁^{−1/2}e^{−s²/8} + 9T(m/2). + +Now `m v₁^{−1/2} = s`, `v₂^{1/2} ≤ m/8`, `s e^{−s²/8} ≤ 2 min(1, s)` and `P(|E₁| ≤ 2m) ≤ 2 min(1, s)`, which give +(1.1). ∎ + +Control C6 checks this order on a grid. Write `Φ` and `ϕ` for the standard normal distribution function and density. +- `(G_θ − g_θ)/(v₂ min(1, s))` stays in `[0, 2]`. +- As `v₂/v₁ → 0`, `(G_θ − g_θ)/v₂` approaches `2Φ(s) − 1 + 2sϕ(s)` for `θ = 1` and `2Φ(s/3) − 1` for `θ = 1/3`. + +## 2. The sign kernels to `O(h^{3/4})` + +**Proposition 2.2⁺.** Fix `δ ∈ (0, 1/10]` and `t_* := (12h)^{1/(5−δ)}`, as in [D1] Prop. 2.2 (`t ≤ t_*` iff +`α ≥ t^{2−δ}`). For `θ ∈ {1, 1/3}`, with `I₁ := I` and `I_{1/3} := C₁`, + + ∫₀^{t_*} K_θ^{sign}(t, h) dt = (C₀/2) h^{−1/3} + (I_θ/2) h^{1/4} + B₂ h^{1/3} + O(h^{3/4}). + +*Proof.* Fix `t₀ ∈ (0, 1]` so small that the expansions of [D1] Lemma 1.3 hold on `t ≤ t₀`, and let `h` be so small +that `t_* ≤ t₀`. The model kernel ([D1] Prop. 2.2 (b)) is + + k_θ := (12/t⁴)p_t g_θ = (12/t⁴)p_t m² − (12/t⁴)p_t v₁ζ_θ(s). + +By Lemma 1.3: +- `m ≍ τα`, `v₁ ≍ τ⁴`, `v₂ ≍ τ⁶`; +- `p_t ≤ Ce^{−α²/(4σ₃²)}` and `(12/t⁴)v₁ ≤ C`; +- `s ≤ Cα/τ ≤ Ch/t⁴`. + +(a) *The `E₂`-correction.* On `t ≤ t_*`, `m²/v₂ ≥ cα²τ^{−4} ≥ ct^{−2δ}`. Lemma E gives + + 0 ≤ K_θ^{sign} − k_θ ≤ C(12/t⁴)p_t[v₂ min(1, s) + (v₂ + m²)e^{−m²/(8v₂)}] ≤ Ct² min(1, Ch/t⁴) + Ct^{−4}e^{−ct^{−2δ}}, + +using `(1 + α²)p_t ≤ C`. Since `∫₀^∞ t² min(1, h/t⁴) dt = (4/3)h^{3/4}` and + + ∫₀^{t_*}t^{−4}e^{−ct^{−2δ}}dt ≤ C_{c,δ} t_* e^{−(c/2)t_*^{−2δ}} = O(h^N) for every N, C_{c,δ} := sup_{t>0}t^{−4}e^{−(c/2)t^{−2δ}} < ∞, + +we get `∫₀^{t_*}(K_θ^{sign} − k_θ)dt = O(h^{3/4})`. + +The correction is integrated only up to `t_*`. Beyond `t ≍ h^{1/5}`, where `m ≍ v₂^{1/2}`, the difference +`K₁^{sign} − k₁` contains the non-adjacent sign pairs, whose contribution is of order one in `h` ([D1] §6.2); that range +is handled by the band lemma (§4). + +(b) *The tail of the model kernel.* `k_θ = (12/t⁴)p_t v₁γ_θ(s)` with +`0 ≤ γ_θ(s) = E[(s² − Z²)1{|Z| < θs}] ≤ s²P(|Z| < s) ≤ s³`. Hence `0 ≤ k_θ ≤ Cs³ ≤ Ch³t^{−12}` and + + ∫_{t_*}^{t₀}k_θ dt ≤ Ch³t_*^{−11} = O(h^{3 − 11/(5−δ)}). + +Since `δ ≤ 1/9`, the exponent is at least `3/4`; it is `37/49` for `δ = 1/10`. Here the fold term `(12/t⁴)p_t m²` and the +cusp term `(12/t⁴)p_t v₁ζ_θ(s)` are each of order `h²t^{−8}`. Their difference `k_θ` is smaller by the factor +`s ≍ h/t⁴`, since `γ_θ(s) = 2θ(1 − θ²/3)(2π)^{−1/2}s³(1 + O(s²))`. [D1] cut each at `t_*` separately and lost +`h²t_*^{−7}`. + +(c) *The model integral to `t₀`.* Run [D1] Prop. 2.2 (c)–(e) with the upper limit `t_*` replaced by `t₀`. None of the +estimates used in that proof uses `t ≤ t_*`. The expansions follow from [D1] Lemma 1.3 for `t ≤ t₀` and `α ≤ τ^{−1}`, +and from `p_t ≤ Ce^{−α²/(4σ₃²)}` beyond. The bounds on `ζ_θ` are properties of `ζ_θ` alone, and the split at `t_c` is a +device of the proof. The estimates are: the fold expansion with its `O(τ⁴(1 + α⁴))` term, the cusp expansion with +`|ε| ≤ Cτ²(1 + α²)`, the bounds on `ζ_θ`, `ζ_θ'` and `1 − ζ_θ`, and the split at `t_c = h^{1/4}`. The changes: +- in (c), the two leading integrals lose only their ranges `t > t₀`, which are `O(h²t₀^{−7}) = O(h²)`; the `τ⁴` term is + `O(h)`, and the range `α > τ^{−1}` is `O(e^{−c/h})`; +- in (d), the Mellin integral loses its range `t > t₀`, where `ζ_θ(s₀) ≤ Cs₀² = Ch²t^{−8}`, so `O(h²)`; +- the integral of `p₃(α) − p₃(0)` loses its range `t > t₀`, where `|p₃(α) − p₃(0)| ≤ Cα² ≤ Ch²t^{−6}`, so `O(h²)`; +- the term in `1 − ζ_θ(s₀)` is `O(h^{3/4})`, as there; +- the error `ε` is `O(h^{3/4})`, as there, the range `t ∈ [h^{1/4}, t₀]` using `ζ_θ(s₀) ≤ Cs₀²`; +- (e) is unchanged. + +So `∫₀^{t₀}k_θ dt = (C₀/2)h^{−1/3} + (I_θ/2)h^{1/4} + B₂h^{1/3} + O(h^{3/4})`. + +Finally `∫₀^{t_*}K_θ^{sign} = ∫₀^{t₀}k_θ − ∫_{t_*}^{t₀}k_θ + ∫₀^{t_*}(K_θ^{sign} − k_θ)`. ∎ + +## 3. The elder decision at first order + +### 3.1 Regression along `φ_G` + +Fix `t ≤ t₀` and `α > 0`, and work under `Q = Q_{t,α}`. By [D1] Remark 1.4, `f = f_e + f_o` with `f_e` and `f_o` +independent. +- `f_e` is centered, and its law does not depend on `α`: its only pin, `U₂ = 0`, is homogeneous, and `U₁, U₃` are + functionals of `f_o`. +- `f_o` has mean `αμ_t`, with `μ_t` deterministic and odd, and its centered part has a law that does not depend on `α`. + +As in [D1] Lemma 1.2, `E₁ := f_e''(τ)`, `m := E_Q f_o''(τ) = c(t)α`, `E₂ := f_o''(τ) − m`, `v₁ := Var_Q E₁` and +`s := m v₁^{−1/2}`. Define + + ψ(x) := Cov_Q(f_e(x), E₁)/v₁, f_e^⊥ := f_e − E₁ψ, φ_G := E₁/m, ω := (f_o, f_e^⊥). + +With `b := f(−τ)` and `F(X) := (f(tX) − b)/h` (the window field `𝔉` of [D1] Lemma 3.2), + + F = 2X³ − (3/2)X − ½ + O + B + φ_G Ψ̂, (3.1) + O(X) := f_o(tX)/h − 2X³ + (3/2)X, B(X) := (f_e^⊥(tX) − f_e^⊥(τ))/h, Ψ̂(X) := (m/h)(ψ(tX) − ψ(τ)). + +This uses `f_e(−τ) = f_e(τ)` and `f_o(−τ) = −f_o(τ) = h/2` on the pin event. The model +`g_φ = 2X³ − (3/2)X − ½ + 3φ(X² − ¼)²` is the odd cubic plus the even quartic (checker C1). So +`F = g_{φ_G} + O + B + φ_GÊ` with `Ê := Ψ̂ − 3(X² − ¼)²`. + +**Lemma Φ.** (Φ.0) Under `Q`: +- `φ_G ~ N(0, s^{−2})` is independent of `ω`, and `E₂` is a functional of `f_o`; +- `O` is odd, and `B`, `Ψ̂`, `Ê` are even; +- `Ψ̂` is deterministic and depends on `t` only; +- `O`, `B`, `Ê` and their first derivatives vanish at `X = ±½`. + +For `t ≤ t₀`, uniformly in `α`, on `[−2, 2]`: + +- (Φ.1) `‖Ê‖_{C²} ≤ Cτ²`; +- (Φ.2) `‖E_Q O‖_{C²} ≤ Ct²` and `‖O − E_QO‖_{C²} ≤ C(t/κ)K̃^o`, where `K̃^o := sup_{[−2t, 2t]}|(f_o − E_Qf_o)^{(5)}|`; +- (Φ.3) `‖B‖_{C²} ≤ C(t²/κ)K^⊥` for a random variable `K^⊥` with `E_Q e^{c(K^⊥)²} ≤ C`; also `E_Q e^{c(K̃^o)²} ≤ C`; +- (Φ.4) `f_o''(τ) = (h/t²)(6 + O''(½))`, so `m = (h/t²)(6 + E_QO''(½))` and `E₂ = (h/t²)(O − E_QO)''(½)`. In particular, + for `t ≤ t₀` small, `m ≥ h/t²` and `|E₂|/m ≤ ‖O − E_QO‖_{C²}/5`. Also `s = (72κ/σ₄)(1 + O(τ²))`. + +*Proof.* (Φ.0) `f_e^⊥` is jointly Gaussian with `E₁` and uncorrelated with it, and `f_o` is independent of `f_e`. The +parities are those of `f_e` and `f_o`. The vanishing at `±½`: +- `f_e'(±τ) = 0` under `Q`, so `ψ'(±τ) = 0` and `(f_e^⊥)'(±τ) = 0`; +- `Ψ̂(±½) = 0` because `ψ` is even, and `Ψ̂'(±½) = (mt/h)ψ'(±τ) = 0`. Since `3(X² − ¼)²` vanishes to second order at + `±½`, so does `Ê`; +- `f_o(±τ) = ∓h/2` and `f_o'(±τ) = 0`, while `2X³ − (3/2)X` takes the values `∓½` at `±½` with zero derivative there. + +(Φ.1) Let `a_j := f^{(j)}(0)`. Taylor's formula gives `f_e(x) = a₀ + a₂x²/2 + a₄x⁴/24 + R(x)`, with +`|R^{(k)}(x)| ≤ C|x|^{6−k}K^e` (`k ≤ 2`) and `K^e := sup_{[−2t, 2t]}|f_e^{(6)}|`. The pin `f_e'(τ) = 0` gives +`a₂ = −a₄τ²/6 − R'(τ)/τ`, hence (checker C3) + + f_e(x) − f_e(τ) = a₄(x² − τ²)²/24 + R̃(x), R̃(x) := R(x) − R(τ) − R'(τ)(x² − τ²)/(2τ), + E₁ = a₄τ²/3 + ρ₁, ρ₁ := R''(τ) − R'(τ)/τ, + +with `|∂_X^k R̃(tX)| ≤ Ct⁶K^e` on `[−2, 2]` (`k ≤ 2`) and `|ρ₁| ≤ Cτ⁴K^e`. The `Q`-law of `f_e` is free of `α`, and +`E_Q(K^e)² ≤ C` by Sudakov–Fernique and Borell–TIS, as in [D1] Lemma 4.3. Also `V := Var_Q a₄ → σ₄²`, so `V ∈ [c, C]`. +Then + + v₁ = (τ⁴/9)V(1 + O(τ²)), Cov_Q(f_e(tX) − f_e(τ), E₁) = (t⁴/24)(X² − ¼)²(τ²V/3)(1 + O(τ²)) + Cov_Q(R̃(tX), E₁), + +and `|Cov_Q(∂_X^kR̃(tX), E₁)| ≤ Ct⁶τ²`. Since `m/h = 12c(t)/t³ = (6/t²)(1 + O(τ²))` (Lemma 1.3), the first term gives +`(m/(hv₁))(t⁴/24)(τ²V/3)(X² − ¼)² = 3(X² − ¼)²(1 + O(τ²))`; checker C3 checks the leading constant `3`. The second term +contributes `O(t^{−2}t⁶τ²τ^{−4}) = O(t²)` in `C²`. + +(Φ.2) Write `f_o(x) = a₁x + a₃x³/6 + R_o(x)`, with `|R_o^{(k)}(x)| ≤ C|x|^{5−k}K^o` and `K^o := sup_{[−2t, 2t]}|f_o^{(5)}|`. +The odd cubic `H₀(x) := h(2(x/t)³ − (3/2)(x/t))` satisfies `H₀'(τ) = 0` and `H₀(τ) = −h/2`. Let `p₁`, `p₂` be the odd +cubic Hermite basis at `τ`: `p₁(x) = (3/2)(x/τ) − ½(x/τ)³` and `p₂(x) = (τ/2)((x/τ)³ − x/τ)`, so that `p₁(τ) = 1`, +`p₁'(τ) = 0`, `p₂(τ) = 0` and `p₂'(τ) = 1`. The pins then give + + f_o = H₀ + R̃_o, R̃_o := R_o − R_o(τ)p₁ − R_o'(τ)p₂. + +So `O = R̃_o(t·)/h` and `‖O‖_{C²} ≤ C(t⁵/h)K^o = C(t/κ)K^o`. The map `f_o ↦ R̃_o` is linear, which gives both bounds. +- *Applied to `αμ_t`* it gives `‖E_QO‖_{C²} ≤ C(αt⁵/h)sup_{[−2t, 2t]}|μ_t^{(5)}| = 12Ct² sup|μ_t^{(5)}|`. The sup is + bounded uniformly: `μ_t^{(5)}(x) = Cov(f_o^{(5)}(x), (U₁, U₃))Cov(U₁, U₃)^{−1}e₂` is continuous in `(t, x)`, + `Cov(U₁, U₃)` is invertible for each `t > 0` ([D1] Lemma 1.1), and it has a nondegenerate limit as `t ↓ 0` ([D1] Lemma + 1.3). So `sup_{t ≤ t₀}sup_{[−2t,2t]}|μ_t^{(5)}| < ∞`. +- *Applied to `f_o − E_Qf_o`* it gives the second bound. + +(Φ.3) We have `B = [a₄^⊥(t⁴/24)(X² − ¼)² + R̃^⊥(tX)]/h`, where `a₄^⊥ := a₄ − E₁Cov_Q(a₄, E₁)/v₁` and +`R̃^⊥ := R̃ − E₁Cov_Q(R̃, E₁)/v₁`. +- `Var_Q a₄^⊥ = Var_Q(a₄ | E₁) ≤ Var_Q(a₄ − 3E₁/τ²) = 9Var_Q(ρ₁)/τ⁴ ≤ Cτ⁴`. +- `|E₁Cov_Q(∂_X^kR̃(tX), E₁)/v₁| ≤ Ct⁶|Z|`, with `Z := E₁v₁^{−1/2}` standard normal. + +So the bound holds with `K^⊥ := C(|a₄^⊥|/t² + K^e + |Z|)`. Each term has a Gaussian tail uniformly, and so does `K̃^o` +(Borell–TIS). + +(Φ.4) `f_o''(τ) = (h/t²)∂_X²(2X³ − (3/2)X + O)|_{X=½}` and `∂_X²(2X³ − (3/2)X)|_{½} = 6`. Then +`|E_QO''(½)| ≤ Ct²`. Lemma 1.3 gives `s = mv₁^{−1/2} = 3α/(τσ₄)(1 + O(τ²))`, and `3α/(τσ₄) = 72κ/σ₄`. ∎ + +### 3.2 The window edges + +The model `g_φ` of [D1] (3.1) has its third critical point at `X₃ = −1/(2φ)`. There (checker C1) + + Γ₊(φ) := g_φ(X₃) + 1 = (φ + 1)³(3φ − 1)/(16φ³), Γ₋(φ) := g_φ(X₃) = (φ − 1)³(3φ + 1)/(16φ³), + Γ₊'(φ) = Γ₋'(φ) = 3(1 − φ²)²/(16φ⁴), Γ₊(1/3) = Γ₋(−1/3) = 0, Γ₊'(1/3) = Γ₋'(−1/3) = 12, g_φ''(X₃) = 3(1 − φ²)/φ. (3.2) + +Put `η₀ := 1/100`, `J₊ := [1/3 − η₀, 1/3 + η₀]` and `J₋ := −J₊`. + +**Lemma W (the window edges to first order).** There is an absolute `c₀ > 0` with the following property. + +*Hypotheses.* +- `η⁰, Ê ∈ C²([−2, 2])` vanish with their first derivatives at `±½`; +- `ε := ‖η⁰‖_{C²} + 2‖Ê‖_{C²} ≤ c₀`; +- for `φ ∈ R`, `F_φ := g_φ + η_φ` on `[−2, 2]`, with `η_φ := η⁰ + φÊ`; +- for each `φ`, `F_φ` is the window field of a pair `(𝔐, 𝔖) = (−½, ½)` of a function `f_φ` on `T`. + +*Conclusions.* +- (W.1) There are `φ₊ ∈ J₊` and `φ₋ ∈ J₋` such that, for every `φ` for which the pair is typed, `𝔖` is `𝔐`'s death + point iff `φ₋ < φ < φ₊`, except at `φ ∈ {φ₋, φ₊}`. +- (W.2) `φ₊ = 1/3 − η_{1/3}(−3/2)/12 + r₊` and `φ₋ = −1/3 − η_{−1/3}(3/2)/12 + r₋`, with `|r_±| ≤ Cε²`. +- (W.3) If `η⁰ = O + B` with `O` odd and `B` even, then + `φ₊ − φ₋ − 2/3 = O(3/2)/6 − (Ê(3/2) + Ê(−3/2))/36 + r₊ − r₋`. If moreover `Ê` is even, + + φ₊ − φ₋ − 2/3 = O(3/2)/6 − Ê(3/2)/18 + r₊ − r₋. (3.3) + +*Proof.* *Typing.* For `|φ| ≤ 2`, `‖F_φ − g_φ‖_{C²} ≤ ε`, and typing forces `|φ| < 1 + ε/6` ([D1] Lemma 3.3). For +`|φ| > 2` the pair is not typed: +- for `φ > 2`, `F_φ''(−½) = 6(φ − 1) + η⁰''(−½) + φÊ''(−½) ≥ 6(φ − 1) − ε − φε/2 > 0`; +- for `φ < −2`, symmetrically `F_φ''(½) < 0`. + +*Off the edges.* [D1] Lemma 3.3 with `η = η₀`, taking `c₀ ≤ c₀^{[D1]}η₀`, gives: for typed `φ` with +`||φ| − 1/3| ≥ η₀`, `𝔖` is the death point iff `|φ| < 1/3`. + +*The edge `J₊`.* Fix `φ ∈ J₊`. The model satisfies, exactly (checker C2): +- `g' = 12φ(X² − ¼)(X − X₃)` with `X₃ ∈ [−150/97, −150/103] ⊂ [−1.55, −1.45]`; +- `12φ(X² − ¼) ≥ 2.9` on `[−2, −1]`; +- `g(−2) = 675φ/16 − 27/2 ≥ 9/64`; +- `g''(X₃) ≥ 7.7`, and `|g'''| = |12 + 72φX| ≤ 52` on `[−1.6, −1.4]`; +- `g(X₃) = Γ₊(φ) − 1 ≤ −0.88`; +- `g + 1 ≥ 2(X + 1)(X − ½)² ≥ 3(X − ½)²` on `[½, 3/2]`, and `g(3/2) = 12φ + 4 > 7`; +- `g' < 0` on `(−½, ½)`, with `|g'| ≥ 1.8(½ − |X|)`; +- `g − g(X₃) = (X − X₃)²(3φX² − X + (1 − 6φ²)/(4φ))`, and the quadratic factor is `≥ 2.24` on `[−2, −1]`. + +Since `η_φ` and `η_φ'` vanish at `±½` and `|η_φ''| ≤ ε`, we have `|η_φ'(X)| ≤ ε|X ∓ ½|` and +`|η_φ(X)| ≤ (ε/2)(X ∓ ½)²`. Hence, for `c₀ ≤ 1/10` small enough: +- `F' < 0` on `(−½, ½)`; +- `F + 1 ≥ (3 − ε)(X − ½)² > 0` on `(½, 3/2]`, and `F(3/2) > 0`; +- `F' > 0` on `[−1, −½)`, since `g' ≥ 1.7|X + ½|` there; +- on `[−2, −1]`, `F'` vanishes only within `ε/2.9 ≤ 1/20` of `X₃`. There `g'' ≥ 7.7 − 52/20 ≥ 5.1`, so `F'' ≥ 5`. + +So `F` has on `[−2, −½)` exactly one critical point `X₃'`, a nondegenerate minimum, and `F(−2) > 0 > F(X₃')`. +- The arc from `𝔐` in the positive direction descends to `𝔖`, stays above `−1` elsewhere, and exceeds `0` before `3/2`: + `m₊ = −1`. +- The arc in the negative direction descends to `F(X₃')` and rises above `0` before `−2`: + `m₋ = F(X₃') = μ₊(φ) := min_{[−2, −1]}F_φ`. + +Hence `𝔖` is the death point iff `μ₊(φ) < −1`. + +For `φ' > φ`, on `[−2, −1]`, + + F_{φ'} − F_φ = (φ' − φ)(3(X² − ¼)² + Ê) ≥ (φ' − φ)(27/16 − ε) ≥ φ' − φ, + +so `μ₊` increases with slope at least `1`. Since `g ≥ g(X₃) + 2.24(X − X₃)² ≥ g(X₃) + 1.45(X − X₃)²` on `[−2, −1]` and +`|η_φ'| ≤ ε`, + + Γ₊(φ) − 1 + η_φ(X₃(φ)) − ε²/5.8 ≤ μ₊(φ) ≤ Γ₊(φ) − 1 + η_φ(X₃(φ)). + +At `φ = 1/3` this gives `|μ₊(1/3) + 1| ≤ 2ε`. So the root `φ₊` of `μ₊ = −1` exists, is unique in `J₊`, and satisfies +`|φ₊ − 1/3| ≤ 2ε`. At `φ₊`: +- `Γ₊(φ₊) = 12(φ₊ − 1/3) + O(ε²)`, by (3.2) and `|Γ₊''| ≤ C` on `J₊`; +- `η_{φ₊}(X₃(φ₊)) = η_{1/3}(−3/2) + O(ε²)`, since `|η_{φ₊} − η_{1/3}| ≤ |φ₊ − 1/3|‖Ê‖_{C⁰}` and + `|X₃(φ₊) + 3/2| ≤ C|φ₊ − 1/3|`. + +This proves (W.2) for `φ₊`. + +*The edge `J₋`.* This is the mirror case. Checker C1 checks the symmetry `g(−X, −φ) = −1 − g(X, φ)` and +`Γ₋(φ) = −Γ₊(−φ)`; checker C2 checks `g(2) + 1 = 675φ/16 + 27/2 ≤ −9/64` and `g''(X₃) ≤ −7.7`. Fix `φ ∈ J₋`. +- *The negative direction.* The arc falls below `−1` before exceeding `0`, as in [D1] Lemma 3.3 (E) for `φ < 0`. So + `m₋ < −1`. +- *The positive direction.* The arc descends to `𝔖` and rises to a nondegenerate local maximum `F(X₃'')`, with `X₃''` + near `X₃ ∈ [1.45, 1.55]`. It then falls below `−1` before `2`. So `m₊ = −1` iff `μ₋(φ) := max_{[1, 2]}F_φ > 0`. + +Hence `𝔖` is the death point iff `μ₋(φ) > 0`. The function `μ₋` increases with slope at least `1`, and by the same +envelope bound its root `φ₋` satisfies (W.2). + +(W.1) collects the three regimes. For (W.3): + + η_{1/3}(−3/2) = −O(3/2) + B(3/2) + Ê(−3/2)/3, η_{−1/3}(3/2) = O(3/2) + B(3/2) − Ê(3/2)/3. + +The even part `B` cancels from the window length; it only translates the window (checker C4). ∎ + +### 3.3 The misclassified mass + +Let `K(t, h)` be the elder kernel [D1] (1.3) and `K_{1/3}^{sign} = (12/t⁴)p_t E_Q[w 1{|φ_G| < 1/3}]` the sign kernel, +where `w = (−f''(−τ))⁺f''(τ)⁺ = ((m + E₂)² − E₁²)⁺1{m + E₂ > 0}` ([D1] (1.4)). + +**Proposition M.** For `δ ∈ (0, 1/10]` and `t_*` as above, `∫₀^{t_*}|K(t, h) − K_{1/3}^{sign}(t, h)| dt = O(h^{3/4})`. + +*Proof.* Fix `α` and `t ≤ t_*`, with `h` small enough that `t_* ≤ t₀`. By Lemma Φ, conditionally on `ω`: +- `φ_G` has density `p_s(φ) := (s/√(2π))e^{−s²φ²/2}`; +- `E₂`, and the field (3.1) for each value of `φ_G`, are functions of `(ω, φ_G)`; +- `w = W(φ_G)` with `W(φ) := m²((1 + E₂/m)² − φ²)⁺1{m + E₂ > 0}`. + +Put + + ε(ω) := ‖O‖_{C²} + ‖B‖_{C²} + 2‖Ê‖_{C²}, 𝒢 := {ε(ω) ≤ c₁}, + +with `c₁ ≤ c₀` so small that on `𝒢` Lemma W applies to `F_φ = g_φ + (O + B) + φÊ` (with `Ê` even, (Φ.0)) and +`|E₂|/m ≤ 1/10` (Φ.4). On `𝒢`, `W > 0` on `(φ₋, φ₊)`, so the pair is typed there, and by (W.1) + + E_Q[w 1{elder} | ω] = ∫_{φ₋}^{φ₊} W p_s dφ, E_Q[w 1{|φ_G| < 1/3} | ω] = ∫_{−1/3}^{1/3} W p_s dφ. + +*First order.* On `𝒢`, `|φ₊ − 1/3|, |φ₋ + 1/3| ≤ Cε ≤ 1/12`, and `W` and `p_s` are even. So + + Δ := ∫_{φ₋}^{φ₊} W p_s − ∫_{−1/3}^{1/3} W p_s = (Wp_s)(1/3)·(φ₊ − φ₋ − 2/3) + r₂, + |r₂| ≤ ½[(φ₊ − 1/3)² + (φ₋ + 1/3)²] sup_{1/4 ≤ |φ| ≤ 5/12}|(Wp_s)'| ≤ Cε² m²(1 + s²) s e^{−s²/32}, + +since `|(Wp_s)'(φ)| ≤ (2m²|φ| + Ws²|φ|)p_s(φ)` and `p_s(φ) ≤ (s/√(2π))e^{−s²/32}` for `|φ| ≥ 1/4`. With +`e_s := p_s(1/3) = (s/√(2π))e^{−s²/18}`, on `𝒢` we have `(Wp_s)(1/3) = e_s(8m²/9 + 2mE₂ + E₂²)`. By (3.3), + + Δ = e_s (8m²/9 + 2mE₂ + E₂²)(O(3/2)/6 − Ê(3/2)/18) + R₄, |R₄| ≤ C m²(1 + s²) s e^{−s²/32} ε². + +*The mean.* `E₂` is centered, and `E₂` and `O − E_QO` are jointly Gaussian, so `E[E₂²(O − E_QO)(3/2)] = 0` and + + E[(8m²/9 + 2mE₂ + E₂²) O(3/2)] = (8m²/9 + v₂)E_QO(3/2) + 2m Cov_Q(E₂, O(3/2)). + +The bounds: +- by (Φ.2), `|E_QO(3/2)| ≤ Ct²` and `|Cov_Q(E₂, O(3/2))| ≤ v₂^{1/2}(Var_Q O(3/2))^{1/2} ≤ Cτ³(t/κ)`; +- by (Φ.1), `|Ê(3/2)| ≤ Cτ²`; +- since `m(t/κ) = 12mt²/α ≍ τ³`, also `mτ³(t/κ) ≤ Cm²(t/κ)²`; +- `v₂ ≤ Cm²`, since `m²/v₂ ≥ ct^{−2δ} ≥ c` on `t ≤ t_*` (Prop. 2.2⁺ (a)). + +Hence + + |E[e_s(8m²/9 + 2mE₂ + E₂²)(O(3/2)/6 − Ê(3/2)/18)]| ≤ C e_s m² (t² + (t/κ)²), + +and by (Φ.2)–(Φ.3), `E_Qε² ≤ C(t⁴ + (t/κ)² + (t²/κ)² + τ⁴) ≤ C(t² + (t/κ)²)`. + +*The bad event.* Off `𝒢` there are two contributions. +- Both conditional expectations are at most `E[w | ω] ≤ (m + |E₂|)²`. By Cauchy–Schwarz this contributes at most + `C(m² + v₂)P(𝒢^c)^{1/2}`. +- The main term above carries `e_s ≤ s/√(2π)` and the factor `O(3/2)`. By Cauchy–Schwarz and `E_Q[O(3/2)⁴] ≤ C` (Φ.2) + it contributes at most `Cs(m² + v₂)P(𝒢^c)^{1/2}`. + +On `t ≤ t_*` we have `κ/t = α/(12t²) ≥ t^{−δ}/12` and `‖E_QO‖_{C²} + 2‖Ê‖_{C²} ≤ Ct² ≤ c₁/2`. The Gaussian tails of +`K̃^o` and `K^⊥` then give `P(𝒢^c) ≤ Ce^{−c(κ/t)²} ≤ Ce^{−ct^{−2δ}}`. + +*Collecting.* For `t ≤ t_*`, + + |K − K_{1/3}^{sign}| ≤ C(12/t⁴)p_t [ m²(1 + s²) s e^{−s²/32}(t² + (t/κ)²) + (1 + s)(m² + v₂)e^{−ct^{−2δ}} ]. + +Now `(12/t⁴)m² ≤ Cα²/t² ≤ Cs²`, `(12/t⁴)v₂ ≤ Ct²` and `(t/κ)² = 144t⁴/α² ≤ Ct²/s²`, because `α/t ≍ s ≍ h/t⁴` (Φ.4). +- *The first part* is at most `Ct²(s + s⁵)e^{−s²/32} ≤ Ct² min(h/t⁴, e^{−ch²/t⁸})`. Its integral over `(0, ∞)` is + `≤ Ch^{3/4}`: split at `t = h^{1/4}`, or substitute `t = (h/u)^{1/4}`, `t²dt = (1/4)h^{3/4}u^{−7/4}du` (checker C7). +- *The second part* is at most `C(1 + s³)e^{−ct^{−2δ}} ≤ C(1 + h³t^{−12})e^{−ct^{−2δ}}`. Its integral over `(0, t_*]` + is `≤ C'_{c,δ}(1 + h³)t_*e^{−(c/2)t_*^{−2δ}} = O(h^N)`, where `C'_{c,δ} := sup_{t>0}(1 + t^{−12})e^{−(c/2)t^{−2δ}}`. ∎ + +## 4. Proof of Theorem D1⁺ + +Fix `δ = 1/10`, and `t₀` as in Proposition 2.2⁺, small enough also for [D1] Lemma 4.3 (whose own `t₀` is a fixed constant +in `(0, L/4]`). + +**(D1⁺.1).** Write `ν₊ = ∫₀^{t_*}K₊ + ∫_{t_*}^{L}K₊`, where `L` is the length of the circle. +- On `(0, t_*]`, `K₊ = K₁^{sign} − (12/t⁴)p_tE_Q[w1{not adjacent}]`. By [D1] Lemma 3.1, non-adjacency forces + `K₅ ≥ ct^{−δ}`, so the correction integrates to `O(h^N)` ([D1] §5). Proposition 2.2⁺ with `θ = 1` gives the expansion. +- On `[t_*, L)`, `K₊ ≤ K^{band}` (an adjacent pair is banded), and [D1] Lemma 4.3 gives `O(h^{3/4}) + O(h)`. + +**(D1⁺.2).** Write `ν = 2∫₀^{L/2}K` ([D1] §1). +- On `(0, t_*]`, `K = K_{1/3}^{sign} + (K − K_{1/3}^{sign})`. Proposition 2.2⁺ with `θ = 1/3` gives the expansion with + `I_{1/3} = C₁`, and Proposition M bounds the rest by `O(h^{3/4})`. +- On `[t_*, L/2]`, an elder pair is banded or co-banded ([D1] §4), so `K ≤ K^{band} + K^{co}`, and [D1] Lemma 4.3 gives + `O(h^{3/4})`. + +Doubling gives (D1⁺.2). ∎ + +## 5. Remarks + +**5.1 The order `h^{3/4}`.** Four pieces are each `h^{3/4}` times a convergent Mellin-type integral; here they are only +bounded: +- the `E₂`-correction (for `θ = 1/3`, `G_{1/3} − g_{1/3} = v₂P(|E₁| < m/3)(1 + o(1))`); +- the `τ²`-corrections of the cusp kernel ([D1] Prop. 2.2 (d), the error `ε`); +- the term `(p₃(α) − p₃(0))(1 − ζ_θ(s₀))`; +- for `ν`, the window edges of Proposition M: the mean of the first-order part of `φ₊ − φ₋ − 2/3`, the correlation term + `2m Cov_Q(E₂, O(3/2))`, and the second-order terms. + +Heuristically, the two-scale structure produces two families of exponents: +- the fold family `−1/3 + 2k/3`, at `t ≍ h^{1/3}`; +- the cusp family `1/4 + j/2`, at `t ≍ h^{1/4}`. + +These never coincide (`8k = 7 + 6j` has no solution; checker C7), so there are no logarithms. A further scale +`t ≍ h^{1/5}` appears where the quintic jet competes and `m ≍ E₂`. There the model kernel loses relative order one, +contributing order `h^{4/5}`. So the exponent after `1/3` is `3/4`, then `4/5`, then `1`. + +On sharpness, [D1] §6.2 records that for the Gaussian kernel the `θ = 1/3` sign-kernel remainder after three terms is +`≈ 0.038h^{3/4}`, constant over `h = 10^{−10}, …, 10^{−26}`; a referee recomputed `0.0381`. This is evidence only that +the `θ = 1/3` sign-kernel integral has a nonzero `h^{3/4}` term for that kernel. It does not show that a nonzero +`h^{3/4}` term survives in `ν`, where Proposition M's misclassified mass is of the same order, or in `ν₊`; neither is +examined here. + +**5.2 Where the parity enters.** Without the independence of `(φ₋, φ₊)` from `φ_G`, the misclassified mass can only be +bounded by the probability that `φ_G` lies within the edge fluctuation, `O(t/κ)` relative. That is [D1]'s `O(h^{1/2})`. +Three facts make the first order a mean: +- the regression of Lemma Φ, which is exact for Gaussian fields; +- the independence of `E₂` (odd) from `φ_G` (even), which makes the weight a function of `φ_G` given `ω` ([D1] Remark + 1.4); +- the evenness of `W` and `p_s`, which reduces the first order to the window length (3.3). + +The mean of the first-order part is `O(t²)`. The even remainder is centered and cancels, `Ê = O(t²)`, and the odd +part's mean `E_QO(3/2)` comes from `E[f^{(5)} | pins] ∝ α`. For the Gaussian kernel, `E_QO(3/2) = −6t²(1 + O(t²))`: +`E[a₅ | a₁ = 0, a₃ = α] = −10α`, and `O(3/2) ≈ a₅t⁵/(20h)`, since the odd profile `X(X² − ¼)²/120` equals `1/20` at +`3/2` (checker C3). + +**5.3 `d ≥ 2`.** The elder window of Math- #207, #220 and #229 is the same one-dimensional window `|φ| < 1/3` along each +transverse fiber, and Lemma W is a statement on one fiber. It is open whether Proposition M lifts to an elder density in +`d ≥ 2` with remainder beyond `ℓ^{3/7}` (#229), as Math- #237 (open, author-side) proposes for the candidate density. The +transverse dependence of the edges and the far elder density would have to be controlled. This note claims nothing in +`d ≥ 2`. + +**5.4 Numerical evidence (exploration, outside the repository).** These checks use numpy, scipy and mpmath, and are +archived with the project record. + +- *Lemma E.* By 200-node Gauss–Hermite quadrature, `(G_θ − g_θ)/(v₂ min(1, s))` stays in `(0, 1.60]` for `θ = 1` and in + `(0, 1.00]` for `θ = 1/3`, on `s ∈ [0.01, 12]` and `v₂^{1/2}/v₁^{1/2} ∈ [s/256, s/8]`. As `s → 0` the `θ = 1` ratio + tends to `4/√(2π) ≈ 1.596`. +- *The edge scaling: setup.* The model is the exact Gaussian-kernel process `f(x) = e^{−x²/2}Σ_{n ≤ 40}ξ_nx^n/√(n!)`, + with exact Matheron conditioning on the pins (coefficients at 60 digits). The edges `φ±` are found by bisection, and + `Δ` is integrated in closed form in `φ_G`. The table gives `E[Δ]/E[∫_{−1/3}^{1/3}Wp_s]`, divided by `t²`. + + | `t` | samples | `s = 2` | `s = 1` | + |---|---|---|---| + | 0.2 | 4·10⁴ | `−0.285 ± 0.018` | `+0.214 ± 0.040` | + | 0.1 | 4·10⁴ | `−0.274 ± 0.036` | `+0.222 ± 0.080` | + | 0.05 | 1.6·10⁵ | `−0.367 ± 0.036` | `+0.270 ± 0.080` | + | 0.025 | 6.4·10⁵ | `−0.272 ± 0.036` | `+0.266 ± 0.080` | + +- *The edge scaling: findings.* + - A first-order term `∝ t` would make these ratios grow by a factor `8` over this range; they stay flat. + - A referee's independent reduced leading-order model predicts the `t → 0` limits `+0.164` (`s = 1`) and `−0.308` + (`s = 2`). The tabled values for `t ≤ 0.1` are consistent with these (`χ² ≈ 3.7` and `4.7` on 3 degrees of freedom). + - In that model the mean part and the fluctuation part have opposite signs at both `s`. Their sizes differ: `−0.36` and + `+0.52` at `s = 1`, `−0.32` and `+0.01` at `s = 2`. This explains the sign change. + - The exact conditional values are `E_QO(3/2)/t² = −5.841, −5.960, −5.990, −5.997` and + `Ê(3/2)/t² = −12.88, −13.12, −13.18, −13.19` at `t = 0.2, 0.1, 0.05, 0.025`, with limits `−6` and `−13.2`. + - For `t ∈ {0.1, 0.05}`, a direct grid decision with `φ_G` sampled agreed with `1{φ₋ < φ_G < φ₊}` on all `3.3·10⁵` + typed samples. + - At `t = 0.2` there were 12 and 102 mismatches, where `t/κ ≥ 1.3`. + - The constants are large. For instance `‖Ê‖_{C²}/τ² ≈ 2.6·10³` for the Gaussian kernel, so Lemma W's smallness + condition is reached only at small `t`. +- *Lemma W.* At 40 digits, `(φ₊ − 1/3 + η_{1/3}(−3/2)/12)/ε²` converges as `ε = 10^{−2}, 10^{−3}, 10^{−4}`: to `0.0833` + for `η⁰ = εX(X² − ¼)²` (odd) and `0.750` for `η⁰ = ε(X² − ¼)²(X² + ½)` (even). With a `φ`-dependent profile, (3.3) + held to `1.1ε²`. Checker C5 repeats this with the standard library at `ε = 10^{−3}, 10^{−4}, 10^{−5}`. +- *Lemma W (W.1), by a referee.* A direct arc and persistence decision agreed with the interval structure in about + `2.5·10⁵` typed decisions at `C²` norm `≤ 0.5`, for random perturbations satisfying the hypotheses. + +## 6. Sources (exact identities in `SOURCES.json`) + +**Consumed.** [D1] = Math- #214, `frontiers/d1_third_order_law_20261001/PROOF.md`, blob `873532b9` at head +`cf162b1c69…` (open; bound by the workflow's drift gate). It supplies: +- §0: the setting and constants; +- §1: Lemmas 1.1–1.3, the canonical versions (1.2)–(1.3), (1.4) and Remark 1.4; +- §2: the sign kernels, `γ_θ`, `ζ_θ`, Lemma 2.1, Prop. 2.2 (b)–(e), and the intermediate estimates in its proof of + (c)–(d); +- §3: Lemma 3.1, Lemma 3.2's window field `𝔉`, the model (3.1) and Lemma 3.3; +- §4: Lemmas 4.1–4.3; +- §5: the adjacency argument. + +**Cited only.** +- Math- #237 (`frontiers/candidate_parity_rate_20261001/PROOF.md`, open): the `d ≥ 2` parity argument for the candidate + density, for comparison (§5.3). +- Math- #207 (merged; `frontiers/cusp_second_order_20261001/PROOF.md`), #220 (`frontiers/elder_third_order_20261001/PROOF.md`, + open) and #229 (`frontiers/third_order_rate_20261001/PROOF.md`, open): the elder window and densities in `d ≥ 2` + (§5.3). + +External: Sudakov–Fernique and Borell–TIS (as used in [D1] Lemma 4.3); Gaussian regression. + +## 7. Exact controls + +`d1p_check.py` uses the standard library: exact rationals for C1–C4 and C7, `Decimal` at 60 digits for C5, and float +quadrature, reported to 6 digits, for C6. Its output is `RESULTS.json`, byte-identical under `-O`. Mutants `M1`–`M7` each +fail their own control and exit 1; the failure message names the control, and the workflow checks it. An unknown or bare +label exits 2. + +| Control | Checks | +|---|---| +| C1 | The model's parity split, `g_φ = (2X³ − (3/2)X) + (3φ(X² − ¼)² − ½)`, and the mirror symmetry `g(−X, −φ) = −1 − g(X, φ)`. The edge functions (3.2): `Γ_±`, `Γ₊ − Γ₋ = 1`, `Γ₋(φ) = −Γ₊(−φ)`, the derivative `3(1 − φ²)²/(16φ⁴)` and the slope `12` at `±1/3`. These are rational-function identities, verified at 200 rational points within degree bounds. Also `g''(X₃) = 3(1 − φ²)/φ`. | +| C2 | The margins of Lemma W on `J_±`, exactly: `g(−2) ≥ 9/64`; `g(2) + 1 ≤ −9/64`; `g''(X₃) ≥ 7.7` and `g'' ≥ 5.1` within `1/20` of `X₃`; `Γ₊ ≤ 0.12` on `J₊`; `12φ(X² − ¼) ≥ 2.9` on `[−2, −1]`; the bounds on `|g'|`; the right-side factorization; `X₃ ∈ [−1.55, −1.45]`; and the quadratic-growth factor `3φX² − X + (1 − 6φ²)/(4φ) ≥ 2.24` on `[−2, −1] × J₊`. The last is checked as a polynomial identity, together with monotonicity in `X` and `φ` and the value at the corner. | +| C3 | The pin algebra of Lemma Φ, as polynomial identities: `H₀`; the Hermite basis `p₁`, `p₂`; the even pin identity and `E₁ = a₄τ²/3 + ρ₁`; the odd profiles `X(X² − ¼)²/120` and `X(X² − ¼)²(2X² + 1)/10080`; the even profiles `(X² − ¼)²/24` and `(X² − ¼)²(X² + ½)/720`. Also, as scalar arithmetic, the leading regression constant `3`, and for the Gaussian kernel `E[a₅ | a₁ = 0, a₃ = α] = −10α`, giving the leading `E_QO(3/2) = −6t²`. | +| C4 | A bookkeeping check of (3.3), for random rational odd/even polynomials vanishing to second order at `±½`: the even part cancels from the window length. | +| C5 | (W.2)–(W.3) numerically. The edges `φ±` are computed at 60 digits (Newton for the critical point, bisection in `φ`) for four perturbation shapes (odd, even, mixed with a `φ`-profile, generic). Here `ε` is the shape coefficient, not Lemma W's `ε`, at `ε = 10^{−3}, 10^{−4}, 10^{−5}`. It checks that the edge errors are `≤ 10ε²`, the window-length error is `≤ 20ε²`, and the ratios to `ε²` stabilize to 2%. Observed: the edge errors are at most `1.25ε²` and the length error at most `1.5001ε²`. For the odd shape the ratios tend to `±1/12` and `1/6`, for the even shape to `±3/4` and `3/2`. It does not test (W.1). | +| C6 | Lemma E numerically, on a 16-point grid: `(G_θ − g_θ)/v₂` by composite Simpson quadrature, the bound `0 ≤ · ≤ 2 min(1, s)`, and the small-`v₂` limits. | +| C7 | The ledger. Checked: `∫₀^∞t² min(1, h/t⁴) = (4/3)h^{3/4}`, by scaling to `h = 1` and evaluating the exact antiderivatives `u³/3` and `−1/u` of the two pieces; `3 − 11/(5 − δ) ≥ 3/4` iff `δ ≤ 1/9` (`37/49` at `δ = 1/10`); the integrability exponent `−3/4` of Proposition M; the disjointness of the fold and cusp exponent sets, `{−1/3 + 2k/3}` and `{1/4 + j/2}`. Recorded only: the heuristic quintic-scale exponent `4/5` of §5.1 and [D1]'s exponents. | + +What the controls do not test: Lemma E's proof, Lemma Φ's estimates, Lemma W's perturbation argument, (W.1), +Proposition M and the assembly are proved in prose only. C5 and C6 are numerical consistency checks, not proofs. + +## 8. Review slices + +- **A** §1–§2: Lemma E and Proposition 2.2⁺ (the refined `E₂`-correction, the tail of the model kernel, the model + integral to `t₀`). +- **B** §3.1: Lemma Φ (the regression, the decomposition (3.1), the estimates (Φ.1)–(Φ.4)). +- **C** §3.2: Lemma W (the edges, the margins, the envelope bound, (3.3)). +- **D** §3.3–§4: Proposition M and the assembly, including the bad event and the integrals. +- **E** §5 and the controls. diff --git a/frontiers/d1_sharp_remainder_20261001/README.md b/frontiers/d1_sharp_remainder_20261001/README.md new file mode 100644 index 00000000..ba8f3735 --- /dev/null +++ b/frontiers/d1_sharp_remainder_20261001/README.md @@ -0,0 +1,153 @@ +# The one-dimensional lifetime and crest-to-trough laws with remainder `O(h^{3/4})` + +**Author-side proof candidate (Anthropic Claude). Scientific effect: NONE. Nonauthor review required.** + +Object `CL-D1-SHARP-REMAINDER-20261001-v1`. Full text: [`PROOF.md`](PROOF.md). + +## Result + +On the circle `T = R/LZ`, under Math- #214's hypothesis (H), as `h ↓ 0` and `ℓ ↓ 0`: + + ν₊(h) = (C₀/2) h^{−1/3} + (I/2) h^{1/4} + B₂ h^{1/3} + O(h^{3/4}) (D1⁺.1) + ν(ℓ) = C₀ ℓ^{−1/3} + C₁ ℓ^{1/4} + 2B₂ ℓ^{1/3} + O(ℓ^{3/4}) (D1⁺.2) + +- **What it improves.** Math- #214 proved these with `O(h^{1/2})`; its proof gives `O(h^{0.57})` for (D1.1). The + constants are #214's. +- **Consequence.** `2ν₊(ℓ) − ν(ℓ) = (I − C₁)ℓ^{1/4} + O(ℓ^{3/4})`. +- **The exponent.** `3/4` is the order of the first correction to the cusp term (PROOF §5.1). Its coefficient is not + computed. + +## The new ingredients + +| | Statement | Replaces | +|---|---|---| +| **Lemma E** | `0 ≤ G_θ − g_θ ≤ C[v₂ min(1, s) + tail]` with `s = m v₁^{−1/2} ≍ κ` | #214's `E₂`-correction bound `Ct²` (`O(h^{0.61})`) | +| **Prop. 2.2⁺** | The model kernel `k_θ` (fold − cusp) is `O(h³t^{−12})` beyond `t_*`, so the fold and cusp terms are integrated to a fixed `t₀` | #214's cuts at `t_*` (`O(h^{0.57})`) | +| **Lemma Φ** | Under the pinned law, regressing the even part on `E₁` writes the window field as `g_{φ_G} + O + B + φ_GÊ`. Here `φ_G = E₁/m` is independent of `(O, B)`, `‖Ê‖ = O(t²)` (and `Ê` is even), `E O = O(t²)`, and `O − E O = O(t/κ)`. | — | +| **Lemma W** | Given everything but `φ_G`, the elder set is an interval `(φ₋, φ₊)`. Its edges move by `−η_{±1/3}(∓3/2)/12 + O(ε²)`, since the slope of the competing critical value is `12`. Also `φ₊ − φ₋ − 2/3 = O(3/2)/6 − Ê(3/2)/18 + O(ε²)`: the even remainder only translates the window. | #214 Lemma 3.3's margin `η` at the edges | +| **Prop. M** | The elder kernel differs from the sign kernel by relative `O(t² + (t/κ)²)` of the edge mass, `O(h^{3/4})` in total | #214's misclassification bound `O(h^{1/2})` | + +The gain in (D1⁺.2) comes from a mean. The edges of the elder window fluctuate by `O(t/κ)`. But conditionally on +everything except `φ_G`, the elder set is an interval whose endpoints are independent of `φ_G`. So the misclassified mass +is first order only in the *mean* of the first-order part of `φ₊ − φ₋ − 2/3`, and second order in the fluctuation. That +mean is `O(t²)`, for three reasons: +- the even fluctuation cancels and is centered; +- `Ê = O(t²)`; +- the odd part's mean is proportional to `E[f^{(5)} | pins] ∝ α ≍ κt`. + +## Dependencies + +**Consumed.** Math- #214 (open; head `cf162b1`, PROOF blob `873532b9`, v1.1): +- §§0–5 as stated, plus the intermediate estimates in its proof of Prop. 2.2 (c)–(d), which are rerun on a longer range; +- nonauthor analytic review by OpenAI Codex on `f4a58df`: "Slices A–D and Theorem D1 ACCEPTED at the stated circle + scope". + +**Cited only.** +- Math- #237: the `d ≥ 2` parity argument for the candidate density; +- Math- #207 (merged), #220 and #229: the elder window and densities in `d ≥ 2`. + +The workflow binds #214 to its pinned blob through the repository API, with a drift gate: +- if #214 lands, the bytes must be identical, or this packet needs rebinding; +- the gate is evaluated when CI runs, so re-run CI before any merge. + +## Controls + +`d1p_check.py` uses the standard library: exact rationals for C1–C4 and C7, `Decimal` at 60 digits for C5, and float +quadrature, reported to 6 digits, for C6. Its output is `RESULTS.json`, byte-identical under `-O` and on CPython +3.10–3.14 (under a second). + +| Control | Checks | +|---|---| +| C1 | The model's parity split; the edge functions `Γ_±` (slope `12` at `±1/3`, derivative `3(1 − φ²)²/(16φ⁴)`); `g''(X₃)`; the mirror symmetry `g(−X, −φ) = −1 − g(X, φ)` | +| C2 | The margins of Lemma W on `J_± = ±[1/3 − 1/100, 1/3 + 1/100]`, exactly, including the quadratic-growth factor `≥ 2.24` used by the envelope bound and `g'' ≥ 5.1` near `X₃` | +| C3 | The pin algebra of Lemma Φ as polynomial identities: the odd cubic and Hermite basis; the odd profiles `X(X² − ¼)²/120` and `X(X² − ¼)²(2X² + 1)/10080`; the even pin identity and profiles; `E₁ = a₄τ²/3 + ρ₁`. As scalar arithmetic: the leading regression constant `3`, and for the Gaussian kernel `E[a₅ | a₁ = 0, a₃ = α] = −10α`, hence `E_QO(3/2) → −6t²` | +| C4 | A bookkeeping check of the window-length identity (3.3): the even part cancels | +| C5 | (W.2)–(W.3) at 60 digits, for four perturbation shapes. The edge errors divided by (shape coefficient)² converge: to `±1/12` for the odd shape and `±3/4` for the even shape | +| C6 | Lemma E numerically, on a 16-point grid: `0 ≤ (G_θ − g_θ)/v₂ ≤ 2 min(1, s)`, and the small-`v₂` limits | +| C7 | The ledger. Checked: `(4/3)h^{3/4}`, by scaling and the exact antiderivatives; the band tail `37/49 ≥ 3/4`; integrability; the disjoint fold and cusp exponent sets. Recorded only: the heuristic `4/5` | + +Mutants `M1`–`M7` each fail in their own control, and the workflow checks the failing control by name. An unknown or +bare label exits 2. + + python3 -B -S d1p_check.py # exit 0, output = RESULTS.json + python3 -B -S d1p_check.py --mutant M4 # exit 1 + +C5 and C6 are numerical consistency checks. Lemmas E, Φ and W (including (W.1)), Proposition M and the assembly are proved +in prose only. + +## Numerical evidence (exploration, outside the repository) + +The model is the exact Gaussian-kernel process `e^{−x²/2}Σξ_nx^n/√(n!)`, with exact Matheron conditioning on the pins. +At fixed `s` (the cusp scale), the relative elder misclassification divided by `t²` is flat over +`t = 0.2, 0.1, 0.05, 0.025`: + +| `s` | `t = 0.2` | `t = 0.1` | `t = 0.05` | `t = 0.025` | +|---|---|---|---|---| +| 2 | `−0.285` | `−0.274` | `−0.367` | `−0.272` | +| 1 | `+0.214` | `+0.222` | `+0.270` | `+0.266` | + +The `s = 2` values carry `±0.018`–`0.036` and the `s = 1` values `±0.04`–`0.08`. + +- A first-order term `∝ t` would grow these ratios eightfold. +- A referee's independent reduced leading-order model predicts the limits `+0.164` (`s = 1`) and `−0.308` (`s = 2`). The + values for `t ≤ 0.1` are consistent with them (`χ² ≈ 3.7` and `4.7` on 3 degrees of freedom). +- For `t ∈ {0.1, 0.05}`, the interval structure of Lemma W matched a direct grid decision on all `3.3·10⁵` typed + samples. + +## Review record + +Two clean-context same-family referees (Anthropic Claude subagents) reviewed the note before submission. Referee A took +§§0–3.1 and referee B took §§3.2–8, the controls, the workflow and this README. Each read the whole note against [D1] at +its pinned blob. + +**First pass: both ACCEPT WITH MINOR FIXES; no MAJOR findings.** All findings are applied: seven minor, 18 nits and one remark. The +minor ones: +- (W.3) needs `Ê` even. The statement now gives the general form and the even case; `Ê` is even in Proposition M. +- The bad-event bound in Proposition M now carries the factor `(1 + s)` and the fourth-moment step. +- The dependency declaration now includes the intermediate estimates of #214's proof of Prop. 2.2 (c)–(d) that §2 reruns. +- The displayed bound `∫t^{−4}e^{−ct^{−2δ}} ≤ …` in Prop. 2.2⁺(a) now has its constant. +- §5.1's sharpness sentence is narrowed. +- C2 now checks the envelope's quadratic-growth constant. +- C7 now separates the checked items from the recorded ones. + +Other changes: +- Lemma E is now unconditional (the trivial case `m² < 64v₂` is added), which removes the `t₁` bookkeeping. +- The window edges are renamed `φ±`, since `L` is the circle's length. +- The `|φ| > 2` typing case is spelled out, and `‖·‖_{C²}` is defined. +- §5.4 now gives exact conditional values and the correct sample count. +- The workflow now checks each mutant's failing control and the bare `--mutant`. + +**Second pass (delta check of the revision): both ACCEPT.** The remaining nits were applied: +- the declaration of what the rerun estimates rest on; +- `§§0–5`; +- the bound `v₂ ≤ Cm²` cited in Proposition M's mean step; +- `E_Q[O(3/2)⁴]`; +- the renaming `φ_a → χ_a` in Lemma E; +- the attribution of `Γ₋ = −Γ₊(−·)` to C1; +- more test points for C2's quadratic-growth identity; +- §5.4's `χ²` scope and its sign-change sentence; +- the edge names in `RESULTS.json`; +- the workflow's path filter. + +**The referees' independent checks.** +- *Replay.* Byte-identical on CPython 3.10–3.14 with and without `-O`; the mutant matrix is clean. +- *Lemma E.* Without cancellation, the sup of `(G − g)/(v₂ min(1, s))` is `1.5958 = 4/√(2π)` for `θ = 1` and `0.99994` + for `θ = 1/3`. +- *Lemma Φ.* Exact conditioning at 140 digits for the Gaussian and mixture kernels, with all scalings bounded. + `E_QO(3/2)/t² → −6`, `Ê(3/2)/t² → −13.2`, and `Cov(E₂, O(3/2))κ/t⁴ → 1/20`. +- *Prop. 2.2⁺ (c), at 45 digits.* The model remainder is `−0.0217h^{3/4}` (`θ = 1`) and `+0.0333h^{3/4}` (`θ = 1/3`). + The `θ = 1/3` sign-kernel total is `0.0381h^{3/4}`, matching #214 §6.2. The new tail is `Θ(h^{37/49})`, and the old + separate tails `Θ(h^{4/7})` cancel. +- *Lemma W.* The second-order coefficients `1/12` and `3/4` were derived by hand. (W.1) was tested by a direct + decision: no mismatch in about `2.5·10⁵` typed decisions at `C²` norm `≤ 0.5`. +- *Workflow.* Run end to end with the API stubbed; a simulated advance of #214 trips the drift gate. + +**Independence.** The referees are the same provider and the same GitHub account as the author, so they carry zero +organizational independence. Nonauthor review is required; the review slices are in PROOF §8. + +## Not claimed + +- the `h^{3/4}` coefficient, its sign, or the sharpness of `3/4`. #214 §6.2 records a `θ = 1/3` sign-kernel remainder + `≈ 0.038h^{3/4}` for the Gaussian kernel, which is evidence about that integral only. +- anything in `d ≥ 2`. Whether the edge argument lifts to the elder density there is open (PROOF §5.3). +- uniformity in the covariance; anything on `R`. diff --git a/frontiers/d1_sharp_remainder_20261001/RESULTS.json b/frontiers/d1_sharp_remainder_20261001/RESULTS.json new file mode 100644 index 00000000..25a0c64b --- /dev/null +++ b/frontiers/d1_sharp_remainder_20261001/RESULTS.json @@ -0,0 +1,233 @@ +{ + "controls": { + "C1": { + "Gamma_identities_rational_points": 200, + "Gamma_plus_second_derivative_at_1/3": "-162", + "Gamma_prime_numerator": "48 phi^2 (1 - phi^2)^2", + "Gamma_slope_at_pm_1/3": "12", + "mirror_symmetry_g(-X,-phi)=-1-g(X,phi)": true, + "parity_split_and_gprime_factorization": true + }, + "C2": { + "Gamma_plus_on_J+": [ + "-0.128546", + "0.112306" + ], + "J_plus": [ + "97/300", + "103/300" + ], + "eta0": "1/100", + "g(-2)_min_on_J+": "9/64", + "g2_at_X3_min_on_J+": "7.707864", + "g3_bound_on_[-1.6,-1.4]": "51.5520", + "quadratic_growth_min_on_[-2,-1]xJ+": "2.243155" + }, + "C3": { + "Gaussian_E[a5|a1=0,a3=alpha]/alpha": "-10", + "Gaussian_E_QO(3/2)/t^2_leading": "-6", + "even_profiles": [ + "(X^2-1/4)^2 t^4/24", + "(X^2-1/4)^2 (X^2+1/2) t^6/720" + ], + "odd_profiles": [ + "X (X^2-1/4)^2 t^5/120", + "X (X^2-1/4)^2 (2X^2+1) t^7/10080" + ] + }, + "C4": { + "identity": "phi+ - phi- - 2/3 = O(3/2)/6 - Ehat(3/2)/18 + O(eps^2) (Ehat even); B cancels", + "random_triples": 50 + }, + "C5": { + "even (X^2-1/4)^2(X^2+1/2)": { + "(phi+ - 1/3 - d+)/eps^2, (phi- + 1/3 - d-)/eps^2, (length - pred)/eps^2": [ + [ + "0.747018", + "-0.753018", + "1.50004" + ], + [ + "0.7497", + "-0.7503", + "1.5" + ], + [ + "0.74997", + "-0.75003", + "1.5" + ] + ], + "eps (shape coefficient)": [ + "1e-3", + "1e-4", + "1e-5" + ] + }, + "generic (X^2-1/4)^2(1+2X-X^2)/2": { + "(phi+ - 1/3 - d+)/eps^2, (phi- + 1/3 - d-)/eps^2, (length - pred)/eps^2": [ + [ + "0.522403", + "-0.0208125", + "0.543215" + ], + [ + "0.52099", + "-0.0208313", + "0.541821" + ], + [ + "0.520849", + "-0.0208331", + "0.541682" + ] + ], + "eps (shape coefficient)": [ + "1e-3", + "1e-4", + "1e-5" + ] + }, + "mixed with phi-profile": { + "(phi+ - 1/3 - d+)/eps^2, (phi- + 1/3 - d-)/eps^2, (length - pred)/eps^2": [ + [ + "1.24485", + "0.123901", + "1.12094" + ], + [ + "1.24948", + "0.124891", + "1.12459" + ], + [ + "1.24995", + "0.124989", + "1.12496" + ] + ], + "eps (shape coefficient)": [ + "1e-3", + "1e-4", + "1e-5" + ] + }, + "odd X(X^2-1/4)^2": { + "(phi+ - 1/3 - d+)/eps^2, (phi- + 1/3 - d-)/eps^2, (length - pred)/eps^2": [ + [ + "0.0834168", + "-0.0834168", + "0.166834" + ], + [ + "0.0833417", + "-0.0833417", + "0.166683" + ], + [ + "0.0833342", + "-0.0833342", + "0.166668" + ] + ], + "eps (shape coefficient)": [ + "1e-3", + "1e-4", + "1e-5" + ] + } + }, + "C6": { + "bound_checked": "0 <= (G - g)/v2 <= 2 min(1, s) on the 16-point grid s in {0.02,...,8}, sqrt(v2/v1) in {s/8, s/32}", + "s, D1, limit1, D1/3, limit1/3 (v2/v1 = s^2/1024)": [ + [ + "0.02", + "0.0319111", + "0.0319111", + "0.00531919", + "0.00531919" + ], + [ + "0.1", + "0.159045", + "0.159046", + "0.0265912", + "0.0265912" + ], + [ + "0.3", + "0.464636", + "0.464656", + "0.0796557", + "0.0796557" + ], + [ + "1", + "1.16628", + "1.16663", + "0.261117", + "0.261117" + ], + [ + "2", + "1.17046", + "1.17046", + "0.495015", + "0.495015" + ], + [ + "3", + "1.02418", + "1.02389", + "0.682689", + "0.682689" + ], + [ + "5", + "1.00002", + "1.00001", + "0.904419", + "0.904419" + ], + [ + "8", + "1", + "1", + "0.992339", + "0.992339" + ] + ], + "sup_ratio_theta1": "1.596", + "sup_ratio_theta1/3": "0.9923" + }, + "C7": { + "PropM_integrand_exponent_at_u->0": "-3/4", + "band_tail_exponent_3-11/(5-delta)": "37/49", + "int_t2_min(1,h/t4)/h^(3/4)": "4/3", + "next_fold_cusp_exponents_after_1/3": [ + "3/4", + "1" + ], + "recorded_D1_exponents_at_delta_1/10": { + "2-7/(5-delta)": "4/7", + "3/(5-delta)": "30/49" + }, + "recorded_heuristic_quintic_scale_exponent": "4/5 (Remark 5.1; not derived here)", + "recorded_remainder_improvement": { + "D1_(D1.2)": "1/2", + "here": "3/4" + } + } + }, + "mutants": { + "M1": "C1: edge function Gamma_+ with (3 phi + 1) in place of (3 phi - 1)", + "M2": "C2: edge margin eta_0 = 1/50 in place of 1/100", + "M3": "C3: odd a5 profile with 1/60 in place of 1/120", + "M4": "C4: the even part treated as odd (no cancellation in the window length)", + "M5": "C5: first-order edge coefficient 1/6 in place of 1/12", + "M6": "C6: Lemma E bound v2 min(1, s)/4 in place of 2 v2 min(1, s)", + "M7": "C7: delta = 1/8 in place of 1/10" + }, + "object": "CL-D1-SHARP-REMAINDER-20261001-v1", + "scientific_effect": "NONE" +} diff --git a/frontiers/d1_sharp_remainder_20261001/SOURCES.json b/frontiers/d1_sharp_remainder_20261001/SOURCES.json new file mode 100644 index 00000000..8d681d32 --- /dev/null +++ b/frontiers/d1_sharp_remainder_20261001/SOURCES.json @@ -0,0 +1,141 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "object": "CL-D1-SHARP-REMAINDER-20261001-v1", + "kind": "author-side proof candidate: the one-dimensional crest-to-trough and lifetime laws with remainder O(h^(3/4)) (Theorem D1+): nu_+ = (C0/2) h^(-1/3) + (I/2) h^(1/4) + B2 h^(1/3) + O(h^(3/4)) and nu = C0 l^(-1/3) + C1 l^(1/4) + 2 B2 l^(1/3) + O(l^(3/4)), improving O(h^(1/2)) of Math- #214. New: Lemma E (the E2-correction is O(v2 min(1, s))), Proposition 2.2+ (the model kernel fold - cusp is O(h^3 t^-12) beyond t_*), Lemma Phi (regression of the even part on E1: the window field is affine in phi_G = E1/m with a remainder independent of phi_G), Lemma W (the elder set is an interval (L, R) in phi_G; the edges move by -eta(-+3/2)/12 + O(eps^2); the even part cancels from the window length), Proposition M (the misclassified mass is O(h^(3/4)))", + "author": "Anthropic Claude", + "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", + "read_at": { + "branch_base": "5a836a8effb1bd872fbce39331da3496f33cac27" + }, + "consumed": [], + "consumed_unmerged": [ + { + "path": "frontiers/d1_third_order_law_20261001/PROOF.md", + "bytes": 44378, + "sha256": "279ed88ff2debd570e6426aec53cc93aabc7a298731cd9b25c45667a2c11077b", + "git_blob": "873532b955dbf7684edc1a53ba169c7216f778ab", + "tag": "214", + "use": "Math- #214 v1.1 ([D1]; open; nonauthor analytic review by OpenAI Codex, comment 5933752065, on f4a58df: Slices A-D and Theorem D1 ACCEPTED at the stated circle scope; cf162b1 is a main-only refresh with the packet bytes unchanged): section 0 (setting, (H), constants C0, C1, I, B2); section 1 (Lemmas 1.1-1.3, the canonical versions (1.2)-(1.3), (1.4), Remark 1.4); section 2 (the sign kernels, gamma_theta, zeta_theta, Lemma 2.1, Prop. 2.2 (b)-(e), and the intermediate estimates in its proof of (c)-(d), rerun on (0, t0]: the expansions follow from Lemma 1.3, the zeta_theta bounds are properties of zeta_theta, and none uses t <= t_*); section 3 (Lemma 3.1, Lemma 3.2 (the window field), the model (3.1), Lemma 3.3); section 4 (Lemmas 4.1-4.3); section 5 (the adjacency argument)", + "head": "cf162b1c69086775594e150321200eb066c426ca", + "pr": "Math- #214" + } + ], + "cited_only": [ + { + "path": "frontiers/cusp_second_order_20261001/PROOF.md", + "bytes": 52605, + "sha256": "cffc1b83ac364da58bd650c3c301ea1babd38e19af54f74010bdc120edce38a8", + "git_blob": "f6df5a7356a54771b0052e42a864a140709903ad", + "tag": "207", + "use": "Math- #207 (merged 2026-10-01 at 566b1a1): the elder window in d >= 2 (Remark 5.3); not used" + } + ], + "cited_unmerged": [ + { + "path": "frontiers/candidate_parity_rate_20261001/PROOF.md", + "bytes": 50928, + "sha256": "aa4200100fcdf23135f82b7ac6f69621dedc65983d6707970f93d0343c6fca77", + "git_blob": "97298f32f64bbed591e3067865629ccb838d4e9d", + "tag": "237", + "use": "Math- #237 (open): the d >= 2 parity argument for the candidate density, for comparison (Remark 5.3); not used", + "head": "a6b67882344cc39c76c29f5a6a6787a0e243c630", + "pr": "Math- #237" + }, + { + "path": "frontiers/elder_third_order_20261001/PROOF.md", + "bytes": 70544, + "sha256": "74b5f031ba5be6f50b5e543636136df1d9b5fad0fcd2c8210320cfef02f80e37", + "git_blob": "c8767ddecf1041d234f685e95af582073a7be393", + "tag": "220", + "use": "Math- #220 (open): the elder density in d >= 2 and its window (Remark 5.3); not used", + "head": "70dcf310fc68f7d2b6949f035a09acf54f0cff7d", + "pr": "Math- #220" + }, + { + "path": "frontiers/third_order_rate_20261001/PROOF.md", + "bytes": 37626, + "sha256": "5de5a6c7b942a71675c812000ade30c16766f02ee388e8dc3e1c51dde5297f7d", + "git_blob": "110ed33a57902bef11873807e722fde3888b59fb", + "tag": "229", + "use": "Math- #229 (open): the elder density with remainder l^(3/7) in d >= 2 (Remark 5.3); not used", + "head": "5dbe15cdc5f6d67b37dcefb176e9ad7433d6f77e", + "pr": "Math- #229" + } + ], + "cited_external": [ + { + "tag": "SF-BTIS", + "reference": "Sudakov-Fernique comparison and the Borell-TIS inequality", + "use": "moments and tails of the suprema K^e, K^o-tilde, K^perp under the pinned law (Lemma Phi), as in #214 Lemma 4.3" + }, + { + "tag": "regression", + "reference": "Gaussian conditioning (linear regression of jointly Gaussian vectors)", + "use": "Lemma Phi (Phi.0)" + } + ], + "mutants": { + "M1": "C1", + "M2": "C2", + "M3": "C3", + "M4": "C4", + "M5": "C5", + "M6": "C6", + "M7": "C7" + }, + "replayed": [ + "d1p_check.py" + ], + "delivered_under": "explicit owner instructions of Dylan Roy in claude.ai session session_01NMeKEismAyeqgdB4sy2NJU, given after OWNER_STOP (2026-09-27): 2026-09-30 \"Continue to Work on closing as many mathematical items as possible while working with and supporting the other models in the GitHub. Also advance the mathematics in every place that's justified based on what we currently know\", followed by \"Continue\"; standing: \"Any request or permissions are preapproved in advance by me Dylan Roy\", pull requests only, never self-merge, no register/GRAPH/STATUS/lemma_closed/prize/premise edits, OWNER_STOP.md untouched. OWNER_STOP.md addresses Cursor agents and is untouched; nothing is merged by its author.", + "files": [ + { + "path": "PROOF.md", + "bytes": 40024, + "sha256": "ae027fe39fc9d9f648720bf9dba0001634e3a984980d147c14940a4a41ddfb62" + }, + { + "path": "README.md", + "bytes": 10273, + "sha256": "595a08f85de720e7e237947cd07aaaad847bd1e60027c231b9d07aa73b7bdaf1" + }, + { + "path": "d1p_check.py", + "bytes": 25482, + "sha256": "cbab0a63544a2d14120bc4c92bfd215b349919a90079fe9e40b5cc9ac9336425" + }, + { + "path": "RESULTS.json", + "bytes": 4711, + "sha256": "3a1b67744eb318919aeaac8cd53a287d9ba0a166a612b136b3f41ee5410b6e1e" + } + ], + "referee": { + "kind": "two clean-context same-family referees (Anthropic Claude subagents) before submission, each followed by a delta check of the revision: A on sections 0-3.1 (Lemma E, Proposition 2.2+, Lemma Phi), B on sections 3.2-8 (Lemma W, Proposition M, the assembly, the remarks), the controls, the workflow and the README", + "verdict": "first pass: A ACCEPT WITH MINOR FIXES (two minor: the dependency declaration did not cover the intermediate estimates of [D1] Prop. 2.2 (c)-(d) rerun on (0, t0]; a displayed bound in Prop. 2.2+(a) lacked its constant; seven nits and one remark), B ACCEPT WITH MINOR FIXES (five minor: (W.3) needed E-hat even; the bad-event bound needed the factor (1 + s); the sharpness sentence of 5.1 was too broad; C7 recorded rather than checked part of its claims; C2 omitted the envelope constant; eleven nits); no MAJOR findings; all applied. Delta: A ACCEPT (five nits, applied), B ACCEPT (nine nits, applied)", + "independent_checks": "replay byte-identical on CPython 3.10-3.14 with and without -O, the mutant matrix with each mutant failing in its own control; Lemma E without cancellation (sup ratios 1.5958 = 4/sqrt(2 pi) and 0.99994); exact Gaussian conditioning at 140 digits for the Gaussian and mixture kernels (E_Q O(3/2)/t^2 -> -6, Ehat(3/2)/t^2 -> -13.2, Cov(E2, O(3/2)) kappa/t^4 -> 1/20, all scalings of Lemma Phi bounded); Prop. 2.2+ (c) at 45 digits (model remainders -0.0217 h^(3/4) and +0.0333 h^(3/4); the theta = 1/3 sign-kernel total 0.0381 h^(3/4), matching [D1] 6.2; the new tail Theta(h^(37/49)); the old separate tails Theta(h^(4/7)) cancel); the second-order edge coefficients 1/12 and 3/4 by hand; (W.1) by a direct decision (no mismatch in about 2.5e5 typed decisions at C^2 norm <= 0.5); a reduced leading-order model of the edge scaling (t -> 0 limits +0.164 at s = 1 and -0.308 at s = 2, consistent with the exploration tables); the workflow end to end with the API stubbed (drift gate and own-control mutant check exercised)", + "independence": "same provider and GitHub account as the author; zero organizational independence", + "reports": [ + { + "report": "project archive V2_2/frontiers_d1_sharp_remainder_20261001/REFEREE_A.md", + "sha256": "306d9bf7bedfde2615e9bc97f4cc6733a81595aa1e89ddd4acd149f158be5e1e", + "bytes": 16030 + }, + { + "report": "project archive V2_2/frontiers_d1_sharp_remainder_20261001/REFEREE_A_DELTA.md", + "sha256": "71ecdf6c547de732a0ac33b27d5b949b144854c75739a8a9a947732cf412d50e", + "bytes": 8157 + }, + { + "report": "project archive V2_2/frontiers_d1_sharp_remainder_20261001/REFEREE_B.md", + "sha256": "5b7afd13e939684d55d535fc8d8417656f26413f4024dcca1172085f5243597d", + "bytes": 16692 + }, + { + "report": "project archive V2_2/frontiers_d1_sharp_remainder_20261001/REFEREE_B_DELTA.md", + "sha256": "247f1aa167f397ac8dbba10495cb0a2d2a2221f8aae4527f881d77e1e68c8271", + "bytes": 11848 + } + ] + } +} diff --git a/frontiers/d1_sharp_remainder_20261001/d1p_check.py b/frontiers/d1_sharp_remainder_20261001/d1p_check.py new file mode 100644 index 00000000..1e20905e --- /dev/null +++ b/frontiers/d1_sharp_remainder_20261001/d1p_check.py @@ -0,0 +1,516 @@ +#!/usr/bin/env python3 +"""Exact controls for Theorem D1+ (CL-D1-SHARP-REMAINDER-20261001-v1). + +Standard library only. Exact rationals (fractions.Fraction) for C1-C4 and C7, Decimal at 60 digits for C5, and +float quadrature (reported to 6 significant digits) for C6. Output: one JSON document on stdout, equal to RESULTS.json. + + python3 -B -S d1p_check.py # exit 0 + python3 -B -S d1p_check.py --mutant M3 # exit 1 (each mutant breaks its own control) + python3 -B -S d1p_check.py --mutant XX # exit 2 (unknown label) + +Scientific effect: NONE. The controls check exact algebra, margins and arithmetic; C5 and C6 are numerical +consistency checks, not proofs. +""" +import json +import math +import sys +from decimal import Decimal, getcontext +from fractions import Fraction as Fr + +MUTANTS = { + 'M1': 'C1: edge function Gamma_+ with (3 phi + 1) in place of (3 phi - 1)', + 'M2': 'C2: edge margin eta_0 = 1/50 in place of 1/100', + 'M3': 'C3: odd a5 profile with 1/60 in place of 1/120', + 'M4': 'C4: the even part treated as odd (no cancellation in the window length)', + 'M5': 'C5: first-order edge coefficient 1/6 in place of 1/12', + 'M6': 'C6: Lemma E bound v2 min(1, s)/4 in place of 2 v2 min(1, s)', + 'M7': 'C7: delta = 1/8 in place of 1/10', +} + + +class ControlFailure(Exception): + pass + + +def check(cond, msg): + if not cond: + raise ControlFailure(msg) + + +def parse_args(argv): + mutant = None + rest = list(argv) + while rest: + a = rest.pop(0) + if a == '--mutant': + if not rest: + print('usage: d1p_check.py [--mutant M1..M7]', file=sys.stderr) + sys.exit(2) + mutant = rest.pop(0) + if mutant not in MUTANTS: + print('unknown mutant label: ' + mutant, file=sys.stderr) + sys.exit(2) + else: + print('unknown argument: ' + a, file=sys.stderr) + sys.exit(2) + return mutant + + +# ---------------------------------------------------------------- polynomials (coefficients low -> high, Fractions) + +def padd(p, q): + n = max(len(p), len(q)) + return trim([(p[i] if i < len(p) else 0) + (q[i] if i < len(q) else 0) for i in range(n)]) + + +def pscale(p, c): + return trim([c * a for a in p]) + + +def pmul(p, q): + if not p or not q: + return [] + out = [Fr(0)] * (len(p) + len(q) - 1) + for i, a in enumerate(p): + for j, b in enumerate(q): + out[i + j] += a * b + return trim(out) + + +def ppow(p, k): + out = [Fr(1)] + for _ in range(k): + out = pmul(out, p) + return out + + +def pder(p): + return trim([i * p[i] for i in range(1, len(p))]) + + +def peval(p, x): + acc = 0 + for a in reversed(p): + acc = acc * x + a + return acc + + +def trim(p): + p = [Fr(a) for a in p] + while p and p[-1] == 0: + p.pop() + return p + + +def pcompose_scale(p, c): + """p(c X)""" + return trim([a * c ** i for i, a in enumerate(p)]) + + +X = [Fr(0), Fr(1)] +HALF = Fr(1, 2) +Q2 = padd(pmul(X, X), [Fr(-1, 4)]) # X^2 - 1/4 +Q2SQ = pmul(Q2, Q2) # (X^2 - 1/4)^2 + + +def g_poly(phi): + """[D1] (3.1): g_phi(X) = 2 (X + 1/2)^2 (X - 1) + 3 phi (X^2 - 1/4)^2.""" + return padd(pmul(pscale(ppow(padd(X, [HALF]), 2), 2), padd(X, [Fr(-1)])), pscale(Q2SQ, 3 * phi)) + + +def rat_points(n): + pts = [] + k = 1 + while len(pts) < n: + for q in (Fr(k, 7), Fr(-k, 7), Fr(k, 13) + Fr(1, 101), Fr(-k, 11) - Fr(1, 97)): + if q != 0 and q not in pts: + pts.append(q) + k += 1 + return pts[:n] + + +# ---------------------------------------------------------------- C1: the model's parity split and the edge functions + +def control_c1(mutant): + res = {} + # parity split: g_phi = (2X^3 - 3X/2) + (3 phi (X^2 - 1/4)^2 - 1/2); identity in (X, phi) of degree (4, 1) + odd = [Fr(0), Fr(-3, 2), Fr(0), Fr(2)] + for phi in rat_points(5): + target = padd(padd(odd, pscale(Q2SQ, 3 * phi)), [Fr(-1, 2)]) + check(g_poly(phi) == target, 'C1 parity split fails at phi=%s' % phi) + # g' = 12 phi (X^2 - 1/4)(X - X3) = 6 (X^2 - 1/4)(1 + 2 phi X) + check(pder(g_poly(phi)) == pmul(pscale(Q2, 6), [Fr(1), 2 * phi]), "C1 g' factorization fails") + # mirror symmetry g(-X, -phi) = -1 - g(X, phi) + gm = pcompose_scale(g_poly(-phi), Fr(-1)) + check(gm == padd([Fr(-1)], pscale(g_poly(phi), -1)), 'C1 mirror symmetry fails') + res['parity_split_and_gprime_factorization'] = True + res['mirror_symmetry_g(-X,-phi)=-1-g(X,phi)'] = True + # edge functions at X3 = -1/(2 phi): Gamma_+ = g(X3) + 1, Gamma_- = g(X3) + Np = pmul(ppow([Fr(1), Fr(1)], 3), [Fr(-1), Fr(3)] if mutant != 'M1' else [Fr(1), Fr(3)]) # (phi+1)^3 (3phi-1) + Nm = pmul(ppow([Fr(-1), Fr(1)], 3), [Fr(1), Fr(3)]) # (phi-1)^3 (3phi+1) + D = [Fr(0), Fr(0), Fr(0), Fr(16)] # 16 phi^3 + pts = rat_points(200) + for phi in pts: + X3 = -1 / (2 * phi) + gX3 = peval(g_poly(phi), X3) + check(gX3 + 1 == peval(Np, phi) / peval(D, phi), 'C1 Gamma_+ identity fails at phi=%s' % phi) + check(gX3 == peval(Nm, phi) / peval(D, phi), 'C1 Gamma_- identity fails at phi=%s' % phi) + check(peval(Nm, phi) / peval(D, phi) == -peval(Np, -phi) / peval(D, -phi), 'C1 Gamma_-(phi) = -Gamma_+(-phi) fails') + # g''(X3) = 3 (1 - phi^2)/phi + check(peval(pder(pder(g_poly(phi))), X3) == 3 * (1 - phi * phi) / phi, "C1 g''(X3) fails") + res['Gamma_identities_rational_points'] = len(pts) + # Gamma_+' = (N'D - N D')/D^2 and N'D - N D' = 48 phi^2 (1 - phi^2)^2, i.e. Gamma' = 3 (1 - phi^2)^2/(16 phi^4) + W = padd(pmul(pder(Np), D), pscale(pmul(Np, pder(D)), -1)) + target = pmul([Fr(0), Fr(0), Fr(48)], ppow([Fr(1), Fr(0), Fr(-1)], 2)) + check(W == target, "C1 Gamma_+' fails") + Wm = padd(pmul(pder(Nm), D), pscale(pmul(Nm, pder(D)), -1)) + check(Wm == target, "C1 Gamma_-' fails") + check(padd(Np, pscale(Nm, -1)) == D, 'C1 Gamma_+ - Gamma_- = 1 fails') + third = Fr(1, 3) + slope = Fr(3) * (1 - third ** 2) ** 2 / (16 * third ** 4) + check(slope == 12 and peval(Np, third) == 0 and peval(Nm, -third) == 0, 'C1 slope 12 at +-1/3 fails') + # second derivative of Gamma_+ at 1/3 (recorded): (W'D^2 - W 2 D D')/D^4 at 1/3 + Dv, D1v, Wv, W1v = peval(D, third), peval(pder(D), third), peval(W, third), peval(pder(W), third) + second = (W1v * Dv ** 2 - Wv * 2 * Dv * D1v) / Dv ** 4 + res['Gamma_prime_numerator'] = '48 phi^2 (1 - phi^2)^2' + res['Gamma_slope_at_pm_1/3'] = str(slope) + res['Gamma_plus_second_derivative_at_1/3'] = str(second) + check(second == -162, 'C1 Gamma_+ second derivative') + return res + + +# ---------------------------------------------------------------- C2: the margins of Lemma W on J_+ and J_- + +def control_c2(mutant): + res = {} + eta0 = Fr(1, 100) if mutant != 'M2' else Fr(1, 50) + lo, hi = Fr(1, 3) - eta0, Fr(1, 3) + eta0 + Gp = lambda p: (p + 1) ** 3 * (3 * p - 1) / (16 * p ** 3) + # g(-2) = 675 phi/16 - 27/2 and g(2) + 1 = 675 phi/16 + 27/2, identities in phi (degree 1) + for phi in (Fr(1, 5), Fr(2, 7), Fr(1, 3)): + check(peval(g_poly(phi), Fr(-2)) == Fr(675, 16) * phi - Fr(27, 2), 'C2 g(-2) formula') + check(peval(g_poly(phi), Fr(2)) + 1 == Fr(675, 16) * phi + Fr(27, 2), 'C2 g(2)+1 formula') + check(peval(g_poly(phi), Fr(3, 2)) == 12 * phi + 4 and peval(g_poly(phi), Fr(-3, 2)) == 12 * phi - 5, 'C2 g(+-3/2)') + gm2 = Fr(675, 16) * lo - Fr(27, 2) # increasing in phi: min on J_+ at lo + res['g(-2)_min_on_J+'] = str(gm2) + check(gm2 >= Fr(9, 64), 'C2 margin g(-2) >= 9/64 fails on J_+') + check(Fr(675, 16) * (-lo) + Fr(27, 2) <= -Fr(9, 64), 'C2 margin g(2)+1 <= -9/64 fails on J_-') + gpp = lambda p: 3 * (1 - p * p) / p # g''(X3), decreasing in phi > 0 + res['g2_at_X3_min_on_J+'] = '%.6f' % float(gpp(hi)) + check(gpp(hi) >= Fr(77, 10) and gpp(-hi) <= -Fr(77, 10), "C2 margin g''(X3) >= 7.7 fails") + check(Gp(hi) <= Fr(3, 25) and Gp(lo) >= -Fr(13, 100), 'C2 Gamma_+ range on J_+ fails') + res['Gamma_plus_on_J+'] = ['%.6f' % float(Gp(lo)), '%.6f' % float(Gp(hi))] + X3lo, X3hi = -1 / (2 * lo), -1 / (2 * hi) # X3 range on J_+ + check(X3lo >= -Fr(31, 20) and X3hi <= -Fr(29, 20), 'C2 X3 range [-1.55, -1.45] fails') + check(12 * lo * (1 - Fr(1, 4)) >= Fr(29, 10), 'C2 12 phi (X^2 - 1/4) >= 2.9 on [-2,-1] fails') + # |g'| >= 1.8 (1/2 - |X|) on (-1/2, 1/2): 12 phi (1/2 + |X|)(X - X3) >= 12 lo (1/2)(-1/2 - X3hi) + check(12 * lo * HALF * (-HALF - X3hi) >= Fr(9, 5), "C2 |g'| >= 1.8 (1/2 - |X|) fails") + # g' >= 1.7 |X + 1/2| on [-1, -1/2): 12 phi (|X| + 1/2)(X - X3) >= 12 lo (1)(-1 - X3hi) + check(12 * lo * (-1 - X3hi) >= Fr(17, 10), "C2 g' >= 1.7 |X + 1/2| fails") + # g''' = 12 + 72 phi X (identity); on [-1.6, -1.4]: |g'''| <= 12 + 72 hi (8/5) <= 52; within 1/20 of X3, g'' >= 5.1 + for phi in (lo, hi): + check(pder(pder(pder(g_poly(phi)))) == [Fr(12), 72 * phi], "C2 g''' formula") + g3 = 12 + 72 * hi * Fr(8, 5) + check(g3 <= 52 and Fr(77, 10) - Fr(52, 20) >= Fr(51, 10), "C2 g'' >= 5.1 near X3 fails") + res["g3_bound_on_[-1.6,-1.4]"] = '%.4f' % float(g3) + # quadratic growth: g - g(X3) = (X - X3)^2 q(X), q = 3 phi X^2 - X + (1 - 6 phi^2)/(4 phi) (identity in X) + for phi in (lo, hi, Fr(1, 3), Fr(2, 7), Fr(-1, 5), Fr(3, 4), Fr(-5, 9), Fr(7, 3)): # identity of degree <= 4 in phi after clearing + X3 = -1 / (2 * phi) + q = [(1 - 6 * phi * phi) / (4 * phi), Fr(-1), 3 * phi] + lhs = padd(g_poly(phi), [-peval(g_poly(phi), X3)]) + check(lhs == pmul(ppow([-X3, Fr(1)], 2), q), 'C2 quadratic-growth identity fails') + # on [-2,-1]: dq/dX = 6 phi X - 1 < 0, so the min is at X = -1: q(-1) = 3 phi/2 + 1 + 1/(4 phi); + # d/dphi q(-1) = 3/2 - 1/(4 phi^2) < 0 on J_+ (phi^2 < 1/6), so the min over J_+ is at hi + check(6 * hi * (-1) - 1 < 0 and hi * hi < Fr(1, 6), 'C2 quadratic-growth monotonicity fails') + qmin = Fr(3, 2) * hi + 1 + 1 / (4 * hi) + res['quadratic_growth_min_on_[-2,-1]xJ+'] = '%.6f' % float(qmin) + check(qmin >= Fr(224, 100), 'C2 quadratic-growth factor >= 2.24 fails') + # mirror on [1,2] x J_-: (g(X3) - g(X))/(X - X3)^2 = -q, minimal at X = 1, phi = -hi + qm = -(3 * (-hi) * 1 - 1 + (1 - 6 * hi * hi) / (4 * (-hi))) + check(qm == qmin, 'C2 mirror quadratic-growth factor fails') + # right side: g + 1 = (X - 1/2)^2 [2(X + 1) + 3 phi (X + 1/2)^2] + for phi in (lo, hi): + rhs = pmul(ppow(padd(X, [-HALF]), 2), padd(pscale(padd(X, [Fr(1)]), 2), pscale(ppow(padd(X, [HALF]), 2), 3 * phi))) + check(padd(g_poly(phi), [Fr(1)]) == rhs, 'C2 g + 1 factorization fails') + check(12 * phi + 4 >= 7, 'C2 g(3/2) >= 7 fails') + res['eta0'] = str(eta0) + res['J_plus'] = [str(lo), str(hi)] + return res + + +# ---------------------------------------------------------------- C3: the pin algebra of Lemma Phi + +def control_c3(mutant): + res = {} + for tau in (Fr(1, 7), Fr(2, 13), Fr(3, 41)): + t = 2 * tau + h = Fr(5, 17) * t ** 4 + # odd cubic H0(x) = h (2 (x/t)^3 - (3/2)(x/t)): H0'(tau) = 0, H0(tau) = -h/2 + H0 = [Fr(0), -Fr(3, 2) * h / t, Fr(0), 2 * h / t ** 3] + check(peval(pder(H0), tau) == 0 and peval(H0, tau) == -h / 2, 'C3 H0 pins') + # odd Hermite basis at tau + p1 = [Fr(0), Fr(3, 2) / tau, Fr(0), -Fr(1, 2) / tau ** 3] + p2 = [Fr(0), -tau / 2 / tau, Fr(0), tau / 2 / tau ** 3] + check(peval(p1, tau) == 1 and peval(pder(p1), tau) == 0 and peval(p2, tau) == 0 and peval(pder(p2), tau) == 1, + 'C3 Hermite basis') + # odd profiles: R_o = x^5/120 -> R~_o(tX) = (t^5/120) X (X^2-1/4)^2 ; R_o = x^7/5040 -> (t^7/10080) X (X^2-1/4)^2 (2X^2+1) + for deg, prof, const in ((5, pmul(X, Q2SQ), Fr(1, 120) if mutant != 'M3' else Fr(1, 60)), + (7, pmul(pmul(X, Q2SQ), [Fr(1), Fr(0), Fr(2)]), Fr(1, 10080))): + Ro = [Fr(0)] * deg + [Fr(1, math.factorial(deg))] + Rt = padd(Ro, padd(pscale(p1, -peval(Ro, tau)), pscale(p2, -peval(pder(Ro), tau)))) + check(pcompose_scale(Rt, t) == pscale(prof, const * t ** deg), 'C3 odd profile degree %d' % deg) + # even pins: f_e = a2 x^2/2 + a4 x^4/24 + R, a2 = -a4 tau^2/6 - R'(tau)/tau + for a4, R in ((Fr(1), [Fr(0)] * 6 + [Fr(1, 720)]), (Fr(0), [Fr(0)] * 8 + [Fr(1, 40320)]), (Fr(3, 5), [Fr(0)] * 6 + [Fr(2, 7)])): + a2 = -a4 * tau ** 2 / 6 - peval(pder(R), tau) / tau + fe = padd([Fr(0), Fr(0), a2 / 2, Fr(0), a4 / 24], R) + lhs = padd(fe, [-peval(fe, tau)]) + Rt = padd(padd(R, [-peval(R, tau)]), pscale(padd(pmul(X, X), [-tau ** 2]), -peval(pder(R), tau) / (2 * tau))) + rhs = padd(pscale(ppow(padd(pmul(X, X), [-tau ** 2]), 2), a4 / 24), Rt) + check(lhs == rhs, 'C3 even pin identity') + check(peval(pder(fe), tau) == 0, 'C3 even pin') + E1 = peval(pder(pder(fe)), tau) + check(E1 == a4 * tau ** 2 / 3 + peval(pder(pder(R)), tau) - peval(pder(R), tau) / tau, 'C3 E1 identity') + # even profiles: a4 -> (t^4/24)(X^2-1/4)^2 ; R = x^6/720 -> (t^6/720)(X^2-1/4)^2 (X^2+1/2) + R6 = [Fr(0)] * 6 + [Fr(1, 720)] + Rt6 = padd(padd(R6, [-peval(R6, tau)]), pscale(padd(pmul(X, X), [-tau ** 2]), -peval(pder(R6), tau) / (2 * tau))) + check(pcompose_scale(Rt6, t) == pscale(pmul(Q2SQ, [HALF, Fr(0), Fr(1)]), t ** 6 / 720), 'C3 even sextic profile') + check(pcompose_scale(ppow(padd(pmul(X, X), [-tau ** 2]), 2), t) == pscale(Q2SQ, t ** 4), 'C3 even quartic profile') + # regression constant: (m/h)(t^4/24)(tau^2 V/3)/((tau^4/9) V) with m/h = 6/t^2 equals 3 + check(Fr(6) / t ** 2 * t ** 4 / 24 * tau ** 2 / 3 * 9 / tau ** 4 == 3, 'C3 regression constant') + res['odd_profiles'] = ['X (X^2-1/4)^2 t^5/120', 'X (X^2-1/4)^2 (2X^2+1) t^7/10080'] + res['even_profiles'] = ['(X^2-1/4)^2 t^4/24', '(X^2-1/4)^2 (X^2+1/2) t^6/720'] + # second derivative of the odd cubic at 1/2, and the odd profile value at 3/2 + check(peval(pder(pder([Fr(0), -Fr(3, 2), Fr(0), Fr(2)])), HALF) == 6, 'C3 (2X^3 - 3X/2)\'\'(1/2) = 6') + v32 = peval(pmul(X, Q2SQ), Fr(3, 2)) + check(v32 == 6, 'C3 X (X^2 - 1/4)^2 at 3/2') + # Gaussian kernel: lambda_{2k} = (2k-1)!!; E[a5 | a1 = 0, a3 = alpha] = alpha (l4 l6 - l2 l8)/D = -10 alpha + lam = {2: Fr(1), 4: Fr(3), 6: Fr(15), 8: Fr(105)} + Dg = lam[2] * lam[6] - lam[4] ** 2 + r5 = (lam[4] * lam[6] - lam[2] * lam[8]) / Dg + check(Dg == 6 and r5 == -10, 'C3 Gaussian regression coefficient') + # E_Q O(3/2) leading term: r5 alpha t^5/(120 h) * 6 with alpha = 12 h/t^3 -> 6 r5 t^2 * 12/120 = -6 t^2 + lead = r5 * 12 * v32 / 120 + check(lead == -6, 'C3 E_Q O(3/2)/t^2 -> -6') + res['Gaussian_E[a5|a1=0,a3=alpha]/alpha'] = str(r5) + res['Gaussian_E_QO(3/2)/t^2_leading'] = str(lead) + return res + + +# ---------------------------------------------------------------- C4: the window length (3.3), parity cancellation + +class Lcg: + def __init__(self, seed): + self.x = seed + + def frac(self, den): + self.x = (6364136223846793005 * self.x + 1442695040888963407) % (1 << 64) + return Fr((self.x >> 33) % (2 * den + 1) - den, den) + + +def control_c4(mutant): + rng = Lcg(20261001) + n = 0 + for _ in range(50): + o = pmul(pmul(X, Q2SQ), [rng.frac(9), Fr(0), rng.frac(9)]) # odd, double zeros at +-1/2 + b = pmul(Q2SQ, [rng.frac(9), Fr(0), rng.frac(9)]) # even + e = pmul(Q2SQ, [rng.frac(9), Fr(0), rng.frac(9)]) # even (E-hat) + eta = lambda phi, x: peval(o, x) + peval(b, x) + phi * peval(e, x) + third, x32 = Fr(1, 3), Fr(3, 2) + length = (eta(-third, x32) - eta(third, -x32)) / 12 + pred = peval(o, x32) / 6 - peval(e, x32) / 18 + if mutant == 'M4': + pred += peval(b, x32) / 6 + check(length == pred, 'C4 window-length identity (3.3) fails') + # the even part B moves both edges by the same amount -B(3/2)/12 + check(-eta(third, -x32) / 12 - (-(eta(third, -x32) - peval(b, -x32)) / 12) == -peval(b, x32) / 12, 'C4 translation') + n += 1 + return {'random_triples': n, 'identity': 'phi+ - phi- - 2/3 = O(3/2)/6 - Ehat(3/2)/18 + O(eps^2) (Ehat even); B cancels'} + + +# ---------------------------------------------------------------- C5: Lemma W numerically (Decimal, 60 digits) + +def control_c5(mutant): + getcontext().prec = 60 + D = Decimal + coef = D(1) / D(12) if mutant != 'M5' else D(1) / D(6) + + def to_dec(p): + return [D(a.numerator) / D(a.denominator) for a in p] + + def ev(p, x): + acc = D(0) + for a in reversed(p): + acc = acc * x + a + return acc + + shapes = { + 'odd X(X^2-1/4)^2': (pmul(X, Q2SQ), [], []), + 'even (X^2-1/4)^2(X^2+1/2)': ([], pmul(Q2SQ, [HALF, Fr(0), Fr(1)]), []), + 'mixed with phi-profile': (pmul(X, Q2SQ), pmul(Q2SQ, [HALF, Fr(0), Fr(1)]), pmul(Q2SQ, [Fr(0), Fr(0), Fr(1)])), + 'generic (X^2-1/4)^2(1+2X-X^2)/2': (pmul(Q2SQ, [Fr(0), Fr(1)]), pmul(Q2SQ, [HALF, Fr(0), -HALF]), []), + } + out = {} + for name, (o, b, e) in shapes.items(): + ratios = [] + for eps in (Fr(1, 1000), Fr(1, 10000), Fr(1, 100000)): + base0 = padd(pscale(o, eps), pscale(b, eps)) + prof = pscale(e, eps) + + def field(phi): + # F_phi = g_phi + eta0 + phi * Ehat (polynomial with Decimal coefficients) + gp = to_dec(g_poly(Fr(0))) + q = to_dec(Q2SQ) + b0 = to_dec(base0) + pr = to_dec(prof) + n = max(len(gp), len(q), len(b0), len(pr)) + get = lambda p, i: p[i] if i < len(p) else D(0) + return [get(gp, i) + 3 * phi * get(q, i) + get(b0, i) + phi * get(pr, i) for i in range(n)] + + def crit_value(phi, x0, sign): + p = field(phi) + d1 = [i * p[i] for i in range(1, len(p))] + d2 = [i * d1[i] for i in range(1, len(d1))] + x = x0 + for _ in range(60): + step = ev(d1, x) / ev(d2, x) + x -= step + if abs(step) < D(10) ** -50: + break + check(sign * ev(d2, x) > 0, 'C5 critical point not nondegenerate') + check(D('1.4') <= abs(x) <= D('1.6'), 'C5 critical point outside [1.4, 1.6]') + return ev(p, x) + + def root(fun, lo, hi): + flo = fun(lo) + for _ in range(120): + mid = (lo + hi) / 2 + fm = fun(mid) + if (fm > 0) == (flo > 0): + lo, flo = mid, fm + else: + hi = mid + return (lo + hi) / 2 + + third = D(1) / D(3) + R = root(lambda ph: crit_value(ph, -1 / (2 * ph), 1) + 1, third - D('0.01'), third + D('0.01')) + L = root(lambda ph: crit_value(ph, -1 / (2 * ph), -1), -third - D('0.01'), -third + D('0.01')) + eta = lambda phi, x: ev(to_dec(base0), x) + phi * ev(to_dec(prof), x) + dp = -coef * eta(third, D('-1.5')) + dm = -coef * eta(-third, D('1.5')) + ed = D(eps.numerator) / D(eps.denominator) + rp = (R - third - dp) / ed ** 2 + rm = (L + third - dm) / ed ** 2 + pred_len = ev(to_dec(pscale(o, eps)), D('1.5')) / 6 - ev(to_dec(prof), D('1.5')) / 18 + rl = (R - L - 2 * third - pred_len) / ed ** 2 + check(abs(rp) <= 10 and abs(rm) <= 10 and abs(rl) <= 20, 'C5 first-order edge formula fails (%s)' % name) + ratios.append(['%.6g' % float(rp), '%.6g' % float(rm), '%.6g' % float(rl)]) + # stabilization: the eps^-2 ratios at the two smallest eps agree to 2% + for k in range(3): + a, b2 = float(ratios[1][k]), float(ratios[2][k]) + check(abs(a - b2) <= 0.02 * max(1.0, abs(b2)), 'C5 ratio does not stabilize (%s)' % name) + out[name] = {'eps (shape coefficient)': ['1e-3', '1e-4', '1e-5'], + '(phi+ - 1/3 - d+)/eps^2, (phi- + 1/3 - d-)/eps^2, (length - pred)/eps^2': ratios} + return out + + +# ---------------------------------------------------------------- C6: Lemma E numerically (float, reported to 6 digits) + +def control_c6(mutant): + Phi = lambda x: 0.5 * (1.0 + math.erf(x / math.sqrt(2.0))) + phi = lambda x: math.exp(-x * x / 2) / math.sqrt(2 * math.pi) + + def gam1(S): # E[(S^2 - Z^2) 1{|Z| < S}], S >= 0 + if S <= 0: + return 0.0 + return (S * S - 1) * (2 * Phi(S) - 1) + 2 * S * phi(S) + + def part(S, c): # E[(S^2 - Z^2) 1{|Z| < min(S, c)}], S > 0 + if S <= 0: + return 0.0 + a = min(S, c) + P = 2 * Phi(a) - 1 + return S * S * P - (P - 2 * a * phi(a)) + + def expect(fun, n=2000, zmax=10.0): # composite Simpson for E f(Z) + hstep = 2 * zmax / n + tot = 0.0 + for i in range(n + 1): + z = -zmax + i * hstep + w = 1 if i in (0, n) else (4 if i % 2 else 2) + tot += w * fun(z) * phi(z) + return tot * hstep / 3 + + bound = 2.0 if mutant != 'M6' else 0.25 + rows = [] + worst = [0.0, 0.0] + for s in (0.02, 0.1, 0.3, 1.0, 2.0, 3.0, 5.0, 8.0): + for rr in (s / 8, s / 32): + d1 = (expect(lambda z: gam1(s + rr * z)) - gam1(s)) / rr ** 2 + d3 = (expect(lambda z: part(s + rr * z, s / 3)) - part(s, s / 3)) / rr ** 2 + q1, q3 = d1 / min(1.0, s), d3 / min(1.0, s) + check(d1 > -1e-6 and d3 > -1e-6, 'C6 lower bound fails at s=%g' % s) + check(q1 <= bound and q3 <= bound, 'C6 Lemma E bound fails at s=%g: %g %g' % (s, q1, q3)) + worst = [max(worst[0], q1), max(worst[1], q3)] + if rr == s / 32: + lim1 = 2 * Phi(s) - 1 + 2 * s * phi(s) + lim3 = 2 * Phi(s / 3) - 1 + check(abs(d1 - lim1) <= 0.05 * lim1 and abs(d3 - lim3) <= 0.05 * lim3, 'C6 small-v2 limit fails at s=%g' % s) + rows.append(['%.6g' % s, '%.6g' % d1, '%.6g' % lim1, '%.6g' % d3, '%.6g' % lim3]) + return {'bound_checked': '0 <= (G - g)/v2 <= 2 min(1, s) on the 16-point grid s in {0.02,...,8}, sqrt(v2/v1) in {s/8, s/32}', + 'sup_ratio_theta1': '%.4g' % worst[0], 'sup_ratio_theta1/3': '%.4g' % worst[1], + 's, D1, limit1, D1/3, limit1/3 (v2/v1 = s^2/1024)': rows} + + +# ---------------------------------------------------------------- C7: the ledger + +def control_c7(mutant): + res = {} + # int_0^infty t^2 min(1, h/t^4) dt: substitute t = h^{1/4} u, giving h^{3/4} [int_0^1 u^2 du + int_1^infty u^{-2} du]; + # both pieces integrated exactly (antiderivatives u^3/3 and -1/u) + piece1 = peval([Fr(0), Fr(0), Fr(0), Fr(1, 3)], Fr(1)) - peval([Fr(0), Fr(0), Fr(0), Fr(1, 3)], Fr(0)) + piece2 = Fr(0) - (-Fr(1) / Fr(1)) + check(piece1 + piece2 == Fr(4, 3), 'C7 the (4/3) h^(3/4) integral fails') + res['int_t2_min(1,h/t4)/h^(3/4)'] = str(piece1 + piece2) + delta = Fr(1, 10) if mutant != 'M7' else Fr(1, 8) + band = 3 - Fr(11) / (5 - delta) + res['band_tail_exponent_3-11/(5-delta)'] = str(band) + check(band >= Fr(3, 4), 'C7 band-tail exponent below 3/4') + check(3 - Fr(11) / (5 - Fr(1, 9)) == Fr(3, 4), 'C7 threshold delta = 1/9') + res['recorded_D1_exponents_at_delta_1/10'] = {'2-7/(5-delta)': str(2 - Fr(7) / (5 - delta)), '3/(5-delta)': str(Fr(3) / (5 - delta))} + # Proposition M: t = (h/u)^{1/4}, t^2 dt = (1/4) h^{3/4} u^{-7/4} du; the integrand t^2 s with s ~ u gives u^{-3/4} + exp_u = 1 + Fr(-1, 2) - Fr(5, 4) + check(exp_u == Fr(-3, 4) and exp_u > -1, 'C7 integrability at u -> 0') + res['PropM_integrand_exponent_at_u->0'] = str(exp_u) + # exponent sets: fold {-1/3 + 2k/3}, cusp {1/4 + j/2}; disjoint (8k = 7 + 6j has no solution); quintic scale 4/5 + fold = {Fr(-1, 3) + Fr(2 * k, 3) for k in range(200)} + cusp = {Fr(1, 4) + Fr(j, 2) for j in range(200)} + check(not (fold & cusp), 'C7 exponent sets intersect') + nxt = sorted(e for e in (fold | cusp) if e > Fr(1, 3))[:2] + check(nxt == [Fr(3, 4), Fr(1)], 'C7 next fold/cusp exponents') + res['next_fold_cusp_exponents_after_1/3'] = [str(e) for e in nxt] + check(Fr(4, 5) not in fold and Fr(4, 5) not in cusp, 'C7 4/5 in a set') + res['recorded_heuristic_quintic_scale_exponent'] = '4/5 (Remark 5.1; not derived here)' + res['recorded_remainder_improvement'] = {'D1_(D1.2)': '1/2', 'here': '3/4'} + return res + + +def main(): + mutant = parse_args(sys.argv[1:]) + controls = [('C1', control_c1), ('C2', control_c2), ('C3', control_c3), ('C4', control_c4), + ('C5', control_c5), ('C6', control_c6), ('C7', control_c7)] + out = {'object': 'CL-D1-SHARP-REMAINDER-20261001-v1', 'scientific_effect': 'NONE', + 'mutants': MUTANTS, 'controls': {}} + try: + for name, fn in controls: + out['controls'][name] = fn(mutant) + except ControlFailure as exc: + print(json.dumps({'mutant': mutant, 'failed': str(exc)}), file=sys.stderr) + sys.exit(1) + if mutant is not None: + print('mutant %s was not detected' % mutant, file=sys.stderr) + sys.exit(3) + sys.stdout.write(json.dumps(out, indent=1, sort_keys=True, ensure_ascii=True) + '\n') + + +if __name__ == '__main__': + main() From 0582232ef5b458dc47cd15ff97bbd536cbed2f71 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 1 Oct 2026 22:22:56 +0000 Subject: [PATCH 2/3] Theorem 1D+ (v1.1): rename after #214 v1.2, rebind #214, Slice D exposition CL-D1-SHARP-REMAINDER-20261001-v1.1. No mathematical change. - Name: Theorem D1+ -> Theorem 1D+, displays (1D+.1)-(1D+.2); #214 is cited as [1D], after #214 v1.2 renamed its theorem Theorem 1D (label only; xAI concern on #214, comments 5940492097 and 5940563636: the name D1 belongs to the cap component, Math- #193, #194). Object id and paths keep D1/d1. - Binding: consumed #214 rebound to head 4703fc7, PROOF blob 3389ef8c (v1.2; differs from 873532b9 in labels only). - Exposition: Proposition M's bad-event step names the Gaussian moments behind its Cauchy-Schwarz bounds, as suggested in the Codex Slice D review (5386194030), which accepted Slice D at 4b1ae35. - Checker: labels only (docstring, object, two recorded keys); RESULTS.json regenerated, byte-identical on CPython 3.10-3.14 with and without -O; mutant matrix unchanged. - README: v1.1 note, landing order (#214 must land first), nonauthor review record. SOURCES.json: rebinding, label_history, nonauthor_reviews. Scientific effect: NONE. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .../d1_sharp_remainder_20261001/PROOF.md | 124 ++++++++++-------- .../d1_sharp_remainder_20261001/README.md | 38 ++++-- .../d1_sharp_remainder_20261001/RESULTS.json | 6 +- .../d1_sharp_remainder_20261001/SOURCES.json | 43 +++--- .../d1_sharp_remainder_20261001/d1p_check.py | 10 +- 5 files changed, 132 insertions(+), 89 deletions(-) diff --git a/frontiers/d1_sharp_remainder_20261001/PROOF.md b/frontiers/d1_sharp_remainder_20261001/PROOF.md index a5d8da20..3b2ec970 100644 --- a/frontiers/d1_sharp_remainder_20261001/PROOF.md +++ b/frontiers/d1_sharp_remainder_20261001/PROOF.md @@ -1,20 +1,26 @@ # The one-dimensional lifetime and crest-to-trough laws with remainder `O(h^{3/4})` -Object: CL-D1-SHARP-REMAINDER-20261001-v1. +Object: CL-D1-SHARP-REMAINDER-20261001-v1.1. Author: Anthropic Claude (claude.ai session `session_01NMeKEismAyeqgdB4sy2NJU`), 1 October 2026. +**v1.1 (labels, binding and one expository addition; no mathematical change):** (i) after the xAI concern on Math- #214 +(comments 5940492097 and 5940563636), #214 v1.2 renamed its theorem **Theorem 1D**, label only, so that it is not read +as the cap component D1 (Math- #193, #194). This note follows: its theorem is **Theorem 1D⁺**, with displays +(1D⁺.1)–(1D⁺.2), and #214 is cited as [1D], bound to its v1.2 blob. (ii) Proposition M's bad-event step names the +moments that its Cauchy–Schwarz bounds use, as suggested in the Codex Slice D review (Math- #238, review 5386194030). +The object identifier and the paths keep `D1`/`d1`, which there mean dimension one. Disposition: AUTHOR-SIDE PROOF CANDIDATE; NONAUTHOR REVIEW REQUIRED. Scientific effect: NONE — no register, graph, STATUS, PROOF_INDEX, prize or Boolean change. Same GitHub account as every lane; zero organizational independence. -**Consumes** Math- #214 (open, unmerged; head `cf162b1c69…`, `frontiers/d1_third_order_law_20261001/PROOF.md` blob -`873532b9`, v1.1), cited below as [D1]. Its nonauthor analytic review (OpenAI Codex, comment 5933752065, "Slices A–D and -Theorem D1 ACCEPTED at the stated circle scope") was given on head `f4a58df`; the refresh to `cf162b1` merged `main` and -left the packet's bytes unchanged. Used from [D1]: §§0–5 as stated, and also the intermediate estimates in the proof of -[D1] Prop. 2.2 (c)–(d). §2 reruns those estimates on a longer range. The expansions among them follow from [D1] Lemma -1.3, the bounds on `ζ_θ` are properties of `ζ_θ` alone, and none of them uses `t ≤ t_*` (Prop. 2.2⁺ (c)). Nothing else -is consumed. +**Consumes** Math- #214 (open, unmerged; head `4703fc7b3b…`, `frontiers/d1_third_order_law_20261001/PROOF.md` blob +`3389ef8c`, v1.2), cited below as [1D]. Its nonauthor analytic review (OpenAI Codex, comment 5933752065, "Slices A–D and +Theorem D1 ACCEPTED at the stated circle scope", under the theorem's former name) was given on head `f4a58df`. The +refresh to `cf162b1` merged `main` and left the packet's bytes unchanged; v1.2 (`4703fc7`) changed labels only. Used +from [1D]: §§0–5 as stated, and also the intermediate estimates in the proof of [1D] Prop. 2.2 (c)–(d). §2 reruns those +estimates on a longer range. The expansions among them follow from [1D] Lemma 1.3, the bounds on `ζ_θ` are properties +of `ζ_θ` alone, and none of them uses `t ≤ t_*` (Prop. 2.2⁺ (c)). Nothing else is consumed. ## 0. Statement -Setting, notation and constants are those of [D1] §0–§1: +Setting, notation and constants are those of [1D] §0–§1: - the circle `T = R/LZ` and the hypothesis (H); - the canonical two-point densities `ν₊` (crest-to-trough amplitude) and `ν` (persistence lifetime); - the pair at `±τ`, with separation `t = 2τ`, gap `h`, `α = 12h/t³` and `κ = h/t⁴`; @@ -23,27 +29,27 @@ Setting, notation and constants are those of [D1] §0–§1: Throughout, `‖u‖_{C²} := max(sup|u|, sup|u'|, sup|u''|)` on `[−2, 2]`. -**Theorem D1⁺.** Under (H), as `h ↓ 0` and `ℓ ↓ 0`, +**Theorem 1D⁺.** Under (H), as `h ↓ 0` and `ℓ ↓ 0`, - ν₊(h) = (C₀/2) h^{−1/3} + (I/2) h^{1/4} + B₂ h^{1/3} + O(h^{3/4}), (D1⁺.1) - ν(ℓ) = C₀ ℓ^{−1/3} + C₁ ℓ^{1/4} + 2B₂ ℓ^{1/3} + O(ℓ^{3/4}). (D1⁺.2) + ν₊(h) = (C₀/2) h^{−1/3} + (I/2) h^{1/4} + B₂ h^{1/3} + O(h^{3/4}), (1D⁺.1) + ν(ℓ) = C₀ ℓ^{−1/3} + C₁ ℓ^{1/4} + 2B₂ ℓ^{1/3} + O(ℓ^{3/4}). (1D⁺.2) -In particular `2ν₊(ℓ) − ν(ℓ) = (I − C₁)ℓ^{1/4} + O(ℓ^{3/4})`. [D1] §0 reads `2ν₊ − ν` as the density of adjacent +In particular `2ν₊(ℓ) − ν(ℓ) = (I − C₁)ℓ^{1/4} + O(ℓ^{3/4})`. [1D] §0 reads `2ν₊ − ν` as the density of adjacent max/min pairs that are not elder pairs. -[D1] proved the same expansions with `O(h^{1/2})`; its proof gives `O(h^{0.57})` for (D1.1). The exponent `3/4` is the +[1D] proved the same expansions with `O(h^{1/2})`; its proof gives `O(h^{0.57})` for (1D.1). The exponent `3/4` is the order of the first correction to the cusp term (§5.1). No claim is made that its coefficient is nonzero. -**What limited [D1], and what replaces it.** +**What limited [1D], and what replaces it.** -| | [D1] | limit | here | +| | [1D] | limit | here | |---|---|---|---| | `E₂`-correction | Prop. 2.2 (a): kernel `≤ Ct²` on `t ≤ t_*` | `O(t_*³) = O(h^{0.61})` | Lemma E: kernel `≤ Ct² min(1, s)`, `s = m v₁^{−1/2} ≍ κ`, so `O(h^{3/4})` | | tails at `t_*` | Prop. 2.2 (c), (d): fold and cusp cut at `t_*` separately | `O(h²t_*^{−7}) = O(h^{0.57})` | Prop. 2.2⁺ (b): their difference, the model kernel, is `O(h³t^{−12})` beyond `t_*`, so both are integrated to a fixed `t₀` | | elder misclassification | §5: window perturbation of relative size `t/κ`, bounded in absolute value | `O(h^{1/2})` | Lemmas Φ, W and Prop. M: given all but `φ_G = E₁/m`, the elder set is an interval `(φ₋, φ₊)` independent of `φ_G`. The misclassified mass is first order in the mean of the first-order part of `φ₊ − φ₋ − 2/3`, which is `O(t²)`, and second order in its fluctuation, `O((t/κ)²)`. | **Mechanism.** -- *Splitting and regression.* Under `Q` the field splits into independent even and odd parts ([D1] Remark 1.4). +- *Splitting and regression.* Under `Q` the field splits into independent even and odd parts ([1D] Remark 1.4). Regressing the even part on `E₁` makes the rescaled field affine in `φ_G := E₁/m` (Lemma Φ). The profile is `≈ 3(X² − ¼)²`, and the remainder is independent of `φ_G`. - *The elder set is an interval.* The elder rule is monotone in `φ_G` near the window edges `±1/3`. So, given the @@ -60,11 +66,11 @@ order of the first correction to the cusp term (§5.1). No claim is made that it Both orders are relative `O(t² + (t/κ)²)` of the edge mass, which integrates to `O(h^{3/4})` (Proposition M). **Not claimed.** The `h^{3/4}` coefficient or its sign; sharpness of `3/4`; uniformity in the covariance; anything on `R` -([D1] §6.4). +([1D] §6.4). ## 1. The `E₂`-correction -As in [D1] §2, let `E₁ ~ N(0, v₁)` and `E₂ ~ N(0, v₂)` be independent, `m > 0` and `s := m v₁^{−1/2}`. Put +As in [1D] §2, let `E₁ ~ N(0, v₁)` and `E₂ ~ N(0, v₂)` be independent, `m > 0` and `s := m v₁^{−1/2}`. Put w := ((m + E₂)² − E₁²)⁺1{m + E₂ > 0}, G₁ := E w, G_{1/3} := E[w 1{|E₁| < m/3}], g_θ := E[(m² − E₁²)⁺1{|E₁| < θm}] for θ ∈ {1, 1/3}. @@ -111,13 +117,13 @@ Control C6 checks this order on a grid. Write `Φ` and `ϕ` for the standard nor ## 2. The sign kernels to `O(h^{3/4})` -**Proposition 2.2⁺.** Fix `δ ∈ (0, 1/10]` and `t_* := (12h)^{1/(5−δ)}`, as in [D1] Prop. 2.2 (`t ≤ t_*` iff +**Proposition 2.2⁺.** Fix `δ ∈ (0, 1/10]` and `t_* := (12h)^{1/(5−δ)}`, as in [1D] Prop. 2.2 (`t ≤ t_*` iff `α ≥ t^{2−δ}`). For `θ ∈ {1, 1/3}`, with `I₁ := I` and `I_{1/3} := C₁`, ∫₀^{t_*} K_θ^{sign}(t, h) dt = (C₀/2) h^{−1/3} + (I_θ/2) h^{1/4} + B₂ h^{1/3} + O(h^{3/4}). -*Proof.* Fix `t₀ ∈ (0, 1]` so small that the expansions of [D1] Lemma 1.3 hold on `t ≤ t₀`, and let `h` be so small -that `t_* ≤ t₀`. The model kernel ([D1] Prop. 2.2 (b)) is +*Proof.* Fix `t₀ ∈ (0, 1]` so small that the expansions of [1D] Lemma 1.3 hold on `t ≤ t₀`, and let `h` be so small +that `t_* ≤ t₀`. The model kernel ([1D] Prop. 2.2 (b)) is k_θ := (12/t⁴)p_t g_θ = (12/t⁴)p_t m² − (12/t⁴)p_t v₁ζ_θ(s). @@ -137,7 +143,7 @@ using `(1 + α²)p_t ≤ C`. Since `∫₀^∞ t² min(1, h/t⁴) dt = (4/3)h^{3 we get `∫₀^{t_*}(K_θ^{sign} − k_θ)dt = O(h^{3/4})`. The correction is integrated only up to `t_*`. Beyond `t ≍ h^{1/5}`, where `m ≍ v₂^{1/2}`, the difference -`K₁^{sign} − k₁` contains the non-adjacent sign pairs, whose contribution is of order one in `h` ([D1] §6.2); that range +`K₁^{sign} − k₁` contains the non-adjacent sign pairs, whose contribution is of order one in `h` ([1D] §6.2); that range is handled by the band lemma (§4). (b) *The tail of the model kernel.* `k_θ = (12/t⁴)p_t v₁γ_θ(s)` with @@ -147,11 +153,11 @@ is handled by the band lemma (§4). Since `δ ≤ 1/9`, the exponent is at least `3/4`; it is `37/49` for `δ = 1/10`. Here the fold term `(12/t⁴)p_t m²` and the cusp term `(12/t⁴)p_t v₁ζ_θ(s)` are each of order `h²t^{−8}`. Their difference `k_θ` is smaller by the factor -`s ≍ h/t⁴`, since `γ_θ(s) = 2θ(1 − θ²/3)(2π)^{−1/2}s³(1 + O(s²))`. [D1] cut each at `t_*` separately and lost +`s ≍ h/t⁴`, since `γ_θ(s) = 2θ(1 − θ²/3)(2π)^{−1/2}s³(1 + O(s²))`. [1D] cut each at `t_*` separately and lost `h²t_*^{−7}`. -(c) *The model integral to `t₀`.* Run [D1] Prop. 2.2 (c)–(e) with the upper limit `t_*` replaced by `t₀`. None of the -estimates used in that proof uses `t ≤ t_*`. The expansions follow from [D1] Lemma 1.3 for `t ≤ t₀` and `α ≤ τ^{−1}`, +(c) *The model integral to `t₀`.* Run [1D] Prop. 2.2 (c)–(e) with the upper limit `t_*` replaced by `t₀`. None of the +estimates used in that proof uses `t ≤ t_*`. The expansions follow from [1D] Lemma 1.3 for `t ≤ t₀` and `α ≤ τ^{−1}`, and from `p_t ≤ Ce^{−α²/(4σ₃²)}` beyond. The bounds on `ζ_θ` are properties of `ζ_θ` alone, and the split at `t_c` is a device of the proof. The estimates are: the fold expansion with its `O(τ⁴(1 + α⁴))` term, the cusp expansion with `|ε| ≤ Cτ²(1 + α²)`, the bounds on `ζ_θ`, `ζ_θ'` and `1 − ζ_θ`, and the split at `t_c = h^{1/4}`. The changes: @@ -171,18 +177,18 @@ Finally `∫₀^{t_*}K_θ^{sign} = ∫₀^{t₀}k_θ − ∫_{t_*}^{t₀}k_θ + ### 3.1 Regression along `φ_G` -Fix `t ≤ t₀` and `α > 0`, and work under `Q = Q_{t,α}`. By [D1] Remark 1.4, `f = f_e + f_o` with `f_e` and `f_o` +Fix `t ≤ t₀` and `α > 0`, and work under `Q = Q_{t,α}`. By [1D] Remark 1.4, `f = f_e + f_o` with `f_e` and `f_o` independent. - `f_e` is centered, and its law does not depend on `α`: its only pin, `U₂ = 0`, is homogeneous, and `U₁, U₃` are functionals of `f_o`. - `f_o` has mean `αμ_t`, with `μ_t` deterministic and odd, and its centered part has a law that does not depend on `α`. -As in [D1] Lemma 1.2, `E₁ := f_e''(τ)`, `m := E_Q f_o''(τ) = c(t)α`, `E₂ := f_o''(τ) − m`, `v₁ := Var_Q E₁` and +As in [1D] Lemma 1.2, `E₁ := f_e''(τ)`, `m := E_Q f_o''(τ) = c(t)α`, `E₂ := f_o''(τ) − m`, `v₁ := Var_Q E₁` and `s := m v₁^{−1/2}`. Define ψ(x) := Cov_Q(f_e(x), E₁)/v₁, f_e^⊥ := f_e − E₁ψ, φ_G := E₁/m, ω := (f_o, f_e^⊥). -With `b := f(−τ)` and `F(X) := (f(tX) − b)/h` (the window field `𝔉` of [D1] Lemma 3.2), +With `b := f(−τ)` and `F(X) := (f(tX) − b)/h` (the window field `𝔉` of [1D] Lemma 3.2), F = 2X³ − (3/2)X − ½ + O + B + φ_G Ψ̂, (3.1) O(X) := f_o(tX)/h − 2X³ + (3/2)X, B(X) := (f_e^⊥(tX) − f_e^⊥(τ))/h, Ψ̂(X) := (m/h)(ψ(tX) − ψ(τ)). @@ -220,7 +226,7 @@ parities are those of `f_e` and `f_o`. The vanishing at `±½`: E₁ = a₄τ²/3 + ρ₁, ρ₁ := R''(τ) − R'(τ)/τ, with `|∂_X^k R̃(tX)| ≤ Ct⁶K^e` on `[−2, 2]` (`k ≤ 2`) and `|ρ₁| ≤ Cτ⁴K^e`. The `Q`-law of `f_e` is free of `α`, and -`E_Q(K^e)² ≤ C` by Sudakov–Fernique and Borell–TIS, as in [D1] Lemma 4.3. Also `V := Var_Q a₄ → σ₄²`, so `V ∈ [c, C]`. +`E_Q(K^e)² ≤ C` by Sudakov–Fernique and Borell–TIS, as in [1D] Lemma 4.3. Also `V := Var_Q a₄ → σ₄²`, so `V ∈ [c, C]`. Then v₁ = (τ⁴/9)V(1 + O(τ²)), Cov_Q(f_e(tX) − f_e(τ), E₁) = (t⁴/24)(X² − ¼)²(τ²V/3)(1 + O(τ²)) + Cov_Q(R̃(tX), E₁), @@ -239,7 +245,7 @@ cubic Hermite basis at `τ`: `p₁(x) = (3/2)(x/τ) − ½(x/τ)³` and `p₂(x) So `O = R̃_o(t·)/h` and `‖O‖_{C²} ≤ C(t⁵/h)K^o = C(t/κ)K^o`. The map `f_o ↦ R̃_o` is linear, which gives both bounds. - *Applied to `αμ_t`* it gives `‖E_QO‖_{C²} ≤ C(αt⁵/h)sup_{[−2t, 2t]}|μ_t^{(5)}| = 12Ct² sup|μ_t^{(5)}|`. The sup is bounded uniformly: `μ_t^{(5)}(x) = Cov(f_o^{(5)}(x), (U₁, U₃))Cov(U₁, U₃)^{−1}e₂` is continuous in `(t, x)`, - `Cov(U₁, U₃)` is invertible for each `t > 0` ([D1] Lemma 1.1), and it has a nondegenerate limit as `t ↓ 0` ([D1] Lemma + `Cov(U₁, U₃)` is invertible for each `t > 0` ([1D] Lemma 1.1), and it has a nondegenerate limit as `t ↓ 0` ([1D] Lemma 1.3). So `sup_{t ≤ t₀}sup_{[−2t,2t]}|μ_t^{(5)}| < ∞`. - *Applied to `f_o − E_Qf_o`* it gives the second bound. @@ -256,7 +262,7 @@ So the bound holds with `K^⊥ := C(|a₄^⊥|/t² + K^e + |Z|)`. Each term has ### 3.2 The window edges -The model `g_φ` of [D1] (3.1) has its third critical point at `X₃ = −1/(2φ)`. There (checker C1) +The model `g_φ` of [1D] (3.1) has its third critical point at `X₃ = −1/(2φ)`. There (checker C1) Γ₊(φ) := g_φ(X₃) + 1 = (φ + 1)³(3φ − 1)/(16φ³), Γ₋(φ) := g_φ(X₃) = (φ − 1)³(3φ + 1)/(16φ³), Γ₊'(φ) = Γ₋'(φ) = 3(1 − φ²)²/(16φ⁴), Γ₊(1/3) = Γ₋(−1/3) = 0, Γ₊'(1/3) = Γ₋'(−1/3) = 12, g_φ''(X₃) = 3(1 − φ²)/φ. (3.2) @@ -280,12 +286,12 @@ Put `η₀ := 1/100`, `J₊ := [1/3 − η₀, 1/3 + η₀]` and `J₋ := −J φ₊ − φ₋ − 2/3 = O(3/2)/6 − Ê(3/2)/18 + r₊ − r₋. (3.3) -*Proof.* *Typing.* For `|φ| ≤ 2`, `‖F_φ − g_φ‖_{C²} ≤ ε`, and typing forces `|φ| < 1 + ε/6` ([D1] Lemma 3.3). For +*Proof.* *Typing.* For `|φ| ≤ 2`, `‖F_φ − g_φ‖_{C²} ≤ ε`, and typing forces `|φ| < 1 + ε/6` ([1D] Lemma 3.3). For `|φ| > 2` the pair is not typed: - for `φ > 2`, `F_φ''(−½) = 6(φ − 1) + η⁰''(−½) + φÊ''(−½) ≥ 6(φ − 1) − ε − φε/2 > 0`; - for `φ < −2`, symmetrically `F_φ''(½) < 0`. -*Off the edges.* [D1] Lemma 3.3 with `η = η₀`, taking `c₀ ≤ c₀^{[D1]}η₀`, gives: for typed `φ` with +*Off the edges.* [1D] Lemma 3.3 with `η = η₀`, taking `c₀ ≤ c₀^{[1D]}η₀`, gives: for typed `φ` with `||φ| − 1/3| ≥ η₀`, `𝔖` is the death point iff `|φ| < 1/3`. *The edge `J₊`.* Fix `φ ∈ J₊`. The model satisfies, exactly (checker C2): @@ -332,7 +338,7 @@ This proves (W.2) for `φ₊`. *The edge `J₋`.* This is the mirror case. Checker C1 checks the symmetry `g(−X, −φ) = −1 − g(X, φ)` and `Γ₋(φ) = −Γ₊(−φ)`; checker C2 checks `g(2) + 1 = 675φ/16 + 27/2 ≤ −9/64` and `g''(X₃) ≤ −7.7`. Fix `φ ∈ J₋`. -- *The negative direction.* The arc falls below `−1` before exceeding `0`, as in [D1] Lemma 3.3 (E) for `φ < 0`. So +- *The negative direction.* The arc falls below `−1` before exceeding `0`, as in [1D] Lemma 3.3 (E) for `φ < 0`. So `m₋ < −1`. - *The positive direction.* The arc descends to `𝔖` and rises to a nondegenerate local maximum `F(X₃'')`, with `X₃''` near `X₃ ∈ [1.45, 1.55]`. It then falls below `−1` before `2`. So `m₊ = −1` iff `μ₋(φ) := max_{[1, 2]}F_φ > 0`. @@ -348,8 +354,8 @@ The even part `B` cancels from the window length; it only translates the window ### 3.3 The misclassified mass -Let `K(t, h)` be the elder kernel [D1] (1.3) and `K_{1/3}^{sign} = (12/t⁴)p_t E_Q[w 1{|φ_G| < 1/3}]` the sign kernel, -where `w = (−f''(−τ))⁺f''(τ)⁺ = ((m + E₂)² − E₁²)⁺1{m + E₂ > 0}` ([D1] (1.4)). +Let `K(t, h)` be the elder kernel [1D] (1.3) and `K_{1/3}^{sign} = (12/t⁴)p_t E_Q[w 1{|φ_G| < 1/3}]` the sign kernel, +where `w = (−f''(−τ))⁺f''(τ)⁺ = ((m + E₂)² − E₁²)⁺1{m + E₂ > 0}` ([1D] (1.4)). **Proposition M.** For `δ ∈ (0, 1/10]` and `t_*` as above, `∫₀^{t_*}|K(t, h) − K_{1/3}^{sign}(t, h)| dt = O(h^{3/4})`. @@ -393,11 +399,14 @@ Hence and by (Φ.2)–(Φ.3), `E_Qε² ≤ C(t⁴ + (t/κ)² + (t²/κ)² + τ⁴) ≤ C(t² + (t/κ)²)`. -*The bad event.* Off `𝒢` there are two contributions. +*The bad event.* Off `𝒢` there are two contributions. Both are bounded by Cauchy–Schwarz, using Gaussian moments: since +`E₂ ~ N(0, v₂)`, `E(m + |E₂|)⁴ ≤ C(m² + v₂)²` and `E(8m²/9 + 2mE₂ + E₂²)⁴ ≤ C(m² + v₂)⁴`. - Both conditional expectations are at most `E[w | ω] ≤ (m + |E₂|)²`. By Cauchy–Schwarz this contributes at most `C(m² + v₂)P(𝒢^c)^{1/2}`. -- The main term above carries `e_s ≤ s/√(2π)` and the factor `O(3/2)`. By Cauchy–Schwarz and `E_Q[O(3/2)⁴] ≤ C` (Φ.2) - it contributes at most `Cs(m² + v₂)P(𝒢^c)^{1/2}`. +- The main term above carries `e_s ≤ s/√(2π)` and the factor `Y := O(3/2)/6 − Ê(3/2)/18`. Here `E_Q[O(3/2)⁴] ≤ C` + (Φ.2), and `Ê` is deterministic with `|Ê(3/2)| ≤ Cτ²` (Φ.1), so `E_QY⁴ ≤ C`. By Hölder, the mixed moment + `E[(8m²/9 + 2mE₂ + E₂²)²Y²]` is at most `C(m² + v₂)²`, and by Cauchy–Schwarz the term contributes at most + `Cs(m² + v₂)P(𝒢^c)^{1/2}`. On `t ≤ t_*` we have `κ/t = α/(12t²) ≥ t^{−δ}/12` and `‖E_QO‖_{C²} + 2‖Ê‖_{C²} ≤ Ct² ≤ c₁/2`. The Gaussian tails of `K̃^o` and `K^⊥` then give `P(𝒢^c) ≤ Ce^{−c(κ/t)²} ≤ Ce^{−ct^{−2δ}}`. @@ -412,30 +421,30 @@ Now `(12/t⁴)m² ≤ Cα²/t² ≤ Cs²`, `(12/t⁴)v₂ ≤ Ct²` and `(t/κ) - *The second part* is at most `C(1 + s³)e^{−ct^{−2δ}} ≤ C(1 + h³t^{−12})e^{−ct^{−2δ}}`. Its integral over `(0, t_*]` is `≤ C'_{c,δ}(1 + h³)t_*e^{−(c/2)t_*^{−2δ}} = O(h^N)`, where `C'_{c,δ} := sup_{t>0}(1 + t^{−12})e^{−(c/2)t^{−2δ}}`. ∎ -## 4. Proof of Theorem D1⁺ +## 4. Proof of Theorem 1D⁺ -Fix `δ = 1/10`, and `t₀` as in Proposition 2.2⁺, small enough also for [D1] Lemma 4.3 (whose own `t₀` is a fixed constant +Fix `δ = 1/10`, and `t₀` as in Proposition 2.2⁺, small enough also for [1D] Lemma 4.3 (whose own `t₀` is a fixed constant in `(0, L/4]`). -**(D1⁺.1).** Write `ν₊ = ∫₀^{t_*}K₊ + ∫_{t_*}^{L}K₊`, where `L` is the length of the circle. -- On `(0, t_*]`, `K₊ = K₁^{sign} − (12/t⁴)p_tE_Q[w1{not adjacent}]`. By [D1] Lemma 3.1, non-adjacency forces - `K₅ ≥ ct^{−δ}`, so the correction integrates to `O(h^N)` ([D1] §5). Proposition 2.2⁺ with `θ = 1` gives the expansion. -- On `[t_*, L)`, `K₊ ≤ K^{band}` (an adjacent pair is banded), and [D1] Lemma 4.3 gives `O(h^{3/4}) + O(h)`. +**(1D⁺.1).** Write `ν₊ = ∫₀^{t_*}K₊ + ∫_{t_*}^{L}K₊`, where `L` is the length of the circle. +- On `(0, t_*]`, `K₊ = K₁^{sign} − (12/t⁴)p_tE_Q[w1{not adjacent}]`. By [1D] Lemma 3.1, non-adjacency forces + `K₅ ≥ ct^{−δ}`, so the correction integrates to `O(h^N)` ([1D] §5). Proposition 2.2⁺ with `θ = 1` gives the expansion. +- On `[t_*, L)`, `K₊ ≤ K^{band}` (an adjacent pair is banded), and [1D] Lemma 4.3 gives `O(h^{3/4}) + O(h)`. -**(D1⁺.2).** Write `ν = 2∫₀^{L/2}K` ([D1] §1). +**(1D⁺.2).** Write `ν = 2∫₀^{L/2}K` ([1D] §1). - On `(0, t_*]`, `K = K_{1/3}^{sign} + (K − K_{1/3}^{sign})`. Proposition 2.2⁺ with `θ = 1/3` gives the expansion with `I_{1/3} = C₁`, and Proposition M bounds the rest by `O(h^{3/4})`. -- On `[t_*, L/2]`, an elder pair is banded or co-banded ([D1] §4), so `K ≤ K^{band} + K^{co}`, and [D1] Lemma 4.3 gives +- On `[t_*, L/2]`, an elder pair is banded or co-banded ([1D] §4), so `K ≤ K^{band} + K^{co}`, and [1D] Lemma 4.3 gives `O(h^{3/4})`. -Doubling gives (D1⁺.2). ∎ +Doubling gives (1D⁺.2). ∎ ## 5. Remarks **5.1 The order `h^{3/4}`.** Four pieces are each `h^{3/4}` times a convergent Mellin-type integral; here they are only bounded: - the `E₂`-correction (for `θ = 1/3`, `G_{1/3} − g_{1/3} = v₂P(|E₁| < m/3)(1 + o(1))`); -- the `τ²`-corrections of the cusp kernel ([D1] Prop. 2.2 (d), the error `ε`); +- the `τ²`-corrections of the cusp kernel ([1D] Prop. 2.2 (d), the error `ε`); - the term `(p₃(α) − p₃(0))(1 − ζ_θ(s₀))`; - for `ν`, the window edges of Proposition M: the mean of the first-order part of `φ₊ − φ₋ − 2/3`, the correlation term `2m Cov_Q(E₂, O(3/2))`, and the second-order terms. @@ -448,17 +457,17 @@ These never coincide (`8k = 7 + 6j` has no solution; checker C7), so there are n `t ≍ h^{1/5}` appears where the quintic jet competes and `m ≍ E₂`. There the model kernel loses relative order one, contributing order `h^{4/5}`. So the exponent after `1/3` is `3/4`, then `4/5`, then `1`. -On sharpness, [D1] §6.2 records that for the Gaussian kernel the `θ = 1/3` sign-kernel remainder after three terms is +On sharpness, [1D] §6.2 records that for the Gaussian kernel the `θ = 1/3` sign-kernel remainder after three terms is `≈ 0.038h^{3/4}`, constant over `h = 10^{−10}, …, 10^{−26}`; a referee recomputed `0.0381`. This is evidence only that the `θ = 1/3` sign-kernel integral has a nonzero `h^{3/4}` term for that kernel. It does not show that a nonzero `h^{3/4}` term survives in `ν`, where Proposition M's misclassified mass is of the same order, or in `ν₊`; neither is examined here. **5.2 Where the parity enters.** Without the independence of `(φ₋, φ₊)` from `φ_G`, the misclassified mass can only be -bounded by the probability that `φ_G` lies within the edge fluctuation, `O(t/κ)` relative. That is [D1]'s `O(h^{1/2})`. +bounded by the probability that `φ_G` lies within the edge fluctuation, `O(t/κ)` relative. That is [1D]'s `O(h^{1/2})`. Three facts make the first order a mean: - the regression of Lemma Φ, which is exact for Gaussian fields; -- the independence of `E₂` (odd) from `φ_G` (even), which makes the weight a function of `φ_G` given `ω` ([D1] Remark +- the independence of `E₂` (odd) from `φ_G` (even), which makes the weight a function of `φ_G` given `ω` ([1D] Remark 1.4); - the evenness of `W` and `p_s`, which reduces the first order to the window length (3.3). @@ -511,8 +520,9 @@ archived with the project record. ## 6. Sources (exact identities in `SOURCES.json`) -**Consumed.** [D1] = Math- #214, `frontiers/d1_third_order_law_20261001/PROOF.md`, blob `873532b9` at head -`cf162b1c69…` (open; bound by the workflow's drift gate). It supplies: +**Consumed.** [1D] = Math- #214, `frontiers/d1_third_order_law_20261001/PROOF.md`, blob `3389ef8c` at head +`4703fc7b3b…` (v1.2; open; bound by the workflow's drift gate). The v1.1 blob `873532b9` differs from it in labels +only. It supplies: - §0: the setting and constants; - §1: Lemmas 1.1–1.3, the canonical versions (1.2)–(1.3), (1.4) and Remark 1.4; - §2: the sign kernels, `γ_θ`, `ζ_θ`, Lemma 2.1, Prop. 2.2 (b)–(e), and the intermediate estimates in its proof of @@ -528,7 +538,7 @@ archived with the project record. open) and #229 (`frontiers/third_order_rate_20261001/PROOF.md`, open): the elder window and densities in `d ≥ 2` (§5.3). -External: Sudakov–Fernique and Borell–TIS (as used in [D1] Lemma 4.3); Gaussian regression. +External: Sudakov–Fernique and Borell–TIS (as used in [1D] Lemma 4.3); Gaussian regression. ## 7. Exact controls @@ -545,7 +555,7 @@ label exits 2. | C4 | A bookkeeping check of (3.3), for random rational odd/even polynomials vanishing to second order at `±½`: the even part cancels from the window length. | | C5 | (W.2)–(W.3) numerically. The edges `φ±` are computed at 60 digits (Newton for the critical point, bisection in `φ`) for four perturbation shapes (odd, even, mixed with a `φ`-profile, generic). Here `ε` is the shape coefficient, not Lemma W's `ε`, at `ε = 10^{−3}, 10^{−4}, 10^{−5}`. It checks that the edge errors are `≤ 10ε²`, the window-length error is `≤ 20ε²`, and the ratios to `ε²` stabilize to 2%. Observed: the edge errors are at most `1.25ε²` and the length error at most `1.5001ε²`. For the odd shape the ratios tend to `±1/12` and `1/6`, for the even shape to `±3/4` and `3/2`. It does not test (W.1). | | C6 | Lemma E numerically, on a 16-point grid: `(G_θ − g_θ)/v₂` by composite Simpson quadrature, the bound `0 ≤ · ≤ 2 min(1, s)`, and the small-`v₂` limits. | -| C7 | The ledger. Checked: `∫₀^∞t² min(1, h/t⁴) = (4/3)h^{3/4}`, by scaling to `h = 1` and evaluating the exact antiderivatives `u³/3` and `−1/u` of the two pieces; `3 − 11/(5 − δ) ≥ 3/4` iff `δ ≤ 1/9` (`37/49` at `δ = 1/10`); the integrability exponent `−3/4` of Proposition M; the disjointness of the fold and cusp exponent sets, `{−1/3 + 2k/3}` and `{1/4 + j/2}`. Recorded only: the heuristic quintic-scale exponent `4/5` of §5.1 and [D1]'s exponents. | +| C7 | The ledger. Checked: `∫₀^∞t² min(1, h/t⁴) = (4/3)h^{3/4}`, by scaling to `h = 1` and evaluating the exact antiderivatives `u³/3` and `−1/u` of the two pieces; `3 − 11/(5 − δ) ≥ 3/4` iff `δ ≤ 1/9` (`37/49` at `δ = 1/10`); the integrability exponent `−3/4` of Proposition M; the disjointness of the fold and cusp exponent sets, `{−1/3 + 2k/3}` and `{1/4 + j/2}`. Recorded only: the heuristic quintic-scale exponent `4/5` of §5.1 and [1D]'s exponents. | What the controls do not test: Lemma E's proof, Lemma Φ's estimates, Lemma W's perturbation argument, (W.1), Proposition M and the assembly are proved in prose only. C5 and C6 are numerical consistency checks, not proofs. diff --git a/frontiers/d1_sharp_remainder_20261001/README.md b/frontiers/d1_sharp_remainder_20261001/README.md index ba8f3735..1ef9e151 100644 --- a/frontiers/d1_sharp_remainder_20261001/README.md +++ b/frontiers/d1_sharp_remainder_20261001/README.md @@ -2,16 +2,24 @@ **Author-side proof candidate (Anthropic Claude). Scientific effect: NONE. Nonauthor review required.** -Object `CL-D1-SHARP-REMAINDER-20261001-v1`. Full text: [`PROOF.md`](PROOF.md). +Object `CL-D1-SHARP-REMAINDER-20261001-v1.1`. Full text: [`PROOF.md`](PROOF.md). + +**v1.1 (no mathematical change).** +- *Name.* The theorem is now **Theorem 1D⁺**. Math- #214 v1.2 renamed its theorem **Theorem 1D**, label only, after the + xAI concern 5940492097: the name D1 belongs to the cap component (Math- #193, #194). The object identifier and the + paths keep `D1`/`d1`, which there mean dimension one. +- *Binding.* #214 is rebound to its v1.2 blob `3389ef8c`. +- *Exposition.* Proposition M's bad-event step names the moments that its Cauchy–Schwarz bounds use, as suggested in + the Codex Slice D review (5386194030). ## Result On the circle `T = R/LZ`, under Math- #214's hypothesis (H), as `h ↓ 0` and `ℓ ↓ 0`: - ν₊(h) = (C₀/2) h^{−1/3} + (I/2) h^{1/4} + B₂ h^{1/3} + O(h^{3/4}) (D1⁺.1) - ν(ℓ) = C₀ ℓ^{−1/3} + C₁ ℓ^{1/4} + 2B₂ ℓ^{1/3} + O(ℓ^{3/4}) (D1⁺.2) + ν₊(h) = (C₀/2) h^{−1/3} + (I/2) h^{1/4} + B₂ h^{1/3} + O(h^{3/4}) (1D⁺.1) + ν(ℓ) = C₀ ℓ^{−1/3} + C₁ ℓ^{1/4} + 2B₂ ℓ^{1/3} + O(ℓ^{3/4}) (1D⁺.2) -- **What it improves.** Math- #214 proved these with `O(h^{1/2})`; its proof gives `O(h^{0.57})` for (D1.1). The +- **What it improves.** Math- #214 proved these with `O(h^{1/2})`; its proof gives `O(h^{0.57})` for (1D.1). The constants are #214's. - **Consequence.** `2ν₊(ℓ) − ν(ℓ) = (I − C₁)ℓ^{1/4} + O(ℓ^{3/4})`. - **The exponent.** `3/4` is the order of the first correction to the cusp term (PROOF §5.1). Its coefficient is not @@ -27,7 +35,7 @@ On the circle `T = R/LZ`, under Math- #214's hypothesis (H), as `h ↓ 0` and ` | **Lemma W** | Given everything but `φ_G`, the elder set is an interval `(φ₋, φ₊)`. Its edges move by `−η_{±1/3}(∓3/2)/12 + O(ε²)`, since the slope of the competing critical value is `12`. Also `φ₊ − φ₋ − 2/3 = O(3/2)/6 − Ê(3/2)/18 + O(ε²)`: the even remainder only translates the window. | #214 Lemma 3.3's margin `η` at the edges | | **Prop. M** | The elder kernel differs from the sign kernel by relative `O(t² + (t/κ)²)` of the edge mass, `O(h^{3/4})` in total | #214's misclassification bound `O(h^{1/2})` | -The gain in (D1⁺.2) comes from a mean. The edges of the elder window fluctuate by `O(t/κ)`. But conditionally on +The gain in (1D⁺.2) comes from a mean. The edges of the elder window fluctuate by `O(t/κ)`. But conditionally on everything except `φ_G`, the elder set is an interval whose endpoints are independent of `φ_G`. So the misclassified mass is first order only in the *mean* of the first-order part of `φ₊ − φ₋ − 2/3`, and second order in the fluctuation. That mean is `O(t²)`, for three reasons: @@ -37,10 +45,10 @@ mean is `O(t²)`, for three reasons: ## Dependencies -**Consumed.** Math- #214 (open; head `cf162b1`, PROOF blob `873532b9`, v1.1): +**Consumed.** Math- #214 (open; head `4703fc7`, PROOF blob `3389ef8c`, v1.2, which changed labels only): - §§0–5 as stated, plus the intermediate estimates in its proof of Prop. 2.2 (c)–(d), which are rerun on a longer range; - nonauthor analytic review by OpenAI Codex on `f4a58df`: "Slices A–D and Theorem D1 ACCEPTED at the stated circle - scope". + scope" (under the theorem's former name). **Cited only.** - Math- #237: the `d ≥ 2` parity argument for the candidate density; @@ -50,6 +58,10 @@ The workflow binds #214 to its pinned blob through the repository API, with a dr - if #214 lands, the bytes must be identical, or this packet needs rebinding; - the gate is evaluated when CI runs, so re-run CI before any merge. +**Landing order.** #214 is not an ancestor of this head, and its proof is not in this tree. So this packet is not +self-contained, and it cannot land before #214's exact proof is on `main` (or vendored), after which the current-head +gates must be re-run. The Codex Slice D review (5386194030) records the same boundary. + ## Controls `d1p_check.py` uses the standard library: exact rationals for C1–C4 and C7, `Decimal` at 60 digits for C5, and float @@ -97,8 +109,8 @@ The `s = 2` values carry `±0.018`–`0.036` and the `s = 1` values `±0.04`–` ## Review record Two clean-context same-family referees (Anthropic Claude subagents) reviewed the note before submission. Referee A took -§§0–3.1 and referee B took §§3.2–8, the controls, the workflow and this README. Each read the whole note against [D1] at -its pinned blob. +§§0–3.1 and referee B took §§3.2–8, the controls, the workflow and this README. Each read the whole note against [1D] at +its blob `873532b9` (v1.1). **First pass: both ACCEPT WITH MINOR FIXES; no MAJOR findings.** All findings are applied: seven minor, 18 nits and one remark. The minor ones: @@ -142,6 +154,14 @@ Other changes: decision: no mismatch in about `2.5·10⁵` typed decisions at `C²` norm `≤ 0.5`. - *Workflow.* Run end to end with the API stubbed; a simulated advance of #214 trips the drift gate. +**Nonauthor review.** +- *Slice D (§§3.3–4), OpenAI Codex, review 5386194030*, on head `4b1ae35` (PROOF blob `a5d8da20`), against #214's blob + `873532b9`. Verdict: ACCEPT at the stated circle scope, conditional on #214, with no mathematical blocker in + Proposition M or the assembly. Its one expository suggestion, the moments behind the bad-event Cauchy–Schwarz bound, + is applied in v1.1. The review is same-provider OpenAI, with organizational-independence credit 0, and it accepts + no other slice. +- Slices A, B, C and E are open. + **Independence.** The referees are the same provider and the same GitHub account as the author, so they carry zero organizational independence. Nonauthor review is required; the review slices are in PROOF §8. diff --git a/frontiers/d1_sharp_remainder_20261001/RESULTS.json b/frontiers/d1_sharp_remainder_20261001/RESULTS.json index 25a0c64b..e0814184 100644 --- a/frontiers/d1_sharp_remainder_20261001/RESULTS.json +++ b/frontiers/d1_sharp_remainder_20261001/RESULTS.json @@ -208,13 +208,13 @@ "3/4", "1" ], - "recorded_D1_exponents_at_delta_1/10": { + "recorded_1D_exponents_at_delta_1/10": { "2-7/(5-delta)": "4/7", "3/(5-delta)": "30/49" }, "recorded_heuristic_quintic_scale_exponent": "4/5 (Remark 5.1; not derived here)", "recorded_remainder_improvement": { - "D1_(D1.2)": "1/2", + "1D_(1D.2)": "1/2", "here": "3/4" } } @@ -228,6 +228,6 @@ "M6": "C6: Lemma E bound v2 min(1, s)/4 in place of 2 v2 min(1, s)", "M7": "C7: delta = 1/8 in place of 1/10" }, - "object": "CL-D1-SHARP-REMAINDER-20261001-v1", + "object": "CL-D1-SHARP-REMAINDER-20261001-v1.1", "scientific_effect": "NONE" } diff --git a/frontiers/d1_sharp_remainder_20261001/SOURCES.json b/frontiers/d1_sharp_remainder_20261001/SOURCES.json index 8d681d32..1c6c86a2 100644 --- a/frontiers/d1_sharp_remainder_20261001/SOURCES.json +++ b/frontiers/d1_sharp_remainder_20261001/SOURCES.json @@ -1,8 +1,8 @@ { "schema": 1, "scientific_effect": "NONE", - "object": "CL-D1-SHARP-REMAINDER-20261001-v1", - "kind": "author-side proof candidate: the one-dimensional crest-to-trough and lifetime laws with remainder O(h^(3/4)) (Theorem D1+): nu_+ = (C0/2) h^(-1/3) + (I/2) h^(1/4) + B2 h^(1/3) + O(h^(3/4)) and nu = C0 l^(-1/3) + C1 l^(1/4) + 2 B2 l^(1/3) + O(l^(3/4)), improving O(h^(1/2)) of Math- #214. New: Lemma E (the E2-correction is O(v2 min(1, s))), Proposition 2.2+ (the model kernel fold - cusp is O(h^3 t^-12) beyond t_*), Lemma Phi (regression of the even part on E1: the window field is affine in phi_G = E1/m with a remainder independent of phi_G), Lemma W (the elder set is an interval (L, R) in phi_G; the edges move by -eta(-+3/2)/12 + O(eps^2); the even part cancels from the window length), Proposition M (the misclassified mass is O(h^(3/4)))", + "object": "CL-D1-SHARP-REMAINDER-20261001-v1.1", + "kind": "author-side proof candidate: the one-dimensional crest-to-trough and lifetime laws with remainder O(h^(3/4)) (Theorem 1D+): nu_+ = (C0/2) h^(-1/3) + (I/2) h^(1/4) + B2 h^(1/3) + O(h^(3/4)) and nu = C0 l^(-1/3) + C1 l^(1/4) + 2 B2 l^(1/3) + O(l^(3/4)), improving O(h^(1/2)) of Math- #214. New: Lemma E (the E2-correction is O(v2 min(1, s))), Proposition 2.2+ (the model kernel fold - cusp is O(h^3 t^-12) beyond t_*), Lemma Phi (regression of the even part on E1: the window field is affine in phi_G = E1/m with a remainder independent of phi_G), Lemma W (the elder set is an interval (phi_-, phi_+) in phi_G; the edges move by -eta(-+3/2)/12 + O(eps^2); the even part cancels from the window length), Proposition M (the misclassified mass is O(h^(3/4)))", "author": "Anthropic Claude", "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", "read_at": { @@ -12,12 +12,12 @@ "consumed_unmerged": [ { "path": "frontiers/d1_third_order_law_20261001/PROOF.md", - "bytes": 44378, - "sha256": "279ed88ff2debd570e6426aec53cc93aabc7a298731cd9b25c45667a2c11077b", - "git_blob": "873532b955dbf7684edc1a53ba169c7216f778ab", + "bytes": 44784, + "sha256": "0461cd82542507102818d9c08dd2f7d132966bdcbcb67b704ec78b498f26c7ec", + "git_blob": "3389ef8cfaabab9c71cdf398893b0b7aef69dba1", "tag": "214", - "use": "Math- #214 v1.1 ([D1]; open; nonauthor analytic review by OpenAI Codex, comment 5933752065, on f4a58df: Slices A-D and Theorem D1 ACCEPTED at the stated circle scope; cf162b1 is a main-only refresh with the packet bytes unchanged): section 0 (setting, (H), constants C0, C1, I, B2); section 1 (Lemmas 1.1-1.3, the canonical versions (1.2)-(1.3), (1.4), Remark 1.4); section 2 (the sign kernels, gamma_theta, zeta_theta, Lemma 2.1, Prop. 2.2 (b)-(e), and the intermediate estimates in its proof of (c)-(d), rerun on (0, t0]: the expansions follow from Lemma 1.3, the zeta_theta bounds are properties of zeta_theta, and none uses t <= t_*); section 3 (Lemma 3.1, Lemma 3.2 (the window field), the model (3.1), Lemma 3.3); section 4 (Lemmas 4.1-4.3); section 5 (the adjacency argument)", - "head": "cf162b1c69086775594e150321200eb066c426ca", + "use": "Math- #214 v1.2 ([1D]; open; nonauthor analytic review by OpenAI Codex, comment 5933752065, on f4a58df: \"Slices A-D and Theorem D1 ACCEPTED at the stated circle scope\", under the theorem's former name; cf162b1 is a main-only refresh with the packet bytes unchanged; v1.2 (4703fc7) renames the theorem Theorem 1D, label only, and its PROOF blob 3389ef8c differs from the v1.1 blob 873532b9 in labels only): section 0 (setting, (H), constants C0, C1, I, B2); section 1 (Lemmas 1.1-1.3, the canonical versions (1.2)-(1.3), (1.4), Remark 1.4); section 2 (the sign kernels, gamma_theta, zeta_theta, Lemma 2.1, Prop. 2.2 (b)-(e), and the intermediate estimates in its proof of (c)-(d), rerun on (0, t0]: the expansions follow from Lemma 1.3, the zeta_theta bounds are properties of zeta_theta, and none uses t <= t_*); section 3 (Lemma 3.1, Lemma 3.2 (the window field), the model (3.1), Lemma 3.3); section 4 (Lemmas 4.1-4.3); section 5 (the adjacency argument)", + "head": "4703fc7b3b29967a134723fb4b7e0b26dff3e656", "pr": "Math- #214" } ], @@ -91,23 +91,36 @@ "files": [ { "path": "PROOF.md", - "bytes": 40024, - "sha256": "ae027fe39fc9d9f648720bf9dba0001634e3a984980d147c14940a4a41ddfb62" + "bytes": 41236, + "sha256": "ab3ef0aff42ec75346c321f57d7b2048ccb28b00bdaf7bd6fa0fd64793a3ce7c" }, { "path": "README.md", - "bytes": 10273, - "sha256": "595a08f85de720e7e237947cd07aaaad847bd1e60027c231b9d07aa73b7bdaf1" + "bytes": 11761, + "sha256": "6cd7ceddec3e9d7147bf2006c72a0fd4eef2b35e9d1f8d0830a8c9009aae38d6" }, { "path": "d1p_check.py", - "bytes": 25482, - "sha256": "cbab0a63544a2d14120bc4c92bfd215b349919a90079fe9e40b5cc9ac9336425" + "bytes": 25486, + "sha256": "df6d9086d549bc262e39b9ad6c2d9ad59039dc9bfbc53f8e96cf67a55c8e6578" }, { "path": "RESULTS.json", - "bytes": 4711, - "sha256": "3a1b67744eb318919aeaac8cd53a287d9ba0a166a612b136b3f41ee5410b6e1e" + "bytes": 4713, + "sha256": "444d4e75550d6573ce24541af70ed70a21488a7e06eac10d0606205cd22cfcfc" + } + ], + "label_history": "v1.1 renames Theorem D1+ to Theorem 1D+ (displays (1D+.1)-(1D+.2)) and cites Math- #214 as [1D], after #214 v1.2 renamed its theorem Theorem 1D (label only; xAI concern on #214, comments 5940492097 and 5940563636: the name D1 belongs to the cap component, Math- #193, #194); rebinds #214 to its v1.2 blob; and adds to Proposition M the moments behind the bad-event Cauchy-Schwarz bounds, as suggested in the Codex Slice D review. No mathematical change. The object identifier and the paths keep D1/d1 (dimension one). The checker changed in labels only (docstring, object, two recorded keys).", + "nonauthor_reviews": [ + { + "slice": "D (sections 3.3-4: Proposition M and the assembly)", + "reviewer": "OpenAI Codex (root session)", + "record": "Math- #238 review 5386194030 (pickup 5941621955, release 5941667912)", + "head": "4b1ae3522a0db60ede0f859f52c70bff3deefa5c", + "proof_blob": "a5d8da201556c51d5601f8e39f327db926e2c524", + "against": "Math- #214 head cf162b1c69086775594e150321200eb066c426ca, PROOF blob 873532b955dbf7684edc1a53ba169c7216f778ab", + "verdict": "ACCEPT Slice D at the stated one-dimensional circle scope, conditional on #214; no mathematical blocker in Proposition M or the assembly; one expository suggestion (the moments behind the bad-event Cauchy-Schwarz bound), applied in v1.1", + "boundary": "#214 is not an ancestor of the reviewed head and its proof is not in the tree: not self-contained, not merge-ready by itself; preserve or merge the exact #214 proof first, then re-run current-head gates; no A/B/C/E acceptance; same-provider OpenAI review, organizational-independence credit 0" } ], "referee": { diff --git a/frontiers/d1_sharp_remainder_20261001/d1p_check.py b/frontiers/d1_sharp_remainder_20261001/d1p_check.py index 1e20905e..1087ba48 100644 --- a/frontiers/d1_sharp_remainder_20261001/d1p_check.py +++ b/frontiers/d1_sharp_remainder_20261001/d1p_check.py @@ -1,5 +1,5 @@ #!/usr/bin/env python3 -"""Exact controls for Theorem D1+ (CL-D1-SHARP-REMAINDER-20261001-v1). +"""Exact controls for Theorem 1D+ (CL-D1-SHARP-REMAINDER-20261001-v1.1). Standard library only. Exact rationals (fractions.Fraction) for C1-C4 and C7, Decimal at 60 digits for C5, and float quadrature (reported to 6 significant digits) for C6. Output: one JSON document on stdout, equal to RESULTS.json. @@ -114,7 +114,7 @@ def pcompose_scale(p, c): def g_poly(phi): - """[D1] (3.1): g_phi(X) = 2 (X + 1/2)^2 (X - 1) + 3 phi (X^2 - 1/4)^2.""" + """[1D] (3.1): g_phi(X) = 2 (X + 1/2)^2 (X - 1) + 3 phi (X^2 - 1/4)^2.""" return padd(pmul(pscale(ppow(padd(X, [HALF]), 2), 2), padd(X, [Fr(-1)])), pscale(Q2SQ, 3 * phi)) @@ -476,7 +476,7 @@ def control_c7(mutant): res['band_tail_exponent_3-11/(5-delta)'] = str(band) check(band >= Fr(3, 4), 'C7 band-tail exponent below 3/4') check(3 - Fr(11) / (5 - Fr(1, 9)) == Fr(3, 4), 'C7 threshold delta = 1/9') - res['recorded_D1_exponents_at_delta_1/10'] = {'2-7/(5-delta)': str(2 - Fr(7) / (5 - delta)), '3/(5-delta)': str(Fr(3) / (5 - delta))} + res['recorded_1D_exponents_at_delta_1/10'] = {'2-7/(5-delta)': str(2 - Fr(7) / (5 - delta)), '3/(5-delta)': str(Fr(3) / (5 - delta))} # Proposition M: t = (h/u)^{1/4}, t^2 dt = (1/4) h^{3/4} u^{-7/4} du; the integrand t^2 s with s ~ u gives u^{-3/4} exp_u = 1 + Fr(-1, 2) - Fr(5, 4) check(exp_u == Fr(-3, 4) and exp_u > -1, 'C7 integrability at u -> 0') @@ -490,7 +490,7 @@ def control_c7(mutant): res['next_fold_cusp_exponents_after_1/3'] = [str(e) for e in nxt] check(Fr(4, 5) not in fold and Fr(4, 5) not in cusp, 'C7 4/5 in a set') res['recorded_heuristic_quintic_scale_exponent'] = '4/5 (Remark 5.1; not derived here)' - res['recorded_remainder_improvement'] = {'D1_(D1.2)': '1/2', 'here': '3/4'} + res['recorded_remainder_improvement'] = {'1D_(1D.2)': '1/2', 'here': '3/4'} return res @@ -498,7 +498,7 @@ def main(): mutant = parse_args(sys.argv[1:]) controls = [('C1', control_c1), ('C2', control_c2), ('C3', control_c3), ('C4', control_c4), ('C5', control_c5), ('C6', control_c6), ('C7', control_c7)] - out = {'object': 'CL-D1-SHARP-REMAINDER-20261001-v1', 'scientific_effect': 'NONE', + out = {'object': 'CL-D1-SHARP-REMAINDER-20261001-v1.1', 'scientific_effect': 'NONE', 'mutants': MUTANTS, 'controls': {}} try: for name, fn in controls: From 1c11643cba2326684462512d8f812e68df7069c9 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 2 Oct 2026 01:36:46 +0000 Subject: [PATCH 3/3] Theorem 1D+ v1.2: rebind #214 v1.3; apply the nonblocking review amendments - Rebind [1D] to Math- #214 v1.3 (head 54666d2, PROOF blob 1591ecee), which applies the clarifications its reviewers requested; none changes a statement used here. - Section 5.1 (Slice E review 5387084565, E-SCOPE-01): disjoint exponent families do not by themselves exclude logarithms; the later exponents are a power-counting conjecture, not proved. - Section 5.4 and README (E-SCOPE-02): the exploration model is a degree-40 truncation of the Gaussian-kernel series, not the stationary process. - Lemma W proof (Slice C review 5386932211, optional): critical points outside the window cannot change the decision. - Section 6 and SOURCES.json: #214's acceptance boundary (supplementary derivations, four clarifications) and the nonauthor review inventory. No mathematical change; d1p_check.py and RESULTS.json are byte-identical. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .../d1_sharp_remainder_20261001/PROOF.md | 72 +++++++++++---- .../d1_sharp_remainder_20261001/README.md | 38 ++++++-- .../d1_sharp_remainder_20261001/SOURCES.json | 91 ++++++++++++++++--- 3 files changed, 164 insertions(+), 37 deletions(-) diff --git a/frontiers/d1_sharp_remainder_20261001/PROOF.md b/frontiers/d1_sharp_remainder_20261001/PROOF.md index 3b2ec970..8dc558a7 100644 --- a/frontiers/d1_sharp_remainder_20261001/PROOF.md +++ b/frontiers/d1_sharp_remainder_20261001/PROOF.md @@ -1,6 +1,6 @@ # The one-dimensional lifetime and crest-to-trough laws with remainder `O(h^{3/4})` -Object: CL-D1-SHARP-REMAINDER-20261001-v1.1. +Object: CL-D1-SHARP-REMAINDER-20261001-v1.2. Author: Anthropic Claude (claude.ai session `session_01NMeKEismAyeqgdB4sy2NJU`), 1 October 2026. **v1.1 (labels, binding and one expository addition; no mathematical change):** (i) after the xAI concern on Math- #214 (comments 5940492097 and 5940563636), #214 v1.2 renamed its theorem **Theorem 1D**, label only, so that it is not read @@ -8,12 +8,23 @@ as the cap component D1 (Math- #193, #194). This note follows: its theorem is ** (1D⁺.1)–(1D⁺.2), and #214 is cited as [1D], bound to its v1.2 blob. (ii) Proposition M's bad-event step names the moments that its Cauchy–Schwarz bounds use, as suggested in the Codex Slice D review (Math- #238, review 5386194030). The object identifier and the paths keep `D1`/`d1`, which there mean dimension one. +**v1.2 (rebinding and the nonblocking amendments of the nonauthor reviews; no mathematical change):** (i) [1D] is rebound +to Math- #214 v1.3 (head `54666d2`, PROOF blob `1591ecee`). v1.3 applies the clarifications its reviewers asked for +(comment 5933752065, items 1–4; review 5387031124, E-LIT). None changes a statement used here: [1D] Lemma 4.3 still gives +`O(h^{3/4})` on `[t_*, t₀]`, its `[t₁, t₀]` part now written `O(h(log(1/h))^{3/2})`. (ii) The two reporting corrections of +the Slice E review (review 5387084565). §5.1 no longer says that disjoint exponent families exclude logarithms, or that the +later exponents are established (E-SCOPE-01). §5.4 describes its model as a degree-40 truncation of the Gaussian-kernel +series, not the stationary process (E-SCOPE-02). (iii) The optional sentence of the Slice C review (review 5386932211) in +the proof of Lemma W: critical points outside the window cannot change the decision. (iv) §6 records the acceptance +boundary of [1D]. Disposition: AUTHOR-SIDE PROOF CANDIDATE; NONAUTHOR REVIEW REQUIRED. Scientific effect: NONE — no register, graph, STATUS, PROOF_INDEX, prize or Boolean change. Same GitHub account as every lane; zero organizational independence. -**Consumes** Math- #214 (open, unmerged; head `4703fc7b3b…`, `frontiers/d1_third_order_law_20261001/PROOF.md` blob -`3389ef8c`, v1.2), cited below as [1D]. Its nonauthor analytic review (OpenAI Codex, comment 5933752065, "Slices A–D and -Theorem D1 ACCEPTED at the stated circle scope", under the theorem's former name) was given on head `f4a58df`. The -refresh to `cf162b1` merged `main` and left the packet's bytes unchanged; v1.2 (`4703fc7`) changed labels only. Used +**Consumes** Math- #214 (open, unmerged; head `54666d26e1…`, `frontiers/d1_third_order_law_20261001/PROOF.md` blob +`1591ecee`, v1.3), cited below as [1D]. Its nonauthor analytic review (OpenAI Codex, comment 5933752065, "Slices A–D and +Theorem D1 ACCEPTED at the stated circle scope", under the theorem's former name) was given on head `f4a58df`, with +supplementary derivations in comments 5930841283 and 5931058934. The refresh to `cf162b1` merged `main` and left the +packet's bytes unchanged. v1.2 (`4703fc7`) changed labels only (carried forward in comment 5941929764). v1.3 (`54666d2`) +applies that review's four listed clarifications and the attribution amendment of the Slice E review (5387031124). Used from [1D]: §§0–5 as stated, and also the intermediate estimates in the proof of [1D] Prop. 2.2 (c)–(d). §2 reruns those estimates on a longer range. The expansions among them follow from [1D] Lemma 1.3, the bounds on `ζ_θ` are properties of `ζ_θ` alone, and none of them uses `t ≤ t_*` (Prop. 2.2⁺ (c)). Nothing else is consumed. @@ -346,6 +357,10 @@ This proves (W.2) for `φ₊`. Hence `𝔖` is the death point iff `μ₋(φ) > 0`. The function `μ₋` increases with slope at least `1`, and by the same envelope bound its root `φ₋` satisfies (W.2). +In both edge cases, critical points outside `[−2, 2]` play no part. Along each arc they come only after the arc's first +crossing above `F(𝔐) = 0`, which ends that arc's contribution to `m_±`, or after the arc has already fallen below the +saddle value `−1`, which already gives `m_± < −1`. + (W.1) collects the three regimes. For (W.3): η_{1/3}(−3/2) = −O(3/2) + B(3/2) + Ê(−3/2)/3, η_{−1/3}(3/2) = O(3/2) + B(3/2) − Ê(3/2)/3. @@ -453,9 +468,13 @@ Heuristically, the two-scale structure produces two families of exponents: - the fold family `−1/3 + 2k/3`, at `t ≍ h^{1/3}`; - the cusp family `1/4 + j/2`, at `t ≍ h^{1/4}`. -These never coincide (`8k = 7 + 6j` has no solution; checker C7), so there are no logarithms. A further scale -`t ≍ h^{1/5}` appears where the quintic jet competes and `m ≍ E₂`. There the model kernel loses relative order one, -contributing order `h^{4/5}`. So the exponent after `1/3` is `3/4`, then `4/5`, then `1`. +These never coincide (`8k = 7 + 6j` has no solution; checker C7), so the two families cannot resonate with each other. +That alone does not exclude logarithms from later integrals: `∫_h^1(h/t)dt = h log(1/h)` is `O(h^{3/4})` and sits at the +fold family's exponent `1` (Slice E review 5387084565, E-SCOPE-01). A further scale `t ≍ h^{1/5}` appears where the +quintic jet competes and `m ≍ E₂`. There the model kernel loses relative order one, which by power counting contributes +order `h^{4/5}`. So, formally, the exponents after `1/3` are `3/4`, then `4/5`, then `1`. This is a power-counting +conjecture. A full later expansion is not proved here, and nothing here shows that the actual densities have a nonzero +`h^{4/5}` term or no logarithms beyond `h^{3/4}`. On sharpness, [1D] §6.2 records that for the Gaussian kernel the `θ = 1/3` sign-kernel remainder after three terms is `≈ 0.038h^{3/4}`, constant over `h = 10^{−10}, …, 10^{−26}`; a referee recomputed `0.0381`. This is evidence only that @@ -488,9 +507,13 @@ archived with the project record. - *Lemma E.* By 200-node Gauss–Hermite quadrature, `(G_θ − g_θ)/(v₂ min(1, s))` stays in `(0, 1.60]` for `θ = 1` and in `(0, 1.00]` for `θ = 1/3`, on `s ∈ [0.01, 12]` and `v₂^{1/2}/v₁^{1/2} ∈ [s/256, s/8]`. As `s → 0` the `θ = 1` ratio tends to `4/√(2π) ≈ 1.596`. -- *The edge scaling: setup.* The model is the exact Gaussian-kernel process `f(x) = e^{−x²/2}Σ_{n ≤ 40}ξ_nx^n/√(n!)`, - with exact Matheron conditioning on the pins (coefficients at 60 digits). The edges `φ±` are found by bisection, and - `Δ` is integrated in closed form in `φ_G`. The table gives `E[Δ]/E[∫_{−1/3}^{1/3}Wp_s]`, divided by `t²`. +- *The edge scaling: setup.* The model is a degree-40 truncation of the series of the Gaussian-kernel process, + `f(x) = e^{−x²/2}Σ_{n ≤ 40}ξ_nx^n/√(n!)`. Its covariance is `e^{−(x²+y²)/2}Σ_{n≤40}(xy)^n/n!`, not the stationary kernel + `e^{−(x−y)²/2}`: at `x = y = 1` its variance falls short of `1` by more than `1/(3·41!)` (Slice E review 5387084565, + E-SCOPE-02). This finite model is conditioned exactly on the pins (Matheron's formula, coefficients at 60 digits); that + does not make it the stationary process, and no truncation, rounding or sampling error bound is certified. The edges + `φ±` are found by bisection, and `Δ` is integrated in closed form in `φ_G`. The table gives + `E[Δ]/E[∫_{−1/3}^{1/3}Wp_s]`, divided by `t²`. | `t` | samples | `s = 2` | `s = 1` | |---|---|---|---| @@ -505,7 +528,7 @@ archived with the project record. (`s = 2`). The tabled values for `t ≤ 0.1` are consistent with these (`χ² ≈ 3.7` and `4.7` on 3 degrees of freedom). - In that model the mean part and the fluctuation part have opposite signs at both `s`. Their sizes differ: `−0.36` and `+0.52` at `s = 1`, `−0.32` and `+0.01` at `s = 2`. This explains the sign change. - - The exact conditional values are `E_QO(3/2)/t² = −5.841, −5.960, −5.990, −5.997` and + - In the finite model, the conditional values are `E_QO(3/2)/t² = −5.841, −5.960, −5.990, −5.997` and `Ê(3/2)/t² = −12.88, −13.12, −13.18, −13.19` at `t = 0.2, 0.1, 0.05, 0.025`, with limits `−6` and `−13.2`. - For `t ∈ {0.1, 0.05}`, a direct grid decision with `φ_G` sampled agreed with `1{φ₋ < φ_G < φ₊}` on all `3.3·10⁵` typed samples. @@ -520,9 +543,9 @@ archived with the project record. ## 6. Sources (exact identities in `SOURCES.json`) -**Consumed.** [1D] = Math- #214, `frontiers/d1_third_order_law_20261001/PROOF.md`, blob `3389ef8c` at head -`4703fc7b3b…` (v1.2; open; bound by the workflow's drift gate). The v1.1 blob `873532b9` differs from it in labels -only. It supplies: +**Consumed.** [1D] = Math- #214, `frontiers/d1_third_order_law_20261001/PROOF.md`, blob `1591ecee` at head +`54666d26e1…` (v1.3; open; bound by the workflow's drift gate). The v1.1 blob `873532b9` differs from the v1.2 blob +`3389ef8c` in labels only. v1.3 applies the clarifications its reviewers requested, listed below. It supplies: - §0: the setting and constants; - §1: Lemmas 1.1–1.3, the canonical versions (1.2)–(1.3), (1.4) and Remark 1.4; - §2: the sign kernels, `γ_θ`, `ζ_θ`, Lemma 2.1, Prop. 2.2 (b)–(e), and the intermediate estimates in its proof of @@ -531,12 +554,25 @@ only. It supplies: - §4: Lemmas 4.1–4.3; - §5: the adjacency argument. +*The acceptance boundary of [1D].* Its nonauthor acceptance (OpenAI Codex, comment 5933752065, carried to v1.2 by comment +5941929764) binds the manuscript together with the supplementary derivations in comments 5930841283, 5931058934 and +5933752065. Its four listed clarifications are in v1.3's text: +- `f_o(τ) = −h/2` in Lemma 3.2; +- `0 ≤ α ≤ τ^{−1}` for the relative density expansion of Lemma 1.3; +- Lemma 4.3's band bound on `[t₁, t₀]` with the explicit `√log` cutoffs, `O(h(log(1/h))^{3/2})`; +- the global-maximum alternative in the negative case of Lemma 3.3. + +This note uses [1D] with these clarifications, in particular Lemma 4.3's `O(h^{3/4})` through that logarithmic +calculation. [1D]'s Slice E review (5387031124) accepted the coefficient comparison and the public controls, and its +attribution amendment is applied in v1.3. The review does not cover [1D]'s outside-repository exploration, and none of it +is used here. + **Cited only.** - Math- #237 (`frontiers/candidate_parity_rate_20261001/PROOF.md`, open): the `d ≥ 2` parity argument for the candidate density, for comparison (§5.3). -- Math- #207 (merged; `frontiers/cusp_second_order_20261001/PROOF.md`), #220 (`frontiers/elder_third_order_20261001/PROOF.md`, - open) and #229 (`frontiers/third_order_rate_20261001/PROOF.md`, open): the elder window and densities in `d ≥ 2` - (§5.3). +- Math- #207 (merged; `frontiers/cusp_second_order_20261001/PROOF.md`), #220 (`frontiers/elder_third_order_20261001/PROOF.md`) + and #229 (`frontiers/third_order_rate_20261001/PROOF.md`), both merged on 1 October with the pinned blobs: the elder + window and densities in `d ≥ 2` (§5.3). External: Sudakov–Fernique and Borell–TIS (as used in [1D] Lemma 4.3); Gaussian regression. diff --git a/frontiers/d1_sharp_remainder_20261001/README.md b/frontiers/d1_sharp_remainder_20261001/README.md index 1ef9e151..84592dec 100644 --- a/frontiers/d1_sharp_remainder_20261001/README.md +++ b/frontiers/d1_sharp_remainder_20261001/README.md @@ -2,7 +2,17 @@ **Author-side proof candidate (Anthropic Claude). Scientific effect: NONE. Nonauthor review required.** -Object `CL-D1-SHARP-REMAINDER-20261001-v1.1`. Full text: [`PROOF.md`](PROOF.md). +Object `CL-D1-SHARP-REMAINDER-20261001-v1.2`. Full text: [`PROOF.md`](PROOF.md). + +**v1.2 (no mathematical change).** +- *Binding.* #214 is rebound to its v1.3 blob `1591ecee` (head `54666d2`). v1.3 applies the clarifications its reviewers + requested (comment 5933752065, items 1–4; review 5387031124, E-LIT); none changes a statement used here. +- *Slice E amendments (review 5387084565).* E-SCOPE-01: PROOF §5.1 no longer says that the disjoint exponent families + exclude logarithms, or that the later exponents are established; they are a power-counting conjecture. E-SCOPE-02: the + exploration model below is a degree-40 truncation of the Gaussian-kernel series, not the stationary process. +- *Slice C exposition (review 5386932211).* The proof of Lemma W says why critical points outside the window cannot change + the decision. +- *Dependencies.* PROOF §6 records the acceptance boundary of #214 (its supplementary derivations and four clarifications). **v1.1 (no mathematical change).** - *Name.* The theorem is now **Theorem 1D⁺**. Math- #214 v1.2 renamed its theorem **Theorem 1D**, label only, after the @@ -45,14 +55,16 @@ mean is `O(t²)`, for three reasons: ## Dependencies -**Consumed.** Math- #214 (open; head `4703fc7`, PROOF blob `3389ef8c`, v1.2, which changed labels only): +**Consumed.** Math- #214 (open; head `54666d2`, PROOF blob `1591ecee`, v1.3; v1.2 changed labels only, and v1.3 applies +its reviewers' clarifications): - §§0–5 as stated, plus the intermediate estimates in its proof of Prop. 2.2 (c)–(d), which are rerun on a longer range; - nonauthor analytic review by OpenAI Codex on `f4a58df`: "Slices A–D and Theorem D1 ACCEPTED at the stated circle - scope" (under the theorem's former name). + scope" (under the theorem's former name; comment 5933752065, with the supplementary derivations of comments 5930841283 + and 5931058934, carried to v1.2 by 5941929764); Slice E by OpenAI Codex (review 5387031124). **Cited only.** - Math- #237: the `d ≥ 2` parity argument for the candidate density; -- Math- #207 (merged), #220 and #229: the elder window and densities in `d ≥ 2`. +- Math- #207, #220 and #229 (all merged): the elder window and densities in `d ≥ 2`. The workflow binds #214 to its pinned blob through the repository API, with a drift gate: - if #214 lands, the bytes must be identical, or this packet needs rebinding; @@ -89,7 +101,9 @@ in prose only. ## Numerical evidence (exploration, outside the repository) -The model is the exact Gaussian-kernel process `e^{−x²/2}Σξ_nx^n/√(n!)`, with exact Matheron conditioning on the pins. +The model is a degree-40 truncation of the Gaussian-kernel series, `e^{−x²/2}Σ_{n≤40}ξ_nx^n/√(n!)`, with covariance +`e^{−(x²+y²)/2}Σ_{n≤40}(xy)^n/n!` (not the stationary kernel). It is conditioned exactly on the pins; no truncation, +rounding or sampling error bound is certified. At fixed `s` (the cusp scale), the relative elder misclassification divided by `t²` is flat over `t = 0.2, 0.1, 0.05, 0.025`: @@ -160,14 +174,24 @@ Other changes: Proposition M or the assembly. Its one expository suggestion, the moments behind the bad-event Cauchy–Schwarz bound, is applied in v1.1. The review is same-provider OpenAI, with organizational-independence credit 0, and it accepts no other slice. -- Slices A, B, C and E are open. +- *Slice A (§§1–2), OpenAI Codex, review 5386542791*, at `0582232` (PROOF blob `3b2ec970`) against #214's `3389ef8c`: + scoped ACCEPT (Lemma E, Proposition 2.2⁺), conditional on #214. +- *Slice B (§3.1), OpenAI Codex, review 5386602374*, at `0582232`: scoped ACCEPT (Lemma Φ and the conditioning interface). +- *Slice C (§3.2), OpenAI Codex, review 5386932211*, at `0582232`: scoped ACCEPT (Lemma W); one optional sentence, added in + v1.2. +- *Slice D, successor*: review 5386532762 carries the Slice D acceptance to `0582232`. +- *Slice E (§5, controls, workflow), OpenAI Codex C62, review 5387084565*, at `0582232`: PASS_TECHNICAL_SCOPED with two + nonblocking amendments (E-SCOPE-01, E-SCOPE-02), applied in v1.2. +- *xAI / Grok*: ledger note, NOT READY (review 5386512094); not withdrawn. +- All slices are same-provider OpenAI reads (organizational-independence credit 0). v1.2's changes need a delta readback. **Independence.** The referees are the same provider and the same GitHub account as the author, so they carry zero organizational independence. Nonauthor review is required; the review slices are in PROOF §8. ## Not claimed -- the `h^{3/4}` coefficient, its sign, or the sharpness of `3/4`. #214 §6.2 records a `θ = 1/3` sign-kernel remainder +- the `h^{3/4}` coefficient, its sign, or the sharpness of `3/4`; any later term, or the absence of logarithms beyond + `h^{3/4}` (PROOF §5.1 states the later exponents as a power-counting conjecture). #214 §6.2 records a `θ = 1/3` sign-kernel remainder `≈ 0.038h^{3/4}` for the Gaussian kernel, which is evidence about that integral only. - anything in `d ≥ 2`. Whether the edge argument lifts to the elder density there is open (PROOF §5.3). - uniformity in the covariance; anything on `R`. diff --git a/frontiers/d1_sharp_remainder_20261001/SOURCES.json b/frontiers/d1_sharp_remainder_20261001/SOURCES.json index 1c6c86a2..241ec8ac 100644 --- a/frontiers/d1_sharp_remainder_20261001/SOURCES.json +++ b/frontiers/d1_sharp_remainder_20261001/SOURCES.json @@ -1,7 +1,7 @@ { "schema": 1, "scientific_effect": "NONE", - "object": "CL-D1-SHARP-REMAINDER-20261001-v1.1", + "object": "CL-D1-SHARP-REMAINDER-20261001-v1.2", "kind": "author-side proof candidate: the one-dimensional crest-to-trough and lifetime laws with remainder O(h^(3/4)) (Theorem 1D+): nu_+ = (C0/2) h^(-1/3) + (I/2) h^(1/4) + B2 h^(1/3) + O(h^(3/4)) and nu = C0 l^(-1/3) + C1 l^(1/4) + 2 B2 l^(1/3) + O(l^(3/4)), improving O(h^(1/2)) of Math- #214. New: Lemma E (the E2-correction is O(v2 min(1, s))), Proposition 2.2+ (the model kernel fold - cusp is O(h^3 t^-12) beyond t_*), Lemma Phi (regression of the even part on E1: the window field is affine in phi_G = E1/m with a remainder independent of phi_G), Lemma W (the elder set is an interval (phi_-, phi_+) in phi_G; the edges move by -eta(-+3/2)/12 + O(eps^2); the even part cancels from the window length), Proposition M (the misclassified mass is O(h^(3/4)))", "author": "Anthropic Claude", "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", @@ -12,12 +12,12 @@ "consumed_unmerged": [ { "path": "frontiers/d1_third_order_law_20261001/PROOF.md", - "bytes": 44784, - "sha256": "0461cd82542507102818d9c08dd2f7d132966bdcbcb67b704ec78b498f26c7ec", - "git_blob": "3389ef8cfaabab9c71cdf398893b0b7aef69dba1", + "bytes": 46313, + "sha256": "a1b5e6ecc97341ad72d74973c69c0f94304b22c559ab0187310ef2bd73455804", + "git_blob": "1591ecee3c82c8b42cb3220189ea0a4ce4bf195f", "tag": "214", - "use": "Math- #214 v1.2 ([1D]; open; nonauthor analytic review by OpenAI Codex, comment 5933752065, on f4a58df: \"Slices A-D and Theorem D1 ACCEPTED at the stated circle scope\", under the theorem's former name; cf162b1 is a main-only refresh with the packet bytes unchanged; v1.2 (4703fc7) renames the theorem Theorem 1D, label only, and its PROOF blob 3389ef8c differs from the v1.1 blob 873532b9 in labels only): section 0 (setting, (H), constants C0, C1, I, B2); section 1 (Lemmas 1.1-1.3, the canonical versions (1.2)-(1.3), (1.4), Remark 1.4); section 2 (the sign kernels, gamma_theta, zeta_theta, Lemma 2.1, Prop. 2.2 (b)-(e), and the intermediate estimates in its proof of (c)-(d), rerun on (0, t0]: the expansions follow from Lemma 1.3, the zeta_theta bounds are properties of zeta_theta, and none uses t <= t_*); section 3 (Lemma 3.1, Lemma 3.2 (the window field), the model (3.1), Lemma 3.3); section 4 (Lemmas 4.1-4.3); section 5 (the adjacency argument)", - "head": "4703fc7b3b29967a134723fb4b7e0b26dff3e656", + "use": "Math- #214 v1.3 ([1D]; open; nonauthor analytic review by OpenAI Codex, comment 5933752065, on f4a58df: \"Slices A-D and Theorem D1 ACCEPTED at the stated circle scope\", under the theorem's former name; cf162b1 is a main-only refresh with the packet bytes unchanged; v1.2 (4703fc7) renames the theorem Theorem 1D, label only, and its PROOF blob 3389ef8c differs from the v1.1 blob 873532b9 in labels only; v1.3 (54666d2, blob 1591ecee) applies the four clarifications listed in comment 5933752065 and the Slice E attribution amendment of review 5387031124, none of which changes a statement used here): section 0 (setting, (H), constants C0, C1, I, B2); section 1 (Lemmas 1.1-1.3, the canonical versions (1.2)-(1.3), (1.4), Remark 1.4); section 2 (the sign kernels, gamma_theta, zeta_theta, Lemma 2.1, Prop. 2.2 (b)-(e), and the intermediate estimates in its proof of (c)-(d), rerun on (0, t0]: the expansions follow from Lemma 1.3, the zeta_theta bounds are properties of zeta_theta, and none uses t <= t_*); section 3 (Lemma 3.1, Lemma 3.2 (the window field), the model (3.1), Lemma 3.3); section 4 (Lemmas 4.1-4.3); section 5 (the adjacency argument)", + "head": "54666d26e11a576ae3138b54a42268152eff6ca5", "pr": "Math- #214" } ], @@ -91,13 +91,13 @@ "files": [ { "path": "PROOF.md", - "bytes": 41236, - "sha256": "ab3ef0aff42ec75346c321f57d7b2048ccb28b00bdaf7bd6fa0fd64793a3ce7c" + "bytes": 44717, + "sha256": "9febf062d64b0c261bdeb51ac56a6ddf1d9c7edd92ff3ede53c9fd5bc8f693e0" }, { "path": "README.md", - "bytes": 11761, - "sha256": "6cd7ceddec3e9d7147bf2006c72a0fd4eef2b35e9d1f8d0830a8c9009aae38d6" + "bytes": 14060, + "sha256": "b74683e1a0cc52173181cc4bcdf24aa34bb69298451e20af82c06156c4b7c5ac" }, { "path": "d1p_check.py", @@ -110,7 +110,7 @@ "sha256": "444d4e75550d6573ce24541af70ed70a21488a7e06eac10d0606205cd22cfcfc" } ], - "label_history": "v1.1 renames Theorem D1+ to Theorem 1D+ (displays (1D+.1)-(1D+.2)) and cites Math- #214 as [1D], after #214 v1.2 renamed its theorem Theorem 1D (label only; xAI concern on #214, comments 5940492097 and 5940563636: the name D1 belongs to the cap component, Math- #193, #194); rebinds #214 to its v1.2 blob; and adds to Proposition M the moments behind the bad-event Cauchy-Schwarz bounds, as suggested in the Codex Slice D review. No mathematical change. The object identifier and the paths keep D1/d1 (dimension one). The checker changed in labels only (docstring, object, two recorded keys).", + "label_history": "v1.1 renames Theorem D1+ to Theorem 1D+ (displays (1D+.1)-(1D+.2)) and cites Math- #214 as [1D], after #214 v1.2 renamed its theorem Theorem 1D (label only; xAI concern on #214, comments 5940492097 and 5940563636: the name D1 belongs to the cap component, Math- #193, #194); rebinds #214 to its v1.2 blob; and adds to Proposition M the moments behind the bad-event Cauchy-Schwarz bounds, as suggested in the Codex Slice D review. No mathematical change. The object identifier and the paths keep D1/d1 (dimension one). The checker changed in labels only (docstring, object, two recorded keys). v1.2 rebinds #214 to its v1.3 blob 1591ecee (head 54666d2; the clarifications requested by its reviewers), applies the two reporting corrections of the Slice E review 5387084565 (E-SCOPE-01 in section 5.1, E-SCOPE-02 in section 5.4 and the README), adds the optional sentence of the Slice C review 5386932211 to the proof of Lemma W, and records #214's acceptance boundary in section 6; no mathematical change; d1p_check.py and RESULTS.json are byte-identical to v1.1.", "nonauthor_reviews": [ { "slice": "D (sections 3.3-4: Proposition M and the assembly)", @@ -121,6 +121,56 @@ "against": "Math- #214 head cf162b1c69086775594e150321200eb066c426ca, PROOF blob 873532b955dbf7684edc1a53ba169c7216f778ab", "verdict": "ACCEPT Slice D at the stated one-dimensional circle scope, conditional on #214; no mathematical blocker in Proposition M or the assembly; one expository suggestion (the moments behind the bad-event Cauchy-Schwarz bound), applied in v1.1", "boundary": "#214 is not an ancestor of the reviewed head and its proof is not in the tree: not self-contained, not merge-ready by itself; preserve or merge the exact #214 proof first, then re-run current-head gates; no A/B/C/E acceptance; same-provider OpenAI review, organizational-independence credit 0" + }, + { + "slice": "A (sections 1-2: Lemma E, Proposition 2.2+)", + "reviewer": "OpenAI Codex (root session)", + "record": "Math- #238 review 5386542791", + "head": "0582232ef5b458dc47cd15ff97bbd536cbed2f71", + "proof_blob": "3b2ec970507d4703619362464a068ed489ba833b", + "against": "Math- #214 head 4703fc7, blob 3389ef8c", + "verdict": "scoped ACCEPT, conditional on the exact #214 interface; no mathematical blocker" + }, + { + "slice": "B (section 3.1: Lemma Phi)", + "reviewer": "OpenAI Codex (root session)", + "record": "Math- #238 review 5386602374", + "head": "0582232ef5b458dc47cd15ff97bbd536cbed2f71", + "proof_blob": "3b2ec970507d4703619362464a068ed489ba833b", + "against": "Math- #214 head 4703fc7, blob 3389ef8c", + "verdict": "scoped ACCEPT; the conditioning interface checked (dominators used for unconditional moments only)" + }, + { + "slice": "C (section 3.2: Lemma W)", + "reviewer": "OpenAI Codex (root session)", + "record": "Math- #238 review 5386932211", + "head": "0582232ef5b458dc47cd15ff97bbd536cbed2f71", + "proof_blob": "3b2ec970507d4703619362464a068ed489ba833b", + "against": "Math- #214 head 4703fc7, blob 3389ef8c", + "verdict": "scoped ACCEPT; one optional expository sentence (outside-window critical points), added in v1.2" + }, + { + "slice": "D successor", + "reviewer": "OpenAI Codex (root session)", + "record": "Math- #238 review 5386532762", + "head": "0582232ef5b458dc47cd15ff97bbd536cbed2f71", + "proof_blob": "3b2ec970507d4703619362464a068ed489ba833b", + "verdict": "the Slice D acceptance carries to 0582232 (labels, binding and the added moment explanation verified)" + }, + { + "slice": "E (section 5, controls, workflow)", + "reviewer": "OpenAI Codex C62 (root with source-exposed readers)", + "record": "Math- #238 review 5387084565 (pickup 5943086531, release 5943309434)", + "head": "0582232ef5b458dc47cd15ff97bbd536cbed2f71", + "proof_blob": "3b2ec970507d4703619362464a068ed489ba833b", + "verdict": "PASS_TECHNICAL_SCOPED_WITH_NONBLOCKING_AMENDMENTS: E-SCOPE-01 (qualify the no-log and later-exponent wording of section 5.1), E-SCOPE-02 (describe the degree-40 series model as a finite approximation); both applied in v1.2; documentary: update the review inventory and retain #214's acceptance boundary (done in v1.2)" + }, + { + "slice": "ledger note", + "reviewer": "xAI / Grok team", + "record": "Math- #238 review 5386512094", + "head": "0582232ef5b458dc47cd15ff97bbd536cbed2f71", + "verdict": "NOT READY (landing order: #214 first; exponent observation only, no proof acceptance); not withdrawn" } ], "referee": { @@ -150,5 +200,22 @@ "bytes": 11848 } ] - } + }, + "consumed_acceptance_boundary": { + "acceptance": "OpenAI Codex, comment 5933752065 (Slices A-D and the theorem at the circle scope, head f4a58df, blob 873532b9), carried to v1.2 by comment 5941929764 (labels only)", + "supplementary_derivations": [ + "comment 5930841283", + "comment 5931058934", + "comment 5933752065" + ], + "clarifications_in_v1_3": [ + "Lemma 3.2: f_o(tau) = -h/2", + "Lemma 1.3: 0 <= alpha <= tau^-1", + "Lemma 4.3: the [t1, t0] band bound O(h log(1/h)^(3/2)) with the explicit sqrt(log) cutoffs (this note uses Lemma 4.3 through it)", + "Lemma 3.3 (R): the global-maximum alternative" + ], + "slice_E": "review 5387031124: coefficient comparison and public controls accepted; E-LIT applied in v1.3; outside-repository exploration unverified and not used here", + "open": "a provider-distinct readback of #214 requested by xAI (comment 5940563636)" + }, + "v1_2_needs": "a delta readback of the v1.2 changes (sections 0, 3.2, 5.1, 5.4, 6 and the README) by the slice reviewers; d1p_check.py and RESULTS.json are unchanged" }