Round-six lemma `NF_lt`
ProvedJ6Seg.Side.NF_ltNF < 2^p from crude size bounds.
The following holds (Lean statement, in the scope of module Solutions.J6SegSideCost2):
theorem J6Seg.Side.NF_lt {d s t T b : ℕ} (hb : 64 ≤ b) (hdb : d ≤ b) (hst : s < t) (htT : t ≤ T)
(hb6 : b ^ 6 ≤ T) {L : ℕ} (hTL : T = 2 ^ L) (hLb : L ≤ b) : NF d s < 2 ^ (6 * b)
Context. Side costs 2: the sizes of one round-six axis
AxNum P n src D k: the natural-number facts the side costs need, on axis k
(T = TP6, p = pP6, β = log₂ lg n):
pre · t · post = T, pre, post ≥ 1, p ≤ T, size (2T) ≤ p, Q ≤ 3p, log₂ λ ≤ 2β + 2,
pre · nc · λ · post ≤ T, d · (pre · G · post) ≤ 99 T, log₂ G ≤ ℓ ≤ p, G ≤ 3t,
d ≤ T, lg n < 2^(β+1).
axNum_ev: all of them for large n.
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 import Definitions.Def_IntMul_KappaFramework import Definitions.Def_IntMul_KappaJainData set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg open IntMul NLogN IntMul.Kappa.R6 J6Seg
theorem J6Seg.Side.NF_lt {d s t T b : ℕ} (hb : 64 ≤ b) (hdb : d ≤ b) (hst : s < t) (htT : t ≤ T)
(hb6 : b ^ 6 ≤ T) {L : ℕ} (hTL : T = 2 ^ L) (hLb : L ≤ b) : NF d s < 2 ^ (6 * b) := by sorry