The integer weight `w = aT gT cT` against `2^{3P-σ} (2α)⁻¹ e_j` (`weight_err`)
ProvedJ6A.weight_errThe integer weight w = aT gT cT against 2^{3P-σ} (2α)⁻¹ e_j.
The following holds (Lean statement, in the scope of module Solutions.J6AMath1):
theorem J6A.weight_err (P σ s t α H k : ℕ) (ht : 0 < t) (hst : s ≤ t) (hα : 2 ≤ α) (hH : 1 ≤ H)
(hP : 2 ≤ P) (hσP : σ ≤ 2 * P)
(hσ : Real.exp (Real.pi * (s * (t - s) * H ^ 2 : ℕ) / ((t ^ 2 * α ^ 2 : ℕ) : ℝ)) ≤ 2 ^ σ) (j : ℤ) :
|((aT P s t α H k j * gT P s t α H k j * cT P σ s t α H k : ℤ) : ℝ) -
2 ^ (3 * P) * (2 ^ σ)⁻¹ * ((2 * α : ℝ)⁻¹ * ew s t α k j)| ≤ 6 * 2 ^ (2 * P)
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*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction. import Definitions.Def_IntMul_Kappa_R6_Defs60 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6A open Complex open IntMul.HvdH IntMul.HvdH.SPf
theorem J6A.weight_err (P σ s t α H k : ℕ) (ht : 0 < t) (hst : s ≤ t) (hα : 2 ≤ α) (hH : 1 ≤ H)
(hP : 2 ≤ P) (hσP : σ ≤ 2 * P)
(hσ : Real.exp (Real.pi * (s * (t - s) * H ^ 2 : ℕ) / ((t ^ 2 * α ^ 2 : ℕ) : ℝ)) ≤ 2 ^ σ) (j : ℤ) :
|((aT P s t α H k j * gT P s t α H k j * cT P σ s t α H k : ℤ) : ℝ) -
2 ^ (3 * P) * (2 ^ σ)⁻¹ * ((2 * α : ℝ)⁻¹ * ew s t α k j)| ≤ 6 * 2 ^ (2 * P) := by sorry