Outside the chirp window the `Sapprox` window distance is `≥ m + 1` (`window_far`)

Outside the chirp window the Sapprox window distance is ≥ m + 1.

The following holds (Lean statement, in the scope of module Solutions.J6AMath1):

theorem J6A.window_far (s t H k m W : ℕ) (ht : 0 < t) (hst : s ≤ t) (hH : 1 ≤ H) (hW : H + m + 3 ≤ W)
    (j : ℤ) (hj : W ≤ (j - jcB s t H k).natAbs ∨ j - jcB s t H k = -W) :
    m + 1 ≤ (j - (((s * k + t - 1) / t : ℕ) : ℤ)).natAbs

Context. A lines (PR #5 block chirp), part 1: the block-chirp S' map and its error

The output axis (length t) is cut into blocks of B = 2H consecutive indices. For an output k the block centre is k_c = ⌊k/B⌋ B + H, the offset κ = k - k_c ∈ [-H, H), and the input centre is j_c = round(s k_c / t). With A = t j - s k_c the exponent of the Gaussian weight splits as

(j - s k/t)² = ((t-s) A² + s (A - t κ)²) / t³ - s (t-s) κ² / t² (expo_split)

so e^{-π(j - sk/t)²/α²} = a · g · C with an input scaling a (per block), a correlation kernel g (per block, a function of j - κ), and an output scaling C = e^{π s(t-s)κ²/(t²α²)} that is the same for every block (ew_split). The machine computes, for every output,

chirpA U k = (Σ_{|j - j_c| < W} aT_j gT_{j-κ} U_{j mod s}) · cT_κ tdiv 2^{3P-σ}

with aT ≈ 2^P a, gT ≈ 2^P g (expNeg) and cT ≈ 2^{P-σ} C / (2α) (expPos, betaT).

chirpA_err: for every input in the disc and every k, ‖chirpA U k - 2^p S'(U/2^p)_k‖ ≤ 12 W 2^{p+σ} / 2^P + 2, as soon as the window contains the Sapprox window (H + m + 3 ≤ W) and e^{π s(t-s)H²/(t²α²)} ≤ 2^σ.

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).