N9.4: Kernel commutator lemma — formal far-range decay bound and J(ε) formula

[Copilot]

Adds a formal Lean 4 proof quantifying how the far-range (j ≥ k + J) kernel contribution decays exponentially and provides an explicit cut-off formula J(ε) to enforce a uniform ε-bound.

New: lean/KernelCommutatorDecay.lean

Decay assumption (KernelDecayHyp):

|K(j, k)| ≤ E0 · exp(−ν · (j − k))   for all j ≥ k

• E0 > 0 — amplitude (encodes time horizon T via E0 = C₀·T)
• ν > 0 — spectral-gap decay rate

Far-range bound (farRange_bound):

∑ₙ |K(k + J + n, k)| ≤ E0 · exp(−ν·J) · (1 − exp(−ν))⁻¹

Proved by comparison against the geometric majorant E0 · exp(−ν·J) · exp(−ν)ⁿ, using tsum_geometric_of_lt_one. Bound is uniform in k.

Optimal cut-off (chooseJ) and main corollary (farRange_le_eps):

J(ε) := ⌈ log(E0 / (ε · (1 − exp(−ν)))) / ν ⌉₊

With J = J(ε), the far-range sum is ≤ ε. Dependence: J grows as (1/ν) · log(E0/ε); larger T/E0 increases J, larger ν decreases it.

Zero sorry, zero axioms. Key auxiliary lemma exp_pow_eq_exp_mul : exp(−ν)ⁿ = exp(−ν·n) proved by induction via Real.exp_add.

Updated: docs/analysis_ns/README.md

Added N9.4 section with the decay assumption, bound formula, J(ε) definition, and a parameter-dependence table.