Round-six lemma `fit_ddle`
ProvedJ6Seg.fit_ddleD_{λ-1} ≤ 2^{⌊p/7⌋} at the fitted parameters.
The following holds (Lean statement, in the scope of module Solutions.J6SegFitA):
theorem J6Seg.fit_ddle (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) :
ddR (α : ℝ) ((t : ℝ) / s) (lam - 1) ≤ 2 ^ (p / 7)
Context. Segmented inverse (S2): fitted parameters and the D_{λ-1} ≤ 2^R bound
lemma19_seg_fit: any 1 ≤ λ ≤ d k, w = 7k (k = ⌊√d⌋ + 1), R = ⌊p/7⌋, P = segPF p d s,
error ≤ 9, ‖B₀‖ ≤ 1/2, and B₀ 0 = 0 exactly (B0seg_zero). lamP d = 2^{⌊log₂ (d k)⌋} is the power-of-two choice used by the
machine (blocks never cross the λ-aligned chunks).
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_ddle (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) :
ddR (α : ℝ) ((t : ℝ) / s) (lam - 1) ≤ 2 ^ (p / 7) := by sorry