diff --git a/.github/workflows/d1-line.yml b/.github/workflows/d1-line.yml new file mode 100644 index 000000000..6fcfc541e --- /dev/null +++ b/.github/workflows/d1-line.yml @@ -0,0 +1,116 @@ +name: D1 line transfer exact controls + +'on': + pull_request: + paths: + - 'frontiers/d1_line_20261004/**' + - '.github/workflows/d1-line.yml' + # bound merged sources (consumed and cited_only in SOURCES.json) + - 'frontiers/d1_third_order_law_20261001/PROOF.md' + - 'frontiers/d1_sharp_remainder_20261001/PROOF.md' + - 'imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md' + - 'reviews/d1_section9_borel_repair_20260925/REPAIR.md' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-controls: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + 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_line_20261004').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_bytes(entry): + # a source read from the checkout must be a regular file whose tree blob is the recorded one + out = subprocess.run(['git', 'ls-tree', '-z', 'HEAD', '--', entry['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() != entry['path']: + raise ValueError('unexpected tree entry for ' + entry['path']) + mode, kind, sha = meta.decode().split() + 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((mode, kind, sha)) + '): ' + 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']) + if manifest.get('consumed_unmerged'): + raise ValueError('this packet declares no unmerged consumed dependency') + # the cited unmerged source (comparison only) is bound to its 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 blob bytes must have the recorded sha256 + 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) + for entry in manifest.get('cited_unmerged', []): + 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' or not same(base64.b64decode(blob['content']), entry): + raise ValueError('cited_unmerged source differs from its pinned blob: ' + entry['path']) + print(json.dumps({'cited_unmerged_bound': entry['path'], 'git_blob': entry['git_blob'], 'head': entry['head']})) + script = str(root / 'line_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'], ['--unknown']): + rc = subprocess.run([sys.executable, *flags, script, *bad], capture_output=True, timeout=600).returncode + if rc != 2: + raise RuntimeError('bad 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_line_20261004/PROOF.md b/frontiers/d1_line_20261004/PROOF.md new file mode 100644 index 000000000..19299a686 --- /dev/null +++ b/frontiers/d1_line_20261004/PROOF.md @@ -0,0 +1,503 @@ +# The one-dimensional lifetime and crest-to-trough laws on the line: Theorems 1D and 1D⁺ for stationary processes on `ℝ` + +Object: CL-D1-LINE-20261004-v1.1. +Author: Anthropic Claude (claude.ai session `session_01NMeKEismAyeqgdB4sy2NJU`), 4 October 2026. Dylan Roy — delegated AI +work. +**v1.1 (before any nonauthor pickup; v1 was `f34ffd7`).** The hypothesis loses v1's (R3a), the decay +`|ρ^{(j)}(x)| ≤ C(1 + |x|)^{−1}` for `j ≤ 2`. (H_ℝ) is now purely spectral: (R1)–(R3) below. Lemma 4.3_ℝ no longer makes +the cross-covariances between the samples and the pins small. Conditioning on the three pin observations lowers at most +three eigenvalues of the samples' covariance (interlacing), and the density bound loses three powers of `ε`, which the +growing number of samples absorbs. The decay needed elsewhere, `ρ, ρ', ρ'' → 0`, follows from (R1) by the Riemann–Lebesgue +lemma (Lemma 4.1_ℝ). Lemma F_ℝ now uses at least `23` cells; its rate, and the theorem, are unchanged. +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. +Before submission, two clean-context same-family referees (Anthropic Claude subagents) read the draft: slices A–B and +C–D of §9. Both returned ACCEPT WITH MINOR FIXES, with no major finding. Their fixes are applied here, and a delta check +found them fixed (`SOURCES.json`, `referee`). v1.1's new material came after that pass: Lemma 4.1_ℝ, the interlacing +form of Lemma 4.3_ℝ, and Lemma F_ℝ with `23` cells. A second delta check by the same referees returned: +- slice C ACCEPT and slice B ACCEPT; +- slices A and D ACCEPT WITH MINOR FIXES, for one sentence of §0 and the packaging. Both are applied. + +**What is new.** Math- #214 proves Theorem 1D on the circle `R/LZ`, and Math- #238 sharpens it to Theorem 1D⁺ (remainder +`O(h^{3/4})`). #214 §6.4 notes that the near-pair analysis is local, and that on the line only the far bound of its +Lemma 4.3 needs a decorrelation hypothesis. This note supplies that bound, and with it the line versions of both theorems, +under the hypothesis (H_ℝ) of §0. The new ingredient is Lemma F_ℝ (§4): a pair that is *banded* (its process stays between +the two endpoint values) over a long interval is unlikely, with an exponential rate in the length. The proof uses three +standard tools: +- Ingham's inequality, for a uniform lower bound on the conditional covariance of many well-separated derivative samples; +- Landau's inequality, on cells of fixed length; +- Gaussian concentration, for the number of cells where the second derivative is large. + +The constants are those of #214 and #238. For the covariance `e^{−x²/2}` on `ℝ`, the crest-to-trough density per crest is +the classical object of Rice (1944/45), Cartwright–Longuet-Higgins (1956) and Lindgren (2019). It is +`f_H(h) = 0.19971814h^{−1/3} − 0.27165891h^{1/4} + 0.41725471h^{1/3} + O(h^{3/4})`. + +**Dependencies (consumed; merged).** +- Math- #214, `frontiers/d1_third_order_law_20261001/PROOF.md`, blob `1591ecee`, merged at `e4ca2b3` ([1D]). Used: §0, the + objects and constants; §1, the pair coordinates, the pinned law `Q = Q_{t,α}`, (1.2)–(1.4), Lemma 1.2, Lemma 1.3 and + Remark 1.4; §2, Proposition 2.2; §3, Lemmas 3.1–3.3 and Corollary 3.4; §4, Lemma 4.1, Lemma 4.2 (near form), and the + part of Lemma 4.3 on `[t_*, t₀]`; §5. +- Math- #238, `frontiers/d1_sharp_remainder_20261001/PROOF.md`, blob `8dc558a7`, merged at `8404169` ([1D⁺]). Used: §0, and + §§1–4 (Lemma E, Proposition 2.2⁺, Lemmas Φ and W, Proposition M, and the assembly). + +**External (standard).** +- Ingham's inequality: A. E. Ingham, *Some trigonometrical inequalities with applications to the theory of series*, + Math. Z. 41 (1936) 367–379. See also R. M. Young, *An Introduction to Nonharmonic Fourier Series*, rev. ed. (2001), Ch. 4, + §1. +- Gaussian concentration for functions that are Lipschitz along the Cameron–Martin space: Borell, Tsirelson–Ibragimov– + Sudakov. See V. I. Bogachev, *Gaussian Measures* (1998), Theorem 4.5.7, or M. Ledoux, *The Concentration of Measure + Phenomenon* (2001), §2.1. +- Borell–TIS and Sudakov–Fernique, as used in [1D] Lemma 4.3. +- Bulinskaya's lemma, as in [1D] Lemma 1.1. +- The two-point Kac–Rice formula with Borel marks, as in [1D] §1. +- Maruyama's theorem: a stationary Gaussian sequence whose covariance tends to `0` is mixing. + +## 0. Statement + +**Setting.** `f` is a centered stationary Gaussian process on `ℝ` with covariance `ρ(x) = E f(0)f(x) = ∫_ℝ e^{iωx}s(ω)dω`, +where the spectral measure has a density `s ≥ 0`. Write `λ_{2j} := (−1)^jρ^{(2j)}(0) = ∫ω^{2j}s(ω)dω`. + +> **(H_ℝ)** +> - (R1) `∫(1 + |ω|)^n s(ω)dω < ∞` for every `n`. +> - (R2) There are `0 < ω₁ < ω₂` and `s₀ > 0` with `s ≥ s₀` almost everywhere on `[ω₁, ω₂]`. +> - (R3) `S₆ := ess sup_ω (1 + ω⁶)s(ω) < ∞`. + +Example: `ρ(x) = e^{−x²/2}`, with `s(ω) = (2π)^{−1/2}e^{−ω²/2}` and `λ_{2j} = (2j − 1)!!`, satisfies (H_ℝ). Take `[ω₁, ω₂] = [1, 2]`, +for instance. (R1) is [1D]'s smoothness, and (R2) replaces [1D]'s positivity of every Fourier coefficient. (R3) bounds +the spectral density with the weight `1 + ω⁶`. No decay rate of `ρ` is assumed: by (R1) and the Riemann–Lebesgue lemma, +`ρ^{(j)}(x) → 0` as `|x| → ∞` for every `j`. [1D] §6.4 asks, on the line, for "uniform nondegeneracy of separated +values". Here that comes from (R2) through Ingham's inequality and interlacing for the samples (Lemma 4.3_ℝ), and from +the Riemann–Lebesgue lemma for the pins (Lemma 4.1_ℝ). + +**Objects** ([1D] §0, with `T` replaced by `ℝ`). By Lemma 1.1_ℝ, almost surely `f` is a Morse function with alternating +maxima and minima and pairwise distinct critical values. By Lemma 1.5_ℝ, almost surely `f` exceeds every level on every +half-line. For a local maximum `M`, put `x₊ := inf{x > M : f(x) > f(M)}` and `x₋ := sup{x < M : f(x) > f(M)}`. These are +finite by Lemma 1.5_ℝ, `x₋ < M < x₊`, and `f(x_±) = f(M)`. +- The **crest-to-trough amplitude** is `H(M) := f(M) − f(S⁺(M))`, where `S⁺(M)` is the next critical point in the positive + direction (a minimum). +- The **persistence lifetime** is `ℓ(M) := f(M) − d(M)`. Here `d(M) := max(m₋, m₊)`, and `m_±` is the minimum of `f` on the + segment between `M` and `x_±`. So on `ℝ` every maximum has a finite bar. + + The minimum `m_±` is attained strictly inside the segment, at a local minimum. The point where `d(M)` is attained is + therefore a minimum `S(M)`, `M`'s **death point**. It is unique, because the critical values are distinct. + +The intensities are `Λ₊(B) := E#{M ∈ [0, 1) : H(M) ∈ B}` and `Λ(B) := E#{M ∈ [0, 1) : ℓ(M) ∈ B}`. `ν₊` and `ν` are their +canonical two-point Kac–Rice versions (1.2_ℝ)–(1.3_ℝ). + +**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}), (1D_ℝ.1) + ν(ℓ) = C₀ ℓ^{−1/3} + C₁ ℓ^{1/4} + 2B₂ ℓ^{1/3} + O(ℓ^{3/4}), (1D_ℝ.2) + +with the constants of [1D] §0, which are explicit functions of `λ₂, λ₄, λ₆, λ₈`: +- `C₀ = 2·72^{−1/6}Γ(7/6)(2π)^{−1/2}p₁₂σ₃^{4/3}`; +- `C₁ = −(8/21)24^{1/4}μ_{7/4}(2π)^{−1/2}p₁₂σ₄^{7/4}/σ₃`; +- `I = (3^{1/4}/2)C₁`; +- `B₂ = 2^{1/2}3^{1/3}Γ(5/6)(2π)^{−1/2}p₁₂σ₃^{2/3}·𝒬/(120λ₂λ₄D)`. + +Here `D := λ₂λ₆ − λ₄²` and the other symbols are those of [1D] §0. In particular, Theorem 1D's (1D.1)–(1D.2) with +`O(h^{1/2})` hold on `ℝ`. + +For `e^{−x²/2}`, the constants are `C₀ = 0.11011038`, `C₁ = −0.22760636`, `I = −0.14977341` and `B₂ = 0.11502229`. On `ℝ` +these are exact: there is no periodization correction. The rate of maxima is `(2π)^{−1}(λ₄/λ₂)^{1/2} = √3/(2π)`, so per +crest `f_H(h) = 0.19971814h^{−1/3} − 0.27165891h^{1/4} + 0.41725471h^{1/3} + O(h^{3/4})`. ([1D] §0 prints the last +coefficient as `0.41725`.) The leading constant is the one of Math- #210. + +**What is not claimed.** +- No uniformity in the covariance, and no explicit constant in any `O(·)`. +- No sharpness of `3/4`, and nothing on the sign of the `h^{3/4}` coefficient ([1D⁺] §0). +- Nothing for spectral measures with a singular part, or for spectral densities that are not bounded below on an interval + away from `0` ((R2)). For example, a spectrum on finitely many points violates Lemma 1.1_ℝ; with two points `±1`, the + process is `A cos x + B sin x`, and `H = 2√(A² + B²)` has no `h^{−1/3}` law (#210 §3). +- Nothing for spectral densities with `(1 + ω⁶)s` unbounded ((R3)). That excludes a spectral pole at `0` (long-range + dependence), and also spiky high-frequency tails, which (R1) alone would allow. + +## 1. The process on `ℝ` + +**Lemma 1.1_ℝ (nondegeneracy).** For distinct `x₁, …, x_k ∈ ℝ` and any `j₀ ≥ 0`, the Gaussian vector +`(f^{(j)}(x_i))_{i ≤ k, j ≤ j₀}` is nondegenerate. Almost surely, `f` is Morse with pairwise distinct critical values. + +*Proof.* `Var Σ c_{ij}f^{(j)}(x_i) = ∫|P(ω)|²s(ω)dω` with `P(ω) := Σ_{i,j}c_{ij}(iω)^je^{iωx_i}`. +- `P` is entire. If the variance vanishes, `P = 0` almost everywhere on `[ω₁, ω₂]` by (R2), hence `P ≡ 0`. +- Writing `P(ω) = Σ_i q_i(ω)e^{iωx_i}` with polynomials `q_i`, the functions `ω^je^{iωx_i}` (distinct `x_i`) are linearly + independent, so every `c_{ij}` vanishes. +- The Morse property and distinct critical values follow from Bulinskaya's lemma. Apply it to `(f', f'')` and to + `(f'(x), f'(y), f(x) − f(y))` on compact subsets of `{x ≠ y}`, exactly as in [1D] Lemma 1.1, then take a countable union. + ∎ + +**Lemma 1.5_ℝ (unboundedness on half-lines).** Almost surely, `sup_{[b,∞)}f = sup_{(−∞,b]}f = +∞` for every `b ∈ ℝ`. + +*Proof.* `ρ(n) → 0` by the Riemann–Lebesgue lemma, since `s ∈ L¹`. So the stationary Gaussian sequence `(f(n))_{n∈ℤ}` is +mixing (Maruyama), hence ergodic. For each `c`, `P(f(0) > c) > 0`, so by Birkhoff's theorem `f(n) > c` for infinitely many +`n ≥ 0` and infinitely many `n ≤ 0`, almost surely. Intersect over `c ∈ ℕ`. ∎ + +**The pair coordinates and the canonical versions.** These are as in [1D] §1: the maximum at `−τ`, the other critical +point at `τ`, `t = 2τ > 0`, and `U` with the density `p_t` and the conditional law `Q = Q_{t,α}`. The coordinate change +`(f'(−τ), f'(τ), f(−τ) − f(τ)) ↦ U` has determinant `12/t⁴`. So + + (12/t⁴)p_t(α) = p_V(0, 0, h), V := (f'(−τ), f'(τ), f(−τ) − f(τ)), (1.1_ℝ) + +the density of `V` at `(0, 0, h)`. `σ(V) = σ(U)`, so `Q` is also the law given `V = (0, 0, h)`. + +**The process under `Q`.** By Gaussian regression, under `Q` the process `f` has the law of `m_{t,h} + X`. Here +`m_{t,h} := Cov(f(·), V)Σ_VV^{−1}(0, 0, h)ᵀ`, and the residual `X := f − Cov(f(·), V)Σ_VV^{−1}V` is independent of `V`. The +entries of `Cov(f(x), V)` are `ρ'(−τ − x)`, `ρ'(τ − x)` and `ρ(−τ − x) − ρ(τ − x)`, which are bounded in `x`. So: +- `m_{t,h}` is bounded, and `X` differs from `f` by a bounded function. By Lemma 1.5_ℝ, `X` is unbounded above on every + half-line almost surely, and so is `f` under `Q`, for every `(t, α)`. +- Off the pins, the vectors `(f'(x), f''(x))`, `(f'(x), f'(y), f(x) − f(y))` and `(f'(x), f(x) − f(±τ))` stay + nondegenerate given `V` (Lemma 1.1_ℝ). By Bulinskaya's lemma, under `Q` the process `f` is Morse with distinct critical + values, and `f''(±τ) ≠ 0`, almost surely. + +So the objects of §0, and the marks below, are defined `Q`-almost surely for every `(t, α)`. + +**The Kac–Rice representation on `ℝ`.** The marked two-point Kac–Rice formula of [1D] §1 holds on `ℝ` for pairs with +`x ∈ [0, 1)` and `y = x + t`, `t > 0`. The marks are Borel functions of `f` on a compact window around the pair, or +increasing limits of such functions. The argument is this: +- On the domain `{x ∈ [0, 1], t ∈ [ε, 1/ε]}`, the pair law is nondegenerate (Lemma 1.1_ℝ). A mark that depends on `f` + restricted to `[x − r, x + r]` is a Borel function on the Polish space `C²([−r, 1 + 1/ε + r])`, which also carries the + pair's segment `[x, x + t]`. The argument of [1D] §1 ([P] §9 as repaired in [E2]) therefore applies verbatim. +- Let `ε ↓ 0`, by monotone convergence. +- The crest-to-trough mark `1{f' < 0 on (−τ, τ)}` depends on `f` on the pair's segment. +- The elder mark `𝔪 := 1{τ = S(−τ)}` is the increasing limit, as `r → ∞`, of + `𝔪·1{x₋ and x₊ of the maximum −τ lie within distance r of −τ}`. Each term is a Borel function of `f` on + `[−τ − r, −τ + r]`. The limit holds `Q`-almost surely by the preceding paragraph, so monotone convergence applies on both + sides of the formula. + +Hence + + ν₊(h) := ∫₀^∞ K₊(t, h) dt, ν(ℓ) := 2∫₀^∞ K(t, ℓ) dt, (1.2_ℝ)–(1.3_ℝ) + +with `K₊` and `K` the kernels (1.2)–(1.3) of [1D]. `K` is for the death point at `+t`. The death point at `−t` gives the same +kernel by the reflection `f ↦ f(−·)`, which preserves the law; this is the factor `2`. (On the circle the reflection gave +`ν = 2∫₀^{L/2}K`.) + +## 2. What transfers from the circle + +The following parts of [1D] and [1D⁺] concern a pair at separation `t ≤ t₀`, for a fixed small `t₀`, or hold for every +`t > 0`. They involve the pinned law `Q`, the jets at the midpoint, and suprema of derivatives over `[−2t, 2t]`: +- [1D] Lemmas 1.2–1.3 and Remark 1.4 (Lemma 1.2 and Remark 1.4 hold for every `t > 0`); §2, including Proposition 2.2; + §3 (Lemmas 3.1–3.3 and Corollary 3.4); Lemma 4.1; the near form of Lemma 4.2; Lemma 4.3 on `[t_*, t₀]`; and, in §5, + the adjacency estimate (the Borell–TIS bound for `{K₅ ≥ ct^{−δ}}` under `Q`, with `K₅` a supremum over `[−2t, 2t]`); +- [1D⁺] §§1–3 (Lemma E, Proposition 2.2⁺, Lemmas Φ and W, and Proposition M), and the part of §4 on `(0, t_*]`. + +Their proofs use the following, all available on `ℝ`: +- the moments `λ_{2j}`; +- the nondegeneracy of finitely many derivatives at one or two points (Lemma 1.1_ℝ, in place of [1D] Lemma 1.1); +- the parity split of [1D] Remark 1.4, which needs only that `ρ` is even; +- Borell–TIS and Sudakov–Fernique for suprema over compact intervals. + +So they hold on `ℝ` with the same proofs. The global parts of [1D] §§0–1 are replaced in §§0–1 above: +- [1D] Lemma 1.1 (the positivity of the Fourier coefficients), by Lemma 1.1_ℝ; +- the normalization `L^{−1}`, the range `t ∈ (0, L)` and the reflection `K(t) = K(L − t)` in (1.2)–(1.3), by + (1.2_ℝ)–(1.3_ℝ); +- the finiteness of the critical set, by its local finiteness (the Morse property, Lemma 1.1_ℝ); and the exclusion of the + global maximum, by Lemma 1.5_ℝ, under which no global maximum exists. + +Three points need a word. +- [1D] Lemma 3.3 holds on `ℝ`, and its global-maximum alternative does not occur. +- In the step of [1D] Lemma 4.3 on `[t₁, t₀]`, `sup|f''|` is the supremum over the band `[−τ, τ]`; Landau's inequality on + the band needs nothing more. (On `ℝ`, `sup_ℝ|f''| = ∞` almost surely.) With this reading, the near part of [1D] Lemma 4.3 + gives + + ∫_{t_*}^{t₀} K^{band}(t, h) dt = O(h^{3/4}). (2.1) + + Here `K^{band}(t, h) := (12/t⁴)p_t(α)E_Q[|f''(−τ)f''(τ)|1{banded}]`, and "banded" means `f(τ) ≤ f ≤ f(−τ)` on `[−τ, τ]`. + Also `t_* := (12h)^{1/(5−δ)}` with `δ ∈ (0, 1/10]`, as in [1D] Proposition 2.2; §5 takes `δ = 1/10`. +- Beyond the list above, [1D⁺] uses the following: + - `E_Q(K^e)² ≤ C` with `K^e = sup_{[−2t,2t]}|f_e^{(6)}|`, in (Φ.1) and, through `K^⊥`, in (Φ.3) and Proposition M; + - the invertibility of `Cov(U₁, U₃)` for `t > 0` in (Φ.2), now by Lemma 1.1_ℝ; + - uniform Gaussian tails of `K̃^o` and `K^⊥` in (Φ.3); + - `E_Q[O(3/2)⁴] ≤ C` in Proposition M. + + Each is a supremum or a moment over `[−2t, 2t]`, bounded by Sudakov–Fernique and Borell–TIS on a compact interval. + +Two facts from [1D] §4 are used in the following form. +- An adjacent typed pair is banded: `f' < 0` on `(−τ, τ)`, so `f` is monotone there. +- An elder pair is banded on the segment between `M` and its death point. If `S(M)` lies on the positive side, the segment + `[M, S(M)]` lies in `[M, x₊]`, so `f ≤ f(M)` on it. Also `f ≥ f(S(M))` there, since `S(M)` minimizes `f` on `[M, x₊]`. + With the maximum at `−τ` and the death point at `τ`, this is the banded event. On the circle, [1D] also needed a + co-banded case (the complementary arc); on `ℝ` there is none. + +## 3. The compact middle range + +**Lemma 3.1_ℝ.** For every fixed `T₀ ≥ t₀`, `∫_{t₀}^{T₀}K^{band}(t, h)dt = O(h²log(1/h))`. + +*Proof.* This is the far part of [1D] Lemma 4.3, on the compact range `t ∈ [t₀, T₀]`, with two changes: +- `sup_T|f''|` is replaced by `B := max(sup_{[−τ,τ]}|f''|, 1)`; +- on `ℝ` there is no complementary arc. + +The steps are as follows. +- **The interior points.** Choose four points `y_i` in `[−τ, τ]` at mutual distances `≥ t₀/8` and at distance `≥ t₀/4` + from both pins. +- **The density bound.** The conditional density of `(f'(y_i))_{i ≤ 4}` given `(V, f''(−τ), f''(τ))` is at most `C`, + uniformly on this compact configuration set. The conditional covariance is nondegenerate by Lemma 1.1_ℝ, applied to the + distinct points `±τ, y_i`, and its determinant is continuous in the configuration. So it is bounded below on the compact + set. +- **Landau's inequality on the band.** Lemma 4.2_ℝ on `Δ = [y_i − t₀/16, y_i + t₀/16] ⊂ [−τ, τ]` gives + `|f'(y_i)| ≤ (hB)^{1/2} + 16h/t₀ ≤ 2(hB)^{1/2}` on the banded event, for small `h`. +- **Truncation of `B`.** Under `Q`, `f''` has mean bounded by `Cα ≤ C` and centered part `f''_c` with + `E_Q sup_{[−τ,τ]}|f''_c| ≤ E sup_{[0,T₀]}|f''|` (Sudakov–Fernique). Borell–TIS gives `B ≤ b_h := C(log(1/h))^{1/2}` + outside an event of `Q`-probability `O(h^{20})`. +- **The kernel bound.** On `{banded} ∩ {B ≤ b_h}`, every `|f'(y_i)|` is at most `ε_h := 2(hb_h)^{1/2}`. Given + `(V, f''(−τ), f''(τ))`, this has probability at most `Cε_h⁴ = Ch²log(1/h)`. On `{B > b_h}` use Cauchy–Schwarz. Hence + `E_Q[|f''(−τ)f''(τ)|1{banded}] ≤ Ch²log(1/h)·E_Q|f''(−τ)f''(τ)| + O(h^{10})`. By (1.1_ℝ), + `(12/t⁴)p_t(α) = p_V(0, 0, h) ≤ C` on `[t₀, T₀]`, again by Lemma 1.1_ℝ and compactness. + +Integrating over the compact range gives the claim. ∎ + +## 4. The far band on `ℝ` + +Fix `w := 4π/(ω₂ − ω₁)`. A **cell** is an interval of length `w`. + +**Lemma 4.1_ℝ (pins far apart).** `Σ_VV` has diagonal `(λ₂, λ₂, 2(ρ(0) − ρ(t)))` and off-diagonal entries `−ρ''(t)`, +`ρ'(t)`, `ρ'(t)`. It is invertible for every `t > 0` (Lemma 1.1_ℝ). There is `T₁` such that +`λ_min(Σ_VV) ≥ c_V := min(λ₂, ρ(0))/2` for `t ≥ T₁`. + +*Proof.* `Cov(f'(y), f'(z)) = −ρ''(z − y)` and `Cov(f'(y), f(z)) = −ρ'(z − y)` give the entries. By (R1), `s`, `ωs` and +`ω²s` are integrable, so `ρ(t)`, `ρ'(t)` and `ρ''(t)` tend to `0` (Riemann–Lebesgue). Gershgorin's theorem then gives the +bound for large `t`. ∎ + +**Lemma 4.2_ℝ (Landau's inequality on an interval).** Let `Δ` be a compact interval with midpoint `y` and length `|Δ| > 0`, +and `g ∈ C²(Δ)`. Put `osc := sup_Δ g − inf_Δ g` and `S := sup_Δ|g''|`. Then `|g'(y)| ≤ (osc·S)^{1/2} + 2osc/|Δ|`. + +*Proof.* If `osc = 0`, `g` is constant and `g'(y) = 0`. Otherwise, for `0 < u ≤ |Δ|/2`, Taylor's formula at `y` gives +`|2ug'(y)| ≤ |g(y + u) − g(y − u)| + u²S ≤ osc + u²S`, so `|g'(y)| ≤ osc/(2u) + uS/2`. +- If `S = 0`, then `g` is affine and `|g'(y)| = osc/|Δ|`. +- If `S > 0` and `(osc/S)^{1/2} ≤ |Δ|/2`, take `u = (osc/S)^{1/2}` to get `(osc·S)^{1/2}`. +- Otherwise `S < 4osc/|Δ|²`, and `u = |Δ|/2` gives `osc/|Δ| + |Δ|S/4 < 2osc/|Δ|`. + +(Checker C1.) ∎ + +**Lemma 4.3_ℝ (a density bound for many samples).** There is `λ_* > 0`, depending only on `s₀`, `ω₁` and `ω₂`, with the +following property. Let `t > 0`, and let `y₀ < … < y_{N−1}` be points of `[−τ, τ]` with `y_{i+1} − y_i ≥ w`. Then for every +`G ⊂ {0, …, N − 1}` with `|G| ≥ 6` and every `ε > 0`, + + P_Q(|f'(y_i)| ≤ ε for all i ∈ G) ≤ (ε(2e/λ_*)^{1/2})^{|G|−3}. (4.1) + +*Proof.* Let `Y := (f'(y_i))_{i∈G}`, `k := |G|` and `m := k − 3`. + +- **Ingham's inequality.** For real `c_i`, + + Var(Σ_G c_if'(y_i)) = ∫|Σ_G c_i(iω)e^{iωy_i}|²s(ω)dω ≥ s₀ω₁²∫_{ω₁}^{ω₂}|Σ_G c_ie^{iωy_i}|²dω ≥ s₀ω₁²c_I Σc_i². + + The constant `c_I > 0` depends only on `w` and `ω₂ − ω₁`, and the last step is Ingham's inequality. The exponents `y_i` + are `w`-separated, and the interval has length `ω₂ − ω₁ = 4π/w > 2π/w`. A translation of the interval multiplies each + term by `e^{iω_cy_i}`, a unit factor. So `λ_min(Σ_YY) ≥ λ_* := s₀ω₁²c_I`. +- **Conditioning on the pins costs at most three dimensions.** Under `Q`, `Y` is Gaussian, given `V = (0, 0, h)`, with + covariance `Σ := Σ_YY − P`, where `P := Σ_YVΣ_VV^{−1}Σ_VY` is positive semidefinite of rank at most `3`. Order + eigenvalues increasingly. For `j ≥ 4`, every `j`-dimensional subspace meets `ker P` in dimension at least `j − 3`, and on + `ker P` the quadratic forms of `Σ` and `Σ_YY` agree. By the Courant–Fischer theorem, `μ_j(Σ) ≥ μ_{j−3}(Σ_YY) ≥ λ_*` + (checker C6). So at most three eigenvalues of `Σ` are below `λ_*`. No decay of the cross-covariances `Σ_YV` is needed. +- **Projection.** Let the rows of the `m × k` matrix `B` be orthonormal eigenvectors of `Σ` for `μ₄, …, μ_k`. Then `BY` is + Gaussian on `ℝ^m` with covariance `diag(μ₄, …, μ_k) ⪰ λ_*·Id`, so its density is at most `(2πλ_*)^{−m/2}`; its mean + does not matter. If `|f'(y_i)| ≤ ε` for all `i ∈ G`, then `‖BY‖₂ ≤ ‖Y‖₂ ≤ εk^{1/2}`. The ball of that radius in `ℝ^m` + has volume `π^{m/2}(εk^{1/2})^m/Γ(m/2 + 1) ≤ (2πek/m)^{m/2}ε^m`, by `Γ(x + 1) ≥ ∫_x^∞ u^xe^{−u}du ≥ x^xe^{−x}` (checker C6 + spot-checks it for `3 ≤ m ≤ 300`). + Since `k ≥ 6`, `k/m ≤ 2`. Multiplying gives `(ekε²/(mλ_*))^{m/2} ≤ (2eε²/λ_*)^{m/2}`, which is (4.1). ∎ + +**Lemma 4.4_ℝ (few rough cells).** Let `t ≥ T₁`, and let `J₀, …, J_{N−1}` be cells in `[−τ, τ]` with disjoint interiors. +Put `S_i := sup_{J_i}|f''|` and `n_R := #{i : S_i > R}`. There are `σ_F`, `R₀` and `h₀`, depending only on `ρ` and `w` (not +on `N`, `t` or the cells), such that for `R ≥ R₀` and `h ≤ h₀`, + + P_Q(n_R ≥ N/2) ≤ exp(−NR²/(8σ_F²)). (4.2) + +*Proof.* Under `Q`, `f = m + X`, with `m := m_{t,h}` and `X` the residual of §1 (whose law is the same under `Q`). +- `|m''| ≤ C_mh`. The entries of `Cov(f''(x), V)` are values of `ρ''` and `ρ'''`, bounded by (R1), and + `λ_min(Σ_VV) ≥ c_V` for `t ≥ T₁` (Lemma 4.1_ℝ). +- `X` is centered. Let `H` be the reproducing kernel Hilbert space of `f`, i.e. its Cameron–Martin space. The Cameron–Martin + space of `X` is the orthogonal complement in `H` of the three representers of `V`, with the `H`-norm. +- Let `Ū` be the smallest interval containing the cells. The law of `X` restricted to `Ū` is a centered Gaussian measure on + the separable Banach space `C²(Ū)`. Its Cameron–Martin space consists of the restrictions `g|_Ū` of the elements `g` of + the space above, with the quotient norm `inf{‖g‖_H : g in that space, g|_Ū = k}`. + +Put `F(k) := (Σ_i sup_{J_i}|k''|²)^{1/2}` for `k ∈ C²(Ū)`, a continuous seminorm. + +**`F` is Lipschitz along the Cameron–Martin space.** Every `g ∈ H` has the form `g(x) = ∫e^{iωx}φ(ω)s(ω)dω` with +`‖g‖_H² = ∫|φ|²s`. By Plancherel, `∫_ℝ|g''|² = 2π∫ω⁴|φ|²s² ≤ 2πS₆‖g‖_H²`, and likewise for `g'''`, with `S₆` from (R3). +On each cell, `sup_{J_i}|u|² ≤ 2(w^{−1}∫_{J_i}|u|² + w∫_{J_i}|u'|²)` (checker C4); apply this to `u = g''`. The cells have +disjoint interiors, so + + F(g)² ≤ 2(w^{−1}∫|g''|² + w∫|g'''|²) ≤ 4πS₆(w^{−1} + w)‖g‖_H² =: σ_F²‖g‖_H². + +`F(g)` depends only on `g|_Ū`. Taking the infimum over the `g` in the Cameron–Martin space of `X` with `g|_Ū = k` gives +`F(k) ≤ σ_F‖k‖` on the Cameron–Martin space of `X|_Ū`. +Also `|F(x + k) − F(x)| ≤ F(k)`, `F` being a seminorm. + +**Concentration.** The Gaussian concentration inequality for such functions gives +`P(F(X) ≥ EF(X) + u) ≤ e^{−u²/(2σ_F²)}` for `u > 0`. + +**The mean of `F(X)`.** +- On each cell, `sup|X''|` is the supremum of the centered process `(x, ±) ↦ ±X''(x)` on `J_i × {±1}`. +- Conditioning does not increase the variance of a linear functional. So the increments of this process have variances at + most those of `(x, ±) ↦ ±f''(x)`. Sudakov–Fernique and stationarity give `E sup_{J_i}|X''| ≤ μ_w := E sup_{[0,w]}|f''|`. +- Borell–TIS (variance `≤ λ₄`, both tails) gives `Var sup_{J_i}|X''| ≤ ∫₀^∞ 2u·2e^{−u²/(2λ₄)}du = 4λ₄`. So + `E sup_{J_i}|X''|² ≤ μ_w² + 4λ₄ ≤ M₂ := (μ_w + 2λ₄^{1/2})²`. +- Hence `EF(X) ≤ (EF(X)²)^{1/2} ≤ (NM₂)^{1/2}`. + +**Conclusion.** On `{n_R ≥ N/2}`, `F(f) ≥ (N/2)^{1/2}R`, and `F(f) ≤ F(m) + F(X) ≤ N^{1/2}C_mh + F(X)`. So +`F(X) − EF(X) ≥ N^{1/2}(R/√2 − C_mh − M₂^{1/2})`. + +Let `R ≥ R₀ := 5(M₂^{1/2} + 1)` and `h ≤ h₀ := 1/C_m`. Then `C_mh + M₂^{1/2} ≤ R/5`. Also `1/√2 − 1/5 ≥ 1/2`, because +`(1/2 + 1/5)² = 49/100 ≤ 1/2` (checker C6). With `4` in place of `5` the step fails, since `(1/2 + 1/4)² > 1/2`. + +So `F(X) − EF(X) ≥ N^{1/2}R/2`, and concentration with `u = N^{1/2}R/2` gives (4.2). ∎ + +**Lemma F_ℝ (the far band).** There is `T₀ ≥ t₀` such that `∫_{T₀}^∞ K^{band}(t, h)dt = O(h²)` as `h ↓ 0`. + +*Proof.* Take `T₀ := max(T₁, t₀, 24w)`. For `t ≥ T₀`, put `N := ⌊(t − 2w)/w⌋ + 1 ≥ 23` and `y_i := −τ + w + iw` for +`0 ≤ i < N`; then `y_{N−1} ≤ τ − w`. Let `J_i` be the cell centred at `y_i`. These cells lie in `[−τ, τ]` and have +disjoint interiors. + +*Banded pairs have small slopes at good cells.* On the banded event, `osc_{J_i}f ≤ h`. Lemma 4.2_ℝ gives +`|f'(y_i)| ≤ (hS_i)^{1/2} + 2h/w`. + +*The good-cell bound.* Let `R := A(log(1/h))^{1/2}`, with `A` fixed and `A² ≥ 2σ_F²`. +- Take `h ≤ h₀` so small that `R ≥ R₀`. +- Put `ε := (hR)^{1/2} + 2h/w` and `q := 4ε(2e/λ_*)^{1/2}`. Then `q ≤ C_qh^{1/2}(log(1/h))^{1/4}`. Take `h` so small that + also `q ≤ 1/16` and `h^{A²/(16σ_F²)} ≤ 1/2`. +- On `{n_R < N/2}`, more than `N/2` cells have `S_i ≤ R`, and on the banded event `|f'(y_i)| ≤ ε` at each of them. So some + `G ⊂ {0, …, N − 1}` with `|G| = ⌈N/2⌉ ≥ 12` has `|f'(y_i)| ≤ ε` for all `i ∈ G`. There are at most `2^N` such `G`. +- Use (4.1) for each `G`, and (4.2) for `{n_R ≥ N/2}`. Since `ε(2e/λ_*)^{1/2} = q/4 ≤ 1`, the exponent `⌈N/2⌉ − 3` may be + lowered to `N/2 − 3`: + + P_Q(banded) ≤ exp(−NR²/(8σ_F²)) + 2^N(q/4)^{N/2−3} = exp(−NR²/(8σ_F²)) + 64q^{N/2−3}. + +*The kernel.* By (1.1_ℝ), Cauchy–Schwarz and `(x + y)^{1/2} ≤ x^{1/2} + y^{1/2}`, + + K^{band}(t, h) ≤ p_V(0, 0, h)·(E_Q[f''(−τ)²f''(τ)²])^{1/2}·P_Q(banded)^{1/2} ≤ C_K(exp(−NR²/(16σ_F²)) + 8q^{N/4−3/2}). + +The constant `C_K` is uniform in `t ≥ T₀`, for two reasons. First, `p_V(0, 0, h) ≤ (2πc_V)^{−3/2}` (Lemma 4.1_ℝ). Second, +under `Q` each `f''(±τ)` is Gaussian with variance `≤ λ₄` and mean `m''(±τ)`, which is at most `C_mh`. + +*Summation.* The set `{t : N(t) = n}` has length `≤ w`, and `exp(−nR²/(16σ_F²)) = h^{nA²/(16σ_F²)}`. The two geometric +series have ratios `h^{A²/(16σ_F²)} ≤ 1/2` and `q^{1/4} ≤ 1/2`, so each is at most twice its first term: + + ∫_{T₀}^∞ K^{band} dt ≤ C_Kw Σ_{n≥23}(h^{nA²/(16σ_F²)} + 8q^{n/4−3/2}) ≤ 2C_Kw(h^{23A²/(16σ_F²)} + 8q^{17/4}). + +Here `23A²/(16σ_F²) ≥ 23/8` and `q^{17/4} ≤ C_q^{17/4}h^{17/8}(log(1/h))^{17/16}`. So the integral is +`O(h^{17/8}(log(1/h))^{17/16})`, which is `O(h²)`. (Checker C5 checks this exponent bookkeeping and the geometric steps at +sample values.) ∎ + +## 5. Proof of Theorem 1D_ℝ + +Fix `δ = 1/10` and `t₀` as in [1D⁺] §4 (small enough for [1D] Lemma 4.3), and `T₀ ≥ t₀` as in Lemma F_ℝ. By (2.1), +Lemma 3.1_ℝ and Lemma F_ℝ, + + ∫_{t_*}^∞ K^{band}(t, h) dt = O(h^{3/4}) + O(h²log(1/h)) + O(h²) = O(h^{3/4}). (5.1) + +**(1D_ℝ.1).** Write `ν₊ = ∫₀^{t_*}K₊ + ∫_{t_*}^∞K₊`. +- On `(0, t_*]` the argument is [1D⁺] §4 verbatim. `K₊ = K₁^{sign} − (12/t⁴)p_tE_Q[(−f''(−τ))⁺f''(τ)⁺1{not adjacent}]`. + Non-adjacency forces `K₅ ≥ ct^{−δ}` ([1D] Lemma 3.1), so the correction integrates to `O(h^k)` for every `k`. + Then [1D⁺] Proposition 2.2⁺ with `θ = 1` gives the three terms with remainder `O(h^{3/4})`. +- On `[t_*, ∞)`, an adjacent pair is banded, so `K₊ ≤ K^{band}`, and (5.1) applies. + +**(1D_ℝ.2).** Write `ν = 2∫₀^∞K`, by (1.3_ℝ). +- On `(0, t_*]`, as in [1D⁺] §4: `K = K_{1/3}^{sign} + (K − K_{1/3}^{sign})`. [1D⁺] Proposition 2.2⁺ with `θ = 1/3` gives the + expansion with `I_{1/3} = C₁`, and [1D⁺] Proposition M bounds the rest by `O(h^{3/4})`. +- On `[t_*, ∞)`, an elder pair is banded (§2), so `K ≤ K^{band}`, and (5.1) applies. + +Doubling gives (1D_ℝ.2). The constants are those of [1D] §0. They depend only on `λ₂, λ₄, λ₆, λ₈`, through `p₁₂`, `σ₃`, `σ₄`, +`D` and `𝒬`. ∎ + +## 6. Remarks + +1. **What changed from the circle.** On `T`, [1D] Lemma 4.3's far part used four interior points, and compactness of the + circle gave a bounded density and a bounded `sup_T|f''|`. + - On `ℝ` the band can be arbitrarily long, so a fixed number of points does not make the kernel integrable in `t`. The + number of cells must grow with `t`. + - Two uniformities then replace compactness. Ingham's inequality gives a covariance lower bound that does not degrade + with the number of samples, and conditioning on the three pin observations lowers at most three eigenvalues + (Lemma 4.3_ℝ). Gaussian concentration controls the number of cells where `f''` is large (Lemma 4.4_ℝ); a union bound + over `N` cells would cost a factor `N`, which is not integrable. + - The price is (R2)–(R3): an absolutely continuous spectrum, with a density bounded below on an interval away from `0` + and bounded with the weight `1 + ω⁶`. No decay rate of the covariance is needed. +2. **The hypotheses.** + - (R2) is used twice: in Lemma 1.1_ℝ, and through Ingham's inequality in Lemma 4.3_ℝ. In the latter, it is used for + `f'`, whose spectral density `ω²s(ω)` vanishes at `0`, hence `ω₁ > 0`. + - For the Gaussian covariance, the samples' covariance is also directly diagonally dominant at spacings `≥ 2`, with + `λ_min ≥ 1/6` uniformly in `N` (checker C2). Ingham's inequality is needed for covariances without such explicit + decay. At spacing `1` the Gaussian row sum is `1 − 5.3·10⁻⁷`: the infinite Toeplitz matrix is then almost singular, + and diagonal dominance gives no usable bound. + - (R3) bounds the Lipschitz constant `σ_F`. + - The decorrelation used is qualitative: `ρ, ρ', ρ'' → 0` (Riemann–Lebesgue), in Lemma 1.5_ℝ and Lemma 4.1_ℝ. v1 + assumed `|ρ^{(j)}(x)| ≤ C(1 + |x|)^{−1}` for `j ≤ 2`, to make the cross-covariances `Σ_YV` small; the interlacing step + of Lemma 4.3_ℝ makes that unnecessary. +3. **Relation to the classical literature (#210).** + - For `ρ = e^{−x²/2}`, (1D_ℝ.1) per crest is the small-amplitude law of crest-to-trough heights of a stationary + Gaussian process on the line. Its leading constant `0.19971814` is #210's `C`. + - #210's two-point check integrates the sign kernel up to `t ≤ 1.5`, without the adjacency mark. The non-adjacent pairs + it includes contribute `O(1)` there, as #210 v1.3 §3 derives from [1D] Lemmas 1.3 and 3.1. #210 §3 notes that #214 + claims nothing on the line. Once this note is reviewed, that sentence can cite Theorem 1D_ℝ instead. +4. **Exploration.** None was needed. The statement is a transfer, and the new lemmas are deterministic or standard + estimates. The checker tests the elementary inequalities that the proof uses (§8). + +## 7. Sources (exact identities in `SOURCES.json`) + +| Tag | Path | Role | +|---|---|---| +| [1D] | `frontiers/d1_third_order_law_20261001/PROOF.md` (blob `1591ecee`, merged `e4ca2b3`) | consumed: §§0–5 as listed above | +| [1D⁺] | `frontiers/d1_sharp_remainder_20261001/PROOF.md` (blob `8dc558a7`, merged `8404169`) | consumed: §§0–4 | +| [P], [E2] | `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` (blob `dfed3b8d`), `reviews/d1_section9_borel_repair_20260925/REPAIR.md` (blob `fe9b9ce4`) | the marked Kac–Rice convention, through [1D] §1 — cited | +| #210 | `reviews/literature_classical_neighbors_20261001/ADDENDUM.md` (Math- #210, open; head `213dd9e`, blob `b289c7cd`) | comparison only (Remark 3) | + +## 8. Exact controls (`line_check.py`; standard library; exact rationals except C3; byte-identical under `-O`) + +- **C1 Landau on an interval (Lemma 4.2_ℝ).** + - Random rational polynomials of degree `≤ 4` are tested on intervals of six lengths. So are S-shaped cubics + `As(1 − (2s/|Δ|)²)` plus small terms, which have `|g'(y)| > 2osc/|Δ|` (counted with an upper bound for `osc`). + - `S = sup|g''|` is computed exactly: `g''` is quadratic, so its maximum is at an endpoint or the vertex. + - `osc` is bounded from below by the values at a grid and at bisection-refined zeros of `g'`. The inequality's right + side increases in `osc`, so a lower bound suffices. + - The inequality is checked in exact arithmetic, and so is the Taylor step `|2ug'(y)| ≤ |g(y + u) − g(y − u)| + u²S`. + - The nearly affine family `g = s + εs²` on a unit interval shows that the term `2osc/|Δ|` is needed: there + `|g'(y)| = 1` while `(osc·S)^{1/2} = (2ε)^{1/2}`. +- **C2 Gaussian covariance: diagonal dominance.** The correlation `−ρ''(kw) = (1 − k²w²)e^{−k²w²/2}` of `f'` samples at + spacing `w`, with `λ₂ = 1`. + - The off-diagonal row sum `2Σ_{k≥1}|1 − k²w²|e^{−k²w²/2}` is bounded above with `e^{−x} ≤ 1/Σ_{j≤40}x^j/j!` and a + geometric tail bound. + - The upper bounds are `0.82207665`, `0.17774502` and `0.01006388` at `w = 2, 3, 4`, each `≤ 5/6`. + - Each term decreases in `w` once `kw ≥ 2 > √3`, because `((x² − 1)e^{−x²/2})' = x(3 − x²)e^{−x²/2}`. + - So for every spacing `w ≥ 2` and every `N`, `λ_min ≥ 1/6`. +- **C3 The constants.** `C₀, C₁, I, B₂` from `λ_{2j} = (2j − 1)!!` and [1D] §0's closed forms, against the printed values. + The per-crest coefficients are checked against `0.19971814`, `−0.27165891` and `0.41725471`. + - Exact: `𝒬 = 1620`, `𝒬/(120λ₂λ₄D) = 3/4`, and [1D]'s decomposition of `𝒬` at the Gaussian moments. + - Floating point: the two printed forms of `C₁` agree. +- **C4 The cell Sobolev bound.** `sup_J|u|² ≤ 2(w^{−1}∫_J|u|² + w∫_J|u'|²)` is checked for random rational polynomials `u` of + degree `≤ 5`, on intervals of five lengths `w`. The integrals are exact, and the supremum is bounded above on a grid with + a derivative margin. + - Proof of the bound: `u(x)² ≤ u(z)² + 2∫_J|uu'|`; average over `z ∈ J` and use `2ab ≤ a²/w + wb²`. This gives + `sup|u|² ≤ 2w^{−1}∫u² + w∫u'²`. + - The constant `1` is false: `u = 1 + (s/w)²/2` on `[0, w]` has `sup|u|² = 9/4 > 103/60 = w^{−1}∫u² + w∫u'²`. The sharp + constant is `coth 1 = 1.313…`. +- **C5 The summation of Lemma F_ℝ**, at sample values. + - `Σ_{n=23}^{M}x^n = (x^{23} − x^{M+1})/(1 − x)`, and `x^{23}/(1 − x) ≤ 2x^{23}`, for `x ∈ {1/2, 1/3, 1/10, 1/1000}`. + - `2^N(q/4)^{N/2−3} = 64q^{N/2−3}`, the step to the union bound's form. + - `N ≥ 23` and `y_{N−1} ≤ τ − w` when `t ≥ 24w`, at sample values. + - The final exponents: `23A²/(16σ_F²) ≥ 23/8 > 2` for `A² ≥ 2σ_F²`, and `(23 − 6)/4·(1/2) = 17/8` with log power `17/16`. +- **C6 The ingredients of Lemmas 4.3_ℝ–4.4_ℝ.** + - Interlacing: for random rational `A = λ·Id + MMᵀ` and `P = Σ_{s≤r}u_su_sᵀ` with `r ≤ 3`, an exact `LDLᵀ` count + (Sylvester's law of inertia) shows that `A − P − λ·Id` has at most `r` negative eigenvalues. A deterministic family + attains `r`. + - Stirling: `Γ(m/2 + 1) ≥ (m/(2e))^{m/2}` for `3 ≤ m ≤ 300`, with rational bounds for `e` and `√π`; and `k/(k − 3) ≤ 2` + for `k ≥ 6`. + - The threshold `R₀ = 5(M₂^{1/2} + 1)`: `(1/2 + 1/5)² ≤ 1/2`. + +**Mutants** (`--mutant M`) exit 1, each in its own control: +- M1 drops the `2osc/|Δ|` term (C1); +- M2 uses the Sobolev constant `1` in place of `2` (C4); +- M3 takes the spacing `w = 1` in place of `2` (C2); +- M4 drops the factor `2` of `C₀` (C3); +- M5 takes `23A²/(32σ_F²)` (C5); +- M6 takes `R₀ = 4(M₂^{1/2} + 1)` (C6); +- M7 allows only `r − 1` small eigenvalues after a rank-`r` conditioning (C6). + +An unknown label exits 2. + +## 9. Review slices + +- **A §§0–1.** The objects on `ℝ`; Lemma 1.1_ℝ, Lemma 1.5_ℝ, the process under `Q`, and the Kac–Rice representation on `ℝ` + with the two marks. +- **B §2.** The claim that the listed parts of [1D] and [1D⁺] are local. Check each for any use of compactness of `T`. +- **C §§3–4.** Lemma 3.1_ℝ; Lemmas 4.1_ℝ–4.4_ℝ (the pin covariance, Landau, Ingham with interlacing, Gaussian + concentration); Lemma F_ℝ. +- **D §5 and the controls.** The assembly, the constants, `line_check.py`. diff --git a/frontiers/d1_line_20261004/README.md b/frontiers/d1_line_20261004/README.md new file mode 100644 index 000000000..5f68c466e --- /dev/null +++ b/frontiers/d1_line_20261004/README.md @@ -0,0 +1,109 @@ +# Theorems 1D and 1D⁺ on the line + +**Author-side proof candidate (Anthropic Claude). Scientific effect: NONE. Nonauthor review required.** + +Object `CL-D1-LINE-20261004-v1.1`. Full text: [`PROOF.md`](PROOF.md). Dylan Roy — delegated AI work. + +**v1.1** was made before any nonauthor pickup; v1 was `f34ffd7`. It drops v1's decay hypothesis on `ρ, ρ', ρ''`, so +(H_ℝ) is now purely spectral. Lemma 4.3_ℝ now uses interlacing: conditioning on the three pin observations lowers at +most three eigenvalues of the samples' covariance, whatever the cross-covariances. The theorem and its rates are +unchanged. + +## Result + +Let `f` be a centered stationary Gaussian process on `ℝ` whose spectral measure has a density `s`. Assume (H_ℝ): +- (R1) all moments `∫|ω|^n s` are finite; +- (R2) `s ≥ s₀ > 0` on some interval `[ω₁, ω₂]` with `ω₁ > 0`; +- (R3) `(1 + ω⁶)s(ω)` is bounded. + +No decay rate of the covariance is assumed. `ρ, ρ', ρ'' → 0` follows from (R1) by the Riemann–Lebesgue lemma. + +Then, per unit length, as `h ↓ 0` and `ℓ ↓ 0`: + + ν₊(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) + +Here `ν₊` is the density of crest-to-trough amplitudes and `ν` that of persistence lifetimes. The constants are those of +Math- #214 §0, functions of `λ₂, λ₄, λ₆, λ₈` only. On the circle these laws are Math- #214 (Theorem 1D, remainder +`O(h^{1/2})`) and Math- #238 (Theorem 1D⁺, `O(h^{3/4})`), both merged. + +For the covariance `e^{−x²/2}`, the classical setting of Rice, Cartwright–Longuet-Higgins and Lindgren, the +crest-to-trough density per crest is + + f_H(h) = 0.19971814 h^{−1/3} − 0.27165891 h^{1/4} + 0.41725471 h^{1/3} + O(h^{3/4}). + +Its leading constant is the one of Math- #210. + +## What is new + +On the circle, compactness bounds the far part of the kernel. On the line a banded pair can be arbitrarily long, so +the number of sample points has to grow with the length of the band. + +| Step | Statement | Tool | +|---|---|---| +| §1 | Nondegeneracy (Lemma 1.1_ℝ); `f` unbounded on half-lines (Lemma 1.5_ℝ), also under the pinned law; the marked two-point Kac–Rice formula on `ℝ` | entire functions; Maruyama + Birkhoff; Gaussian regression; monotone limits of compact-window marks | +| §2 | The parts of #214 and #238 that are local transfer verbatim | review of each step for global objects | +| Lemma 3.1_ℝ | `∫_{t₀}^{T₀}K^{band} = O(h²log(1/h))` | #214 Lemma 4.3's far argument on a compact range | +| Lemma 4.1_ℝ | the pin covariance is uniformly nondegenerate for `t ≥ T₁` | Riemann–Lebesgue + Gershgorin | +| Lemma 4.2_ℝ | `\|g'(y)\| ≤ (osc·S)^{1/2} + 2osc/\|Δ\|` at the midpoint `y` of an interval `Δ` | Landau | +| Lemma 4.3_ℝ | `P_Q(\|f'(y_i)\| ≤ ε, i ∈ G) ≤ (ε(2e/λ_*)^{1/2})^{\|G\|−3}` for `w`-separated samples, `\|G\| ≥ 6` | Ingham's inequality + interlacing (at most three eigenvalues drop) | +| Lemma 4.4_ℝ | `P_Q(at least N/2 of N cells have sup\|f''\| > R) ≤ exp(−NR²/(8σ_F²))` | Gaussian concentration along the Cameron–Martin space | +| Lemma F_ℝ | `∫_{T₀}^∞K^{band} = O(h^{17/8}(log(1/h))^{17/16}) = O(h²)` | Lemmas 4.1_ℝ–4.4_ℝ, with at least `23` cells | + +## Dependencies + +**Consumed (merged; bytes bound in `SOURCES.json`).** +- Math- #214, `frontiers/d1_third_order_law_20261001/PROOF.md`, blob `1591ecee`, merged at `e4ca2b3` ([1D]). +- Math- #238, `frontiers/d1_sharp_remainder_20261001/PROOF.md`, blob `8dc558a7`, merged at `8404169` ([1D⁺]). + +**Cited.** `[P]` (`UNIFORM_MATRIX_CAP_AND_LIFETIME.md`, blob `dfed3b8d`) and `[E2]` (`REPAIR.md`, blob `fe9b9ce4`), the +marked Kac–Rice convention, through [1D] §1. Math- #210 (open; head `213dd9e`, addendum blob `b289c7cd`) is cited for +comparison only and is bound through the repository API. + +## Controls + +`line_check.py` uses only the standard library. It uses exact rationals, except that C3 evaluates the closed-form +constants in floating point. Its output is `RESULTS.json`, byte-identical with and without `-O` on CPython 3.10–3.14. + +| Control | What it checks | +|---|---| +| C1 | Landau's inequality on 300 polynomials and the Taylor step, exactly. A nearly affine family shows that the term `2osc/\|Δ\|` is needed, and S-shaped cubics (with `osc` bounded above) that `(osc·S)^{1/2}` is | +| C2 | For the Gaussian kernel, the `f'`-sample covariance at spacing `w ≥ 2` is diagonally dominant with `λ_min ≥ 1/6`, using rigorous rational bounds for `e^{−x}` | +| C3 | `C₀, C₁, I, B₂` and the per-crest coefficients against the printed values; `𝒬 = 1620` and `𝒬/(120λ₂λ₄D) = 3/4` exactly | +| C4 | The cell Sobolev bound with constant `2`, on 155 polynomials; the witness `1 + (s/w)²/2` shows that the constant `1` is false | +| C5 | The geometric steps and exponent bookkeeping of Lemma F_ℝ (at least `23` cells), at sample values | +| C6 | Interlacing by exact inertia counts (`LDLᵀ`, Sylvester), with a family attaining the bound; Stirling's lower bound for the ball volume; the threshold `R₀ = 5(M₂^{1/2} + 1)` of Lemma 4.4_ℝ | + +Replay: + + python3 -B -S line_check.py # exit 0; stdout = RESULTS.json + python3 -B -S line_check.py --mutant M1 # M1–M7 exit 1, each in its own control + python3 -B -S line_check.py --mutant XX # exit 2 + +The workflow `.github/workflows/d1-line.yml` checks the packet tree and file identities, the consumed and cited sources, +both replay modes, the mutants and the bad arguments. + +## Review + +Before submission, two clean-context same-family referees (Anthropic Claude subagents) read the draft. Both returned +ACCEPT WITH MINOR FIXES on their slices, with no major finding. Their fixes are applied, and a delta check of the +revision found them fixed; `SOURCES.json` (`referee`) lists what they found and what changed. v1.1's new material +(Lemma 4.1_ℝ, the interlacing Lemma 4.3_ℝ, and Lemma F_ℝ with `23` cells) came after that pass. A second delta check +returned ACCEPT on slices B and C, and ACCEPT WITH MINOR FIXES on slices A and D, for one sentence of §0 and the +packaging; both are applied. One author-side +correction, made before the referee pass, changed a constant: the threshold of Lemma 4.4_ℝ is `R₀ = 5(M₂^{1/2} + 1)`, +because the factor `4` does not give `R/√2 − R/4 ≥ R/2`. These referees share a provider with the author and give no +independence credit. + +**Requested:** a nonauthor review, by slices (PROOF §9): +- **A** §§0–1: the objects on `ℝ`, Lemmas 1.1_ℝ and 1.5_ℝ, the process under `Q`, and the Kac–Rice representation; +- **B** §2: that the listed parts of #214 and #238 are local; +- **C** §§3–4: Lemma 3.1_ℝ, Lemmas 4.1_ℝ–4.4_ℝ and Lemma F_ℝ; +- **D** §5 and the controls. + +## Not claimed + +- No uniformity in the covariance, and no explicit constant in any `O(·)`. +- No sharpness of the remainder `3/4`. +- Nothing without (R2) (for instance, spectra on finitely many points), or for spectral densities with `(1 + ω⁶)s` + unbounded ((R3)), such as a spectral pole at `0` (long-range dependence) or spiky high-frequency tails. diff --git a/frontiers/d1_line_20261004/RESULTS.json b/frontiers/d1_line_20261004/RESULTS.json new file mode 100644 index 000000000..795a3c232 --- /dev/null +++ b/frontiers/d1_line_20261004/RESULTS.json @@ -0,0 +1,153 @@ +{ + "controls": { + "C1": { + "cases_with_|g'(y)|>2osc/|Delta|_(osc_bounded_above)": 61, + "interval_lengths": [ + "1/2", + "1", + "2", + "3", + "4", + "25/2" + ], + "nearly_affine_g=s+eps*s^2_unit_interval": { + "1/10": { + "S": "1/5", + "osc": "1", + "osc*S": "1/5", + "|g'(0)|": "1" + }, + "1/100": { + "S": "1/50", + "osc": "1", + "osc*S": "1/50", + "|g'(0)|": "1" + }, + "1/1000": { + "S": "1/500", + "osc": "1", + "osc*S": "1/500", + "|g'(0)|": "1" + }, + "1/1000000": { + "S": "1/500000", + "osc": "1", + "osc*S": "1/500000", + "|g'(0)|": "1" + } + }, + "polynomials_tested": 300, + "reading": "both terms are needed: the S-shaped cubics have |g'(y)| > 2 osc/|Delta|, and on the nearly affine family |g'(y)|^2 = 1 > osc*S = 2 eps" + }, + "C2": { + "conclusion": "lambda_min >= 1 - 5/6 = 1/6 for every spacing w >= 2 and every N (Gershgorin)", + "monotone_for_w>=2": "((x^2-1) e^(-x^2/2))' = x (3 - x^2) e^(-x^2/2) < 0 for x >= 2", + "w=2": { + "lambda_min_lower": "0.17792335", + "row_sum_upper": "0.82207665" + }, + "w=3": { + "lambda_min_lower": "0.82225498", + "row_sum_upper": "0.17774502" + }, + "w=4": { + "lambda_min_lower": "0.98993612", + "row_sum_upper": "0.01006388" + } + }, + "C3": { + "D": "6", + "Q": "1620", + "Q/(120 l2 l4 D)": "3/4", + "lambda_2j": [ + "1", + "3", + "15", + "105" + ], + "rate_of_maxima": "0.27566445", + "sigma3^2": "6", + "sigma4^2": "30", + "values_8_decimals": { + "B2": "0.11502229", + "C0": "0.11011038", + "C1": "-0.22760636", + "I": "-0.14977341", + "per_crest_h^(-1/3)": "0.19971814", + "per_crest_h^(1/3)": "0.41725471", + "per_crest_h^(1/4)": "-0.27165891" + } + }, + "C4": { + "interval_lengths": [ + "1/2", + "1", + "2", + "4", + "25/2" + ], + "max_sup^2/(w^-1 int u^2 + w int u'^2)": "1.310680", + "polynomials_tested": 155, + "reading": "the bound holds with constant 2; constant 1 fails on the witness (9/4 > 103/60)", + "sharp_constant_coth(1)_float": "1.313035", + "witness_u=1+(s/w)^2/2": { + "w=1": { + "sup_u^2": "9/4", + "w^-1 int u^2 + w int u'^2": "103/60" + }, + "w=1/2": { + "sup_u^2": "9/4", + "w^-1 int u^2 + w int u'^2": "103/60" + }, + "w=2": { + "sup_u^2": "9/4", + "w^-1 int u^2 + w int u'^2": "103/60" + }, + "w=25/2": { + "sup_u^2": "9/4", + "w^-1 int u^2 + w int u'^2": "103/60" + }, + "w=4": { + "sup_u^2": "9/4", + "w^-1 int u^2 + w int u'^2": "103/60" + } + } + }, + "C5": { + "N(t)": "N = floor((t - 2w)/w) + 1 >= 23 for t >= 24 w, y_(N-1) <= tau - w, and ceil(N/2) >= 12 (at w = 5/2)", + "exponents": { + "h^(23 A^2/(16 sigma_F^2)) at A^2 = 2 sigma_F^2": "23/8", + "margin over h^2": "1/8", + "q^(N/4 - 3/2) at N = 23, with q = O(h^(1/2) log^(1/4))": "h^(17/8) log^(17/16)" + }, + "geometric": "sum_{n=23}^{M} x^n = (x^23 - x^(M+1))/(1-x) and x^23/(1-x) <= 2 x^23 for x in {1/2, 1/3, 1/10, 1/1000}; the ratios are <= 1/2 when q <= 1/16 and h^(A^2/(16 sigma_F^2)) <= 1/2", + "square_root": "P^(1/2) <= exp(-N R^2/(16 sigma_F^2)) + 8 q^(N/4 - 3/2)", + "union_bound_step": "2^N (q/4)^(N/2-3) = 64 q^(N/2-3) with q/4 = eps (2e/lambda_*)^(1/2)" + }, + "C6": { + "R0_threshold": { + "(1/2 + 1/5)^2": "49/100", + "R0": "5 (M2^(1/2) + 1)", + "needed": "<= 1/2" + }, + "factor_4_fails": "(1/2 + 1/4)^2 = 9/16 > 1/2", + "interlacing": { + "attaining_cases": 15, + "random_cases": 90, + "statement": "A - P - lam Id has at most rank(P) negative eigenvalues when A - lam Id >= 0" + }, + "stirling": "Gamma(m/2 + 1) >= (m/(2e))^(m/2) for 3 <= m <= 300; k/(k-3) <= 2 for k >= 6" + } + }, + "mutants": { + "M1": "C1: the Landau bound without the term 2 osc/|Delta|", + "M2": "C4: the cell Sobolev constant 1 in place of 2", + "M3": "C2: the Gaussian sample spacing w = 1 in place of 2", + "M4": "C3: C0 without its factor 2", + "M5": "C5: the band exponent 23 A^2/(32 sigma_F^2) in place of 23 A^2/(16 sigma_F^2)", + "M6": "C6: the threshold R0 = 4 (M2^(1/2) + 1) in place of 5 (M2^(1/2) + 1)", + "M7": "C6: only r - 1 small eigenvalues allowed after a rank-r conditioning" + }, + "object": "CL-D1-LINE-20261004-v1.1", + "scientific_effect": "NONE" +} diff --git a/frontiers/d1_line_20261004/SOURCES.json b/frontiers/d1_line_20261004/SOURCES.json new file mode 100644 index 000000000..999b00621 --- /dev/null +++ b/frontiers/d1_line_20261004/SOURCES.json @@ -0,0 +1,148 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "object": "CL-D1-LINE-20261004-v1.1", + "kind": "author-side proof candidate: Theorems 1D and 1D+ for stationary Gaussian processes on the line under (H_R) = (R1) all spectral moments finite, (R2) s >= s0 > 0 on [omega1, omega2] with omega1 > 0, (R3) ess sup (1 + omega^6) s < infinity (no decay rate of rho is assumed): 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)), with the constants of Math- #214. New: Lemma 1.5_R and the process under Q; the Kac-Rice representation on R; Lemma 3.1_R (the compact middle range); Lemma 4.1_R (the pin covariance, Riemann-Lebesgue); Lemma 4.2_R (Landau on an interval); Lemma 4.3_R (Ingham + interlacing: conditioning on the pins lowers at most three eigenvalues); Lemma 4.4_R (Gaussian concentration for the number of rough cells); Lemma F_R (the far band is O(h^2))", + "author": "Anthropic Claude", + "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", + "attribution": "Dylan Roy - delegated AI work; actual performer Anthropic Claude", + "read_at": { + "branch_base": "f34ffd748ac00507fb3ef2abd01cdeb6eb7bb43e" + }, + "consumed": [ + { + "path": "frontiers/d1_third_order_law_20261001/PROOF.md", + "bytes": 46313, + "sha256": "a1b5e6ecc97341ad72d74973c69c0f94304b22c559ab0187310ef2bd73455804", + "git_blob": "1591ecee3c82c8b42cb3220189ea0a4ce4bf195f", + "tag": "1D", + "pr": "Math- #214", + "merged_at": "e4ca2b3", + "use": "Theorem 1D on the circle (v1.3): section 0 (objects, constants C0, C1, I, B2); section 1 (pair coordinates, the pinned law Q, (1.2)-(1.4), Lemmas 1.2-1.3, Remark 1.4); section 2 (Proposition 2.2); section 3 (Lemmas 3.1-3.3, Corollary 3.4); section 4 (Lemma 4.1, the near form of Lemma 4.2, Lemma 4.3 on [t_*, t0], read with sup|f''| over the band); section 5 (the adjacency argument). Global parts replaced: Lemma 1.1, the normalization and reflection of (1.2)-(1.3), the far part of Lemma 4.3 and the co-banded case" + }, + { + "path": "frontiers/d1_sharp_remainder_20261001/PROOF.md", + "bytes": 44717, + "sha256": "9febf062d64b0c261bdeb51ac56a6ddf1d9c7edd92ff3ede53c9fd5bc8f693e0", + "git_blob": "8dc558a735f8a8fdf82b698726b2881c2655281f", + "tag": "1D+", + "pr": "Math- #238", + "merged_at": "8404169", + "use": "Theorem 1D+ on the circle (v1.2): section 0, and sections 1-4 (Lemma E, Proposition 2.2+, Lemmas Phi and W, Proposition M, the assembly); the assembly is redone on the line in PROOF section 5" + } + ], + "consumed_unmerged": [], + "cited_only": [ + { + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "bytes": 40261, + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "tag": "P", + "use": "the marked two-point Kac-Rice convention (section 9), through [1D] section 1" + }, + { + "path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", + "bytes": 9062, + "sha256": "845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f", + "git_blob": "fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a", + "tag": "E2", + "use": "the Borel repair of [P] section 9, through [1D] section 1" + } + ], + "cited_unmerged": [ + { + "path": "reviews/literature_classical_neighbors_20261001/ADDENDUM.md", + "bytes": 16207, + "sha256": "5e3903ad05b0566a1e999b0e69b309a4165578705d687f4a3021d22ebd1e1e42", + "git_blob": "b289c7cd4be29fad6913aa4d753899cb0ef851aa", + "tag": "210", + "pr": "Math- #210", + "head": "213dd9eb8ba83de242516b10c999fbe56d17fd3f", + "use": "Math- #210 v1.3 (open): the classical crest-to-trough literature and the d = 1 remark whose leading constant 0.19971814 this note proves on the line (Remark 3); comparison only" + } + ], + "cited_external": [ + { + "tag": "Ingham", + "reference": "A. E. Ingham, Some trigonometrical inequalities with applications to the theory of series, Math. Z. 41 (1936) 367-379; R. M. Young, An Introduction to Nonharmonic Fourier Series (2001), ch. 4 sec. 1", + "use": "Lemma 4.3_R: a lower bound for the covariance of w-separated f'-samples, uniform in their number" + }, + { + "tag": "GC", + "reference": "Gaussian concentration for functions Lipschitz along the Cameron-Martin space (Borell; Tsirelson-Ibragimov-Sudakov); Bogachev, Gaussian Measures (1998), Thm 4.5.7; Ledoux, The Concentration of Measure Phenomenon (2001), sec. 2.1", + "use": "Lemma 4.4_R" + }, + { + "tag": "SF-BTIS", + "reference": "Sudakov-Fernique comparison and the Borell-TIS inequality", + "use": "Lemmas 3.1_R and 4.4_R; the local parts of [1D] and [1D+]" + }, + { + "tag": "Maruyama", + "reference": "a stationary Gaussian sequence with covariance tending to 0 is mixing", + "use": "Lemma 1.5_R" + }, + { + "tag": "Bulinskaya", + "reference": "Bulinskaya's lemma", + "use": "Lemma 1.1_R and the process under Q" + } + ], + "mutants": { + "M1": "C1", + "M2": "C4", + "M3": "C2", + "M4": "C3", + "M5": "C5", + "M6": "C6", + "M7": "C6" + }, + "label_history": "v1 (f34ffd7, opened 2026-10-04 06:46Z) assumed |rho^(j)(x)| <= C (1 + |x|)^-1 for j <= 2, and Lemma 4.3_R bounded the conditional covariance by a Schur complement with small cross-covariances. v1.1, before any nonauthor pickup, drops that hypothesis: Lemma 4.3_R uses interlacing (at most three eigenvalues drop) and loses three powers of eps; Lemma 4.1_R gets the pin covariance from Riemann-Lebesgue; Lemma F_R uses at least 23 cells. The theorem, its rates and its constants are unchanged; checker C5 and C6 updated, mutant M7 added.", + "replayed": [ + "line_check.py" + ], + "delivered_under": "explicit owner instructions of Dylan Roy in claude.ai session session_01NMeKEismAyeqgdB4sy2NJU: \"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, no register/GRAPH/STATUS/lemma_closed/prize/premise edits, OWNER_STOP.md untouched. The author does not merge its own PR.", + "files": [ + { + "path": "PROOF.md", + "bytes": 38349, + "sha256": "e8e401bd82cabd3f876812c1089f5c0bf3a6240c48b836776aed8f535489c7a9" + }, + { + "path": "README.md", + "bytes": 7259, + "sha256": "1ace3aa3cbaa0bb2b34ab954c9d9a742ffd9e1ef33845dcbc1ee9a1317a51f5b" + }, + { + "path": "line_check.py", + "bytes": 22809, + "sha256": "c65101264b1de6615518ee76eac584a4525b5bd363da96898b4f7eb8d193a6cf" + }, + { + "path": "RESULTS.json", + "bytes": 4245, + "sha256": "4ddcf4d664d4c115c172393be15f463764a49b0f730b540b3de1a40224c5bae2" + } + ], + "referee": { + "kind": "two clean-context same-family referees (Anthropic Claude subagents) on the draft before submission: A on slices A-B (sections 0-2 and 5, including a line-by-line search of [1D] and [1D+] for global objects), B on slices C-D (sections 3-5, the constants and line_check.py); same provider as the author, zero independence credit", + "verdict": "first pass: A ACCEPT WITH MINOR FIXES (slices A and B), B ACCEPT WITH MINOR FIXES (slices C and D), no MAJOR. Delta check of the revision: every finding FIXED; A: slice A ACCEPT, slice B one wrong reference introduced by the B3 fix (applied: E_Q(K^e)^2 is used in (Phi.1), (Phi.3) and Proposition M, not Lemma E) and two NITs (applied); B: slice C ACCEPT, slice D one provenance wording in the README (applied: the R0 correction was the author's, before the referees) and NITs (applied: T0 >= t0 in Lemma 3.1_R, the quotient-norm infimum, omega in SOURCES kind, the S-shaped cubic count now uses an upper bound for osc). The second referee's scratch import left a __pycache__ directory in the packet, which was removed", + "applied": [ + "A1: the marks are defined Q-almost surely for every (t, alpha): the process under Q is m_{t,h} + X with a bounded mean and a residual X independent of V (section 1)", + "A2-A3: the Kac-Rice marks are compact-window Borel functions or increasing limits of them; the window space is C^2([-r, 1 + 1/eps + r])", + "A4: Lemma 1.5_R uses the Riemann-Lebesgue lemma, not (R3a)", + "A5: x_+- defined as an infimum/supremum (the first point above f(M) does not exist)", + "B1, B3-B6: section 2 lists the parts that transfer (including the adjacency estimate of [1D] section 5 and the (0, t_*] part of [1D+] section 4) and how each global part is replaced; the [t1, t0] step of [1D] Lemma 4.3 is read with the supremum over the band; the extra uses of [1D+] section 3 are listed", + "B2/C-3: symbol clashes removed (cell length w, pin margin a, count n_R, Lipschitz constant sigma_F, constants C_Y, C_m, C_q, C_K; delta is only [1D]'s exponent)", + "C-1/O2: Lemma 4.2_R stated for any interval with midpoint y; Lemma 3.1_R uses J = [y_i - t0/16, y_i + t0/16]", + "C-2: the Cameron-Martin space of the restricted conditioned residual, with the quotient norm", + "C-4: the geometric ratios are <= 1/2 for small h", + "C-5 to C-8: the truncation level b_h, the case osc = 0, T0 >= t0, M2 = (mu_w + 2 lambda4^(1/2))^2, and \"A >= 1\" removed", + "D-1 to D-4 and O1, O3, O4: RESULTS.json and SOURCES.json added; section 8 describes the S-shaped cubics, and C3 and C5 describe what is checked at sample values; Remark 3 cites #210 v1.3 for the O(1) claim", + "author before the referees: the threshold of Lemma 4.4_R was R0 = 4(M2^(1/2) + 1), which does not give R/sqrt(2) - R/4 >= R/2; it is now 5(M2^(1/2) + 1) (checker C6, mutant M6)" + ], + "v1_1_delta": "second delta check by the same referees on v1.1: A slice A ACCEPT WITH MINOR FIXES (the section 0 sentence on [1D] section 6.4's \"uniform nondegeneracy of separated values\", applied) and slice B ACCEPT; B slice C ACCEPT (one NIT: prove Gamma(x+1) >= (x/e)^x in the text, applied) and slice D ACCEPT WITH MINOR FIXES (regenerate SOURCES.json with M7, applied; README slice list, applied); other NITs applied (README table order, (R3) wording, provenance sentence). Referee B checked the interlacing under the actual pinned law for the sinc kernel (at most 2 eigenvalues of Cov(Y|V) below lambda_min(Sigma_YY) in 24 configurations with samples at the pins) and the ball-volume chain for k up to 10^6", + "independent_checks": "referee B: constants at 40 digits (mpmath) match the printed values; the Gaussian C2 row sums are 0.82207664, 0.17774501 and 0.010063879, and 1 - 5.2948e-7 at spacing 1; Plancherel and F(g)^2 <= sigma_F^2 ||g||^2 sampled on 200 RKHS elements (max ratio 0.069); Ingham with w = 4 pi on [1, 2] (min Gram eigenvalue 0.709 over 400 sets); the Lemma 4.3_R chain for the sinc kernel; Landau on 3000 random functions (max ratio 0.52)" + } +} diff --git a/frontiers/d1_line_20261004/line_check.py b/frontiers/d1_line_20261004/line_check.py new file mode 100644 index 000000000..912d0f9dc --- /dev/null +++ b/frontiers/d1_line_20261004/line_check.py @@ -0,0 +1,504 @@ +#!/usr/bin/env python3 +"""Exact controls for Theorem 1D_R (CL-D1-LINE-20261004-v1): Theorems 1D and 1D+ on the line. + +Standard library only. Exact rationals (fractions.Fraction) for C1, C2, C4, C5 and C6. C3 evaluates the closed-form +constants of [1D] section 0 in floating point and compares them with the printed 8-decimal values. Output: one JSON +document on stdout, equal to RESULTS.json. + + python3 -B -S line_check.py # exit 0 + python3 -B -S line_check.py --mutant M3 # exit 1 (each mutant breaks its own control) + python3 -B -S line_check.py --mutant XX # exit 2 (unknown label) + +Notation as in PROOF.md section 4: w is an interval (cell) length or a sample spacing, sigma_F the Lipschitz constant +of Lemma 4.4_R. + +Scientific effect: NONE. The controls check the elementary inequalities, constants and summations that the proof uses +(PROOF.md section 8). They do not check the probabilistic steps. +""" +import json +import math +import sys +from fractions import Fraction as Fr + +OBJECT = 'CL-D1-LINE-20261004-v1.1' + +MUTANTS = { + 'M1': 'C1: the Landau bound without the term 2 osc/|Delta|', + 'M2': 'C4: the cell Sobolev constant 1 in place of 2', + 'M3': 'C2: the Gaussian sample spacing w = 1 in place of 2', + 'M4': 'C3: C0 without its factor 2', + 'M5': 'C5: the band exponent 23 A^2/(32 sigma_F^2) in place of 23 A^2/(16 sigma_F^2)', + 'M6': 'C6: the threshold R0 = 4 (M2^(1/2) + 1) in place of 5 (M2^(1/2) + 1)', + 'M7': 'C6: only r - 1 small eigenvalues allowed after a rank-r conditioning', +} + + +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: line_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 trim(p): + p = [Fr(a) for a in p] + while p and p[-1] == 0: + p.pop() + return p + + +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 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 pder(p): + return trim([i * p[i] for i in range(1, len(p))]) + + +def peval(p, x): + acc = Fr(0) + for a in reversed(p): + acc = acc * x + a + return acc + + +def pint(p, a, b): + """exact integral of p over [a, b]""" + anti = [Fr(0)] + [c / (i + 1) for i, c in enumerate(p)] + return peval(anti, b) - peval(anti, a) + + +def show(p): + return '[' + ', '.join(map(str, p)) + ']' + + +class Lcg: + def __init__(self, seed): + self.x = seed + + def nxt(self): + self.x = (6364136223846793005 * self.x + 1442695040888963407) % (1 << 64) + return self.x >> 33 + + def frac(self, den): + """a rational in [-1, 1] with denominator den""" + return Fr(self.nxt() % (2 * den + 1) - den, den) + + +def ceil_dec(x, digits): + """decimal string of the rational x rounded up (towards +infinity) at the given number of digits""" + scale = 10 ** digits + n = -((-x.numerator * scale) // x.denominator) + sign = '-' if n < 0 else '' + n = abs(n) + return '%s%d.%0*d' % (sign, n // scale, digits, n % scale) + + +def floor_dec(x, digits): + """decimal string of the rational x >= 0 rounded down at the given number of digits""" + scale = 10 ** digits + n = (x.numerator * scale) // x.denominator + return '%d.%0*d' % (n // scale, digits, n % scale) + + +# ---------------------------------------------------------------- C1: Landau's inequality on an interval (Lemma 4.2_R) + +def landau_case(c, w, grid=64, steps=40): + """g(s) = sum c[k] s^k on Delta = [-w/2, w/2], midpoint 0, |Delta| = w. + Returns |g'(0)|, a lower and an upper bound for osc_Delta g, S = sup_Delta |g''| (exact), and the Taylor-step + verdict. Upper bound: every point is within w/(2 grid) of a grid point, and |g'| <= sum k |c_k| (w/2)^(k-1).""" + g = trim(c) + g1 = pder(g) + g2 = pder(g1) + half = w / 2 + cands = [-half, half] + if len(g2) == 3: + v = -g2[1] / (2 * g2[2]) + if -half < v < half: + cands.append(v) + S = max(abs(peval(g2, x)) for x in cands) + pts = [-half + w * Fr(k, grid) for k in range(grid + 1)] + vals = [peval(g, x) for x in pts] + for k in range(grid): + lo, hi = pts[k], pts[k + 1] + flo, fhi = peval(g1, lo), peval(g1, hi) + if flo != 0 and fhi != 0 and (flo > 0) != (fhi > 0): + for _ in range(steps): + mid = (lo + hi) / 2 + fm = peval(g1, mid) + if (fm > 0) == (flo > 0): + lo, flo = mid, fm + else: + hi = mid + vals.append(peval(g, lo)) + vals.append(peval(g, hi)) + osc = max(vals) - min(vals) + slope = sum(k * abs(ck) * half ** (k - 1) for k, ck in enumerate(g) if k >= 1) + osc_up = osc + (w / grid) * slope + a = abs(peval(g1, Fr(0))) + taylor = True + for u in (half, half / 2, half / 4, half / 8): + taylor = taylor and abs(2 * u * peval(g1, Fr(0))) <= abs(peval(g, u) - peval(g, -u)) + u * u * S + return a, osc, osc_up, S, taylor + + +def landau_holds(a, osc, S, w, mutant): + """|g'(y)| <= (osc S)^(1/2) + 2 osc/|Delta|, decided exactly: + with b = 2 osc/|Delta|, either a <= b or (a - b)^2 <= osc S""" + b = Fr(0) if mutant == 'M1' else 2 * osc / w + return a <= b or (a - b) ** 2 <= osc * S + + +def control_c1(mutant): + rng = Lcg(20261004) + lengths = [Fr(1, 2), Fr(1), Fr(2), Fr(3), Fr(4), Fr(25, 2)] + n = 0 + sqrt_needed = 0 + for w in lengths: + cases = [] + for _ in range(40): + # degree <= 4, scaled to the interval: g(s) = sum c_k (2 s/w)^k + cases.append([rng.frac(9) * (2 / w) ** k for k in range(5)]) + for _ in range(10): + # S-shaped cubics g = A s (1 - (2s/w)^2) + small terms: |g'(y)| exceeds 2 osc/|Delta| + A = 1 + abs(rng.frac(9)) + cases.append([rng.frac(9) / 50, A, rng.frac(9) / (50 * w), -4 * A / w ** 2]) + for c in cases: + a, osc, osc_up, S, taylor = landau_case(c, w) + check(taylor, 'C1 Taylor step fails (|Delta|=%s, g=%s)' % (w, show(c))) + check(landau_holds(a, osc, S, w, mutant), 'C1 Landau bound fails (|Delta|=%s, g=%s)' % (w, show(c))) + if a > 2 * osc_up / w: + sqrt_needed += 1 + n += 1 + check(sqrt_needed >= len(lengths) * 10, 'C1 the S-shaped cubics should need the term (osc S)^(1/2)') + # the nearly affine family g = s + eps s^2 on a unit interval: |g'(0)| = 1, osc = 1, S = 2 eps + affine = {} + for eps in (Fr(1, 10), Fr(1, 100), Fr(1, 1000), Fr(1, 10 ** 6)): + a, osc, osc_up, S, taylor = landau_case([Fr(0), Fr(1), eps], Fr(1)) + check(a == 1 and osc == 1 and S == 2 * eps and taylor, 'C1 nearly affine family: exact values') + check(landau_holds(a, osc, S, Fr(1), mutant), + 'C1 Landau bound fails on the nearly affine family (eps=%s)' % eps) + check(osc * S < a * a, "C1 nearly affine family: (osc S)^(1/2) < |g'(0)|") + affine[str(eps)] = {"|g'(0)|": '1', 'osc': '1', 'S': str(S), 'osc*S': str(osc * S)} + return {'interval_lengths': [str(w) for w in lengths], 'polynomials_tested': n, + "cases_with_|g'(y)|>2osc/|Delta|_(osc_bounded_above)": sqrt_needed, + 'nearly_affine_g=s+eps*s^2_unit_interval': affine, + 'reading': "both terms are needed: the S-shaped cubics have |g'(y)| > 2 osc/|Delta|, and on the nearly " + "affine family |g'(y)|^2 = 1 > osc*S = 2 eps"} + + +# ---------------------------------------------------------------- C2: Gaussian f'-samples, diagonal dominance + +def exp_neg_upper(x, n=40): + """e^(-x) <= 1/sum_{j<=n} x^j/j! for rational x >= 0""" + s, term = Fr(0), Fr(1) + for j in range(n + 1): + s += term + term = term * x / (j + 1) + return 1 / s + + +def rowsum_upper(w, m=6): + """an upper bound for 2 sum_{k>=1} |1 - k^2 w^2| e^(-k^2 w^2/2) (requires w >= 1)""" + tot = Fr(0) + for k in range(1, m): + x = k * k * w * w + tot += abs(1 - x) * exp_neg_upper(x / 2) + # k >= m: |1 - k^2 w^2| <= k^2 w^2 and e^(-k^2 w^2/2) <= q^k with q = e^(-m w^2/2); + # sum_{k>=m} k^2 q^k <= m^2 q^m sum_{j>=0} (1+j)^2 q^j = m^2 q^m (1+q)/(1-q)^3 + q = exp_neg_upper(m * w * w / 2) + check(0 < q < 1, 'C2 tail ratio') + tail = w * w * m * m * q ** m * (1 + q) / (1 - q) ** 3 + return 2 * (tot + tail) + + +def control_c2(mutant): + res = {} + bound = Fr(5, 6) + spacings = [Fr(2), Fr(3), Fr(4)] if mutant != 'M3' else [Fr(1), Fr(3), Fr(4)] + for w in spacings: + u = rowsum_upper(w) + check(u <= bound, 'C2 row sum bound %s exceeds 5/6 at w=%s' % (ceil_dec(u, 8), w)) + res['w=%s' % w] = {'row_sum_upper': ceil_dec(u, 8), 'lambda_min_lower': floor_dec(1 - u, 8)} + # monotonicity for w >= 2: d/dx (x^2 - 1) e^(-x^2/2) = x (3 - x^2) e^(-x^2/2), negative once x^2 > 3 + lhs = padd(pder([Fr(-1), Fr(0), Fr(1)]), pmul([Fr(-1), Fr(0), Fr(1)], [Fr(0), Fr(-1)])) + check(lhs == [Fr(0), Fr(3), Fr(0), Fr(-1)], 'C2 derivative identity') + check(Fr(2) ** 2 > 3, 'C2 k w >= 2 > sqrt(3)') + res['monotone_for_w>=2'] = "((x^2-1) e^(-x^2/2))' = x (3 - x^2) e^(-x^2/2) < 0 for x >= 2" + res['conclusion'] = 'lambda_min >= 1 - 5/6 = 1/6 for every spacing w >= 2 and every N (Gershgorin)' + return res + + +# ---------------------------------------------------------------- C3: the constants of [1D] section 0, Gaussian kernel + +def control_c3(mutant): + lam = {2: Fr(1), 4: Fr(3), 6: Fr(15), 8: Fr(105)} # (2j - 1)!! + l2, l4, l6, l8 = lam[2], lam[4], lam[6], lam[8] + D = l2 * l6 - l4 ** 2 + s3sq, s4sq = D / l2, l8 - l6 ** 2 / l4 + Q = 4 * l2 ** 2 * l4 * l8 + 26 * l2 * l4 ** 2 * l6 - 5 * l2 ** 2 * l6 ** 2 - 25 * l4 ** 4 + check(D == 6 and s3sq == 6 and s4sq == 30 and Q == 1620, 'C3 Gaussian moments') + check(Q / (120 * l2 * l4 * D) == Fr(3, 4), 'C3 Q/(120 l2 l4 D) = 3/4') + check(Q == 4 * l2 ** 2 * (l4 * l8 - l6 ** 2) + D * (25 * l4 ** 2 - l2 * l6) + and Q == 4 * l2 ** 2 * l4 * s4sq + D * (24 * l4 ** 2 - D), 'C3 decomposition of Q at the Gaussian moments') + check(l2 * l6 <= 25 * l4 ** 2, 'C3 sufficient condition for B2 > 0') + s3, s4 = math.sqrt(float(s3sq)), math.sqrt(float(s4sq)) + p12 = 1 / (2 * math.pi * math.sqrt(float(l2 * l4))) + pref = 2.0 if mutant != 'M4' else 1.0 + C0 = pref * 72 ** (-1 / 6) * math.gamma(7 / 6) * (2 * math.pi) ** -0.5 * p12 * s3 ** (4 / 3) + mu = 2 ** (7 / 8) * math.gamma(11 / 8) / math.sqrt(math.pi) + C1 = -(8 / 21) * 24 ** 0.25 * mu * (2 * math.pi) ** -0.5 * p12 * s4 ** 1.75 / s3 + C1b = (-(2 ** (25 / 8) / 7) * 3 ** -0.75 * math.pi ** -2 * math.gamma(11 / 8) * s4 ** 1.75 / s3 + * float(l2 * l4) ** -0.5) + check(abs(C1 - C1b) <= 1e-12 * abs(C1), 'C3 the two printed forms of C1') + I = 3 ** 0.25 / 2 * C1 + B2 = 2 ** 0.5 * 3 ** (1 / 3) * math.gamma(5 / 6) * (2 * math.pi) ** -0.5 * p12 * s3 ** (2 / 3) * float(Fr(3, 4)) + rate = math.sqrt(float(l4 / l2)) / (2 * math.pi) + got = {'C0': '%.8f' % C0, 'C1': '%.8f' % C1, 'I': '%.8f' % I, 'B2': '%.8f' % B2, + 'per_crest_h^(-1/3)': '%.8f' % (C0 / 2 / rate), 'per_crest_h^(1/4)': '%.8f' % (I / 2 / rate), + 'per_crest_h^(1/3)': '%.8f' % (B2 / rate)} + printed = {'C0': '0.11011038', 'C1': '-0.22760636', 'I': '-0.14977341', 'B2': '0.11502229', + 'per_crest_h^(-1/3)': '0.19971814', 'per_crest_h^(1/4)': '-0.27165891', + 'per_crest_h^(1/3)': '0.41725471'} + for k in sorted(printed): + check(got[k] == printed[k], 'C3 %s = %s, printed %s' % (k, got[k], printed[k])) + check('%.5f' % (B2 / rate) == '0.41725', 'C3 [1D] prints the h^(1/3) per-crest coefficient as 0.41725') + check('%.8f' % rate == '%.8f' % (math.sqrt(3) / (2 * math.pi)), 'C3 rate of maxima sqrt(3)/(2 pi)') + return {'lambda_2j': ['1', '3', '15', '105'], 'D': str(D), 'sigma3^2': str(s3sq), 'sigma4^2': str(s4sq), + 'Q': str(Q), 'Q/(120 l2 l4 D)': '3/4', 'values_8_decimals': got, 'rate_of_maxima': '%.8f' % rate} + + +# ---------------------------------------------------------------- C4: the cell Sobolev bound + +def sobolev_case(c, w, grid=256): + """u(s) = sum c[k] (s/w)^k on [0, w]: an exact lower bound and a rigorous upper bound for sup|u|, and the base + w^-1 int u^2 + w int u'^2""" + u = trim([ck / w ** k for k, ck in enumerate(c)]) + du = pder(u) + I0 = pint(pmul(u, u), Fr(0), w) + I1 = pint(pmul(du, du), Fr(0), w) + M1 = sum(k * abs(ck) for k, ck in enumerate(c)) / w # >= sup |u'| on [0, w] + eta = w / grid + lo = max(abs(peval(u, w * Fr(j, grid))) for j in range(grid + 1)) + up = lo + eta / 2 * M1 + return lo, up, I0 / w + w * I1 + + +def control_c4(mutant): + rng = Lcg(4102026) + const = Fr(2) if mutant != 'M2' else Fr(1) + lengths = [Fr(1, 2), Fr(1), Fr(2), Fr(4), Fr(25, 2)] + n = 0 + worst = Fr(0) + witness = {} + for w in lengths: + cases = [[Fr(1), Fr(0), Fr(1, 2)]] # the witness 1 + (s/w)^2/2 + cases += [[rng.frac(9) for _ in range(6)] for _ in range(30)] + for c in cases: + lo, up, base = sobolev_case(c, w) + check(up * up <= const * base, 'C4 Sobolev bound fails (w=%s, u=%s)' % (w, show(c))) + if base > 0: + worst = max(worst, lo * lo / base) + n += 1 + lo, up, base = sobolev_case(cases[0], w) + check(lo * lo == Fr(9, 4) and base == Fr(103, 60), 'C4 the witness is scale invariant') + witness['w=%s' % w] = {'sup_u^2': str(lo * lo), "w^-1 int u^2 + w int u'^2": str(base)} + check(Fr(9, 4) > Fr(103, 60), 'C4 the constant 1 is false') + return {'polynomials_tested': n, 'interval_lengths': [str(w) for w in lengths], + "max_sup^2/(w^-1 int u^2 + w int u'^2)": ceil_dec(worst, 6), + 'witness_u=1+(s/w)^2/2': witness, + 'sharp_constant_coth(1)_float': '%.6f' % (math.cosh(1.0) / math.sinh(1.0)), + 'reading': 'the bound holds with constant 2; constant 1 fails on the witness (9/4 > 103/60)'} + + +# ---------------------------------------------------------------- C5: the summation of Lemma F_R, at sample values + +def control_c5(mutant): + res = {} + for x in (Fr(1, 2), Fr(1, 3), Fr(1, 10), Fr(1, 1000)): + for M in (23, 30, 50): + s = sum(x ** n for n in range(23, M + 1)) + check(s == (x ** 23 - x ** (M + 1)) / (1 - x), 'C5 geometric partial sum') + check(x ** 23 / (1 - x) <= 2 * x ** 23, 'C5 x^23/(1-x) <= 2 x^23') + check(Fr(1, 2) ** 4 == Fr(1, 16), 'C5 q^(1/4) <= 1/2 iff q <= 1/16') + res['geometric'] = ('sum_{n=23}^{M} x^n = (x^23 - x^(M+1))/(1-x) and x^23/(1-x) <= 2 x^23 for x in ' + '{1/2, 1/3, 1/10, 1/1000}; the ratios are <= 1/2 when q <= 1/16 and ' + 'h^(A^2/(16 sigma_F^2)) <= 1/2') + for r in (Fr(1, 3), Fr(2, 7), Fr(1, 100)): + q = 4 * r * r # q = 4 r^2, so q/4 = r^2 and q^(1/2) = 2 r + for N in range(23, 61, 2): # odd N: N/2 - 3 = (N - 6)/2, half-integer + lhs = 2 ** N * (r * r) ** ((N - 7) // 2) * r # (q/4)^(N/2 - 3) = r^(N - 6) + rhs = 64 * q ** ((N - 7) // 2) * (2 * r) # 64 q^(N/2 - 3) = 64 q^((N-7)/2) q^(1/2) + check(lhs == rhs, 'C5 2^N (q/4)^(N/2-3) = 64 q^(N/2-3)') + for N in range(24, 61, 2): + check(2 ** N * (r * r) ** ((N - 6) // 2) == 64 * q ** ((N - 6) // 2), 'C5 2^N (q/4)^(N/2-3) = 64 q^(N/2-3)') + res['union_bound_step'] = '2^N (q/4)^(N/2-3) = 64 q^(N/2-3) with q/4 = eps (2e/lambda_*)^(1/2)' + w = Fr(5, 2) + T0 = 24 * w + for t in (T0, T0 + Fr(1, 7), T0 + 3 * w, T0 + 100): + N = (t - 2 * w) // w + 1 + check(N >= 23, 'C5 N >= 23') + check(-t / 2 + w + (N - 1) * w <= t / 2 - w, 'C5 the last point lies in [-tau + w, tau - w]') + check((N + 1) // 2 >= 12, 'C5 |G| = ceil(N/2) >= 12 >= 6') + res['N(t)'] = 'N = floor((t - 2w)/w) + 1 >= 23 for t >= 24 w, y_(N-1) <= tau - w, and ceil(N/2) >= 12 (at w = 5/2)' + A2_over_sigma2 = Fr(2) # the smallest admissible A^2/sigma_F^2 + exp_h = (Fr(23, 32) if mutant == 'M5' else Fr(23, 16)) * A2_over_sigma2 + check(exp_h > 2, 'C5 band exponent %s not > 2' % exp_h) + exp_q = (Fr(23, 4) - Fr(3, 2)) * Fr(1, 2) # q^(23/4 - 3/2) = q^(17/4), q ~ h^(1/2) + log_q = (Fr(23, 4) - Fr(3, 2)) * Fr(1, 4) + check(exp_q == Fr(17, 8) and exp_q > 2 and log_q == Fr(17, 16), 'C5 q-exponents') + res['exponents'] = {'h^(23 A^2/(16 sigma_F^2)) at A^2 = 2 sigma_F^2': str(exp_h), + 'q^(N/4 - 3/2) at N = 23, with q = O(h^(1/2) log^(1/4))': 'h^(%s) log^(%s)' % (exp_q, log_q), + 'margin over h^2': str(min(exp_h, exp_q) - 2)} + check(Fr(1, 2) * Fr(1, 8) == Fr(1, 16), 'C5 square root of the banded probability') + res['square_root'] = 'P^(1/2) <= exp(-N R^2/(16 sigma_F^2)) + 8 q^(N/4 - 3/2)' + return res + + +# ---------------------------------------------------------------- C6: the ingredients of Lemmas 4.3_R and 4.4_R + +def negative_pivots(S): + """number of negative eigenvalues of the symmetric rational matrix S, by exact LDL^T without pivoting + (Sylvester's law of inertia); returns None if a zero pivot occurs""" + n = len(S) + M = [row[:] for row in S] + neg = 0 + for i in range(n): + piv = M[i][i] + if piv == 0: + return None + if piv < 0: + neg += 1 + for r in range(i + 1, n): + f = M[r][i] / piv + if f: + for c in range(i, n): + M[r][c] -= f * M[i][c] + return neg + + +def e_bounds(): + lo, t = Fr(0), Fr(1) + for j in range(30): + lo += t + t = t / (j + 1) + return lo, lo + 2 * t # the tail after 30 terms is below twice the next term + + +def control_c6(mutant): + res = {} + rng = Lcg(97531) + lam = Fr(1, 3) + cases = attained = 0 + for k in (4, 5, 6, 8, 10): + for r in (1, 2, 3): + for _ in range(6): + Mx = [[rng.frac(5) for _ in range(k)] for _ in range(k)] + MMt = [[sum(Mx[i][l] * Mx[j][l] for l in range(k)) for j in range(k)] for i in range(k)] + us = [[rng.frac(7) for _ in range(k)] for _ in range(r)] + S = [[MMt[i][j] - sum(u[i] * u[j] for u in us) for j in range(k)] for i in range(k)] + neg = negative_pivots(S) # A - P - lam Id = M M^T - P + if neg is None: + continue + check(neg <= r, 'C6 interlacing: %d negative eigenvalues after a rank-%d downdate' % (neg, r)) + cases += 1 + # a family that attains r: P = c sum_{s<=r} e_s e_s^T with c > trace(M M^T) + Mx = [[rng.frac(5) for _ in range(k)] for _ in range(k)] + MMt = [[sum(Mx[i][l] * Mx[j][l] for l in range(k)) for j in range(k)] for i in range(k)] + c = sum(MMt[i][i] for i in range(k)) + 1 + S = [[MMt[i][j] - (c if i == j and i < r else 0) for j in range(k)] for i in range(k)] + neg = negative_pivots(S) + check(neg is not None and neg == r, 'C6 the attaining family') + allowed = r - 1 if mutant == 'M7' else r + check(neg <= allowed, + 'C6 interlacing allows only %d small eigenvalues after a rank-%d conditioning' % (allowed, r)) + attained += 1 + res['interlacing'] = {'random_cases': cases, 'attaining_cases': attained, + 'statement': 'A - P - lam Id has at most rank(P) negative eigenvalues when A - lam Id >= 0'} + elo, ehi = e_bounds() + sqrtpi_lo = Fr(17724, 10000) # sqrt(pi) = 1.77245... + check(sqrtpi_lo ** 2 < Fr(314159, 100000), 'C6 sqrt(pi) lower bound') + for m in range(3, 301): + # Gamma(m/2 + 1) >= (m/(2e))^(m/2), i.e. Gamma(m/2 + 1)^2 >= (m/(2e))^m; use e >= elo + if m % 2 == 0: + n = m // 2 + g2 = Fr(1) + for i in range(2, n + 1): + g2 *= i + g2 = g2 * g2 + else: + # Gamma(n + 3/2) = (2n+2)! sqrt(pi)/(4^(n+1) (n+1)!) + n = (m - 1) // 2 + num, den = 1, 1 + for i in range(2, 2 * n + 3): + num *= i + for i in range(2, n + 2): + den *= i + g2 = (Fr(num, 4 ** (n + 1) * den) * sqrtpi_lo) ** 2 + check(g2 >= (Fr(m, 2) / elo) ** m, 'C6 Stirling lower bound fails at m=%d' % m) + for k in range(6, 200): + check(Fr(k, k - 3) <= 2, 'C6 k/(k-3) <= 2') + res['stirling'] = 'Gamma(m/2 + 1) >= (m/(2e))^(m/2) for 3 <= m <= 300; k/(k-3) <= 2 for k >= 6' + c = Fr(4) if mutant == 'M6' else Fr(5) + check((Fr(1, 2) + 1 / c) ** 2 <= Fr(1, 2), + 'C6 threshold R0 = %s (M2^(1/2) + 1) does not give R/sqrt(2) - R/%s >= R/2' % (c, c)) + res['R0_threshold'] = {'R0': '%s (M2^(1/2) + 1)' % c, '(1/2 + 1/%s)^2' % c: str((Fr(1, 2) + 1 / c) ** 2), + 'needed': '<= 1/2'} + check((Fr(1, 2) + Fr(1, 4)) ** 2 > Fr(1, 2), 'C6 the factor 4 fails') + res['factor_4_fails'] = '(1/2 + 1/4)^2 = 9/16 > 1/2' + 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)] + out = {'object': OBJECT, '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()