Round-six lemma `fit_PE`
ProvedJ6Seg.fit_PEAn auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.
The following holds (Lean statement, in the scope of module Solutions.J6SegFitB):
theorem J6Seg.fit_PE (p d s t α lam : ℕ) [NeZero s] [NeZero t] (hst : s < t)
(hcop : Nat.Coprime s t) (hα : 2 ≤ α) (hαp : α ^ 2 ≤ p) (hx3 : 3 * s ≤ α ^ 2 * (t - s))
(hd : 2 ≤ d) (h6d : 6 * d ^ 2 ≤ s) (h48 : 48 ≤ α ^ 2) (hpα : p < 48 * d * (α + 1) ^ 2)
(hθ : 3 * d ^ 2 * (t - s) ≤ s) (h48d : 48 * d * α ^ 2 ≤ p) (hp : 100 ≤ p)
(hl1 : 1 ≤ lam) (hlF : lam ≤ lamF d) (hDle' : ddR (α : ℝ) ((t : ℝ) / s) (lam - 1) ≤ 2 ^ (p / 7)) :
1000 * fullG lam (wF d) s t α (1 / 2) ≤ 2 ^ segPF p d s ∧
200 * segE p (segPF p d s) lam (wF d) s t α ≤ 2 ^ p ∧
segE p (segPF p d s) lam (wF d) s t α ≤ 3
Context. Segmented inverse (S2): the precision budget and the Gaussian tail at the fitted parameters
fit_PE: 1000 · G ≤ 2^P (P = segPF p d s) and 200 · segE ≤ 2^p, given D_{λ-1} ≤ 2^{⌊p/7⌋}.
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_Defs61 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg open Complex Real open IntMul.HvdH IntMul.HvdH.Res IntMul.HvdH.P47
theorem J6Seg.fit_PE (p d s t α lam : ℕ) [NeZero s] [NeZero t] (hst : s < t)
(hcop : Nat.Coprime s t) (hα : 2 ≤ α) (hαp : α ^ 2 ≤ p) (hx3 : 3 * s ≤ α ^ 2 * (t - s))
(hd : 2 ≤ d) (h6d : 6 * d ^ 2 ≤ s) (h48 : 48 ≤ α ^ 2) (hpα : p < 48 * d * (α + 1) ^ 2)
(hθ : 3 * d ^ 2 * (t - s) ≤ s) (h48d : 48 * d * α ^ 2 ≤ p) (hp : 100 ≤ p)
(hl1 : 1 ≤ lam) (hlF : lam ≤ lamF d) (hDle' : ddR (α : ℝ) ((t : ℝ) / s) (lam - 1) ≤ 2 ^ (p / 7)) :
1000 * fullG lam (wF d) s t α (1 / 2) ≤ 2 ^ segPF p d s ∧
200 * segE p (segPF p d s) lam (wF d) s t α ≤ 2 ^ p ∧
segE p (segPF p d s) lam (wF d) s t α ≤ 3 := by sorry