diff --git a/.github/workflows/d1-third-order-law.yml b/.github/workflows/d1-third-order-law.yml new file mode 100644 index 000000000..f0c561424 --- /dev/null +++ b/.github/workflows/d1-third-order-law.yml @@ -0,0 +1,70 @@ +name: D1 third-order law controls + +'on': + pull_request: + paths: + - 'frontiers/d1_third_order_law_20261001/**' + - '.github/workflows/d1-third-order-law.yml' + # bound merged sources (cited_only in SOURCES.json) + - 'reviews/literature_lifetime_law_recon_20260929/RECONNAISSANCE.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: 15 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('frontiers/d1_third_order_law_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']) + for entry in manifest['consumed'] + manifest['cited_only']: + data = pathlib.Path(entry['path']).read_bytes() + framed = b'blob ' + str(len(data)).encode() + b'\0' + data + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256'] or hashlib.sha1(framed).hexdigest() != entry['git_blob']: + raise ValueError('merged source drifted: ' + entry['path']) + if manifest.get('consumed_unmerged'): + raise ValueError('this packet declares no unmerged dependency') + script = str(root / 'd1_check.py') + expected = (root / 'RESULTS.json').read_bytes() + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], check=True, capture_output=True, timeout=600).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in manifest['mutants']: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], capture_output=True, timeout=600).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + rc = subprocess.run([sys.executable, *flags, script, '--mutant', 'M9'], capture_output=True, timeout=600).returncode + if rc != 2: + raise RuntimeError('unknown mutant label not rejected with exit 2') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/frontiers/d1_third_order_law_20261001/PROOF.md b/frontiers/d1_third_order_law_20261001/PROOF.md new file mode 100644 index 000000000..1591ecee3 --- /dev/null +++ b/frontiers/d1_third_order_law_20261001/PROOF.md @@ -0,0 +1,506 @@ +# The one-dimensional lifetime and crest-to-trough laws to third order: `C₀ℓ^{−1/3} + C₁ℓ^{1/4} + 2B₂ℓ^{1/3} + O(ℓ^{1/2})` + +Object: CL-D1-THIRD-ORDER-20261001-v1.3. +Author: Anthropic Claude (claude.ai session `session_01NMeKEismAyeqgdB4sy2NJU`), 1 October 2026. +**v1.1 (after the Codex review of v1 on Math- #214, head `2aedcaa`):** (i) the sign of `B₂` is not fixed by (H) — v1's +README asserted `B₂ > 0`; §0 now gives the decomposition `𝒬 = 4λ₂²λ₄σ₄² + D(24λ₄² − D)`, the sufficient condition +`λ₂λ₆ ≤ 25λ₄²` and Codex's counterexample (checker C5); (ii) v1's far form of Lemma 4.2 claimed a bounded joint density +of `(f'(y_i), f''(±τ))` given `U`, which is false as the pins merge (`v₁ ≍ τ⁴`, `v₂ ≍ τ⁶`); it now states and proves the +bound that Lemma 4.3 uses — the density of `(f'(y_i))` conditional on `U` *and* `f''(±τ)` — and Lemma 4.3's far part now +controls the conditional mean of `f''` under `Q` explicitly. The theorem's statement is unchanged. +**v1.2 (label only; xAI concern on #214, comments 5940492097 and 5940563636):** the theorem is renamed **Theorem 1D** +(dimension one), and its displays (1D.1)–(1D.2), so that it is not read as the cap component D1 (Math- #193, #194). No +mathematical change. The object identifier and the paths keep `D1`/`d1`, which there mean dimension one; `d1_check.py` +and `RESULTS.json` are byte-identical to v1.1. +**v1.3 (clarifications requested by the nonauthor reviews; no change to any statement, constant or control):** (i) the +four manuscript clarifications listed in the OpenAI Codex acceptance of Slices A–D (Math- #214, comment 5933752065): +`f_o(τ) = −h/2` in the proof of Lemma 3.2 (a sign typo; the solved coefficients were already right); `0 ≤ α ≤ τ^{−1}` in +Lemma 1.3; in Lemma 4.3 the band bound on `[t₁, t₀]` with the explicit `√log` cutoffs, which give `O(h(log(1/h))^{3/2})` +in place of the printed `O(h log(1/h))` (comment 5931058934; both are `o(h^{3/4})`); and the global-maximum alternative +in the negative case of Lemma 3.3 (R). (ii) §6.3's attribution, narrowed as the Slice E review asked (review 5387031124, +E-LIT): Pérez calls smooth random-field topology an open research area, and does not single out this short-bar law. +`d1_check.py` and `RESULTS.json` are byte-identical to v1.1. +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. +**Dependencies: none.** The proof is self-contained (Gaussian conditioning, the two-point Kac–Rice formula, Taylor's +formula, Markov's polynomial inequality). Cited for comparison only: Math- #207 (Theorem CU, `d ≥ 2`; its (CU.2) at +`d = 1` is this note's `C₁`, §6.1), Math- #210 (the `d = 1` remark whose leading constant this note proves), and the +merged literature reconnaissance `reviews/literature_lifetime_law_recon_20260929/RECONNAISSANCE.md`. + +## 0. Statement + +**Setting.** `T = R/LZ` (`L > 0`) and `f` a centered stationary Gaussian process on `T` with covariance +`ρ(x) = E f(0)f(x)`, under the hypothesis + +> **(H)** `ρ ∈ C^∞(T)` and `ρ̂(n) := L^{−1}∫_T ρ(x)e^{−2πinx/L}dx > 0` for every `n ∈ Z`. + +Example: the periodization `Σ_k e^{−(x+kL)²/2}` of the Gaussian kernel (`ρ̂(n) = (2π)^{1/2}L^{−1}e^{−2π²n²/L²}`), the +one-dimensional analogue of the SIDE24 torus field. Write `λ_{2j} := (−1)^jρ^{(2j)}(0)`, `a_j := f^{(j)}(0)`, + + D := λ₂λ₆ − λ₄², σ₃² := D/λ₂ = Var(a₃ | a₁), σ₄² := λ₈ − λ₆²/λ₄ = Var(a₄ | a₂), + p₁₂ := (2π)^{−1}(λ₂λ₄)^{−1/2} = density of (a₁, a₂) at 0, p₃(α) := (2πσ₃²)^{−1/2}e^{−α²/(2σ₃²)}. + +**Objects.** By (H) and Lemma 1.1, almost surely `f` is a Morse function with finitely many critical points, alternating +maxima and minima, with pairwise distinct critical values. For a local maximum `M`: + +- the **crest-to-trough amplitude** `H(M) := f(M) − f(S⁺(M))`, `S⁺(M)` the next critical point in the positive + direction (a minimum); +- if `M` is not the global maximum, the **persistence lifetime** `ℓ(M) := f(M) − d(M)` of the superlevel filtration, + `d(M) := sup_γ min f∘γ` over paths from `M` to points higher than `f(M)` (the elder rule; in one dimension + `d(M) = max(m₋, m₊)`, `m_±` the minimum of `f` along the arc from `M` in direction `±` up to the first point higher + than `f(M)`). The point where `d(M)` is attained is a minimum `S(M)`, `M`'s **death point** (elder partner). + +The intensities `Λ₊(B) := L^{−1}E#{M : H(M) ∈ B}` and `Λ(B) := L^{−1}E#{M not global : ℓ(M) ∈ B}` are absolutely +continuous; `ν₊`, `ν` denote 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^{1/2}), (1D.1) + ν(ℓ) = C₀ ℓ^{−1/3} + C₁ ℓ^{1/4} + 2B₂ ℓ^{1/3} + O(ℓ^{1/2}), (1D.2) + +with, writing `μ_q := E|Z|^q` for a standard normal `Z` (`μ_{7/4} = 2^{7/8}Γ(11/8)π^{−1/2}`), + + 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}/σ₃ = −(2^{25/8}/7) 3^{−3/4} π^{−2} Γ(11/8) σ₄^{7/4} σ₃^{−1}(λ₂λ₄)^{−1/2}, + I = (3^{1/4}/2) C₁, + B₂ = 2^{1/2}3^{1/3} Γ(5/6) (2π)^{−1/2} p₁₂ σ₃^{2/3} · 𝒬/(120λ₂λ₄D), 𝒬 := 4λ₂²λ₄λ₈ + 26λ₂λ₄²λ₆ − 5λ₂²λ₆² − 25λ₄⁴. + +So `C₁ < 0 < C₀`; `I − C₁ = (1 − 3^{1/4}/2)|C₁| > 0` is the density coefficient of adjacent max/min pairs that are +not elder pairs, `2ν₊(ℓ) − ν(ℓ) = (I − C₁)ℓ^{1/4} + O(ℓ^{1/2})`. + +**The sign of `B₂`** is that of `𝒬`, and (checker C5) + + 𝒬 = 4λ₂²(λ₄λ₈ − λ₆²) + D(25λ₄² − λ₂λ₆) = 4λ₂²λ₄σ₄² + D(24λ₄² − D), + +so `B₂ > 0` whenever `λ₂λ₆ ≤ 25λ₄²` (the Gaussian kernel has `λ₂λ₆/λ₄² = 5/3`, the mixture of §6.2 `1625/867`). The sign +is not fixed by (H) (Codex, review of v1 on #214): for `L = 2π` and the spectrum with weights `1 − 10⁻⁵` and `10⁻⁵` at the +frequencies `1` and `40`, `λ₂λ₆/λ₄² ≈ 58.8` and `𝒬 ≈ −7.09·10⁸ < 0`; adding small positive, rapidly decaying weights at +every other frequency gives (H) and, `𝒬` being continuous in `(λ₂, λ₄, λ₆, λ₈)`, keeps `𝒬 < 0`. + +For the Gaussian kernel (`λ_{2j} = (2j − 1)!!`; the periodization changes them by `O(L^{2j}e^{−L²/2})`, invisible +below for `L ≥ 10`): `C₀ = 0.11011038`, `C₁ = −0.22760636`, `I = −0.14977341`, `B₂ = 0.11502229`, `𝒬/(120λ₂λ₄D) = 3/4`. Per +crest (dividing `ν₊` by the rate `(2π)^{−1}(λ₄/λ₂)^{1/2}` of maxima) the crest-to-trough density is +`f_H(h) = 0.19971814 h^{−1/3} − 0.27165891 h^{1/4} + 0.41725 h^{1/3} + O(h^{1/2})`; its leading constant is #210's. + +**Mechanism.** A short bar is a fold: a maximum `M` and an adjacent minimum `S` at separation `t` with gap +`h ≈ αt³/12`, `α ≈ f'''`. Integrating the fold law over `t` gives `C₀h^{−1/3}` (scale `t ≍ h^{1/3}`). At `t ≍ h^{1/4}` +the quartic jet competes with the cubic (the cusp): on that scale the pair sees the quartic ridge +`g(X) = κ[2(X + ½)²(X − 1) + 3φ(X² − ¼)²]`, `κ = h/t⁴`, `φ = f''''/(72κ)` — the case `d = 1` of #207's ridge — and the +pair is adjacent iff `|φ| < 1`, an elder pair iff `|φ| < 1/3`; the fold law overcounts there, and integrating the +deficit over the scale gives the `h^{1/4}` terms. The `h^{1/3}` term collects the `τ²`-corrections of the pinned law at +the fold scale and the finite part of the cusp integrand's `τ`-tail (§2). + +**What is not claimed.** No statement on `R` (§6.4); no uniformity in the covariance; no explicit constant in the +`O(·)`; the `O(h^{1/2})` is not claimed sharp (the proof gives `O(h^{0.57})` for (1D.1); the numerics of §6.2 suggest +the next terms are `O(h^{3/4})`). + +## 1. Two-point representation and the pinned law + +**Lemma 1.1 (nondegeneracy).** For distinct `x₁, …, x_k ∈ T` and any `J`, the Gaussian vector +`(f^{(j)}(x_i))_{i ≤ k, j ≤ J}` is nondegenerate. Hence `f` is a.s. Morse with distinct critical values. + +*Proof.* `f(x) = Σ_n ρ̂(n)^{1/2}ξ_n e^{2πinx/L}` with independent standard complex Gaussians (`ξ_{−n} = ξ̄_n`). A linear +combination `Σ c_{ij}f^{(j)}(x_i)` has variance `Σ_n ρ̂(n)|P(n)|²`, `P(n) := Σ_{i,j}c_{ij}(2πin/L)^j z_i^n`, +`z_i := e^{2πix_i/L}` distinct; it vanishes iff `P(n) = 0` for all `n ∈ Z` (as all `ρ̂(n) > 0`), i.e. iff all the +polynomial coefficients vanish (the sequences `n^j z_i^n` are linearly independent: their generating functions have +poles of distinct locations). The Morse property and the distinctness of critical values then follow from Bulinskaya's +lemma applied to `(f', f'')` and to `(f'(x), f'(y), f(x) − f(y))` on `{x ≠ y}`. ∎ + +**The pair coordinates.** By stationarity put the maximum at `−τ` and the other critical point at `τ`, `t := 2τ ∈ (0, L)` +the distance from `−τ` to `τ` in the positive direction. Define + + U₁ := (f'(−τ) + f'(τ))/2, U₂ := (f'(τ) − f'(−τ))/t, U₃ := (6/t²)(f'(−τ) + f'(τ)) + 12(f(−τ) − f(τ))/t³. + +On the pin event `{f'(±τ) = 0, f(−τ) − f(τ) = h}` one has `U = (0, 0, α)`, `α := 12h/t³`, and the linear map +`(f'(−τ), f'(τ), f(−τ) − f(τ)) ↦ U` has determinant `12/t⁴`. Let `p_t(α)` be the density of `U` at `(0, 0, α)` and +`Q = Q_{t,α}` the conditional law of `f` given `U = (0, 0, α)`; set `κ := h/t⁴ = α/(12t)`. + +**The canonical versions.** The marked two-point Kac–Rice formula (e.g. Azaïs–Wschebor 2009, Ch. 6, for zeros of +`(f'(x), f'(y))` on `{x ≠ y}` with a bounded Borel weight; the marked form is the one-dimensional case of the argument +of [P] §9 as repaired in [E2]) gives, for bounded Borel `ψ ≥ 0` and Borel marks `𝔪`, +`L^{−1}E Σ_{(x,y)} 𝔪 ψ(f(x) − f(y)) = ∫ψ(h)∫₀^L (12/t⁴)p_t(α)E_Q[(−f''(−τ))⁺f''(τ)⁺𝔪]dt dh`, the sum over ordered pairs +`(x, y)` of a local maximum `x` and a local minimum `y` (the weight `(−f''(−τ))⁺f''(τ)⁺` vanishes on the other types), with +`y` at distance `t ∈ (0, L)` from `x` in the positive direction. With `𝔪 = 1{f' < 0 on (−τ, τ)}` (then `τ = S⁺(−τ)`) and +`𝔪 = 1{τ = S(−τ)}`: + + ν₊(h) := ∫₀^L K₊(t, h) dt, K₊(t, h) := (12/t⁴) p_t(α) E_Q[(−f''(−τ))⁺ f''(τ)⁺ 1{f' < 0 on (−τ, τ)}], (1.2) + ν(ℓ) := ∫₀^L K(t, ℓ) dt, K(t, ℓ) := (12/t⁴) p_t(α) E_Q[(−f''(−τ))⁺ f''(τ)⁺ 1{τ = S(−τ)}]. (1.3) + +Reflection `x ↦ −x` preserves the law and maps a pair at positive distance `t` to one at `L − t`, so `K(t, ℓ) = K(L − t, ℓ)` +and `ν(ℓ) = 2∫₀^{L/2}K(t, ℓ)dt`. + +**Lemma 1.2 (reflection structure).** Under `Q_{t,α}`: `E_Q f''(±τ) = ±c(t)α` for a function `c(t)`; with +`E₁ := (f''(τ) + f''(−τ))/2` and `E₂ := (f''(τ) − f''(−τ))/2 − c(t)α`, the pair `(E₁, E₂)` is centered Gaussian with a +law independent of `α`, `Cov(E₁, E₂) = 0`, variances `v₁(t), v₂(t)`, and with `m := c(t)α` + + −f''(−τ) = m − E₁ + E₂, f''(τ) = m + E₁ + E₂, (−f''(−τ))⁺f''(τ)⁺ = ((m + E₂)² − E₁²)⁺ 1{m + E₂ > 0}. (1.4) + +*Proof.* Let `R f := f(−·)`; `Rf` has the law of `f`. Then `U(Rf) = (−U₁, U₂, −U₃)(f)` and `(Rf)''(±τ) = f''(∓τ)`. +Conditional means are linear in the conditioning value: `E_Q f''(±τ) = m_±α`. By invariance, +`m₊α = E[(Rf)''(τ) | U(Rf) = (0,0,α)] = E[f''(−τ) | U(f) = (0, 0, −α)] = −m₋α`; so `m₊ = −m₋ =: c(t)`, and `E₁` is +centered. Conditional covariances do not depend on the conditioning value, and the same invariance gives +`Var_Q f''(τ) = Var_Q f''(−τ)`, i.e. `Cov(E₁, E₂) = 0`. The last identity: for `m + E₂ > 0` the product of the two +factors is `(m + E₂)² − E₁²`, positive iff `m + E₂ > |E₁|`; if `m + E₂ ≤ 0` the factors have nonpositive sum. ∎ + +**Lemma 1.3 (expansions).** As `τ ↓ 0` (none of the first five quantities depends on `α`), + + c(t) = τ(1 + c₂τ² + O(τ⁴)), c₂ = −(λ₂λ₈ − λ₄λ₆)/(15D), + det Cov(U) = λ₄D(1 + d₂τ² + O(τ⁴)), d₂ = (8λ₄²λ₆ − 3λ₂λ₄λ₈ − 5λ₂λ₆²)/(15λ₄D), + [Cov(U)^{−1}]₃₃ = σ₃^{−2}(1 + q₂τ² + O(τ⁴)), q₂ = (λ₂²λ₈ − 6λ₂λ₄λ₆ + 5λ₄³)/(5λ₂D), + v₁(t) = (τ⁴σ₄²/9)(1 + O(τ²)), v₂(t) = (τ⁶/225)(λ₁₀ − (λ₆³ − 2λ₄λ₆λ₈ + λ₂λ₈²)/D)(1 + O(τ²)), + +and `p_t(α) = (2π)^{−3/2}(det Cov U)^{−1/2}exp(−α²[Cov(U)^{−1}]₃₃/2)`. In particular +`p_t(α) = p₁₂p₃(α)(1 + τ²u(α) + O(τ⁴(1 + α⁴)))` for `0 ≤ α ≤ τ^{−1}`, `u(α) := −d₂/2 − q₂α²/(2σ₃²)`, and +`p_t(α) ≤ Ce^{−α²/(4σ₃²)}` for all `α` and `τ ≤ τ₀`. Each quantity is an even function of `τ` (`c` odd). + +*Proof.* Taylor's formula at `0` (all `a_j`, remainders bounded by `τ^K sup|f^{(K+1)}|`) gives + + U₁ = a₁ + a₃τ²/2 + a₅τ⁴/24 + …, U₂ = a₂ + a₄τ²/6 + a₆τ⁴/120 + …, U₃ = a₃ + a₅τ²/10 + a₇τ⁴/280 + …, + (f''(τ) − f''(−τ))/2 = τ(U₃ + a₅τ²/15 + a₇τ⁴/210 + …), E₁ = U₂ + a₄τ²/3 + a₆τ⁴/30 + …, + +(the coefficient of `a₁` in `U₃` cancels: `(3/τ²)a₁ − (3/τ³)a₁τ = 0`), with `E a_ia_j = (−1)^{(i−j)/2}λ_{i+j}` for `i ≡ j` +mod 2 and `0` otherwise. Odd and even jets are independent, so `{U₁, U₃, (f''(τ) − f''(−τ))/2}` is independent of +`{U₂, E₁}`; `Cov(U)` is block diagonal. Then (i) `c(t)α = E[(f''(τ) − f''(−τ))/2 | U₁ = 0, U₃ = α] = τ(α + (τ²/15)E[a₅ | +U₁ = 0, U₃ = α] + O(τ⁴α))` and `E[a₅ | a₁ = 0, a₃ = α] = α(λ₄λ₆ − λ₂λ₈)/D`; (ii) `Var U₁ = λ₂ − λ₄τ² + O(τ⁴)`, +`Var U₃ = λ₆ − λ₈τ²/5 + O(τ⁴)`, `Cov(U₁, U₃) = −λ₄ + (3/5)λ₆τ² + O(τ⁴)`, so `det Cov(U₁, U₃) = D − (τ²/5)(λ₂λ₈ − λ₄λ₆) ++ O(τ⁴)`, `[Cov U^{−1}]₃₃ = Var U₁/det Cov(U₁, U₃)` and `Var U₂ = λ₄ − λ₆τ²/3 + O(τ⁴)`, which give `q₂` and `d₂`; (iii) +`v₁ = Var(E₁ | U₂) = (τ⁴/9)Var(a₄ | a₂)(1 + O(τ²))`; (iv) `E₂ = τ³(a₅ − E[a₅ | U₁, U₃])/15 + O(τ⁵)`, whence `v₂`. Evenness: +`U` is invariant under `τ ↦ −τ` (which exchanges the pins) and `(f''(τ) − f''(−τ))/2` changes sign. The bounds on +`p_t` follow from `Cov U → Cov(a₁, a₂, a₃)` (nondegenerate). ∎ + +(Checker C4 verifies every coefficient above exactly, as Laurent series with rational coefficients computed from the +covariance itself — not through the jets — for two kernels.) + +**Remark 1.4 (parity split).** Put `f_e(x) := (f(x) + f(−x))/2` and `f_o(x) := (f(x) − f(−x))/2`. Since `ρ` is even, +`Cov(f_e(x), f_o(y)) = 0`, so the Gaussian processes `f_e` and `f_o` are independent. `U₁ = f_o'(τ)`, +`U₃ = (12/t²)f_o'(τ) − (24/t³)f_o(τ)` and `(f''(τ) − f''(−τ))/2 = f_o''(τ)` are functionals of `f_o`, while +`U₂ = 2f_e'(τ)/t` and `E₁ = f_e''(τ)` are functionals of `f_e`. Hence under `Q` the processes `f_e` and `f_o` remain +independent, and `E₁` is independent of `f_o`. + +## 2. The sign kernels and their asymptotics + +For `θ ∈ {1, 1/3}` define the **sign kernels** (explicit functions of `(t, h)`; `m = c(t)α`) + + K_θ^{sign}(t, h) := (12/t⁴) p_t(α) G_θ, G₁ := E((m + E₂)² − E₁²)⁺1{m + E₂ > 0}, G_{1/3} := E((m + E₂)² − E₁²)⁺1{m + E₂ > 0}1{|E₁| < m/3}, + +the expectations over independent `E₁ ~ N(0, v₁)`, `E₂ ~ N(0, v₂)`. By (1.4), `K₁^{sign}` is the two-point density of +(maximum, minimum) pairs with gap `h` *without* the adjacency mark; `K_{1/3}^{sign}` adds the window `|φ_G| < 1/3`, +`φ_G := E₁/m`, which §3 shows is the elder rule at the pair scale. For `Z` standard normal and `s ≥ 0` put + + γ_θ(s) := E[(s² − Z²)1{|Z| < θs}] = s² − ζ_θ(s), ζ_θ(s) := E[Z²1{|Z| < θs}] + s²P(|Z| ≥ θs), + +so `0 ≤ ζ_θ(s) ≤ C min(1, s²)` and `|1 − ζ_θ(s)| ≤ C(1 + s²)e^{−θ²s²/2}`; `ζ₁(s) = E min(Z², s²)`. + +**Lemma 2.1 (Mellin integrals).** `∫₀^∞ ζ_θ(s)s^{−5/4}ds = k_θμ_{7/4}` with `k_θ = 4θ^{1/4} + (4/7)θ^{−7/4}`: +`k₁ = 32/7`, `k_{1/3} = (64/7)3^{−1/4}`; hence `k₁/k_{1/3} = 3^{1/4}/2`. + +*Proof.* Fubini: for fixed `z`, `∫₀^∞(z²1{|z| < θs} + s²1{|z| ≥ θs})s^{−5/4}ds = z²∫_{|z|/θ}^∞ s^{−5/4}ds + +∫₀^{|z|/θ}s^{3/4}ds = |z|^{7/4}(4θ^{1/4} + (4/7)θ^{−7/4})`. ∎ + +**Proposition 2.2.** Fix `δ ∈ (0, 1/10]` and put `t_* := (12h)^{1/(5 − δ)}`, so that `t ≤ t_*` iff `α ≥ t^{2−δ}`. Then + + ∫₀^{t_*} K_θ^{sign}(t, h) dt = (C₀/2) h^{−1/3} + (I_θ/2) h^{1/4} + B₂ h^{1/3} + O(h^{0.57}), I₁ := I, I_{1/3} := C₁. + +*Proof.* **(a) The `E₂`-correction.** Put `g_θ(m, v₁) := E(m² − E₁²)⁺1{|E₁| < θm}`. For fixed `a := |E₁|` the map +`e ↦ (m + e − a)⁺(m + e + a)` is convex (it vanishes for `e ≤ a − m` and equals `(m + e)² − a²` beyond, with right +derivative `2a ≥ 0` at the kink), and `E₂` is centered and independent of `E₁`; hence +`0 ≤ G_θ − g_θ ≤ v₂ + 2E[|E₁||E₂|1{||E₁| − m| ≤ |E₂|}]`. In the straddle term, on `{|E₂| ≤ m/2}` one has +`|E₁| ∈ [m/2, 3m/2]`, where the density of `|E₁|` is `≤ Cv₁^{−1/2}e^{−s²/8}` (`s := m v₁^{−1/2}`); the complement has +`E[|E₁||E₂|1{|E₂| > m/2}] ≤ C(v₁v₂)^{1/2}e^{−m²/(8v₂)}`, and `m²/v₂ ≍ α²/τ⁴ ≥ t^{−2δ}` on `{t ≤ t_*}`. Hence +`0 ≤ G_θ − g_θ ≤ C(v₂ + m v₂ v₁^{−1/2}e^{−s²/8}) + O(t^{N})` for every `N`. With `v₁ ≍ τ⁴`, `v₂ ≍ τ⁶`, `m ≍ τα`, +`s ≍ α/t`: the error kernel is `≤ C p_t(α)(t² + αt e^{−cα²/t²}) ≤ C t²` (as `xe^{−cx²}` is bounded), and +`∫₀^{t_*}Ct²dt = O(t_*³) = O(h^{3/(5−δ)})`. + +**(b) Scaling.** `g_θ(m, v₁) = v₁γ_θ(s)` with `s := m v₁^{−1/2}`, so `(12/t⁴)p_t g_θ = (12/t⁴)p_t m² − (12/t⁴)p_t v₁ζ_θ(s)`. + +**(c) The fold part.** By Lemma 1.3, `(12/t⁴)p_t m² = (3α²/t²)p₁₂p₃(α)[1 + τ²(u(α) + 2c₂) + O(τ⁴(1 + α⁴))]` for +`α ≤ τ^{−1}` (the complement, `t < (6h)^{1/2}`, contributes `O(e^{−c/h})` to this and to every term below, since there +`α ≥ τ^{−1} ≥ ch^{−1/2}` and `p_t(α) ≤ Ce^{−α²/(4σ₃²)}`). Substituting `α = 12h/t³`, +`dt = (1/3)(12h)^{1/3}α^{−4/3}dα`, `τ² = (12h/α)^{2/3}/4`: + + ∫₀^∞ (3α²/t²)p₁₂p₃(α) dt = p₁₂(12h)^{−1/3}∫₀^∞ α^{4/3}p₃(α)dα = (C₀/2)h^{−1/3}, + ∫₀^∞ (3α²/t²)p₁₂p₃(α)τ²(u(α) + 2c₂) dt = (1/4)p₁₂(12h)^{1/3}∫₀^∞ α^{2/3}p₃(α)(u(α) + 2c₂)dα =: B₂^{(1)}h^{1/3}, + +the `τ⁴`-term gives `O(h)`, and the part `t > t_*` of the first integral is `O(h²t_*^{−7}) = O(h^{0.57})`. + +**(d) The cusp part.** For `α ≤ τ^{−1}`, `(12/t⁴)p_t v₁ζ_θ(s) = (σ₄²/12)p₁₂p₃(α)ζ_θ(s₀)(1 + ε)` with `s₀ := 3α/(τσ₄)` +and `|ε| ≤ Cτ²(1 + α²)`: by Lemma 1.3, `(12/t⁴)v₁ = (σ₄²/12)(1 + O(τ²))`, `p_t = p₁₂p₃(α)(1 + O(τ²(1 + α²)))` and +`s = s₀(1 + O(τ²))`, while `|ζ_θ'(s)| ≤ C min(s, e^{−θ²s²/4})` and `ζ_θ(s₀) ≥ c min(1, s₀²)`. Note `s₀ = 72h/(σ₄t⁴)`. Split `p₃(α) = p₃(0) + (p₃(α) − p₃(0))`: + +- `p₃(0)∫₀^∞ζ_θ(s₀(t))dt = p₃(0)(72h/σ₄)^{1/4}(1/4)∫₀^∞ζ_θ(s)s^{−5/4}ds = p₃(0)(72h/σ₄)^{1/4}k_θμ_{7/4}/4` (Lemma 2.1); + with the prefactor `−σ₄²p₁₂/12` this is `(I_θ/2)h^{1/4}`: + `I_θ/2 = −(σ₄²/48)(72/σ₄)^{1/4}k_θμ_{7/4}p₁₂p₃(0)`, i.e. `I = −(4/21)72^{1/4}…`, `C₁ = −(8/21)24^{1/4}μ_{7/4}(2π)^{−1/2}p₁₂σ₄^{7/4}/σ₃`. +- `∫₀^∞(p₃(α) − p₃(0))ζ_θ(s₀)dt = ∫₀^∞(p₃(α) − p₃(0))dt − ∫₀^∞(p₃(α) − p₃(0))(1 − ζ_θ(s₀))dt`. The first equals + `(1/3)(12h)^{1/3}∫₀^∞(p₃(α) − p₃(0))α^{−4/3}dα` (convergent at both ends); with the prefactor this is + `B₂^{(2)}h^{1/3}`, `B₂^{(2)} := −(σ₄²p₁₂/36)12^{1/3}∫₀^∞(p₃(α) − p₃(0))α^{−4/3}dα > 0`. The second is `O(h^{3/4})`: + `|p₃(α) − p₃(0)| ≤ C min(1, α²)` and `|1 − ζ_θ(s₀)| ≤ C(1 + s₀²)e^{−θ²s₀²/2}`; on `{s₀ ≤ 1}` = `{t ≥ ct_c}`, + `t_c := h^{1/4}`, use `α² = 144h²t^{−6}`; on `{s₀ ≥ 1}` substitute `t = (72h/(σ₄s₀))^{1/4}`. +- The error `ε`: on `{t ≤ t_c}` it is `≤ C∫₀^{t_c}τ²dt`, on `{t ≥ t_c}` use `ζ_θ(s₀) ≤ Cs₀² = Ch²t^{−8}`; both `O(h^{3/4})`. +- The part `t > t_*`: `ζ_θ(s₀) ≤ Cs₀²`, so `O(h²t_*^{−7})`. + +**(e) Closed forms.** `∫₀^∞α^{q}p₃(α)dα = σ₃^q 2^{(q−1)/2}Γ((q + 1)/2)(2π)^{−1/2}` (`q > −1`) gives `C₀`. Since +`Γ(11/6) = (5/6)Γ(5/6)`, `∫₀^∞α^{8/3}p₃ = (5/3)σ₃²∫₀^∞α^{2/3}p₃`, so `B₂^{(1)} = (1/4)·12^{1/3}p₁₂M(2c₂ − d₂/2 − 5q₂/6)`, +`M := ∫₀^∞α^{2/3}p₃ = 2^{−1/6}Γ(5/6)(2π)^{−1/2}σ₃^{2/3}`; and `∫₀^∞(e^{−x²/2} − 1)x^{−4/3}dx = 2^{−7/6}Γ(−1/6) = +−6·2^{−7/6}Γ(5/6)` gives `B₂^{(2)} = 12^{1/3}p₁₂M·σ₄²/(12σ₃²)`. Then + + B₂ := B₂^{(1)} + B₂^{(2)} = 12^{1/3}p₁₂M[(2c₂ − d₂/2 − 5q₂/6)/4 + σ₄²/(12σ₃²)] = 12^{1/3}p₁₂M·𝒬/(120λ₂λ₄D), + +the last equality being the polynomial identities `30λ₂λ₄D(2c₂ − d₂/2 − 5q₂/6) = −6λ₂²λ₄λ₈ + 26λ₂λ₄²λ₆ + 5λ₂²λ₆² − +25λ₄⁴` and `120λ₂λ₄D·σ₄²/(12σ₃²) = 10λ₂²(λ₄λ₈ − λ₆²)`, whose sum is `𝒬` (checker C5). Collecting (a)–(d) proves the +proposition. ∎ + +## 3. Adjacency and the elder rule at the pair scale + +Write `K₅ := sup_{[−2t, 2t]}(|f^{(5)}| + |f^{(6)}|)`. + +**Lemma 3.1 (Rolle).** If `f'(±τ) = 0` and `f'` has two further zeros in `(−τ, τ)`, then `|U₃| ≤ 5τ²K₅`. + +*Proof.* `f''''` vanishes at some `ξ ∈ (−τ, τ)` and `f'''` at two points, so `|f'''| ≤ t²K₅` on `[−τ, τ]`, in particular +`|a₃| ≤ 4τ²K₅`; and `|U₃ − a₃| ≤ (3/(2τ²))(2τ⁴K₅/24) + (3/(2τ³))(2τ⁵K₅/120) = (3/20)τ²K₅`. ∎ + +**Lemma 3.2 (the window field; #207 Theorem CU.1 at `d = 1`).** Let `f(−τ) = b`, `f(τ) = b − h`, `f'(±τ) = 0`, +`𝔉(X) := [f(tX) − b]/h` and `g(X) := 2(X + ½)²(X − 1) + 3φ(X² − ¼)²` with `φ := f''''(0)t⁴/(72h)`. With +`K^o := sup_{[−2t,2t]}|f_o^{(5)}|` and `K^e := sup_{[−2t,2t]}|f_e^{(6)}|` (Remark 1.4), +`‖𝔉 − g‖_{C²([−2, 2])} ≤ C(tK^o + t²K^e)/κ`. + +*Proof.* As in #207 (CU.1) with no transverse variable, divided by `κ`, keeping track of parity. The even pins +`f_e'(τ) = 0` and `f_e(τ) = b − h/2` involve only even jets and even remainders (of order 6 for `f_e`); the odd pins +`f_o'(τ) = 0` and `f_o(τ) = −h/2` only odd jets and odd remainders (of order 5). They give `ϑ₂ = −(t²/24)f₄ + O(K^et⁴)`, +`ϑ₀ − b = (−κ/2 + f₄/384)t⁴ + O(K^et⁶)`, `ϑ₃ = 12κt + O(K^ot²)` and `ϑ₁ = −(3/2)κt³ + O(K^ot⁴)`, and `t^{−4}` times the +degree-4 Taylor polynomial is `κg`. The Taylor remainder is `O(K^o|x|⁵ + K^e|x|⁶)`. After division by `h = κt⁴`, each +correction and its two `X`-derivatives are `O((tK^o + t²K^e)/κ)` on `[−2, 2]`. ∎ + +The model has `g(−½) = 0`, `g(½) = −1`, `g'(X) = 6(X + ½)(X − ½)(1 + 2φX)`, the third critical point `X₃ = −1/(2φ)`, and + + g(X) = (X + ½)²[2(X − 1) + 3φ(X − ½)²], g(X) + 1 = (X − ½)²[2(X + 1) + 3φ(X + ½)²], + g(X₃) = (φ − 1)³(3φ + 1)/(16φ³), g(X₃) + 1 = (φ + 1)³(3φ − 1)/(16φ³). (3.1) + +**Lemma 3.3 (the window decides, with margins).** Let `η ∈ (0, 1/4]`, `F ∈ C²([−2, 2])` with `F(−½) = 0`, `F(½) = −1`, +`F'(±½) = 0`, `F''(−½) < 0 < F''(½)`, and `‖F − g‖_{C²([−2,2])} ≤ ε ≤ c₀η` (`c₀` absolute). Let `𝔐, 𝔖` be the points +`−½, ½` of the rescaled field `F = 𝔉`. Then: +(E) if `|φ| ≤ 1/3 − η`, `𝔖` is `𝔐`'s death point; +(R) if `|φ| ≥ 1/3 + η`, `𝔖` is not `𝔐`'s death point. (Typing forces `|φ| < 1 + ε/6`, since `g''(∓½) = ∓6(1 ∓ φ)`.) + +*Proof.* (E) From (3.1), for `|φ| ≤ 1/3`: the bracket `2(X − 1) + 3φ(X − ½)²` is at most `−1` on `[−3/2, −½]` (convex or +increasing in `X`, value `−5 + 12φ ≤ −1` at `−3/2` and `−3 + 3φ ≤ −2` at `−½`), so `g ≤ −(X + ½)²` there and +`g(−3/2) = −5 + 12φ ≤ −1 − 12η` when `φ ≤ 1/3 − η` (and `≤ −5` when `φ ≤ 0`); and for `φ ≥ −1/3` the bracket +`2(X + 1) + 3φ(X + ½)² ≥ 2(X + 1) − (X + ½)² ≥ 1` on `[½, 3/2]`, so `g + 1 ≥ (X − ½)²` there, while +`g(3/2) = 4(1 + 3φ) ≥ 12η`. On `[−½, ½]`, `g' < 0` (as `1 + 2φX > 0`), so `g ∈ (−1, 0)` inside. With `ε` small, `F` keeps +these sign patterns: near `±½` by `F''(−½) ≤ g''(−½) + ε = −6(1 − φ) + ε < 0` and `F''(½) ≥ 6(1 + φ) − ε > 0`, away +from `±½` by the quadratic margins. Hence the arc from `𝔐` in the negative direction reaches `F(−3/2) < −1` while +`F < 0`, so `m₋ < −1`; the arc in the positive direction stays `> −1` except at `𝔖` and exceeds `0` at `3/2`, so +`m₊ = −1 = F(𝔖)`. Thus `d(𝔐) = max(m₋, m₊) = F(𝔖)`. +(R) If `1/3 + η ≤ φ < 1`: `X₃ ∈ (−3/2, −½)` is the only critical point of `g` in `[−2, −½)`, a minimum with +`g(X₃) + 1 = (φ + 1)³(3φ − 1)/(16φ³) ≥ (3φ − 1)/2 ≥ 3η/2` (as `(1 + 1/φ)³/16 ≥ 1/2` for `φ ≤ 1`), and +`g(−2) = (9/4)(−6 + 75φ/4) ≥ 9/16`; so `F > −1 + η` on `[−2, −½]` and `F(−2) > 0`: the negative arc from `𝔐` exceeds +`F(𝔐)` before reaching `−1`, `m₋ > −1 = F(𝔖)`, and `d(𝔐) ≥ m₋ > F(𝔖)`. +If `−1 < φ ≤ −1/3 − η`: `X₃ ∈ (½, 3/2)` is a maximum with `g(X₃) ≤ (3φ + 1)/2 ≤ −3η/2`, `g(2) + 1 = (9/4)(6 − 75|φ|/4) ≤ +−9/16`, and `g < 0` on `(−½, 2]`; so the positive arc from `𝔐` falls below `−1` before exceeding `0`: `m₊ < −1`; and +`m₋ < −1` as in (E) (`φ < 0`). Then `d(𝔐) < F(𝔖)` if `𝔐` is not the global maximum; if it is, `𝔐` has no finite +partner. Either way `𝔖` is not `𝔐`'s death point. (Lemma 3.3 is applied only through Corollary 3.4, for `t ≤ t_*`, where +Lemma 3.2 makes `ε` small.) +If `1 ≤ φ < 1 + ε/6`: `g' < 0` on `[−2, −½)` (the factor `1 + 2φX` is negative there), so `g ≥ 0` on `[−2, −½]`, +`g(−2) ≥ 9/16`, and `F ≥ −ε > −1` there with `F(−2) > 0`: `m₋ > −1`. If `−1 − ε/6 < φ ≤ −1`: the bracket +`2(X + 1) + 3φ(X + ½)² ≤ 2(X + 1) − 3(X + ½)² < 0` on `(½, 2]`, so `g < −1` there and the (R) argument for `φ < 0` applies +verbatim. ∎ + +(Checker C3 verifies (3.1), the critical-point structure, the margins used above, and the decision itself by exact +one-dimensional persistence of the quartic for 117 rational `φ`.) + +**Corollary 3.4 (the elder decision at the pair scale).** On `{t ≤ t_*}` (i.e. `α ≥ t^{2−δ}`) let `(−τ, τ)` be a typed +pair and define `φ_G := E₁/m`. Then `|φ_G − φ| ≤ C(τ²|φ| + t²K^e/κ)` and, outside the event + + 𝔅 := {C(tK^o/κ + t²K^e/κ + τ²) ≥ c₀ min(||φ_G| − 1/3|, 1/4)}, + +`τ = S(−τ)` iff `|φ_G| < 1/3`. + +*Proof.* `E₁ = f_e''(τ)` and, on `U₂ = 0`, `a₂ = −a₄τ²/6 + O(τ⁴K^e)`, so `E₁ = a₄τ²/3 + O(τ⁴K^e)`; `m = τα(1 + c₂τ² + O(τ⁴))` +(Lemma 1.3); and `φ = a₄t⁴/(72h) = a₄τ/(3α)`. So `φ_G = φ(1 − c₂τ² + O(τ⁴)) + O(τ³K^e/α)`, and `τ³/α = τ²/(24κ)`. Apply +Lemma 3.3 with `ε = C(tK^o + t²K^e)/κ` (Lemma 3.2) and `η := min(||φ| − 1/3|, 1/4)`, transported from `φ` to `φ_G` by +the first bound (the deterministic `τ²` term is why `𝔅` contains `τ²`). ∎ + +## 4. Thin pairs: the band lemma and the flat band + +A pair at `±τ` with gap `h` is **banded** if `f(τ) ≤ f ≤ f(−τ)` on `[−τ, τ]` (the arc of length `t`), and +**co-banded** if the same holds on the complementary arc (length `L − t`). Every adjacent typed pair (crest-to-trough) +is banded (monotone). An elder pair is banded or co-banded: `f > f(S)` and `f ≤ f(M)` along the arc on which the death +value `d(M) = m_±` is attained, i.e. the arc from `M` to its death point (not necessarily the arc of length `t`). + +**Lemma 4.1 (band lemma).** Let `k ≥ 4`, `t ≤ 1`, the pair banded with gap `h`, and `K := sup_{[−τ,τ]}|f^{(k+2)}|`. Then +`|a_j| ≤ C_k(h + τ^{k+2}K)τ^{−j}` for `1 ≤ j ≤ k + 1`, and `|f''(±τ)| ≤ C_k(hτ^{−2} + τ^kK)`. + +*Proof.* With `P` the Taylor polynomial of `f` at `0` of degree `k + 1`, `|f − P| ≤ τ^{k+2}K/(k + 2)!` on `[−τ, τ]`, so +`|P − f(τ) − h/2| ≤ h/2 + τ^{k+2}K`; Markov's inequality for polynomials of degree `k + 1` on `[−τ, τ]` bounds +`P^{(j)}(0) = a_j`, and `f''(±τ) = P''(±τ) + O(τ^kK)`. ∎ + +**Lemma 4.2 (interior values).** For fixed `−1 < ξ₁ < … < ξ_N < 1` with `∫_{−1}^1 Π_{i}(ξ − ξ_i)(ξ² − 1)dξ ≠ 0`, the +conditional density under `Q_{t,α}` of `(f'(τξ_i))_{i ≤ N}` is at most `C τ^{−N(N+5)/2}` for `τ ≤ τ₀`. (Far form) Fix +`t₀ ∈ (0, L/4]`. For points `y₁, …, y_N` at mutual distances `≥ t₀/8` and at distance `≥ t₀/4` from both pins, the +conditional density of `(f'(y_i))_{i ≤ N}` given `U`, and also given `(U, f''(−τ), f''(τ))`, is at most `C`, uniformly +in `t ∈ (0, L)` and in such points. (The joint density of `(f'(y_i), f''(±τ))` given `U` is *not* bounded: as `t ↓ 0` +the pair `f''(±τ)` has conditional variances `v₁ ≍ τ⁴` and `v₂ ≍ τ⁶`, Lemma 1.3. v1 stated that joint bound; Lemma 4.3 +uses only the conditional one.) + +*Proof.* `(f'(−τ), f'(τ), f(−τ) − f(τ), f'(τξ₁), …, f'(τξ_N)) = A_τ(a₁, …, a_{N+3}) + O(τ^{N+3})`, where `A_τ = +B·diag(τ^{j−1})` up to one factor `τ` in the integral row and `B` (evaluations of polynomials of degree `N + 2` at +`−1, 1, ξ_i` and the integral over `[−1, 1]`) is invertible by the stated condition; so the covariance determinant of the +full vector is `≍ τ^{(N+3)(N+2) + 2}` and that of the pin vector `≍ τ⁸` (the case `N = 0`), and the Schur complement has +determinant `≍ τ^{N(N+5)}`. Far form: a Gaussian conditional density is at most `(2π)^{−N/2}` times the inverse square +root of the determinant of the conditional covariance, which depends only on the σ-algebra `𝒢` conditioned on, and +continuously on `(t, y)`. For `t ∈ [ε, L − ε]` the vector `(f'(y_i), f'(±τ), f(−τ) − f(τ), f''(±τ))` is nondegenerate +(a surjective linear image of derivatives at distinct points, Lemma 1.1), so the determinant is bounded below by +compactness. As `t ↓ 0`, `σ(U, f''(±τ)) = σ(W_τ)` with +`W_τ := (U₁, U₂, U₃, (E₁ − U₂)/τ², ((f''(τ) − f''(−τ))/2 − τU₃)/τ³)`, and the expansions in the proof of Lemma 1.3 +(`E₁ − U₂ = a₄τ²/3 + O(τ⁴)`, `(f''(τ) − f''(−τ))/2 − τU₃ = a₅τ³/15 + O(τ⁵)`, remainders bounded in `L²`) give +`W_τ → (a₁, a₂, a₃, a₄/3, a₅/15)` in `L²`, jointly with `(f'(y_i))` and uniformly in admissible `y`. This limit and +`(f'(y_i))` are jointly nondegenerate (Lemma 1.1; the `y_i` stay at distance `≥ t₀/8` from the merged point and from each +other), so the conditional determinant converges to a positive limit, uniformly; for `𝒢 = σ(U)` keep the first three +entries. As `t ↑ L` the pins merge at `L/2` across the complementary arc; `σ(U)` and `σ(U, f''(±τ))` are the +corresponding σ-algebras of the pair at distance `L − t`, and the same argument applies there. ∎ + +**Lemma 4.3 (thin pairs are negligible).** Let `K^{band}(t, h) := (12/t⁴)p_t(α)E_Q[|f''(−τ)f''(τ)|1{banded}]` and +`K^{co}(t, h)` the same with `1{co-banded}`. Then `∫_{t_*}^{t₀}K^{band}dt = O(h^{3/4})`, `∫_{t₀}^{L}K^{band}dt = O(h)` +and `∫_{t_*}^{L/2}K^{co}dt = O(h)`. + +*Proof.* Take `k = 8`, `N = 2`. Under `Q`, `(a₄, …, a₉)` has a density bounded uniformly in `τ ≤ τ₀` and `α` +(`Cov(a₄..a₉ | U) → Cov(a₄..a₉ | a₁, a₂, a₃)`), and `K` is sub-Gaussian with mean `O(1 + α)`; decomposing `K` dyadically +and using Lemma 4.1, for `t ≤ t₁ := h^{1/10}` the kernel is `≤ C t^{−4}(h/t²)²Π_{j=4}^{9}min(1, h t^{−j}) + O(h^{10})`. +On `[t_*, h^{1/5}]` only `j = 4` is active: `≤ Ch³t^{−12}`, integral `≤ Ch³t_*^{−11} = O(h^{0.75})`; on +`[h^{1/m}, h^{1/(m+1)}]`, `5 ≤ m ≤ 9`, the bound is `h^{m−1}t^{−8−Σ_{j=4}^{m}j}`, with integral `O(h^{4/5})` for `m = 5` +and smaller beyond (the dyadic decomposition of `K` adds at most powers of `log(1/h)`, absorbed since +`3 − 11/(5 − δ) > 3/4`). For `t ∈ [t₁, t₀]`: banded with `h ≤ t^{10}` gives `|f''(±τ)| ≤ C τ⁸(1 + K)` (Lemma 4.1) and, by +Landau's inequality on the band, `|f'(τξ_i)| ≤ 2(h max(sup|f''|, 1))^{1/2}`; truncating `K` and `sup|f''|` at +`R := C(log(1/h))^{1/2}` (the complement has probability `O(h^{10})`), the Hessian product is `≤ Ct^{16}R²`, the two +interior derivative values are `≤ C(hR)^{1/2}`, and Lemma 4.2 bounds their probability by `ChRt^{−7}`. So +`K^{band} ≤ Ct^{−4}·t^{16}R²·hRt^{−7} = ChR³t⁵`, integrable, total `O(h(log(1/h))^{3/2})` (v1.2 printed `O(h log(1/h))`; +comment 5931058934). + +*Far.* The band (resp. co-band) arc has length `≥ t₀` (resp. `≥ L/2`); take `N = 4` points on it at mutual distances +`≥ t₀/8` and at distance `≥ t₀/4` from both pins, where Landau's inequality gives `|f'(y_i)| ≤ 2(hB)^{1/2}`, +`B := max(sup_T|f''|, 1)`. Put `u := min(t, L − t)` and `α_u := 12h/u³`. The kernel `(12/t⁴)p_t(α)` is the density of +`(f'(−τ), f'(τ), f(−τ) − f(τ))` at `(0, 0, h)`, invariant under `t ↦ L − t` (§1), so it equals `(12/u⁴)p_u(α_u)`. +Under `Q`, `f''` is Gaussian; its mean is linear in the conditioning value and bounded by `Cα_u` (for `u ≤ t₀` by Lemma +1.3 at the merged point — `σ(U)` is that of the pair at distance `u` — and by compactness otherwise), and its centered part +`f''_c` satisfies `E_Q sup_T|f''_c| ≤ E sup_T|f''|` (Sudakov–Fernique: conditioning does not increase the variance of +`f''(x) ∓ f''(y)`) and `P_Q(sup_T|f''_c| ≥ E sup_T|f''| + r) ≤ e^{−r²/(2λ₄)}` (Borell–TIS). Let `A` be large. +- Where `α_u ≤ A(log(1/h))^{1/2}`: `B ≤ C_A(log(1/h))^{1/2}` outside an event of `Q`-probability `O(h^{20})`, and on it + the mark forces `|f'(y_i)| ≤ C_Ah^{1/2}(log(1/h))^{1/4}`. By the far form of Lemma 4.2, conditionally on + `(U, f''(−τ), f''(τ))`, `E_Q[|f''(−τ)f''(τ)|1{mark}] ≤ C_Ah²log(1/h)·E_Q|f''(−τ)f''(τ)| + O(h^{10}(1 + α_u)²)`. +- Where `α_u > A(log(1/h))^{1/2}` (so `u ≤ τ₀`): `p_u(α_u) ≤ Ce^{−α_u²/(4σ₃²)}` (Lemma 1.3) and + `E_Q|f''(−τ)f''(τ)| ≤ C(1 + α_u)²`; as `(12/u⁴)du = 4(12h)^{−1}dα_u`, this range contributes `O(h^{10})` for `A` large. + +Finally `∫(12/t⁴)p_t(α)E_Q|f''(−τ)f''(τ)|dt` over `[t₀, L)` (resp. `[t_*, L/2]`) is `O(h^{−1/3})` (near a merging of +the pins it is the near-pair integral), and `∫(12/t⁴)p_t(α)(1 + α_u)²dt = O(h^{−1})`. So both far parts are +`O(h^{5/3}log(1/h)) = O(h)`. ∎ + +## 5. Proof of Theorem 1D + +**(1D.1).** Split `ν₊ = ∫₀^{t_*} + ∫_{t_*}^{t₀} + ∫_{t₀}^{L}`. On `(0, t_*]`, `K₊ = K₁^{sign} − (12/t⁴)p_tE_Q[(⋯)⁺1{not +adjacent}]` and non-adjacency forces `K₅ ≥ ct^{−δ}` (Lemma 3.1), whose `Q`-probability is `≤ exp(−ct^{−2δ})` (Borell–TIS +for the conditioned process; `α ≤ t^{−δ}/C` or `p₃(α)` is negligible); the correction is `O(h^{N})` for every `N`. +Proposition 2.2 (`θ = 1`) gives the expansion. On `[t_*, t₀]`, `K₊ ≤ K^{band}`: `O(h^{3/4})`; on `[t₀, L)`, +`K₊ ≤ K^{band}`: `O(h)` (Lemma 4.3). Total remainder `O(h^{0.57})`. + +**(1D.2).** `ν = 2∫₀^{L/2}K dt`. On `(0, t_*]`, by Corollary 3.4, `K = K_{1/3}^{sign}` up to (i) the event `𝔅` and (ii) +`{K₅ ≥ ct^{−δ}}`; (ii) is `O(h^N)` as above. For (i), `𝔅` forces `|E₁| ∈ m[1/3 − x, 1/3 + x]` with +`x := C(tK^o/κ + t²K^e/κ + τ²)/c₀` (or `x ≥ 1/4`, which needs `K^o + K^e ≥ ct^{−δ}`, an `O(h^N)` event). Since +`E₁ ~ N(0, v₁)` is independent of `K^o` under `Q` (Remark 1.4), the `K^o`- and `τ²`-parts of the window have probability +`≤ C(tE[K^o]/κ + τ²)s e^{−s²/20}` (`s = m v₁^{−1/2}`), with `E_Q[K^o] ≤ C(1 + α)`. The `K^e`-part is correlated with `E₁`; +summing `min(P(K^e ≥ 2^j), C(t²2^j/κ)s e^{−s²/20})` over dyadic shells costs at most a factor `C(1 + α)(log(1/h))^{1/2}`. +The weight is `((m + E₂)² − E₁²)⁺ ≤ 2m² + 2E₂²`. Using `κ = α/(12t)`, `(12/t⁴)m² ≍ α²/t²` and `s ≍ α/t`, the misclassified +part of the kernel is `≤ C p₃(α)(1 + α)·(α²/t²)·[(t²/α)(α/t) + τ²·(α/t)]e^{−cα²/t²}·(1 + t(log(1/h))^{1/2})`, i.e. +`≤ C p₃(α)(1 + α)(α²/t)e^{−cα²/t²}(1 + t(log(1/h))^{1/2})`, plus `O(h^N)`. Over `{t ≤ h^{1/4}}` (where `α ≳ t`) its +integral is `O(h^{1/2})` after the substitution `t = (72h/(σ₄s₀))^{1/4}`; over `{t ≥ h^{1/4}}` it is +`≤ C∫_{h^{1/4}}h²t^{−7}dt = O(h^{1/2})`. Proposition 2.2 with `θ = 1/3`, doubled, gives the expansion. On `[t_*, L/2]`, an +elder pair is banded or co-banded (§4), so `K ≤ K^{band} + K^{co}` and Lemma 4.3 applies. Total remainder `O(ℓ^{1/2})`. ∎ + +## 6. Remarks + +**6.1 The case `d = 1` of Theorem CU (#207).** (CU.2) reads `c₁ = −(192/7)2^{1/4}∫_{S^{d−1}}p_G(0)p_{V_u}(0)(2π)^{−1/2}τ_u^{−1} +E[|Y|^{7/4}|Δ|^{1/4}1{A<0} | …]dσ(u)`. At `d = 1`: `S⁰ = {±1}` with counting measure, `A` is the empty matrix (`Δ = 1`, +`1{A < 0} = 1`, `adj(A)γ = 0`), so `Y = f₄/12`, `p_Gp_V = p₁₂`, `τ_u = σ₃`, and `E|f₄/12|^{7/4} = 12^{−7/4}σ₄^{7/4}μ_{7/4}`. +The result equals `C₁` exactly: `(192/7)2^{1/4}·2·12^{−7/4} = (2^{15/4}/7)3^{−3/4}` and `(8/21)24^{1/4} = (2^{15/4}/7)3^{−3/4}` +(checker C1). Likewise `I/C₁ = 3^{1/4}/2` is (CU′.1)'s `I^{cand}/c₁`, and `I − C₁ > 0` is (CU′.2)'s rejected coefficient. +The one-dimensional window `|φ| < 1/3` is #207's elder window with no transverse fiber. The two proofs are independent: +here the pair-scale kernel is an explicit Gaussian integral and the elder rule is decided on a fixed window (§3); +#207 needs the fiber reduction, the stability proposition and a window-probability lemma in `d ≥ 2`. So this note is an +independent check of #207's normalization `(192/7)2^{1/4}` and of the loss integral, in the one dimension where +everything is explicit — not a proof of any part of #207. + +**6.2 Numerical evidence (exploration, not part of the proof).** +- *Exact two-point Rice integral* (checker C6; standard library, about three seconds: Decimal for the Gaussian + conditioning, a closed form or a split Gauss–Legendre rule for `G₁`). It evaluates + `dev(h) := h^{1/3}∫₀^{t₀}K₁^{sign}dt/(C₀/2) − 1` for `h = 10^{−11}, …, 10^{−16}` and fits + `dev/h^{7/12} = a + b h^{1/12} + r h^{−1/4}`; the last term is the non-adjacent sign pairs inside `t₀`, an `O(1)` part of + `K₁^{sign}` that the adjacency mark removes from `ν₊`. Gaussian kernel (`t₀ = 0.04`): `a = −1.3602117`, + `b = 2.0892177`, against `I/C₀ = −1.3602115`, `B₂/(C₀/2) = 2.0892180`. Mixture kernel `(e^{−x²/2} + e^{−2x²})/2` + (`t₀ = 0.01`; `λ₂, λ₄, λ₆, λ₈ = 5/2, 51/2, 975/2, 26985/2`): `a = −1.4697391`, `b = 2.1373811`, against + `−1.4697376`, `2.1373703`. An mpmath computation at 50–130 digits down to `h = 10^{−24}` agrees (outside the + repository). +- *Monte Carlo of the persistence and crest-to-trough densities* (numpy; outside the repository per the standard-library + rule; archived with the project record): exact spectral synthesis of the periodized Gaussian kernel on circles of length + `≈ 1.05·10⁵`, total length `8.4·10⁷`, critical points by bracketed Newton on degree-6 Taylor polynomials from exact + grid derivatives, exact one-dimensional persistence. Over `ℓ ∈ [10⁻⁵, 10⁻²]` the ratio of the empirical `ν` to the + three-term law is `1.000 ± 0.003` (to the leading term alone it drifts to `0.95`); the density of adjacent max/min pairs + that are *not* elder pairs, fitted as `Aℓ^{1/4} + Bℓ^{3/4}`, gives `A = 0.07779 ± 0.00080` against + `I − C₁ = 0.0778330` (`χ²/dof = 0.6`); non-adjacent bars are `< 0.2%` of all bars at `ℓ ≤ 0.05`. +- *Pre-review referee computations (same author family; not acceptance).* An independent implementation of the sign + kernels (conditioning from the closed-form covariance at `40 + 12log₁₀(1/t)` digits, `h` down to `10^{−40}`) gave the + `h^{1/4}` coefficients `−0.0748867035` (`θ = 1`) and `−0.1138031794` (`θ = 1/3`) against `I/2` and `C₁/2`, and the `h^{1/3}` + coefficient `0.11502229` against `B₂` (relative agreement `10^{−9}` to `10^{−11}`); after the three terms the remainder + divided by `h^{3/4}` is constant (`≈ 0.038`, `θ = 1/3`) over `h = 10^{−10}, …, 10^{−26}`, so for the sign kernels the next + term is of order `h^{3/4}`. A second independent Monte Carlo (`2.6·10⁷` length) gave `ν`/three-term `= 0.9961 ± 0.0026` + and `ν₊`/three-term `= 0.9986 ± 0.0037` on `[10⁻³, 10⁻²)`, rejecting the one- and two-term laws (`|z| ≥ 14`). +- *Why plain histograms look flat.* For the Gaussian kernel the second and third terms nearly cancel on + `10⁻⁴ ≤ ℓ ≤ 10⁻²`: `ν/(C₀ℓ^{−1/3}) − 1 = ℓ^{7/12}(−2.067 + 2.089ℓ^{1/12}) + …` (`−1.6%` at `ℓ = 10⁻³`), and for the + crest-to-trough density `−1.360 + 2.089ℓ^{1/12}` vanishes at `ℓ ≈ 0.006`. + +**6.3 Literature.** #147 and #210 found no small-amplitude exponent for the crest-to-trough law in Rice 1944/45, +Cartwright–Longuet-Higgins 1956, Lindgren 1972 or Lindgren 2019 (whose exact joint law of adjacent extremes contains +(1D.1) implicitly). Pérez (arXiv:2012.09459v3, §1.1) describes smooth random-field topology as an open research area; +that general observation does not identify this particular short-bar asymptotic. Theorem 1D makes #210's remark a theorem +on the circle and adds two terms. The searches cited here did not locate the formula and do not establish novelty; the +database pass of #147 remains to be run. + +**6.4 The line.** The near-pair analysis (§§1–3, Lemma 4.1) is local. On `R` the far bound of Lemma 4.3 needs a +decorrelation hypothesis (uniform nondegeneracy of separated values); with, e.g., exponentially decaying `ρ^{(j)}` the +same proof applies. Not claimed here. + +## 7. Sources (exact identities in `SOURCES.json`) + +Cited for comparison only (nothing is consumed): Math- #207 `frontiers/cusp_second_order_20261001/PROOF.md` (v1.1, head +`826b8be`); Math- #210 `reviews/literature_classical_neighbors_20261001/ADDENDUM.md` (v1.1, head `7929169`); merged +`reviews/literature_lifetime_law_recon_20260929/RECONNAISSANCE.md` (`003b9879`); for the marked Kac–Rice convention [P] +`imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` §9 and [E2] +`reviews/d1_section9_borel_repair_20260925/REPAIR.md`. External: J.-M. Azaïs and M. Wschebor, *Level Sets and Extrema of +Random Processes and Fields* (Wiley, 2009), Ch. 6; Markov's and Landau's inequalities; Bulinskaya's lemma. + +## 8. Exact controls and exploration + +`d1_check.py` (standard library; output `RESULTS.json`, byte-identical under `-O`; mutants M1–M5 exit 1, an unknown label +exits 2): +- **C1** the constants: exponent bookkeeping in `2^a3^bπ^c` with rational exponents — (CU.2) at `d = 1` equals `C₁`, the two + printed forms of `C₁` agree, `I/C₁ = 3^{1/4}/2`, `C₀` from the fold integral. +- **C2** Lemma 2.1: `k_θ` exactly for `θ = 1, 1/3`, and a quadrature check of `∫ζ_θ s^{−5/4}`. +- **C3** the model (3.1): polynomial identities; the critical-point structure; the margins of Lemma 3.3 at rational `φ` + (including the extension to `1 ≤ |φ| ≤ 6/5`); the + decision by exact persistence of `g` for 117 rational `φ ∈ (−1, 1)`: elder iff `|φ| < 1/3`. +- **C4** Lemma 1.3: block structure and the coefficients `c₂, d₂, q₂`, `v₁`, `v₂` as exact Laurent series in `τ` computed from + the covariance (not from the jets) for the Gaussian kernel and the mixture `(e^{−x²/2} + e^{−2x²})/2`. +- **C5** the `B₂` assembly: the polynomial identity of §2(e) (exact multivariate polynomials) and the Gaussian-kernel value + `𝒬/(120λ₂λ₄D) = 3/4`; (v1.1) the sign decomposition `𝒬 = 4λ₂²λ₄σ₄² + D(24λ₄² − D)` of §0, `λ₂λ₆ ≤ 25λ₄²` and + `𝒬 > 0` for both kernels, and `𝒬 < 0` (exact rationals) for the two-mode spectrum of §0. +- **C6** the two-point Rice integral (§6.2), both kernels: fitted `a`, `b` within `2·10⁻⁴` and `3·10⁻³` of the predictions. + +What the controls do not test: Lemma 1.1, the Kac–Rice representation, the error bounds of Proposition 2.2, Lemmas 3.2–4.3 +and the assembly (§5) are proved in prose only; C6 is a numerical consistency check of Proposition 2.2's constants, not a +proof. + +## 9. Review slices + +- **A** §1: the pair coordinates and Jacobian, Lemma 1.2 (reflection), Lemma 1.3 (the jet expansions and their coefficients). +- **B** §2: Proposition 2.2 — the convexity bound (a), the split (b)–(d), the closed forms (e) and the `B₂` identity. +- **C** §3: Lemmas 3.1–3.3 and Corollary 3.4 — the model, the margins, the window decision. +- **D** §4–§5: the band lemma, interior densities, thin and far pairs, and the assembly, including the misclassification + bound in (1D.2). +- **E** §6: the comparison with #207 and the numerical evidence. diff --git a/frontiers/d1_third_order_law_20261001/README.md b/frontiers/d1_third_order_law_20261001/README.md new file mode 100644 index 000000000..ec37ea655 --- /dev/null +++ b/frontiers/d1_third_order_law_20261001/README.md @@ -0,0 +1,134 @@ +# The one-dimensional lifetime and crest-to-trough laws to third order (CL-D1-THIRD-ORDER-20261001-v1.3) + +Author-side proof candidate, Anthropic Claude, 1 October 2026. Scientific effect NONE. Nonauthor review required. +v1.1 applies the two findings of the Codex review of v1 (head `2aedcaa`); see *Review record* below. +v1.2 renames the theorem **Theorem 1D** (dimension one), label only, after the xAI concern 5940492097: the name D1 +belongs to the cap component (Math- #193, #194). No mathematical change. +v1.3 applies the clarifications the nonauthor reviews asked for: the four of the Codex acceptance (comment 5933752065: a +sign typo, a range, a logarithm, the global-maximum alternative) and the narrowed Pérez attribution of the Slice E review +(5387031124). No statement, constant or control changes. +**No dependencies:** self-contained (Gaussian conditioning, the two-point Kac–Rice formula, Taylor, Markov and Landau +inequalities). Math- #207 (Theorem CU, `d ≥ 2`) and #210 (the `d = 1` literature remark) are cited for comparison only. + +**Statement (Theorem 1D).** Let `f` be a stationary Gaussian process on the circle `R/LZ` whose covariance `ρ` is `C^∞` +with all Fourier coefficients positive (e.g. the periodized `e^{−x²/2}`, the one-dimensional SIDE24 field). Let `ν₊(h)` be +the density per unit length of crest-to-trough amplitudes (maximum to the next minimum) and `ν(ℓ)` that of persistence +lifetimes (superlevel `H₀`, elder rule), both in their canonical Kac–Rice versions. Then + + ν₊(h) = (C₀/2)h^{−1/3} + (I/2)h^{1/4} + B₂h^{1/3} + O(h^{1/2}), + ν(ℓ) = C₀ℓ^{−1/3} + C₁ℓ^{1/4} + 2B₂ℓ^{1/3} + O(ℓ^{1/2}), + +with explicit constants in the spectral moments: `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}/σ₃ < 0`, `I = (3^{1/4}/2)C₁`, and +`B₂ = 2^{1/2}3^{1/3}Γ(5/6)(2π)^{−1/2}p₁₂σ₃^{2/3}𝒬/(120λ₂λ₄D)`, where +`𝒬 = 4λ₂²λ₄λ₈ + 26λ₂λ₄²λ₆ − 5λ₂²λ₆² − 25λ₄⁴ = 4λ₂²λ₄σ₄² + D(24λ₄² − D)`. + +The sign of `B₂` is that of `𝒬`. It is positive when `λ₂λ₆ ≤ 25λ₄²`, which covers the Gaussian kernel and the mixture +below. It is **not** fixed by (H): Codex's two-mode spectrum (weights `1 − 10⁻⁵` and `10⁻⁵` at frequencies `1` and `40`, +made admissible by small positive weights elsewhere) has `𝒬 ≈ −7.09·10⁸`. v1 wrote `B₂ > 0` here; that was an +overstatement. + +Here `σ₃² = Var(f''' | f')`, `σ₄² = Var(f'''' | f'')`, `p₁₂` is the density of `(f', f'')` at `0`, and +`μ_{7/4} = E|Z|^{7/4}`. + +For `e^{−x²/2}` the constants are `C₀ = 0.11011038`, `C₁ = −0.22760636`, `I = −0.14977341` and `B₂ = 0.11502229`. The +leading crest-to-trough constant per crest is `0.19971814`, #210's constant, so its remark becomes a theorem on the +circle. Adjacent max/min pairs that are not elder pairs have density `(I − C₁)ℓ^{1/4} + O(ℓ^{1/2})`. + +**Mechanism.** +- *Leading term.* The leading term is the fold law: a maximum and the adjacent minimum at separation `t`, gap + `≈ f'''t³/12`, at scale `t ≍ ℓ^{1/3}`. +- *The `ℓ^{1/4}` terms.* These come from the cusp scale `t ≍ ℓ^{1/4}`. There the pair sees #207's quartic ridge with no + transverse fiber: it is adjacent iff `|φ| < 1` and an elder pair iff `|φ| < 1/3`, where `φ = f''''t⁴/(72ℓ)`. The fold law + overcounts on this scale, and the deficit is a Mellin integral `k_θμ_{7/4}`, with `k₁ = 32/7` and `k_{1/3} = (64/7)3^{−1/4}`. +- *The `ℓ^{1/3}` term.* This collects the `τ²`-corrections of the pinned Gaussian law at the fold scale, plus the finite + part of the cusp integrand. + +**Structure of the proof.** +1. Under the pinned law, the pair kernel is an explicit Gaussian integral `(12/t⁴)p_t(α)E((m + E₂)² − E₁²)⁺`. This is exact, + by a reflection symmetry that makes `E₁ ⊥ E₂`. +2. Its asymptotics give the three terms (Proposition 2.2). +3. On a fixed window `[−2, 2]` the elder rule is decided by the quartic model, with explicit margins (Lemma 3.3). +4. Thin and far pairs are negligible by a band lemma (Markov's inequality) and a flat-band (Landau) bound. + +**Relation to #207.** +- (CU.2) at `d = 1` equals `C₁` exactly. +- `I/C₁ = 3^{1/4}/2` is (CU′.1)'s ratio. +- The proofs are independent, so this is a one-dimensional check of #207's normalization `(192/7)2^{1/4}` and of its elder + window. It is not a proof of any part of #207. + +**Numerical evidence (exploration).** +- *Deterministic two-point Rice integral (stdlib; control C6).* For `e^{−x²/2}` it fits the `h^{1/4}` coefficient + `−1.3602117` (prediction `I/C₀ = −1.3602115`) and the `h^{1/3}` coefficient `2.0892177` (prediction `B₂/(C₀/2) = 2.0892180`). + For the mixture `(e^{−x²/2} + e^{−2x²})/2` the fits are `−1.4697391` and `2.1373811`, against `−1.4697376` and `2.1373703`. +- *Monte Carlo (numpy, outside the repository).* Total length `8.4·10⁷`. Persistence lifetimes match the three-term law to + `1.000 ± 0.003` on `[10⁻⁵, 10⁻²]`, and the rejected-adjacent-pair coefficient is `0.07779 ± 0.00080` against + `I − C₁ = 0.0778330`. +- *Why plain histograms look flat.* The second and third terms nearly cancel on `10⁻⁴ ≤ ℓ ≤ 10⁻²`. + +**Not claimed:** anything on the line `R` (needs a decorrelation hypothesis, §6.4); uniformity in the covariance; constants in +the `O(·)`; sharpness of `O(h^{1/2})`. + +**Files.** +- `PROOF.md`. +- `d1_check.py`: standard library. Its output is `RESULTS.json`, byte-identical under `-O`. Mutants M1–M5 exit 1, and an + unknown label exits 2. Run time is about three seconds. Its controls: + - **C1** the constants, by exponent bookkeeping: (CU.2) at `d = 1`, the printed forms, `C₀`, `I/C₁`, and the `B₂` + prefactors. + - **C2** the Mellin integrals `k_θ`. + - **C3** the model identities (3.1), the margins of Lemma 3.3, and the decision by exact persistence for 117 rational `φ`. + - **C4** the pinned-law expansions, as exact Laurent series from the covariance, for two kernels. + - **C5** the `B₂` polynomial identities, the sign decomposition of `𝒬`, `𝒬 > 0` for both kernels, and `𝒬 < 0` for the + two-mode spectrum. + - **C6** the two-point Rice integral, a numerical check with tolerance. +- `SOURCES.json` (exact identities of the cited sources). + +**Referee record before any nonauthor review (same author family; not acceptance).** Two clean-context Claude referee passes +read v1 before the PR. + +*Slices A/B (§§1–2): no false claim.* +- Independent sympy verification of every coefficient in Lemma 1.3 for a general covariance. +- An independent high-precision Rice computation down to `h = 10⁻⁴⁰`. It confirms `I/2`, `C₁/2` and `B₂` to `10⁻⁹`–`10⁻¹¹`, + and shows that the next term of the sign kernels is `O(h^{3/4})`. +- One gap: Proposition 2.2(a), where the straddle term's kernel is `αt`, not `αt³`. Repaired with its Gaussian factor; the + bound is now `≤ Ct²`. +- Minor points, all applied. + +*Slices C/D (§§3–5).* +- Lemma 3.3's case analysis was confirmed (sympy), as were Lemmas 3.1, 3.2, 4.1 and 4.2 (including the `τ^{N(N+5)}` scaling, + and that the invertibility condition is necessary), the bookkeeping of ν, and an independent Monte Carlo + (`2.6·10⁷`, three-term law `0.996 ± 0.003`). +- It found two errors, both repaired: + - Corollary 3.4's misclassification window omitted the deterministic `τ²` shift between `φ_G` and `φ`; + - "elder pairs are banded" holds only on the arc of the death point. The co-banded case is now bounded separately. +- It found one gap: a `√log` loss in the misclassification sum. This is removed by the parity split (Remark 1.4: the odd + part of the field, which carries the first-order window error, is independent of `E₁`). +- Minor points, all applied. + +**Review record (nonauthor).** The Codex review of v1 (`2aedcaa`, 1 October 2026) made two findings, both applied in v1.1: +- **P2 (correct): `B₂ > 0` is not implied by (H).** The README claim is withdrawn. §0 of `PROOF.md` now gives the sign + decomposition, the sufficient condition and the counterexample, all three checked exactly in C5. The theorem never used + the sign. +- **P1 (correct): the far form of Lemma 4.2 as stated was false.** It claimed a bounded joint density of + `(f'(y_i), f''(±τ))` given `U`. As the pins merge, the conditional variances of `f''(±τ)` are `≍ τ⁴, τ⁶`, so that + density is unbounded. The far-pair bound needs only the density of `(f'(y_i))` *conditional on* `U` and `f''(±τ)`. + v1.1 states that bound and proves it: the conditioning σ-algebra is that of + `W_τ = (U₁, U₂, U₃, (E₁ − U₂)/τ², ((f''(τ) − f''(−τ))/2 − τU₃)/τ³)`, which converges to the jet + `(a₁, a₂, a₃, a₄/3, a₅/15)`, jointly nondegenerate with far values. Lemma 4.3's far part now also controls the + conditional mean of `f''` under `Q`, by the symmetry `t ↦ L − t`, Sudakov–Fernique and Borell–TIS. + +**What the controls do not test:** Lemma 1.1, the Kac–Rice representation, the error bounds of Proposition 2.2, Lemmas +3.2–4.3 and the assembly (§5) are proved in prose only. Review slices (PROOF.md §9): +- **A** the pinned law; +- **B** the explicit asymptotics; +- **C** the window decision; +- **D** thin and far pairs, and the assembly; +- **E** the comparison with #207 and the numerics. + +**Nonauthor reviews on file** (all OpenAI Codex; same GitHub account, organizational-independence credit 0): +- Slices A–D and the theorem at the circle scope: comment 5933752065 (head `f4a58df`), with the supplementary derivations + in comments 5930841283 and 5931058934; carried to v1.2 by comment 5941929764 (labels only). v1.3 applies its four listed + clarifications. +- Slice E: review 5387031124 (head `4703fc7`): the coefficient comparison and the public controls accepted; the attribution + amendment E-LIT, applied in v1.3; the exploration outside the repository is author-reported and was not verified. +- xAI: the naming concern (5940492097, 5940563636), answered by v1.2; a provider-distinct readback remains open. diff --git a/frontiers/d1_third_order_law_20261001/RESULTS.json b/frontiers/d1_third_order_law_20261001/RESULTS.json new file mode 100644 index 000000000..f8e2aa059 --- /dev/null +++ b/frontiers/d1_third_order_law_20261001/RESULTS.json @@ -0,0 +1,173 @@ +{ + "checks": { + "C1_constants": { + "info": { + "B2_part2_closed_form": true, + "B2_prefactor_2^(1/2)3^(1/3)": true, + "C0_from_fold_integral": true, + "C1_printed_forms_agree": true, + "CU2_at_d1_equals_C1": true, + "I_over_C1_is_3^(1/4)/2": true, + "cusp_assembly_gives_C1": true + }, + "passed": true + }, + "C2_mellin": { + "info": { + "k1": "32/7", + "k_(1/3)": "64/7 * 3^(-1/4)", + "quadrature_ratio_to_k_mu": { + "1": 1.0, + "1/3": 1.0 + } + }, + "passed": true + }, + "C3_model_window": { + "info": { + "critical_values_(3.1)": true, + "decision_elder_iff_|phi|<1/3": true, + "identities": { + "g + 1 = (X-1/2)^2[2(X+1) + 3 phi (X+1/2)^2]": true, + "g = (X+1/2)^2[2(X-1) + 3 phi (X-1/2)^2]": true, + "g' = 6(X+1/2)(X-1/2)(1 + 2 phi X)": true + }, + "lemma_3.3_extension_|phi|>=1": true, + "lemma_3.3_margins": true, + "n_phi": 117 + }, + "passed": true + }, + "C4_pinned_series": { + "info": { + "(exp(-x^2/2)+exp(-2x^2))/2": { + "c2": "-2840/1137", + "checks": { + "c = tau(1 + c2 tau^2 + ...)": true, + "det = l4 D (1 + d2 tau^2 + ...)": true, + "inv33 = (l2/D)(1 + q2 tau^2 + ...)": true, + "parity": true, + "v1 = sigma4^2 tau^4/9 + ...": true, + "v2 = (tau^6/225) Var(a5|a1,a3) + ...": true, + "zero_blocks": true + }, + "d2": "-268015/19329", + "lambda": { + "10": "968625/2", + "12": "42588315/2", + "2": "5/2", + "4": "51/2", + "6": "975/2", + "8": "26985/2" + }, + "q2": "-5129/1895" + }, + "exp(-x^2/2)": { + "c2": "-2/3", + "checks": { + "c = tau(1 + c2 tau^2 + ...)": true, + "det = l4 D (1 + d2 tau^2 + ...)": true, + "inv33 = (l2/D)(1 + q2 tau^2 + ...)": true, + "parity": true, + "v1 = sigma4^2 tau^4/9 + ...": true, + "v2 = (tau^6/225) Var(a5|a1,a3) + ...": true, + "zero_blocks": true + }, + "d2": "-11/3", + "lambda": { + "10": "945", + "12": "10395", + "2": "1", + "4": "3", + "6": "15", + "8": "105" + }, + "q2": "-1" + } + }, + "passed": true + }, + "C5_B2_assembly": { + "info": { + "gauss_Q_over_120l2l4D_is_3/4": true, + "identity_30l2l4D(2c2-d2/2-5q2/6)": true, + "identity_Q=4l2^2l4s4^2+D(24l4^2-D)": true, + "identity_sum_equals_Q": true, + "two_mode_1_40_eps1e-5_sign_not_fixed_by_H": { + "Q": "-7.08561071e+08", + "Q<0": true, + "l2l6/l4^2": "58.816210", + "l2l6>25l4^2": true + }, + "values": { + "(exp(-x^2/2)+exp(-2x^2))/2": { + "Q/(120 l2 l4 D)": "66423/25772", + "Q>0": true, + "agree": true, + "bracket": "66423/25772", + "l2l6/l4^2": "1625/867", + "sufficient_l2l6<=25l4^2": true + }, + "exp(-x^2/2)": { + "Q/(120 l2 l4 D)": "3/4", + "Q>0": true, + "agree": true, + "bracket": "3/4", + "l2l6/l4^2": "5/3", + "sufficient_l2l6<=25l4^2": true + } + } + }, + "passed": true + }, + "C6_rice_integral": { + "info": { + "(exp(-x^2/2)+exp(-2x^2))/2": { + "B2": 0.28802137, + "C0": 0.26951003, + "C1": -0.60195554, + "I": -0.39610902, + "a_pred_I/C0": -1.4697376, + "b_pred_B2/(C0/2)": 2.1373703, + "dev/h^(7/12)": { + "1e-11": -1.210789, + "1e-12": -1.256001, + "1e-13": -1.293318, + "1e-14": -1.32412, + "1e-15": -1.349544, + "1e-16": -1.370527 + }, + "fit_a": -1.4697, + "fit_b": 2.137, + "t0": 0.01, + "within_tolerance": true + }, + "exp(-x^2/2)": { + "B2": 0.11502229, + "C0": 0.11011038, + "C1": -0.22760636, + "I": -0.14977341, + "a_pred_I/C0": -1.3602115, + "b_pred_B2/(C0/2)": 2.089218, + "dev/h^(7/12)": { + "1e-11": -1.107096, + "1e-12": -1.151288, + "1e-13": -1.187764, + "1e-14": -1.21787, + "1e-15": -1.242718, + "1e-16": -1.263223 + }, + "fit_a": -1.3602, + "fit_b": 2.089, + "t0": 0.04, + "within_tolerance": true + } + }, + "passed": true + } + }, + "mutant": null, + "object": "CL-D1-THIRD-ORDER-20261001-v1.1 exact controls", + "passed": true, + "scientific_effect": "NONE" +} diff --git a/frontiers/d1_third_order_law_20261001/SOURCES.json b/frontiers/d1_third_order_law_20261001/SOURCES.json new file mode 100644 index 000000000..46f3b0091 --- /dev/null +++ b/frontiers/d1_third_order_law_20261001/SOURCES.json @@ -0,0 +1,246 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "object": "CL-D1-THIRD-ORDER-20261001-v1.3", + "kind": "author-side proof candidate (Theorem 1D: the one-dimensional crest-to-trough and persistence lifetime densities on the circle to third order with remainder O(h^(1/2))); self-contained; nothing consumed; nonauthor review required. Control C6 is a numerical consistency check (two-point Rice integral), not a proof.", + "author": "Anthropic Claude", + "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", + "read_at": { + "branch_base": "3e0a91b69892b9717564c592e7a966492a81566a" + }, + "consumed": [], + "consumed_unmerged": [], + "cited_only": [ + { + "path": "reviews/literature_lifetime_law_recon_20260929/RECONNAISSANCE.md", + "bytes": 13738, + "sha256": "16628983f7833419e33c7b04cdb2e0d49076bccfbe7a6d457bf90efba63aa4ec", + "git_blob": "003b98794f02fd5c1cd45ed263bf2818b556e6ab", + "tag": "recon147", + "use": "literature position (section 6.3): no small-gap exponent located under the memo's protocol; the memo's sentence that Perez states the smooth case as open overstates arXiv:2012.09459v3 (section 1.1 calls smooth random-field topology an open research area), corrected in section 6.3 after the Slice E review 5387031124 (E-LIT)" + }, + { + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "bytes": 40261, + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "tag": "P", + "use": "section 9 marked Kac-Rice convention (the d-dimensional argument, applied in d = 1)" + }, + { + "path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", + "bytes": 9062, + "sha256": "845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f", + "git_blob": "fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a", + "tag": "E2", + "use": "Borel repair of the marked Kac-Rice formula (convention only)" + } + ], + "cited_unmerged": [ + { + "path": "frontiers/cusp_second_order_20261001/PROOF.md", + "bytes": 52605, + "sha256": "cffc1b83ac364da58bd650c3c301ea1babd38e19af54f74010bdc120edce38a8", + "git_blob": "f6df5a7356a54771b0052e42a864a140709903ad", + "tag": "207", + "use": "comparison only (section 6.1): (CU.2) at d = 1 equals C1; (CU-prime.1) ratio 3^(1/4)/2; the proof of Lemma 3.2 follows CU.1", + "head": "826b8be512e86f2de73c33d6ac7a76908dc2e0e6", + "pr": "Math- #207" + }, + { + "path": "reviews/literature_classical_neighbors_20261001/ADDENDUM.md", + "bytes": 13195, + "sha256": "f185d70d1e7f289163fd85a99bb9518da7cc3ead5da39db99e570ecde8b4f88e", + "git_blob": "fc0a84dcfb0e106316f6e10a9bedd87d578e9c4c", + "tag": "210", + "use": "comparison only: the d = 1 remark f_H(h) ~ C h^(-1/3) whose constant Theorem 1D proves", + "head": "792916912796874c7113258aceffc26ab965de5b", + "pr": "Math- #210" + } + ], + "cited_external": [ + { + "tag": "AW09", + "reference": "J.-M. Azais and M. Wschebor, Level Sets and Extrema of Random Processes and Fields, Wiley (2009), Ch. 6", + "use": "two-point (marked) Kac-Rice formula" + }, + { + "tag": "Markov", + "reference": "A. A. Markov / V. A. Markov, inequality for derivatives of polynomials on an interval", + "use": "Lemma 4.1" + }, + { + "tag": "Landau", + "reference": "E. Landau (1913), interpolation inequality |g'| <= 2 (sup|g| sup|g''|)^(1/2)", + "use": "flat band, Lemma 4.3" + }, + { + "tag": "Bulinskaya", + "reference": "E. V. Bulinskaya (1961), on the mean number of crossings of a level by a stationary Gaussian process", + "use": "Lemma 1.1 (Morse property, distinct critical values)" + }, + { + "tag": "BorellTIS", + "reference": "Borell-Tsirelson-Ibragimov-Sudakov inequality", + "use": "tails of suprema of conditioned derivatives" + } + ], + "mutants": [ + "M1", + "M2", + "M3", + "M4", + "M5" + ], + "replayed": [ + "d1_check.py" + ], + "not_replayed": [], + "exploration_outside_repository": { + "summary": "numpy Monte Carlo (exact spectral synthesis, total length 8.4e7) and an mpmath Rice computation (50-130 digits); not part of this packet (standard-library rule)", + "location": "project record (claude.ai project, not public): V2_2/frontiers_d1_third_order_law_20261001/exploration/; identified by SHA-256 below", + "status": "author-reported exploration; not verified by a nonauthor (Slice E review 5387031124: UNVERIFIED, excluded from proof inputs); no proof step uses it", + "files": [ + { + "path": "README.md", + "bytes": 1793, + "sha256": "2b32d5e8fb2b184251ea0cb736df8428298489df967e1eb10135c351d72c874d" + }, + { + "path": "analysis2.json", + "bytes": 4033, + "sha256": "72b38410f48d1530659bd3c408a57b6e7099504b4515b0871597a33a5ff22450" + }, + { + "path": "analyze2.py", + "bytes": 1819, + "sha256": "0f2e29467ff1b6abe081185f666339ef52776ed4f0416eeed1657347f3906bcb" + }, + { + "path": "consts.py", + "bytes": 1098, + "sha256": "768172c8f1981ae6bb61cb36dc739fe6f2b2f3986038965ca4112fedac8e8837" + }, + { + "path": "rice_mp2.py", + "bytes": 3384, + "sha256": "fabfe882bc7ae462285d9749ec8190f03aff9112c04e54668e3bb5c9bcfbbe8b" + }, + { + "path": "rice_mpmath_runs.txt", + "bytes": 1063, + "sha256": "fb2f101bbfb3bbdc2ca0a8ed6bc11b3ef48cb05464e61adbd1c27f25cbd9c53f" + }, + { + "path": "run_rice.py", + "bytes": 588, + "sha256": "d3eba22e5b22d4b8081a76c7461c8b8edb08614411a6beadd47bd45fe498291c" + }, + { + "path": "sim1d.py", + "bytes": 5731, + "sha256": "b975ed0e816f0e8a62b06c41884f34f8d429d1783f08f85741ff0be49c66b299" + }, + { + "path": "sim2.py", + "bytes": 2481, + "sha256": "2de9dc9420f7b31a8714b05a82e93c9ed0014fbb39f411b0f092c3890ca4d71b" + } + ] + }, + "referee": { + "kind": "pre-submission clean-context referee passes, same author family (two Anthropic Claude subagents); NOT acceptance, NOT independent", + "slices_AB": "no false claim; Lemma 1.3 coefficients verified symbolically for a general covariance; independent Rice computation to h = 1e-40 confirms I/2, C1/2, B2 to 1e-9..1e-11 and a next term O(h^(3/4)); one gap (Prop 2.2(a): the straddle term kernel is alpha t, not alpha t^3) repaired with its Gaussian factor; minor points applied (Kac-Rice display restricted to (max, min) pairs; uniformity statements; the e^{-c/h} complement; I - C1 = 0.0778330)", + "slices_CD": "Lemma 3.3 case analysis, Lemmas 3.1, 3.2, 4.1, 4.2 and the counting of nu confirmed (sympy, mpmath, independent Monte Carlo 2.6e7: three-term law 0.996 +- 0.003); two errors repaired (Corollary 3.4: the misclassification window now includes the deterministic tau^2 shift between phi_G and phi; elder pairs are banded or co-banded, the co-banded kernel bounded by the flat band on the long arc); one gap repaired (sqrt(log) loss in the misclassification sum removed by the parity split, Remark 1.4); minor points applied (eta <= 1/4 and the extension of Lemma 3.3 to |phi| >= 1; far-region exponents with conditioning on f''(+-tau); merged-pin limit in Lemma 4.2; the unused adjacency claim dropped)" + }, + "automated_nonauthor": [ + { + "reviewer": "chatgpt-codex-connector[bot] (OpenAI Codex, automated PR review)", + "review_id": 5375298473, + "reviewed_commit": "2aedcaa6d4b0a89795dcafc4f5fce22fb418a403", + "date": "2026-10-01", + "findings": [ + { + "id": "P2", + "thread": 4152125662, + "claim": "README: B2 > 0 is not implied by (H); two-mode spectrum (weights 1 - 1e-5, 1e-5 at frequencies 1, 40) has Q ~ -7.09e8", + "verdict": "correct", + "disposition": "v1.1: positivity claim withdrawn; PROOF section 0 gives Q = 4 l2^2 l4 s4^2 + D(24 l4^2 - D), the sufficient condition l2 l6 <= 25 l4^2 and the counterexample; checker C5 verifies all three exactly; the theorem never used the sign" + }, + { + "id": "P1", + "thread": 4152125664, + "claim": "Lemma 4.2 far form: the joint conditional density of (f'(y_i), f''(+-tau)) given U is unbounded as the pins merge (v1 ~ tau^4, v2 ~ tau^6)", + "verdict": "correct (the v1 statement was false; the proof of Lemma 4.3 needs only the conditional density given U and f''(+-tau))", + "disposition": "v1.1: Lemma 4.2 far form restated as the density of (f'(y_i)) conditional on (U, f''(+-tau)), bounded uniformly in t via W_tau -> (a1, a2, a3, a4/3, a5/15); Lemma 4.3 far part rewritten (kernel symmetry t -> L - t, conditional mean of f'' under Q bounded by C alpha_u, Sudakov-Fernique and Borell-TIS truncation)" + } + ], + "note": "the P1 error had passed the same-family referee pass of slices C/D; the automated review is nonauthor but not a full mathematical acceptance" + } + ], + "files": [ + { + "path": "PROOF.md", + "bytes": 46313, + "sha256": "a1b5e6ecc97341ad72d74973c69c0f94304b22c559ab0187310ef2bd73455804" + }, + { + "path": "README.md", + "bytes": 10219, + "sha256": "b2b3c8fd81b93d38cc16f9fd5bd7db38d7b09e3627d216d8e61db97156896b3e" + }, + { + "path": "d1_check.py", + "bytes": 30682, + "sha256": "5a668ffbef036f19bef2e7ea5ab9b00dcf2bcfd2bb2419b4a087634af4aefbbc" + }, + { + "path": "RESULTS.json", + "bytes": 4066, + "sha256": "05795a038510493a36b6b6803efbd57cfa41951bd968a3a1f10b06d51d20da66" + } + ], + "label_history": "v1.2 renames Theorem D1 to Theorem 1D (dimension one), label only, after the xAI concern on #214 (comments 5940492097, 5940563636): the name D1 belongs to the cap component (Math- #193, #194). Paths unchanged; d1_check.py and RESULTS.json are byte-identical to v1.1 and keep its object label (their controls are unchanged).", + "nonauthor_reviews": [ + { + "scope": "Slices A-D and the theorem at the circle scope", + "reviewer": "OpenAI Codex (delegated AI review)", + "record": "comment 5933752065", + "head": "f4a58df9247dfa9ada2b756ecd7629c0b2faf5b5", + "proof_blob": "873532b955dbf7684edc1a53ba169c7216f778ab", + "supplementary": [ + "comment 5930841283", + "comment 5931058934" + ], + "carried_forward": "comment 5941929764 (v1.2, labels only)", + "clarifications_requested": [ + "Lemma 3.2: f_o(tau) = -h/2", + "Lemma 4.3: explicit O(h log(1/h)^(3/2)) cutoff bound", + "Lemma 1.3: 0 <= alpha <= tau^-1", + "Lemma 3.3 (R): the global-maximum alternative" + ], + "disposition": "all four applied in v1.3" + }, + { + "scope": "Slice E (section 6, controls, sources)", + "reviewer": "OpenAI Codex (delegated AI review)", + "record": "review 5387031124", + "head": "4703fc7b3b29967a134723fb4b7e0b26dff3e656", + "proof_blob": "3389ef8cfaabab9c71cdf398893b0b7aef69dba1", + "findings": [ + "coefficient comparison ACCEPTED", + "public controls reproduced", + "E-LIT: narrow the Perez attribution (AMEND)", + "outside-repository exploration UNVERIFIED" + ], + "disposition": "E-LIT applied in v1.3 (section 6.3); exploration identified by hash, status kept" + }, + { + "scope": "naming", + "reviewer": "xAI / Grok team", + "record": "comments 5940492097, 5940563636", + "disposition": "v1.2 rename to Theorem 1D; a provider-distinct readback remains open" + } + ], + "v1_3_changes": "clarifications requested by the nonauthor reviews (comment 5933752065 items 1-4; review 5387031124 E-LIT); no change to any statement, constant or control; d1_check.py and RESULTS.json byte-identical to v1.1" +} diff --git a/frontiers/d1_third_order_law_20261001/d1_check.py b/frontiers/d1_third_order_law_20261001/d1_check.py new file mode 100644 index 000000000..7316eee86 --- /dev/null +++ b/frontiers/d1_third_order_law_20261001/d1_check.py @@ -0,0 +1,752 @@ +#!/usr/bin/env python3 +"""Exact controls for CL-D1-THIRD-ORDER-20261001-v1.1 (frontiers/d1_third_order_law_20261001/PROOF.md). +Standard library only. Run: python3 -B -S d1_check.py (and with -O; output byte-identical). +Mutants: --mutant M1|M2|M3|M4|M5 must exit 1; an unknown label exits 2. + + C1 the constants: exponent bookkeeping over primes and symbols, rational exponents + ((CU.2) of Math- #207 at d = 1 equals C1; the two printed forms of C1; C0 from the fold integral; I/C1; B2 prefactors) + C2 Lemma 2.1: k_theta = 4 theta^(1/4) + (4/7) theta^(-7/4) exactly for theta = 1, 1/3, and a quadrature check + C3 the model (3.1): polynomial identities in (X, phi); X3 and the critical values; the margins of Lemma 3.3 at rational + phi; the decision by exact one-dimensional persistence of the quartic for 117 rational phi: elder iff |phi| < 1/3 + C4 Lemma 1.3: exact Laurent series in tau computed from the covariance, for exp(-x^2/2) and (exp(-x^2/2)+exp(-2x^2))/2 + C5 the B2 assembly: exact multivariate polynomial identities; Q/(120 l2 l4 D) = 3/4 for the Gaussian kernel; + v1.1: Q = 4 l2^2 l4 s4^2 + D(24 l4^2 - D), so Q > 0 if l2 l6 <= 25 l4^2 (both kernels), and Q < 0 for a two-mode + spectrum (the sign of B2 is not fixed by (H); Codex review on Math- #214) + C6 the two-point Rice integral (Decimal conditioning, float quadrature): fitted a, b against I/C0 and B2/(C0/2) +""" +import argparse +import json +import math +import sys +from decimal import Decimal, getcontext +from fractions import Fraction as F + +MUTANT = None + + +# ----------------------------------------------------------------------------------------------- C1: exponent bookkeeping +def factor_int(n): + out = {} + p = 2 + while p*p <= n: + while n % p == 0: + out[p] = out.get(p, 0) + 1 + n //= p + p += 1 + if n > 1: + out[n] = out.get(n, 0) + 1 + return out + + +class Mono: + """sign * prod base^exp with bases primes (int) or symbols (str) and Fraction exponents.""" + + def __init__(self, sign=1, exps=None): + self.sign = sign + self.exps = {k: F(v) for k, v in (exps or {}).items() if F(v) != 0} + + @staticmethod + def rat(q): + q = F(q) + if q == 0: + raise ValueError('zero') + e = {} + for p, k in factor_int(abs(q.numerator)).items(): + e[p] = e.get(p, 0) + k + for p, k in factor_int(q.denominator).items(): + e[p] = e.get(p, 0) - k + return Mono(1 if q > 0 else -1, e) + + @staticmethod + def sym(name, power=1): + return Mono(1, {name: power}) + + def __mul__(self, o): + e = dict(self.exps) + for k, v in o.exps.items(): + e[k] = e.get(k, 0) + v + return Mono(self.sign*o.sign, e) + + def __pow__(self, r): + r = F(r) + if self.sign < 0 and r.denominator != 1: + raise ValueError('negative base') + return Mono(self.sign**int(r) if r.denominator == 1 else 1, {k: v*r for k, v in self.exps.items()}) + + def __eq__(self, o): + return self.sign == o.sign and self.exps == o.exps + + def __neg__(self): + return Mono(-self.sign, self.exps) + + +def R(q): + return Mono.rat(q) + + +def check_C1(): + two, three = R(2), R(3) + pi = Mono.sym('pi') + mu74 = (two**F(7, 8))*Mono.sym('G(11/8)')*(pi**F(-1, 2)) # E|Z|^{7/4} + p12 = (R(2)*pi)**-1*Mono.sym('l2l4', F(-1, 2)) # (2 pi)^{-1}(l2 l4)^{-1/2} + s3, s4 = Mono.sym('s3'), Mono.sym('s4') + common = (R(2)*pi)**F(-1, 2)*p12*(s3**-1)*(s4**F(7, 4))*mu74 # (2 pi)^{-1/2} p12 s4^{7/4} mu / s3 + k1 = F(32, 7) + if MUTANT == 'M2': + k1 = F(4) + # C1 as printed: -(8/21) 24^{1/4} * common + C1_a = -(R(F(8, 21))*R(24)**F(1, 4)*common) + # C1 second printed form: -(2^{25/8}/7) 3^{-3/4} pi^{-2} G(11/8) s4^{7/4} s3^{-1} (l2 l4)^{-1/2} + C1_b = -(two**F(25, 8)*R(F(1, 7))*three**F(-3, 4)*pi**-2*Mono.sym('G(11/8)')*(s4**F(7, 4))*(s3**-1) + * Mono.sym('l2l4', F(-1, 2))) + # (CU.2) of #207 at d = 1: -(192/7) 2^{1/4} * 2 (two points of S^0) * p12 (2 pi)^{-1/2} s3^{-1} 12^{-7/4} s4^{7/4} mu + C1_cu = -(R(F(192, 7))*two**F(1, 4)*R(2)*p12*(R(2)*pi)**F(-1, 2)*(s3**-1)*R(12)**F(-7, 4)*(s4**F(7, 4))*mu74) + # cusp-coefficient assembly, Proposition 2.2(d): theta-coefficient/2 = -(s4^2/48)(72/s4)^{1/4} k mu p12 p3(0) + p30 = (R(2)*pi)**F(-1, 2)*(s3**-1) + def cusp(k): + return -(s4**2*R(F(1, 48))*R(72)**F(1, 4)*(s4**F(-1, 4))*R(k)*mu74*p12*p30*R(2)) + C1_cusp = cusp(F(64, 7)*1)*three**F(-1, 4) # k_{1/3} = (64/7) 3^{-1/4} + I_cusp = cusp(k1) + ratio_ok = (I_cusp*(C1_cusp**-1) == three**F(1, 4)*R(F(1, 2))) + # C0: 2 * p12 12^{-1/3} sigma3^{4/3} 2^{1/6} G(7/6) (2 pi)^{-1/2} = 2 * 72^{-1/6} G(7/6) (2 pi)^{-1/2} p12 sigma3^{4/3} + C0_fold = R(2)*p12*R(12)**F(-1, 3)*(s3**F(4, 3))*two**F(1, 6)*Mono.sym('G(7/6)')*(R(2)*pi)**F(-1, 2) + C0_print = R(2)*R(72)**F(-1, 6)*Mono.sym('G(7/6)')*(R(2)*pi)**F(-1, 2)*p12*(s3**F(4, 3)) + # B2 prefactors: 12^{1/3} M = 2^{1/2} 3^{1/3} G(5/6)(2 pi)^{-1/2} s3^{2/3}; B2^(2) = 12^{1/3} p12 M s4^2/(12 s3^2) + M = two**F(-1, 6)*Mono.sym('G(5/6)')*(R(2)*pi)**F(-1, 2)*(s3**F(2, 3)) + pref_ok = (R(12)**F(1, 3)*M == two**F(1, 2)*three**F(1, 3)*Mono.sym('G(5/6)')*(R(2)*pi)**F(-1, 2)*(s3**F(2, 3))) + FP = (R(2)*pi)**F(-1, 2)*(s3**F(-4, 3))*R(-6)*two**F(-7, 6)*Mono.sym('G(5/6)') # int (p3 - p3(0)) a^{-4/3} + B2b_lhs = -(s4**2*p12*R(F(1, 36))*R(12)**F(1, 3)*FP) + B2b_rhs = R(12)**F(1, 3)*p12*M*(s4**2)*R(F(1, 12))*(s3**-2) + checks = { + 'C1_printed_forms_agree': C1_a == C1_b, + 'CU2_at_d1_equals_C1': C1_cu == C1_a, + 'cusp_assembly_gives_C1': C1_cusp == C1_a, + 'I_over_C1_is_3^(1/4)/2': ratio_ok, + 'C0_from_fold_integral': C0_fold == C0_print, + 'B2_prefactor_2^(1/2)3^(1/3)': pref_ok, + 'B2_part2_closed_form': B2b_lhs == B2b_rhs, + } + return all(checks.values()), {k: v for k, v in checks.items()} + + +# ----------------------------------------------------------------------------------------------- C2: Mellin integrals +def zeta(theta, s): + a = theta*s + P_in = math.erf(a/math.sqrt(2)) + phi = math.exp(-a*a/2)/math.sqrt(2*math.pi) + return (P_in - 2*a*phi) + s*s*(1 - P_in) + + +def check_C2(): + # k_theta = 4 theta^{1/4} + (4/7) theta^{-7/4}; for theta = 1/3 both terms are rational multiples of 3^{-1/4} + k1 = F(4) + F(4, 7) + k13_coef = F(4) + F(4, 7)*9 # 4*3^{-1/4} + (4/7)*3^{7/4} = (4 + 36/7) 3^{-1/4} + if MUTANT == 'M2': + k1 = F(4) + exact = (k1 == F(32, 7)) and (k13_coef == F(64, 7)) + mu = 2**(7/8)*math.gamma(11/8)/math.sqrt(math.pi) + # quadrature in w = log s on [-60, W], W = log(60/theta) (beyond, zeta = 1 to double precision), plus the tail 4 e^{-W/4} + num = {} + for label, theta, k in (('1', 1.0, float(k1)), ('1/3', 1/3, float(k13_coef)*3**-0.25)): + n, a, b = 60000, -60.0, math.log(60/theta) + hstep = (b - a)/n + tot = 0.0 + for i in range(n + 1): + w = a + i*hstep + c = 1 if i in (0, n) else (4 if i % 2 else 2) + tot += c*zeta(theta, math.exp(w))*math.exp(-w/4) + tot = tot*hstep/3 + 4*math.exp(-b/4) + num[label] = round(tot/(k*mu), 9) + quad_ok = all(abs(v - 1) < 1e-7 for v in num.values()) + return exact and quad_ok, {'k1': str(k1), 'k_(1/3)': '%s * 3^(-1/4)' % k13_coef, + 'quadrature_ratio_to_k_mu': num} + + +# ----------------------------------------------------------------------------------------------- C3: the model +def pmul(a, b): + out = {} + for (i, j), x in a.items(): + for (k, l), y in b.items(): + out[(i + k, j + l)] = out.get((i + k, j + l), 0) + x*y + return {k: v for k, v in out.items() if v != 0} + + +def padd(*ps): + out = {} + for p in ps: + for k, v in p.items(): + out[k] = out.get(k, 0) + v + return {k: v for k, v in out.items() if v != 0} + + +def pc(c, p): + return {k: c*v for k, v in p.items() if c*v != 0} + + +X = {(1, 0): F(1)} # variables: (power of X, power of phi) +PHI = {(0, 1): F(1)} +ONE = {(0, 0): F(1)} + + +def lin(c0, c1): # c0 + c1 X + return padd({(0, 0): F(c0)}, {(1, 0): F(c1)}) + + +def g_poly(): + xp, xm = lin(F(1, 2), 1), lin(F(-1, 2), 1) + t1 = pc(2, pmul(pmul(xp, xp), lin(-1, 1))) + t2 = pc(3, pmul(PHI, pmul(pmul(xp, xm), pmul(xp, xm)))) + return padd(t1, t2) + + +def pderiv_X(p): + return {(i - 1, j): v*i for (i, j), v in p.items() if i > 0} + + +def peval(p, x, ph): + return sum(v*F(x)**i*F(ph)**j for (i, j), v in p.items()) + + +def gval(x, ph): + return 2*(x + F(1, 2))**2*(x - 1) + 3*ph*(x*x - F(1, 4))**2 + + +def decide(ph): + """Exact 1-D persistence of the model g at M = -1/2: returns (typed&adjacent, elder).""" + gpp_M = 6*(-1)*(1 - ph) # g''(-1/2) = -6(1 - phi) + gpp_S = 6*(1 + ph) + crit = [F(-1, 2), F(1, 2)] + if ph != 0: + crit.append(F(-1, 1)/(2*ph)) + crit = sorted(set(crit)) + adjacent = not any(F(-1, 2) < c < F(1, 2) for c in crit) + typed = gpp_M < 0 < gpp_S and adjacent + vals = {c: gval(c, ph) for c in crit} + gM, gS = vals[F(-1, 2)], vals[F(1, 2)] + # behaviour at -inf / +inf + if ph > 0: + end_left, end_right = 1, 1 + elif ph < 0: + end_left, end_right = -1, -1 + else: + end_left, end_right = -1, 1 + iM = crit.index(F(-1, 2)) + + def excursion(direction): + mn = gM + i = iM + direction + while 0 <= i < len(crit): + v = vals[crit[i]] + if v > gM: + return mn + mn = min(mn, v) + i += direction + end = end_left if direction < 0 else end_right + return mn if end > 0 else None # None = -infinity + mL, mR = excursion(-1), excursion(+1) + vals_d = [m for m in (mL, mR) if m is not None] + if not vals_d: + return typed, False + d = max(vals_d) + return typed, typed and d == gS + + +def check_C3(): + g = g_poly() + xp, xm = lin(F(1, 2), 1), lin(F(-1, 2), 1) + f1 = pmul(pmul(xp, xp), padd(pc(2, lin(-1, 1)), pc(3, pmul(PHI, pmul(xm, xm))))) + f2 = pmul(pmul(xm, xm), padd(pc(2, lin(1, 1)), pc(3, pmul(PHI, pmul(xp, xp))))) + gp_expected = pc(6, pmul(pmul(xp, xm), padd(ONE, pc(2, pmul(PHI, X))))) + ident = { + 'g = (X+1/2)^2[2(X-1) + 3 phi (X-1/2)^2]': padd(g, pc(-1, f1)) == {}, + 'g + 1 = (X-1/2)^2[2(X+1) + 3 phi (X+1/2)^2]': padd(g, ONE, pc(-1, f2)) == {}, + "g' = 6(X+1/2)(X-1/2)(1 + 2 phi X)": padd(pderiv_X(g), pc(-1, gp_expected)) == {}, + } + window = F(1, 2) if MUTANT == 'M1' else F(1, 3) + phis = [F(k, 59) for k in range(-58, 59) if k != 0] # 116 values in (-1, 1) + phis.append(F(1, 1000)) + crit_ok, margin_ok, decision_ok = True, True, True + eta = F(1, 30) + for ph in phis: + x3 = F(-1)/(2*ph) + if gval(x3, ph) != (ph - 1)**3*(3*ph + 1)/(16*ph**3) or gval(x3, ph) + 1 != (ph + 1)**3*(3*ph - 1)/(16*ph**3): + crit_ok = False + typed, elder = decide(ph) + if typed != (abs(ph) < 1): + decision_ok = False + if typed and elder != (abs(ph) < window): + decision_ok = False + # margins of Lemma 3.3 + if abs(ph) <= F(1, 3) - eta: + if not (gval(F(-3, 2), ph) <= -1 - 12*eta and gval(F(3, 2), ph) >= 12*eta): + margin_ok = False + for i in range(0, 41): + xl = F(-3, 2) + F(i, 40) # [-3/2, -1/2] + if not gval(xl, ph) <= -(xl + F(1, 2))**2: + margin_ok = False + xr = F(1, 2) + F(i, 40) # [1/2, 3/2] + if not gval(xr, ph) + 1 >= (xr - F(1, 2))**2: + margin_ok = False + if F(1, 3) + eta <= ph < 1: + if not (F(-3, 2) < x3 < F(-1, 2) and gval(F(-2), ph) >= F(9, 16) + and gval(x3, ph) + 1 >= F(1, 2)*(3*ph - 1)): + margin_ok = False + if -1 < ph <= -F(1, 3) - eta: + if not (F(1, 2) < x3 < F(3, 2) and gval(F(2), ph) + 1 <= -F(9, 16) + and gval(x3, ph) <= F(1, 2)*(3*ph + 1)): + margin_ok = False + # extension of (R) to 1 <= |phi| <= 6/5 (typed pairs with |phi| < 1 + eps/6) + ext_ok = True + for ph in (F(1), F(21, 20), F(11, 10), F(6, 5)): + if not gval(F(-2), ph) >= F(9, 16): + ext_ok = False + for i in range(0, 60): + xl = F(-2) + F(i, 40) # [-2, -1/2) + if not (gval(xl, ph) >= 0 and peval(pderiv_X(g), xl, ph) < 0): + ext_ok = False + for i in range(1, 61): + xr = F(1, 2) + F(i, 40) # (1/2, 2] + if not gval(xr, -ph) + 1 < 0: + ext_ok = False + ok = all(ident.values()) and crit_ok and margin_ok and decision_ok and ext_ok + return ok, {'identities': ident, 'critical_values_(3.1)': crit_ok, 'lemma_3.3_margins': margin_ok, + 'lemma_3.3_extension_|phi|>=1': ext_ok, 'decision_elder_iff_|phi|<1/3': decision_ok, 'n_phi': len(phis)} + + +# ----------------------------------------------------------------------------------------------- C4: pinned-law series +NS = 16 + + +def smul(a, b): + out = {} + for i, x in a.items(): + for j, y in b.items(): + k = i + j + if k < NS: + out[k] = out.get(k, 0) + x*y + return {k: v for k, v in out.items() if v != 0} + + +def sadd(a, b, cb=1): + out = dict(a) + for k, v in b.items(): + out[k] = out.get(k, 0) + cb*v + return {k: v for k, v in out.items() if v != 0} + + +def sscale(a, c): + return {k: c*v for k, v in a.items() if c*v != 0} + + +def sinv(a): + m = min(a) + a0 = a[m] + u = {k - m: v/a0 for k, v in a.items() if k != m} + out, term = {0: F(1)}, {0: F(1)} + for _ in range(NS + 8): + term = smul(term, sscale(u, -1)) + if not term: + break + out = sadd(out, term) + return {k - m: v/a0 for k, v in out.items() if k - m < NS} + + +def rho_der_series(rc, n, d): + """Series in tau of rho^{(n)}(x) at x = d * 2 tau, d in {-1, 0, 1}; rho(x) = sum_k rc[k] x^{2k}.""" + out = {} + for k, r in enumerate(rc): + p = 2*k - n + if p < 0: + continue + c = r*F(math.factorial(2*k), math.factorial(p)) + if d == 0: + if p == 0: + out[0] = out.get(0, 0) + c + elif p < NS: + out[p] = out.get(p, 0) + c*F(2*d)**p + return {k: v for k, v in out.items() if v != 0} + + +def pinned_series(rc): + pts = [(1, -1), (1, 1), (0, -1), (0, 1), (2, -1), (2, 1)] # f'(-t/2), f'(t/2), f(-t/2), f(t/2), f''(-t/2), f''(t/2) + + def cov(a, b): + (i, si), (j, sj) = pts[a], pts[b] + return sscale(rho_der_series(rc, i + j, (si - sj)//2), (-1)**j) + C = [[cov(a, b) for b in range(6)] for a in range(6)] + ti, ti2, ti3 = {-1: F(1, 2)}, {-2: F(1, 4)}, {-3: F(1, 8)} + U1 = {0: {0: F(1, 2)}, 1: {0: F(1, 2)}} + U2 = {0: sscale(ti, -1), 1: ti} + U3 = {0: sscale(ti2, 6), 1: sscale(ti2, 6), 2: sscale(ti3, 12), 3: sscale(ti3, -12)} + O = {4: {0: F(-1, 2)}, 5: {0: F(1, 2)}} + E1 = {4: {0: F(1, 2)}, 5: {0: F(1, 2)}} + + def V(A, B): + out = {} + for a, ca in A.items(): + for b, cb in B.items(): + out = sadd(out, smul(smul(ca, cb), C[a][b])) + return out + zero_blocks = all(not V(A, B) for A, B in ((U1, U2), (U2, U3), (O, U2), (E1, U1), (E1, U3), (O, E1))) + v11, v13, v33, v22 = V(U1, U1), V(U1, U3), V(U3, U3), V(U2, U2) + det2 = sadd(smul(v11, v33), smul(v13, v13), -1) + idet = sinv(det2) + o1, o3 = V(O, U1), V(O, U3) + b3 = smul(sadd(smul(o3, v11), smul(o1, v13), -1), idet) + b1 = smul(sadd(smul(o1, v33), smul(o3, v13), -1), idet) + e2 = V(E1, U2) + return {'zero_blocks': zero_blocks, 'det': smul(det2, v22), 'inv33': smul(v11, idet), 'c': b3, + 'v1': sadd(V(E1, E1), smul(smul(e2, e2), sinv(v22)), -1), + 'v2': sadd(V(O, O), sadd(smul(b1, o1), smul(b3, o3)), -1)} + + +def kernels(): + K = 14 + gauss = [F((-1)**k, 2**k*math.factorial(k)) for k in range(K)] + mix = [(F((-1)**k, 2**k*math.factorial(k)) + F((-2)**k, math.factorial(k)))/2 for k in range(K)] + return {'exp(-x^2/2)': gauss, '(exp(-x^2/2)+exp(-2x^2))/2': mix} + + +def lambdas(rc): + return {2*j: (-1)**j*rc[j]*math.factorial(2*j) for j in range(1, 7)} + + +def formulas(lam): + l2, l4, l6, l8, l10 = (lam[i] for i in (2, 4, 6, 8, 10)) + Dd = l2*l6 - l4**2 + c2 = -(l2*l8 - l4*l6)/(15*Dd) + if MUTANT == 'M3': + c2 = -c2 + return {'D': Dd, 'c2': c2, + 'd2': (8*l4**2*l6 - 3*l2*l4*l8 - 5*l2*l6**2)/(15*l4*Dd), + 'q2': (l2**2*l8 - 6*l2*l4*l6 + 5*l4**3)/(5*l2*Dd), + 'v1_4': (l8 - l6**2/l4)/9, + 'v2_6': (l10 - (l6**3 - 2*l4*l6*l8 + l2*l8**2)/Dd)/225} + + +def check_C4(): + info, ok = {}, True + for name, rc in kernels().items(): + lam = lambdas(rc) + fm = formulas(lam) + s = pinned_series(rc) + l2, l4 = lam[2], lam[4] + Dd = fm['D'] + parity = (all(k % 2 == 0 for k in s['det']) and all(k % 2 == 0 for k in s['inv33']) + and all(k % 2 == 1 for k in s['c']) and all(k % 2 == 0 for k in s['v1']) and all(k % 2 == 0 for k in s['v2'])) + res = { + 'zero_blocks': s['zero_blocks'], + 'parity': parity, + 'c = tau(1 + c2 tau^2 + ...)': s['c'].get(1) == 1 and s['c'].get(3) == fm['c2'], + 'det = l4 D (1 + d2 tau^2 + ...)': s['det'].get(0) == l4*Dd and s['det'].get(2) == l4*Dd*fm['d2'], + 'inv33 = (l2/D)(1 + q2 tau^2 + ...)': s['inv33'].get(0) == l2/Dd and s['inv33'].get(2) == l2/Dd*fm['q2'], + 'v1 = sigma4^2 tau^4/9 + ...': min(s['v1']) == 4 and s['v1'][4] == fm['v1_4'], + 'v2 = (tau^6/225) Var(a5|a1,a3) + ...': min(s['v2']) == 6 and s['v2'][6] == fm['v2_6'], + } + ok = ok and all(res.values()) + info[name] = {'checks': res, 'lambda': {str(k): str(v) for k, v in lam.items()}, + 'c2': str(fm['c2']), 'd2': str(fm['d2']), 'q2': str(fm['q2'])} + return ok, info + + +# ----------------------------------------------------------------------------------------------- C5: B2 assembly +VARS = ('l2', 'l4', 'l6', 'l8') + + +def mono(**kw): + return {tuple(kw.get(v, 0) for v in VARS): F(1)} + + +def mpoly_mul(a, b): + out = {} + for ka, va in a.items(): + for kb, vb in b.items(): + k = tuple(x + y for x, y in zip(ka, kb)) + out[k] = out.get(k, 0) + va*vb + return {k: v for k, v in out.items() if v != 0} + + +def mpoly_add(*ps): + out = {} + for p in ps: + for k, v in p.items(): + out[k] = out.get(k, 0) + v + return {k: v for k, v in out.items() if v != 0} + + +def mpc(c, p): + return {k: c*v for k, v in p.items() if c*v != 0} + + +def check_C5(): + l2, l4, l6, l8 = (mono(**{v: 1}) for v in VARS) + D = mpoly_add(mpoly_mul(l2, l6), mpc(-1, mpoly_mul(l4, l4))) + sgn = -1 if MUTANT == 'M3' else 1 + # 30 l2 l4 D * 2 c2 = -4 l2 l4 (l2 l8 - l4 l6) + t_c = mpc(-4*sgn, mpoly_mul(mpoly_mul(l2, l4), mpoly_add(mpoly_mul(l2, l8), mpc(-1, mpoly_mul(l4, l6))))) + # 30 l2 l4 D * (-d2/2) = -l2 (8 l4^2 l6 - 3 l2 l4 l8 - 5 l2 l6^2) + t_d = mpc(-1, mpoly_mul(l2, mpoly_add(mpc(8, mpoly_mul(mpoly_mul(l4, l4), l6)), mpc(-3, mpoly_mul(mpoly_mul(l2, l4), l8)), + mpc(-5, mpoly_mul(mpoly_mul(l2, l6), l6))))) + # 30 l2 l4 D * (-5 q2/6) = -5 l4 (l2^2 l8 - 6 l2 l4 l6 + 5 l4^3) + t_q = mpc(-5, mpoly_mul(l4, mpoly_add(mpoly_mul(mpoly_mul(l2, l2), l8), mpc(-6, mpoly_mul(mpoly_mul(l2, l4), l6)), + mpc(5, mpoly_mul(mpoly_mul(l4, l4), l4))))) + lhs1 = mpoly_add(t_c, t_d, t_q) + rhs1 = mpoly_add(mpc(-6, mono(l2=2, l4=1, l8=1)), mpc(26, mono(l2=1, l4=2, l6=1)), mpc(5, mono(l2=2, l6=2)), + mpc(-25, mono(l4=4))) + # 120 l2 l4 D * s4^2/(12 s3^2) = 10 l2^2 (l4 l8 - l6^2) + t_s = mpc(10, mpoly_mul(mpoly_mul(l2, l2), mpoly_add(mpoly_mul(l4, l8), mpc(-1, mpoly_mul(l6, l6))))) + c26 = 25 if MUTANT == 'M4' else 26 + Q = mpoly_add(mpc(4, mono(l2=2, l4=1, l8=1)), mpc(c26, mono(l2=1, l4=2, l6=1)), mpc(-5, mono(l2=2, l6=2)), + mpc(-25, mono(l4=4))) + id1 = mpoly_add(lhs1, mpc(-1, rhs1)) == {} + id2 = mpoly_add(lhs1, t_s, mpc(-1, Q)) == {} + # v1.1 sign decomposition: Q = 4 l2^2 (l4 l8 - l6^2) + D (25 l4^2 - l2 l6) = 4 l2^2 l4 s4^2 + D (24 l4^2 - D) + sgn_dec = mpoly_add(mpc(4, mpoly_mul(mpoly_mul(l2, l2), mpoly_add(mpoly_mul(l4, l8), mpc(-1, mpoly_mul(l6, l6))))), + mpoly_mul(D, mpoly_add(mpc(25, mpoly_mul(l4, l4)), mpc(-1, mpoly_mul(l2, l6))))) + id3 = mpoly_add(Q, mpc(-1, sgn_dec)) == {} + # individual coefficient formulas against the exact rational values of C4 (Gaussian kernel and mixture) + vals = {} + for name, rc in kernels().items(): + lam = lambdas(rc) + fm = formulas(lam) + L2, L4, L6, L8 = (lam[i] for i in (2, 4, 6, 8)) + Dd = fm['D'] + s3sq, s4sq = Dd/L2, L8 - L6**2/L4 + bracket = (2*fm['c2'] - fm['d2']/2 - 5*fm['q2']/6)/4 + s4sq/(12*s3sq) + Qv = 4*L2**2*L4*L8 + c26*L2*L4**2*L6 - 5*L2**2*L6**2 - 25*L4**4 + vals[name] = {'bracket': str(bracket), 'Q/(120 l2 l4 D)': str(Qv/(120*L2*L4*Dd)), + 'agree': bracket == Qv/(120*L2*L4*Dd), + 'l2l6/l4^2': str(L2*L6/L4**2), 'sufficient_l2l6<=25l4^2': L2*L6 <= 25*L4**2, 'Q>0': Qv > 0} + gauss_34 = vals['exp(-x^2/2)']['Q/(120 l2 l4 D)'] == '3/4' + # the sign of B2 is not fixed by (H) (Codex review on Math- #214): two-mode spectrum, weights 1 - 1e-5 and 1e-5 at + # frequencies 1 and 40 (L = 2 pi); adding small positive weights at every other frequency gives (H) and, by + # continuity of Q in (l2, l4, l6, l8), keeps Q < 0 + eps = F(1, 10**5) + lt = [(1 - eps) + eps*F(40)**(2*j) for j in range(5)] + Qt = 4*lt[1]**2*lt[2]*lt[4] + c26*lt[1]*lt[2]**2*lt[3] - 5*lt[1]**2*lt[3]**2 - 25*lt[2]**4 + two_mode = {'Q': '%.8e' % float(Qt), 'Q<0': Qt < 0, 'l2l6/l4^2': '%.6f' % float(lt[1]*lt[3]/lt[2]**2), + 'l2l6>25l4^2': lt[1]*lt[3] > 25*lt[2]**2} + signs_ok = (all(v['sufficient_l2l6<=25l4^2'] and v['Q>0'] for v in vals.values()) + and two_mode['Q<0'] and two_mode['l2l6>25l4^2']) + ok = id1 and id2 and id3 and gauss_34 and signs_ok and all(v['agree'] for v in vals.values()) + return ok, {'identity_30l2l4D(2c2-d2/2-5q2/6)': id1, 'identity_sum_equals_Q': id2, + 'identity_Q=4l2^2l4s4^2+D(24l4^2-D)': id3, 'values': vals, + 'gauss_Q_over_120l2l4D_is_3/4': gauss_34, + 'two_mode_1_40_eps1e-5_sign_not_fixed_by_H': two_mode} + + +# ----------------------------------------------------------------------------------------------- C6: two-point Rice +getcontext().prec = 60 +D_ = Decimal + + +def He(n, x): + h0, h1 = D_(1), x + if n == 0: + return h0 + for k in range(1, n): + h0, h1 = h1, x*h1 - k*h0 + return h1 + + +def rder(kernel, n, x): + g = (-1)**n*He(n, x)*(-(x*x)/2).exp() + if kernel == 'gauss': + return g + return (g + (-1)**n*D_(2)**n*He(n, 2*x)*(-2*x*x).exp())/2 + + +def solve(M, b): + n = len(M) + A = [M[i][:] + [b[i]] for i in range(n)] + for i in range(n): + p = max(range(i, n), key=lambda r: abs(A[r][i])) + A[i], A[p] = A[p], A[i] + for r in range(n): + if r != i: + f = A[r][i]/A[i][i] + A[r] = [x - f*y for x, y in zip(A[r], A[i])] + return [A[i][n]/A[i][i] for i in range(n)] + + +def det3(M): + return (M[0][0]*(M[1][1]*M[2][2] - M[1][2]*M[2][1]) - M[0][1]*(M[1][0]*M[2][2] - M[1][2]*M[2][0]) + + M[0][2]*(M[1][0]*M[2][1] - M[1][1]*M[2][0])) + + +def gauss_legendre(n): + xs, ws = [], [] + for i in range(1, n + 1): + x = math.cos(math.pi*(i - 0.25)/(n + 0.5)) + for _ in range(100): + p0, p1 = 1.0, x + for k in range(2, n + 1): + p0, p1 = p1, ((2*k - 1)*x*p1 - (k - 1)*p0)/k + dp = n*(x*p1 - p0)/(x*x - 1) + dx = p1/dp + x -= dx + if abs(dx) < 1e-16: + break + xs.append(x) + ws.append(2/((1 - x*x)*dp*dp)) + return xs, ws + + +GX, GW = gauss_legendre(20) +XO, WO = gauss_legendre(24) + + +def Phi(x): + return 0.5*math.erfc(-x/math.sqrt(2)) + + +def phi_(x): + return math.exp(-x*x/2)/math.sqrt(2*math.pi) + + +def Epos(mx, my, sx, sy, rho): + """E[X^+ Y^+] for (X, Y) ~ N((mx, my), [[sx^2, rho sx sy], [., sy^2]]) (closed form when both means are far).""" + a, b = mx/sx, my/sy + if a > 30 and b > 30: + return sx*sy*(a*b + rho) + if a < -30 or b < -30: + return 0.0 + s = sy*math.sqrt(max(1 - rho*rho, 0.0)) + beta = rho*sy/sx + lo, hi = max(0.0, mx - 13*sx), mx + 13*sx + if hi <= 0: + return 0.0 + cuts = {lo, hi} + cuts.update(mx + k*sx for k in range(-12, 13) if lo < mx + k*sx < hi) + if beta != 0: + xk = mx - my/beta + if lo < xk < hi: + cuts.add(xk) + wk = s/abs(beta) + for j in (0.5, 1, 2, 4, 8, 16, 32, 64): + for sg in (-1, 1): + if lo < xk + sg*j*wk < hi: + cuts.add(xk + sg*j*wk) + cuts = sorted(cuts) + tot = 0.0 + for u, v in zip(cuts[:-1], cuts[1:]): + for x, w in zip(GX, GW): + xx = u + (v - u)*(x + 1)/2 + m2 = my + beta*(xx - mx) + inner = m2*Phi(m2/s) + s*phi_(m2/s) if s > 0 else max(m2, 0.0) + tot += w*(v - u)/2*xx*phi_((xx - mx)/sx)/sx*inner + return tot + + +def g_rice(kernel, t, h): + t, h, z = D_(repr(t)), D_(repr(h)), D_(0) + pts = [(0, z), (1, z), (2, z), (0, t), (1, t), (2, t)] + C = [[(-1)**j*rder(kernel, i + j, si - sj) for (j, sj) in pts] for (i, si) in pts] + U = [[z, D_('0.5'), z, z, D_('0.5'), z], [z, -1/t, z, z, 1/t, z], [12/t**3, 6/t**2, z, -12/t**3, 6/t**2, z]] + T = [[z, z, -1, z, z, z], [z, z, z, z, z, D_(1)]] + + def cv(a, b): + return sum(a[i]*C[i][j]*b[j] for i in range(6) for j in range(6) if a[i] and b[j]) + CUU = [[cv(a, b) for b in U] for a in U] + u = [z, z, 12*h/t**3] + x = solve(CUU, u) + y = [solve(CUU, [cv(Tk, a) for a in U]) for Tk in T] + m = [sum(cv(Tk, U[k])*x[k] for k in range(3)) for Tk in T] + S = [[cv(T[i], T[j]) - sum(cv(T[i], U[k])*y[j][k] for k in range(3)) for j in range(2)] for i in range(2)] + q = sum(u[k]*x[k] for k in range(3)) + pU = float((-q/2).exp()/((2*D_(math.pi))**3*det3(CUU)).sqrt()) + sx, sy = float(S[0][0].sqrt()), float(S[1][1].sqrt()) + rho = float(S[0][1]/(S[0][0]*S[1][1]).sqrt()) + jac = 1.0 if MUTANT == 'M5' else 12.0 + return pU*jac/float(t)**4*Epos(float(m[0]), float(m[1]), sx, sy, rho) + + +def rice_F(kernel, h, t0, sig3): + lh = math.log(h) + main = [math.log(12*h/(m*sig3))/3 for m in (40, 20, 10, 6, 4, 2.5, 1.5, 1, 0.5, 0.25)] + cuts = sorted(c for c in main + [lh/4 - 1, lh/4 - 0.5, lh/4, lh/4 + 0.5, lh/4 + 1, lh/4 + 2, math.log(t0)] + if c <= math.log(t0)) + tot = 0.0 + for a, b in zip(cuts[:-1], cuts[1:]): + for x, w in zip(XO, WO): + ww = a + (b - a)*(x + 1)/2 + tt = math.exp(ww) + tot += w*(b - a)/2*tt*g_rice(kernel, tt, h) + return tot + + +def lstsq3(rows, ys): + A = [[sum(r[i]*r[j] for r in rows) for j in range(3)] for i in range(3)] + b = [sum(r[i]*y for r, y in zip(rows, ys)) for i in range(3)] + M = [A[i][:] + [b[i]] for i in range(3)] + for i in range(3): + p = max(range(i, 3), key=lambda r: abs(M[r][i])) + M[i], M[p] = M[p], M[i] + for r in range(3): + if r != i: + f = M[r][i]/M[i][i] + M[r] = [x - f*y for x, y in zip(M[r], M[i])] + return [M[i][3]/M[i][i] for i in range(3)] + + +def constants_float(lam): + l2, l4, l6, l8 = (float(lam[i]) for i in (2, 4, 6, 8)) + Dd = l2*l6 - l4**2 + s3, s4 = math.sqrt(Dd/l2), math.sqrt(l8 - l6**2/l4) + p12 = 1/(2*math.pi*math.sqrt(l2*l4)) + C0 = 2*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 + Icand = 3**0.25/2*C1 + Q = 4*l2**2*l4*l8 + 26*l2*l4**2*l6 - 5*l2**2*l6**2 - 25*l4**4 + B2 = 2**0.5*3**(1/3)*math.gamma(5/6)*(2*math.pi)**-0.5*p12*s3**(2/3)*Q/(120*l2*l4*Dd) + return {'C0': C0, 'C1': C1, 'I': Icand, 'B2': B2, 'sigma3': s3} + + +def check_C6(): + out, ok = {}, True + ks = kernels() + for kname, kernel, t0 in (('exp(-x^2/2)', 'gauss', 0.04), ('(exp(-x^2/2)+exp(-2x^2))/2', 'mix', 0.01)): + cst = constants_float(lambdas(ks[kname])) + a_pred, b_pred = cst['I']/cst['C0'], cst['B2']/(cst['C0']/2) + rows, ys, pts = [], [], {} + for e in (11, 12, 13, 14, 15, 16): + h = 10.0**(-e) + dev = h**(1/3)*rice_F(kernel, h, t0, cst['sigma3'])/(cst['C0']/2) - 1 + y = dev/h**(7/12) + rows.append([1.0, h**(1/12), h**-0.25]) + ys.append(y) + pts['1e-%d' % e] = float('%.6f' % y) + fa, fb, fr = lstsq3(rows, ys) + good = abs(fa - a_pred) < 2e-4 and abs(fb - b_pred) < 3e-3 + ok = ok and good + out[kname] = {'t0': t0, 'C0': float('%.8f' % cst['C0']), 'C1': float('%.8f' % cst['C1']), + 'I': float('%.8f' % cst['I']), 'B2': float('%.8f' % cst['B2']), + 'a_pred_I/C0': float('%.7f' % a_pred), 'b_pred_B2/(C0/2)': float('%.7f' % b_pred), + 'dev/h^(7/12)': pts, 'fit_a': float('%.4f' % fa), 'fit_b': float('%.3f' % fb), 'within_tolerance': good} + return ok, out + + +# ----------------------------------------------------------------------------------------------- main +def main(): + global MUTANT + ap = argparse.ArgumentParser() + ap.add_argument('--mutant', default=None) + args = ap.parse_args() + if args.mutant is not None and args.mutant not in ('M1', 'M2', 'M3', 'M4', 'M5'): + sys.stderr.write('unknown mutant label\n') + return 2 + MUTANT = args.mutant + results = {} + for name, fn in (('C1_constants', check_C1), ('C2_mellin', check_C2), ('C3_model_window', check_C3), + ('C4_pinned_series', check_C4), ('C5_B2_assembly', check_C5), ('C6_rice_integral', check_C6)): + ok, info = fn() + results[name] = {'passed': bool(ok), 'info': info} + out = {'object': 'CL-D1-THIRD-ORDER-20261001-v1.1 exact controls', 'scientific_effect': 'NONE', + 'mutant': MUTANT, 'passed': all(r['passed'] for r in results.values()), 'checks': results} + sys.stdout.write(json.dumps(out, indent=1, sort_keys=True) + '\n') + return 0 if out['passed'] else 1 + + +if __name__ == '__main__': + sys.exit(main())