From b497cc92dedebb985bfe5df0f14b7f6a486905c0 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 3 Apr 2026 17:58:08 +0000 Subject: [PATCH 1/2] Initial plan From 54f4f007e89818c6a2c07efa4eda5461261ec018 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 3 Apr 2026 18:13:51 +0000 Subject: [PATCH 2/2] N9.4: add KernelCommutatorDecay.lean with formal far-range bound proof MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - KernelDecayHyp structure: |K(j,k)| ≤ E0·exp(−ν·(j−k)), E0/ν/T documented - farRange_bound: ∑ₙ |K(k+J+n,k)| ≤ E0·exp(−ν·J)·(1−exp(−ν))⁻¹ (zero sorry) - chooseJ: J(ε) = ⌈log(E0/(ε·(1−exp(−ν))))/ν⌉₊ - farRange_le_eps: with J=J(ε), far-range ≤ ε uniformly in k (zero sorry) - docs/analysis_ns/README.md: N9.4 section with assumptions/bound/J(ε)/dependence table Agent-Logs-Url: https://github.com/TOTOGT/DM3-lab/sessions/cc3a9150-34f6-48b8-9b61-8cd41596f4b6 Co-authored-by: TOTOGT <266586635+TOTOGT@users.noreply.github.com> --- docs/analysis_ns/README.md | 49 ++++++ lean/KernelCommutatorDecay.lean | 262 ++++++++++++++++++++++++++++++++ 2 files changed, 311 insertions(+) create mode 100644 lean/KernelCommutatorDecay.lean diff --git a/docs/analysis_ns/README.md b/docs/analysis_ns/README.md index 68dbf40..618cffb 100644 --- a/docs/analysis_ns/README.md +++ b/docs/analysis_ns/README.md @@ -11,3 +11,52 @@ Guidelines: Current status: waiting for observable definition (A/B events, class space, scale parameter, admissibility, windowing/weighting, baseline p0) from N9.2 #8 / N9.1 #9. +--- + +## N9.4 — Kernel Commutator Lemma: Far-Range Decay + +**Formal Lean 4 proof:** `lean/KernelCommutatorDecay.lean` + +### Kernel decay assumption + +The curvature operator **K** in the AXLE chain C → K → F → U acts at discrete scales +j ∈ ℤ through a kernel K(j, k). The decay hypothesis (`KernelDecayHyp`) states: + +``` +|K(j, k)| ≤ E0 · exp(−ν · (j − k)) for all j ≥ k +``` + +Constants: + +| Symbol | Role | Sign | +|--------|------|------| +| E0 | Amplitude bound (may encode a time horizon T via E0 = C₀ · T) | > 0 | +| ν | Spectral-gap decay rate | > 0 | +| T | Scale / time horizon (enters via E0) | > 0 | +| ε | Far-range tolerance | > 0 | +| J | Far-range cut-off index | ∈ ℕ | + +### Far-range bound + +For any base scale k and cut-off J: + +``` +∑_{n ≥ 0} |K(k + J + n, k)| ≤ E0 · exp(−ν · J) · (1 − exp(−ν))⁻¹ +``` + +Proof: comparison with the geometric series ∑ exp(−ν)ⁿ = (1 − exp(−ν))⁻¹. +The bound is **uniform in k**. + +### Choice of J(ε) + +``` +J(ε) := ⌈ log(E0 / (ε · (1 − exp(−ν)))) / ν ⌉₊ +``` + +With J = J(ε), the far-range sum is ≤ ε (theorem `farRange_le_eps`). + +**Dependence on E0, ν, T:** +- J(ε) ~ (1/ν) · log(E0 / ε) as ε → 0. +- Larger E0 (or T) → larger J(ε). +- Larger ν (faster decay) → smaller J(ε). + diff --git a/lean/KernelCommutatorDecay.lean b/lean/KernelCommutatorDecay.lean new file mode 100644 index 0000000..4796aaa --- /dev/null +++ b/lean/KernelCommutatorDecay.lean @@ -0,0 +1,262 @@ +/- + N9.4 — Kernel Commutator Lemma: Far-Range Decay + G6 LLC · Pablo Nogueira Grossi · Newark NJ · 2026 + MIT License + + Quantifies how the far-range (j ≥ k + J) contribution of a + convolution-type kernel is controlled by exponential decay, and + provides the explicit formula for J(ε) ensuring far-range ≤ ε + uniformly. + + Parameters + ---------- + E0 : ℝ — kernel amplitude bound (E0 > 0) + ν : ℝ — decay exponent (ν > 0) + T : ℝ — summation / scale horizon (T > 0) [enters via E0 · T product] + ε : ℝ — tolerance (ε > 0) + J : ℕ — far-range cut-off index + + Operator context + ---------------- + In the AXLE chain C → K → F → U, the curvature operator K acts at + discrete scales j ∈ ℤ. Two scales j and k interact through the + kernel K(j, k). When |j − k| ≥ J (far range), the kernel decay + assumption guarantees the interaction is uniformly small. + + Main results + ------------ + · farRange_bound : ∑ₙ |K(k + J + n, k)| ≤ E0 · exp(−ν·J) · (1 − exp(−ν))⁻¹ + · chooseJ : J(ε) := ⌈log(E0 / (ε · (1 − exp(−ν)))) / ν⌉₊ + · farRange_le_eps : with J = J(ε), far-range sum ≤ ε +-/ + +import Mathlib.Analysis.SpecialFunctions.Log.Basic +import Mathlib.Topology.Algebra.InfiniteSum.Basic +import Mathlib.Analysis.SpecificLimits.Basic +import Mathlib.Topology.Algebra.InfiniteSum.Order + +namespace TOGT + +-- ============================================================ +-- SECTION N9.4.1: KERNEL DECAY ASSUMPTIONS AND CONSTANTS +-- ============================================================ + +/-- Kernel decay hypothesis for the AXLE curvature operator K. + + The kernel K : ℤ → ℤ → ℝ satisfies an exponential decay bound + in the scale separation j − k: + + |K(j, k)| ≤ E0 · exp(−ν · (j − k)) for all j ≥ k + + Constants: + · E0 > 0 : amplitude bound (may depend on the time horizon T via E0 = C · T) + · ν > 0 : decay rate (determined by the spectral gap of the curvature) + + This is the standing assumption for all far-range estimates. + It captures the off-diagonal decay standard in Calderón–Zygmund + and pseudodifferential operator theory. -/ +structure KernelDecayHyp (K : ℤ → ℤ → ℝ) (E0 ν : ℝ) : Prop where + /-- Amplitude bound is positive. -/ + E0_pos : 0 < E0 + /-- Decay rate is positive. -/ + ν_pos : 0 < ν + /-- Pointwise exponential decay for j ≥ k. -/ + decay : ∀ (j k : ℤ), k ≤ j → + |K j k| ≤ E0 * Real.exp (-ν * (↑(j - k) : ℝ)) + +-- ============================================================ +-- SECTION N9.4.2: GEOMETRIC SERIES AUXILIARY LEMMAS +-- ============================================================ + +private lemma exp_neg_nonneg (ν : ℝ) : 0 ≤ Real.exp (-ν) := + le_of_lt (Real.exp_pos _) + +private lemma exp_neg_lt_one {ν : ℝ} (hν : 0 < ν) : Real.exp (-ν) < 1 := by + rw [Real.exp_lt_one_iff]; linarith + +/-- The series ∑ₙ exp(−ν)ⁿ is summable for ν > 0. -/ +private lemma summable_exp_geo (ν : ℝ) (hν : 0 < ν) : + Summable (fun n : ℕ => Real.exp (-ν) ^ n) := + summable_geometric_of_lt_one (exp_neg_nonneg ν) (exp_neg_lt_one hν) + +/-- The series ∑ₙ exp(−ν)ⁿ = (1 − exp(−ν))⁻¹ for ν > 0. + This is the key geometric-series identity. -/ +private lemma tsum_exp_geo (ν : ℝ) (hν : 0 < ν) : + ∑' n : ℕ, Real.exp (-ν) ^ n = (1 - Real.exp (-ν))⁻¹ := + tsum_geometric_of_lt_one (exp_neg_nonneg ν) (exp_neg_lt_one hν) + +/-- exp(−ν)ⁿ = exp(−ν · n). Proved by induction on n using exp_add. -/ +private lemma exp_pow_eq_exp_mul (ν : ℝ) (n : ℕ) : + Real.exp (-ν) ^ n = Real.exp (-ν * ↑n) := by + induction n with + | zero => simp + | succ k ih => + rw [pow_succ, ih, ← Real.exp_add] + congr 1 + push_cast + ring + +-- ============================================================ +-- SECTION N9.4.3: FAR-RANGE BOUND +-- ============================================================ + +/-- **Far-range bound.** + + Under KernelDecayHyp K E0 ν, for any base scale k : ℤ and + cut-off J : ℕ, the series of absolute kernel values over all + far-range displacements n ≥ 0 satisfies: + + ∑ₙ |K(k + J + n, k)| ≤ E0 · exp(−ν · J) · (1 − exp(−ν))⁻¹ + + Proof strategy + ────────────── + 1. Bound each term by the geometric majorant + |K(k+J+n, k)| ≤ E0 · exp(−ν·J) · exp(−ν)ⁿ. + 2. The majorant series is summable (geometric series, ratio exp(−ν) < 1). + 3. Apply the comparison test and evaluate the geometric sum. + + Dependence: the bound scales as E0 (amplitude), decays in ν (rate), + and in J (cut-off); if E0 incorporates a time horizon T, the + dependence on T appears linearly through E0 · T. -/ +theorem farRange_bound + (K : ℤ → ℤ → ℝ) (E0 ν : ℝ) + (hK : KernelDecayHyp K E0 ν) + (k : ℤ) (J : ℕ) : + ∑' n : ℕ, |K (k + ↑J + ↑n) k| ≤ + E0 * Real.exp (-ν * ↑J) * (1 - Real.exp (-ν))⁻¹ := by + -- Step 1: pointwise bound on each term + have hmaj : ∀ n : ℕ, |K (k + ↑J + ↑n) k| ≤ + E0 * Real.exp (-ν * ↑J) * Real.exp (-ν) ^ n := by + intro n + -- The index k + J + n is ≥ k + have hle : k ≤ k + ↑J + ↑n := by + have h1 : (0 : ℤ) ≤ ↑J := Int.coe_nat_nonneg J + have h2 : (0 : ℤ) ≤ ↑n := Int.coe_nat_nonneg n + linarith + -- Apply the decay hypothesis + have hdecay := hK.decay (k + ↑J + ↑n) k hle + -- Simplify the cast of the scale difference + have hcast : (↑(k + ↑J + ↑n - k) : ℝ) = (↑J : ℝ) + ↑n := by + push_cast; ring + rw [hcast] at hdecay + -- Factor the exponential and convert to geometric form + calc |K (k + ↑J + ↑n) k| + ≤ E0 * Real.exp (-ν * (↑J + ↑n)) := hdecay + _ = E0 * (Real.exp (-ν * ↑J) * Real.exp (-ν) ^ n) := by + rw [show -ν * ((↑J : ℝ) + ↑n) = (-ν * ↑J) + (-ν * ↑n) by ring, + Real.exp_add, exp_pow_eq_exp_mul] + _ = E0 * Real.exp (-ν * ↑J) * Real.exp (-ν) ^ n := by ring + -- Step 2: the majorant series is summable + have hg_sum : Summable (fun n : ℕ => E0 * Real.exp (-ν * ↑J) * Real.exp (-ν) ^ n) := + (summable_exp_geo ν hK.ν_pos).mul_left _ + -- Step 3: the kernel series is summable by comparison + have hf_sum : Summable (fun n : ℕ => |K (k + ↑J + ↑n) k|) := + Summable.of_norm_bounded _ hg_sum (fun n => by + simp only [Real.norm_eq_abs, abs_abs]; exact hmaj n) + -- Step 4: compare the sums and evaluate the geometric series + calc ∑' n : ℕ, |K (k + ↑J + ↑n) k| + ≤ ∑' n : ℕ, E0 * Real.exp (-ν * ↑J) * Real.exp (-ν) ^ n := + tsum_le_tsum hmaj hf_sum hg_sum + _ = E0 * Real.exp (-ν * ↑J) * ∑' n : ℕ, Real.exp (-ν) ^ n := by + rw [tsum_mul_left] + _ = E0 * Real.exp (-ν * ↑J) * (1 - Real.exp (-ν))⁻¹ := by + rw [tsum_exp_geo ν hK.ν_pos] + +-- ============================================================ +-- SECTION N9.4.4: CHOICE OF J(ε) AND MAIN COROLLARY +-- ============================================================ + +/-- **Optimal cut-off index J(ε).** + + Given amplitude E0, decay rate ν, and tolerance ε, define: + + J(ε) := ⌈ log(E0 / (ε · (1 − exp(−ν)))) / ν ⌉₊ + + This is the smallest natural number J such that the far-range + bound E0 · exp(−ν · J) · (1 − exp(−ν))⁻¹ is ≤ ε. + + Dependence: + · Larger E0 (or larger T when E0 = C · T) → larger J(ε). + · Larger ν (faster decay) → smaller J(ε). + · Smaller ε (tighter tolerance) → larger J(ε). + · Growth: J(ε) ~ (1/ν) · log(E0 / ε) as ε → 0. -/ +noncomputable def chooseJ (E0 ν ε : ℝ) : ℕ := + ⌈Real.log (E0 / (ε * (1 - Real.exp (-ν)))) / ν⌉₊ + +/-- **Main corollary: far-range ≤ ε with J = J(ε).** + + Under KernelDecayHyp K E0 ν, for any base scale k and ε > 0, + setting J = chooseJ E0 ν ε yields: + + ∑ₙ |K(k + J(ε) + n, k)| ≤ ε + + This is the kernel commutator lemma for the AXLE operator chain: + truncating the scale interaction at J(ε) incurs error ≤ ε + uniformly in k. -/ +theorem farRange_le_eps + (K : ℤ → ℤ → ℝ) (E0 ν ε : ℝ) + (hK : KernelDecayHyp K E0 ν) + (hε : 0 < ε) + (k : ℤ) : + ∑' n : ℕ, |K (k + ↑(chooseJ E0 ν ε) + ↑n) k| ≤ ε := by + set J := chooseJ E0 ν ε with hJ_def + -- 1 − exp(−ν) > 0 because exp(−ν) < 1 + have h1mexp_pos : 0 < 1 - Real.exp (-ν) := by + linarith [exp_neg_lt_one hK.ν_pos] + -- The argument of the logarithm is positive + have harg_pos : 0 < E0 / (ε * (1 - Real.exp (-ν))) := + div_pos hK.E0_pos (mul_pos hε h1mexp_pos) + -- J ≥ log(...) / ν by the ceiling definition + have hJ_ge : Real.log (E0 / (ε * (1 - Real.exp (-ν)))) / ν ≤ (↑J : ℝ) := + Nat.le_ceil _ + -- Therefore exp(−ν · J) ≤ ε · (1 − exp(−ν)) / E0 + have hexp_bound : Real.exp (-ν * ↑J) ≤ ε * (1 - Real.exp (-ν)) / E0 := by + have hlog_le : Real.log (E0 / (ε * (1 - Real.exp (-ν)))) ≤ ν * ↑J := by + have := (div_le_iff hK.ν_pos).mp hJ_ge; linarith + calc Real.exp (-ν * ↑J) + ≤ Real.exp (-Real.log (E0 / (ε * (1 - Real.exp (-ν))))) := by + apply Real.exp_le_exp.mpr; linarith + _ = (E0 / (ε * (1 - Real.exp (-ν))))⁻¹ := by + rw [Real.exp_neg, Real.exp_log harg_pos] + _ = ε * (1 - Real.exp (-ν)) / E0 := by + rw [inv_div] + -- Apply farRange_bound and simplify with the above estimate + have hbound := farRange_bound K E0 ν hK k J + have h1mexp_nn : 0 ≤ (1 - Real.exp (-ν))⁻¹ := + inv_nonneg.mpr (le_of_lt h1mexp_pos) + calc ∑' n : ℕ, |K (k + ↑J + ↑n) k| + ≤ E0 * Real.exp (-ν * ↑J) * (1 - Real.exp (-ν))⁻¹ := hbound + _ ≤ E0 * (ε * (1 - Real.exp (-ν)) / E0) * (1 - Real.exp (-ν))⁻¹ := by + apply mul_le_mul_of_nonneg_right _ h1mexp_nn + exact mul_le_mul_of_nonneg_left hexp_bound (le_of_lt hK.E0_pos) + _ = ε := by + have hE0ne : E0 ≠ 0 := hK.E0_pos.ne' + have h1mne : 1 - Real.exp (-ν) ≠ 0 := h1mexp_pos.ne' + field_simp [hE0ne, h1mne] + +/- + FINAL STATUS — N9.4: + + DEFINITIONS: + · KernelDecayHyp — exponential decay |K(j,k)| ≤ E0·exp(−ν·(j−k)) + · chooseJ — explicit J(ε) = ⌈log(E0/(ε·(1−e^{−ν})))/ν⌉₊ + + PROVED — zero sorry, zero axioms: + · exp_pow_eq_exp_mul — exp(−ν)ⁿ = exp(−ν·n) [by induction] + · summable_exp_geo — ∑ exp(−ν)ⁿ is summable for ν > 0 + · tsum_exp_geo — ∑ exp(−ν)ⁿ = (1 − exp(−ν))⁻¹ + · farRange_bound — far-range tsum ≤ E0·exp(−ν·J)·(1−exp(−ν))⁻¹ + · farRange_le_eps — with J = J(ε), far-range sum ≤ ε [MAIN RESULT] + + DEPENDENCE ON PARAMETERS: + · E0 : amplitude constant (may encode time horizon T as E0 = C₀·T). + Larger E0 → larger J(ε) ~ (1/ν)·log(E0/ε). + · ν : decay rate. Larger ν → smaller J(ε); faster geometric decay. + · T : enters through E0 = C₀·T. J(ε) ~ (1/ν)·log(T/ε) as T grows. + · ε : tolerance. J(ε) ~ (1/ν)·log(1/ε) as ε → 0. + + The bound E0·exp(−ν·J)·(1−exp(−ν))⁻¹ is uniform in k, confirming + that J(ε) controls the far-range error across all base scales. +-/ + +end TOGT