The `M`-independent part of `fermatW_facts`

The M-independent part of fermatW_facts. -/ def M00 : MulSpec := ⟨fun _ _ => 0, fun _ _ => True⟩ set_option maxHeartbeats 4000000 in theorem fwdIn_of (K N : ℕ) (h : KF K N) (U : List (ℤ × ℤ)) (hUl : U.length = (mkParams K N).S) (hUB : BD.LB U (BD.Bq (mkParams K N))) (hFI : BD.LB (BD.ftIn (mkParams K N) U) (BD.Bq (mkParams K N))) : EX.FwdInX (mkParams K N) (FWW.FwPre (mkParams K N)) (BSf K N) (BBf K N) (mmK K N) (QK K N) U := by have pf := h.pf have hK1 : 1 ≤ K := by have := h.K20; omega have hBqP := BD.Bq_lt K N h.K20 h.big have hpBq := BD.pow_p_le_Bq (mkParams K N) have hP := pf.P_eq have hp := pf.p_eq have hEb := pf.Eb have hSz0 : BSf K N 0 = Nat.size (BD.Bq (mkParams K N)) := by unfold BSf; simp have hmm : Nat.size (BD.Bq (mkParams K N)) ≤ mmK K N := by have := BSf_mm K N 0 (Nat.zero_le ); rwa [hSz0] at this have hpsz : (mkParams K N).p + 1 ≤ Nat.size (BD.Bq (mkParams K N)) := Nat.lt_size.2 hpBq have hPm : (mkParams K N).P < mmK K N := by have : Nat.size (BD.Bq (mkParams K N)) + 2 * (mkParams K N).p ≤ mmK K N := by unfold mmK BSf; omega omega have hPQ : (mkParams K N).P + 1 ≤ QK K N := by unfold QK; omega have hlo := pf.lo have hT := h.TT have hchL : (chirpL (mkParams K N)).length = EX.TT (mkParams K N) := by rw [ST.chirpL_length]; rfl have hfx := fwdX_len K N hK1 U have hTr : EX.TT (mkParams K N) = 2 ^ (mkParams K N).logOuter * (mkParams K N).r := by rw [hT, ← hlo, pow_add]; rfl have hftl : (GL.ftlV (mkParams K N) (GL.fwdX (mkParams K N) U)).length = 2 ^ (mkParams K N).logOuter * (mkParams K N).r := by unfold GL.ftlV; rw [List.length_zipWith, hchL, hfx, min_self, hTr] have hchl' : (chirpL (mkParams K N)).length = 2 ^ (mkParams K N).logOuter * (mkParams K N).r := by rw [hchL, hTr] have hFI' : BD.LB (GL.ftlV (mkParams K N) (GL.fwdX (mkParams K N) U)) (BD.Bq (mkParams K N)) := hFI have hch := BD.chirpL_LB (mkParams K N) have hpP : 2 ^ (mkParams K N).p < 2 ^ (mkParams K N).P := Nat.pow_lt_pow_right (by norm_num) (by omega) have fw := FWW.fermatW_facts M00 (mkParams K N) (mkParams K N).logOuter (by omega) le_rfl _ _ hftl hchl' refine ⟨hUl, ?, ⟨hftl, hchl', abs_lt_of_LB hFI' hBqP, abs_lt_of_LB hch hpP⟩, ?, ?, ?, ?⟩ · rw [hSz0]; exact GB_of_LB' hUB (size_lt _) · rw [fw.1, hTr] · exact GB_of_LB' (BD.fermatW_LB _ _ _) (lt_of_lt_of_le (Nat.pow_lt_pow_right (by norm_num) (Nat.lt_succ_self _)) (Nat.pow_le_pow_right (by norm_num) hPQ)) · refine GB_of_LB' (BD.convL_LB _ _ _) (lt_of_le_of_lt (Nat.div_le_self _ ) ?) exact Nat.pow_lt_pow_right (by norm_num) hPm · have e0 : BBf K N 0 = Nat.size (BD.Bq (mkParams K N) + BD.BC (mkParams K N)) := by unfold BBf; simp rw [e0] exact GB_of_LB' (BD.FtL_LB _ ) (lt_of_le_of_lt (by omega) (size_lt )) theorem big_of (K N : ℕ) (hK : 20 ≤ K) (hN : n0K K ≤ N) : 2 ^ (2 ^ (8 * K) + 1) ≤ N := (n0K_big K).trans hN theorem inU_of (K N : ℕ) (h : KF K N) (a : ℕ) : EX.FwdInX (mkParams K N) (FWW.FwPre (mkParams K N)) (BSf K N) (BBf K N) (mmK K N) (QK K N) (GL.exU (mkParams K N) (uOf K N a)) := by obtain ⟨-, -, -, -, c5, -, -, -, -, c10, -, -, -, -, -, -, -, -, -, -, -, -⟩ := BD.refStep_LB_mkParams K N h.K20 h.big a a refine fwdIn_of K N h _ ? c5 c10 simp [GL.exU, uOf, crtIn_length, Params.S] theorem inW_of (K N : ℕ) (h : KF K N) (a b : ℕ) : EX.FwdInX (mkParams K N) (FWW.FwPre (mkParams K N)) (BSf K N) (BBf K N) (mmK K N) (QK K N) (GL.exW (mkParams K N) (uOf K N a) (uOf K N b)) := by obtain ⟨-, -, -, -, -, -, -, -, -, -, -, c12, -, -, -, -, -, -, c19, -, -, -⟩ := BD.refStep_LB_mkParams K N h.K20 h.big a b have hK1 : 1 ≤ K := by have := h.K20; omega refine fwdIn_of K N h _ ? c19 c12 simp only [GL.exW, List.length_zipWith, fwdL_len K N hK1, min_self] /-! ## smallF, smallM -/ theorem size_mul_le (x y : ℕ) : Nat.size (x * y) ≤ Nat.size x + Nat.size y := by apply Nat.size_le.2 rw [pow_add] exact Nat.mul_lt_mul'' (size_lt x) (size_lt y) theorem size_pow_le (x n : ℕ) (hn : 1 ≤ n) : Nat.size (x ^ n) ≤ n * Nat.size x := by apply Nat.size_le.2 rw [mul_comm, pow_mul] exact Nat.pow_lt_pow_left (size_lt x) (by omega) theorem size_le_self (x : ℕ) : Nat.size x ≤ x := Nat.size_le.2 Nat.lt_two_pow_self set_option maxHeartbeats 4000000 in theorem smallF_of (K N : ℕ) (h : KF K N) : (mkParams K N).fn + 1 < N := by have pf := h.pf have hfn : (mkParams K N).fn = 4 * 2 ^ (mkParams K N).e * (mkParams K N).P := rfl have hP := pf.P_eq have hp5 := h.p5 have hEb := pf.Eb have hKe := pf.Ke have hB64 := pf.B64 have hB8 := pf.B8 have hbB := pf.bB have hNl := pf.N_low have hK := h.K20 set b := (mkParams K N).b set B := Nat.size b set e := (mkParams K N).e have h20 : 20 * e ≤ K * e := Nat.mul_le_mul_right _ hK have hP12 : (mkParams K N).P ≤ 16 * b := by omega have h1 : (mkParams K N).fn + 1 ≤ 2 ^ e * (64 * b) := by rw [hfn] have : 1 ≤ 2 ^ e := Nat.one_le_two_pow have : 1 ≤ b := by omega nlinarith have h2 : 2 ^ e * (64 * b) < 2 ^ (e + (B + 6)) := by rw [pow_add] apply Nat.mul_lt_mul_of_pos_left _ (by positivity) rw [pow_add]; norm_num; omega have h3 : 2 ^ (e + (B + 6)) ≤ 2 ^ (b - 1) := Nat.pow_le_pow_right (by norm_num) (by omega) omega set_option maxHeartbeats 8000000 in theorem smallM_of (K N : ℕ) (h : KF K N) : mmK K N < N := by have pf := h.pf have hP := pf.P_eq have hp := pf.p_eq have hp5 := h.p5 have hEb := pf.Eb have hB64 := pf.B64 have hB8 := pf.B8 have hbB := pf.bB have hNl := pf.N_low have hX := pf.X64 have hα1 := pf.α1 have hK := h.K20 have hBqs := BD.Bq_size K N h.K20 h.big have hBqP := BD.Bq_lt K N h.K20 h.big have hBC : BD.BC (mkParams K N) ≤ 2 ^ (mkParams K N).P := by unfold BD.BC have : 2 ^ (mkParams K N).P / 2 ^ ((mkParams K N).p + (mkParams K N).logT) ≤ 2 ^ (mkParams K N).P / 2 := Nat.div_le_div_left (le_trans (by norm_num) (Nat.pow_le_pow_right (by norm_num) (show 1 ≤ (mkParams K N).p + (mkParams K N).logT by omega))) (by norm_num) have : 2 * (2 ^ (mkParams K N).P / 2) ≤ 2 ^ (mkParams K N).P := Nat.mul_div_le _ _ omega have emm : mmK K N = Nat.size (BD.Bq (mkParams K N)) + K * Nat.size (BD.cS1 (mkParams K N).p (mkParams K N).α) + (Nat.size (BD.Bq (mkParams K N) + BD.BC (mkParams K N)) + K * Nat.size (BD.cB1 (mkParams K N).p (mkParams K N).α (BD.Jm (mkParams K N)))) + 2 * (mkParams K N).p + BD.Jm (mkParams K N) * Nat.size (BD.cE1 (mkParams K N).p (mkParams K N).α) + Nat.size (BD.Jm (mkParams K N) + 1) + Nat.size (4 * (mkParams K N).p + 35) + 64 := rfl set q := mkParams K N with hq set b := q.b set B := Nat.size b set p := q.p set α := q.α have hbB2 : b ≤ 2 ^ B := hbB.le have hαb : α ≤ b := by have : α ≤ α ^ 2 := by nlinarith have : α ^ 2 ≤ 6 * K * α ^ 2 := Nat.le_mul_of_pos_left _ (by omega) omega have hKb : K ≤ b := by have := size_le_self b; omega set Y := 2 ^ (4 * B + 10) with hY have pB : ∀ n, n ≤ 4 * B + 10 → 2 ^ n ≤ Y := fun n hn => Nat.pow_le_pow_right (by norm_num) hn -- basic exponent bounds have e1 : 4 * p + 35 < 2 ^ (B + 6) := by rw [pow_add]; norm_num; omega have hcs : ceilSqrt p ≤ p := CR.ceilSqrt_le_self p have e2 : 2 * sWidth p α + 1 < 2 ^ (2 * B + 5) := by unfold sWidth have : ceilSqrt p * α ≤ (5 * b) * b := Nat.mul_le_mul (by omega) hαb have : b * b ≤ 2 ^ B * 2 ^ B := Nat.mul_le_mul hbB2 hbB2 rw [show 2 * B + 5 = B + B + 5 by ring, pow_add, pow_add]; norm_num; nlinarith have e3 : 2 * eWidth p α + 1 < 2 ^ (B + 6) := by unfold eWidth have : (ceilSqrt p + α - 1) / α ≤ ceilSqrt p + α - 1 := Nat.div_le_self _ _ rw [pow_add]; norm_num; omega have sS : Nat.size (BD.cS1 p α) ≤ 3 * B + 11 := by apply Nat.size_le.2; unfold BD.cS1 calc (2 * sWidth p α + 1) * (4 * p + 35) < 2 ^ (2 * B + 5) * 2 ^ (B + 6) := Nat.mul_lt_mul'' e2 e1 _ = 2 ^ (3 * B + 11) := by rw [← pow_add]; ring_nf have sE : Nat.size (BD.cE1 p α) ≤ 2 * B + 12 := by apply Nat.size_le.2; unfold BD.cE1 calc (2 * eWidth p α + 1) * (4 * p + 35) < 2 ^ (B + 6) * 2 ^ (B + 6) := Nat.mul_lt_mul'' e3 e1 _ = 2 ^ (2 * B + 12) := by rw [← pow_add]; ring_nf have hJ1 : 1 ≤ BD.Jm q := by unfold BD.Jm; exact Nat.le_add_left 1 _ have hJle : BD.Jm q ≤ 4 * K * p + 1 := by unfold BD.Jm; have := Nat.div_le_self (4 * q.K * p) (α ^ 2); exact Nat.add_le_add_right this 1 set Jm := BD.Jm q have hJm : Jm < 2 ^ (2 * B + 6) := by have : K * p ≤ b * (5 * b) := Nat.mul_le_mul hKb hp5 have : b * b ≤ 2 ^ B * 2 ^ B := Nat.mul_le_mul hbB2 hbB2 rw [show 2 * B + 6 = B + B + 6 by ring, pow_add, pow_add]; norm_num; nlinarith have hB2 : 2 * B + 12 ≤ 2 ^ B := by have := size_le_self b; omega have sB : Nat.size (BD.cB1 p α Jm) ≤ 3 * B + 12 + Jm * (2 * B + 12) := by unfold BD.cB1 have a1 := size_mul_le (4 * p + 35) (Jm * BD.cE1 p α ^ Jm) have a2 := size_mul_le Jm (BD.cE1 p α ^ Jm) have a3 := size_pow_le (BD.cE1 p α) Jm hJ1 have a4 : Nat.size (4 * p + 35) ≤ B + 6 := Nat.size_le.2 e1 have a5 : Nat.size Jm ≤ 2 * B + 6 := Nat.size_le.2 hJm have a6 : Jm * Nat.size (BD.cE1 p α) ≤ Jm * (2 * B + 12) := Nat.mul_le_mul_left _ sE omega have t1 : K * Nat.size (BD.cS1 p α) ≤ Y := by have : K * Nat.size (BD.cS1 p α) < 2 ^ (B + (B + 1)) := lt_pow_mul (show K ≤ 2 ^ B by omega) (show Nat.size (BD.cS1 p α) < 2 ^ (B + 1) by rw [pow_succ]; omega) exact this.le.trans (pB _ (by omega)) have hJE : Jm * (2 * B + 12) < 2 ^ (3 * B + 6) := by have := lt_pow_mul hB2 hJm rw [show B + (2 * B + 6) = 3 * B + 6 by ring] at this rw [mul_comm]; exact this have t2 : K * Nat.size (BD.cB1 p α Jm) ≤ Y := by have h3 : 3 * B + 12 < 2 ^ (3 * B + 6) := by have : 2 ^ B ≤ 2 ^ (3 * B + 6) := Nat.pow_le_pow_right (by norm_num) (by omega) omega have : K * Nat.size (BD.cB1 p α Jm) < 2 ^ (B + (3 * B + 7)) := lt_pow_mul (show K ≤ 2 ^ B by omega) (show Nat.size (BD.cB1 p α Jm) < 2 ^ (3 * B + 7) by rw [pow_succ]; omega) exact this.le.trans (pB _ (by omega)) have t3 : Jm * Nat.size (BD.cE1 p α) ≤ Y := by have : Jm * Nat.size (BD.cE1 p α) ≤ Jm * (2 * B + 12) := Nat.mul_le_mul_left _ sE exact this.trans (hJE.le.trans (pB _ (by omega))) have t4 : Nat.size (Jm + 1) ≤ Y := by have : Nat.size (Jm + 1) ≤ 2 * B + 7 := Nat.size_le.2 (by rw [pow_succ]; omega) have : 2 * B + 7 < 2 ^ (2 * B + 7) := Nat.lt_two_pow_self have := pB (2 * B + 7) (by omega) omega have hpY : 16 * b ≤ Y := by have : 16 * 2 ^ B = 2 ^ (B + 4) := by rw [pow_add]; ring have := pB (B + 4) (by omega) omega have t5 : Nat.size (BD.Bq q + BD.BC q) ≤ q.P + 1 := by apply Nat.size_le.2; rw [pow_succ]; omega have t6 : Nat.size (4 * p + 35) ≤ B + 6 := Nat.size_le.2 e1 have hmm : mmK K N ≤ 16 * Y := by rw [emm] omega have h16 : 16 * Y = 2 ^ (4 * B + 14) := by rw [hY, show 4 * B + 14 = 4 * B + 10 + 4 by ring, pow_add]; ring have : 2 ^ (4 * B + 14) < 2 ^ (b - 1) := Nat.pow_lt_pow_right (by norm_num) (by omega) omega /-! ## The main statement

The following holds (Lean statement, in the scope of module NLogN.HNk2):

theorem NLogN.NK.numOK_of (K N : ℕ) (hK : 20 ≤ K) (hN : 2 ^ (2 ^ (8 * K) + 1) ≤ N) : ST.NumOK K N

Context. The lemma belongs to the part Task K, part 2: the input conditions FwdInX, smallF, smallM and NumOK.

Formalization Note. This is a lemma of the Lean development NLogN, a multitape-Turing-machine implementation of the Harvey–van der Hoeven $O(n\log n)$ integer multiplication algorithm, used in the proof of NLogN.FIN.theorem_1_1_nlogn : IntMul.MulTimeBound fun n => n * Real.log n. All names refer to the definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8 (namespace NLogN), built on the platform model Def_IntMul_MultitapeModel and the published reference Def_IntMul_HvdH_MachineRef. The machine layer: IState HS is a state of 64 item stacks; RM programs have a semantics p.run s, a definedness predicate p.ok M s and a cost p.cost M s relative to a multiplication spec M : MulSpec; zsz z is the bit length of $|z|$.