Prove2Me

Harvey–van der Hoeven machine development, part 8: definitions for the final O(n log n) assembly

Definition
IntMul_HvdH_M_Defs8

by xuanji · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

harvey-van-der-hoeven-tminteger-multiplicationturing-machines

Definitions (Lean namespace NLogN) for a multitape-Turing-machine implementation of the Harvey–van der Hoeven O(nlog⁡n)O(n\log n) integer multiplication algorithm, continuing IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs4 (part 8): the programs and cost functions of the recursive step (parameter, chirp, key, CRT and resampling phases, the tensor/axis combinators and the Gaussian resampling tables) and the final assembly constants.

Source modules (in order): NLogN.HSt3, NLogN.HSt4, NLogN.HSt5, NLogN.HSt6, NLogN.HSt7, NLogN.HSt8, NLogN.HSt9, NLogN.HSt10, NLogN.HStNum, NLogN.HSt11, NLogN.HSt12, NLogN.HNk1, NLogN.HNk2, NLogN.HFin3, NLogN.HFin4, NLogN.HFin5.

The file was generated by deleting from the development all theorems not needed by the definitions; it keeps all definitions plus the few lemmas the definitions themselves need (proof fields of structures, decreasing_by facts) and simple @[simp]/rfl lemmas.

Definition code
-- Harvey–van der Hoeven multitape-TM development (NLogN), generated by skeleton subtraction.

import Definitions.Def_IntMul_HvdH_M_Defs7

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: NLogN.HSt3
/-!
# The recursive step, part 3: the program `stepP K` (namespace `NLogN.ST`)

Phases (each one stack-neutral except for its documented outputs):

* `fetchP`   : `a` (XA), `b` (XB) ↦ `a :: b` on `30`.
* `nbP`      : `N` (XN) ↦ `N` on `34`, `Nat.size N` on `35` (via `blenRM`).
* `parPh K`  : `CR.parP K` (all parameters of `mkParams K N`), `kb = logT + 2` on `2`.
* `keyPh K`  : CRT keys on `3`, the source lengths (reversed) on `41`; records consumed.
* `chirpPh`  : `S` on `1`, the chirp table on `28`.
* `crtPh`    : `u = crtIn (chunks a)` on `0`, `v = crtIn (chunks b)` on `30`.
* `midP K`   : temporaries, environment (`GL`, `Glob`, `FwCtx` registers), descriptors, the
  exact convolution `exCore` (= `EX.exactLW`), teardown.
* `tailP`    : drop chirp, `crtOutP`, drop keys, `evalP`, result onto `XR`.
* `popPar`   : pop the parameter registers and `34`, `35`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.ST

open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref

/-- The exact convolution program; definitionally `EX.exactLW M q kbw hMB …` for every `M`. -/
def exCore : RM :=
  RM.seqL [GL.scaleP GL.gPM,
    RM.seqL [EX.sPhase, RM.seqL [GL.copyP GL.gPN, GL.zipP GL.sgConjMul GL.gPN, GL.copyP GL.gPN,
      RM.seqL [GL.xferP GL.gD FWW.wI1 (GL.cnt2 GL.gPN), GL.xferP GL.gZA FWW.wI2 (GL.cnt2 GL.gPN), FWW.fwWrap,
        GL.xferP FWW.wO GL.gD (GL.cnt2 GL.gPN), GL.tdivP GL.gPN], GL.copyP GL.gPN, GL.zipP GL.sgConjMul GL.gPN], EX.bPhase],
    GL.xferP GL.gD GL.gSA (GL.cnt2 GL.gPM), GL.xferP GL.gV GL.gD (.reg GL.gPM),
    GL.scaleP GL.gPM,
    RM.seqL [EX.sPhase, RM.seqL [GL.copyP GL.gPN, GL.zipP GL.sgConjMul GL.gPN, GL.copyP GL.gPN,
      RM.seqL [GL.xferP GL.gD FWW.wI1 (GL.cnt2 GL.gPN), GL.xferP GL.gZA FWW.wI2 (GL.cnt2 GL.gPN), FWW.fwWrap,
        GL.xferP FWW.wO GL.gD (GL.cnt2 GL.gPN), GL.tdivP GL.gPN], GL.copyP GL.gPN, GL.zipP GL.sgConjMul GL.gPN], EX.bPhase],
    GL.xferP GL.gSA GL.gZA (GL.cnt2 GL.gPM), GL.zipP GL.sgMulConj GL.gPM,
    RM.seqL [EX.sPhase, RM.seqL [GL.copyP GL.gPN, GL.zipP GL.sgConjMul GL.gPN, GL.copyP GL.gPN,
      RM.seqL [GL.xferP GL.gD FWW.wI1 (GL.cnt2 GL.gPN), GL.xferP GL.gZA FWW.wI2 (GL.cnt2 GL.gPN), FWW.fwWrap,
        GL.xferP FWW.wO GL.gD (GL.cnt2 GL.gPN), GL.tdivP GL.gPN], GL.copyP GL.gPN, GL.zipP GL.sgConjMul GL.gPN], EX.bPhase],
    GL.roundP GL.gPM]

/-! ## The phases -/

def fetchP : RM :=
  RM.seqL [.rs (.push 30 (.reg Top.XB)), .rs (.pop Top.XB), .rs (.push 30 (.reg Top.XA)),
    .rs (.pop Top.XA)]

def nbP : RM :=
  RM.seqL [.rs (.push 4 (.reg Top.XN)), Top.blenRM, .rs (.push 35 (.reg 26)), .rs (.pop 26),
    .rs (.pop 4), .rs (.push 34 (.reg Top.XN))]

def parPh (K : ℕ) : RM := RM.seqL [.rs (CR.parP K), .rs (.push 2 (.add (.reg 37) (.lit 2)))]

def keyPh (K : ℕ) : RM :=
  RM.seqL [GL.xferP 40 4 (.lit ((4 * K : ℕ) : ℤ)),
    .rs (EX.pushes [(15, .reg 28), (16, .lit (K : ℤ)), (17, .lit ((4 * K : ℕ) : ℤ))]),
    .rs CR.keyGen, .rs (EX.pops [15, 16, 17]), slLoop K]

def chirpPh : RM :=
  RM.seqL [.rs (.push 1 (.reg 28)), CR.chirpP CR.twR, GL.xferP 0 28 (.add (.reg 9) (.reg 9))]

def crtPh : RM := RM.seqL [CR.crtInP, CR.crtInP, GL.xferP 0 30 (.reg 1)]

/-- Temporaries: `p` (43), `S` (45), `logT` (46), `r` (47), `r/2` (48), `K - dh` (49), `T` (50),
`logOuter` (51), `fn` (54). -/
def tmpL : List (Fin HS × Ex HS) :=
  [(43, .reg 17), (45, .reg 1), (46, .reg 37), (47, .reg 5), (48, .reg 6), (49, .reg 7),
    (50, .reg 9), (51, .reg 39), (54, .reg 26)]

/-- `eWidth p α = (cs + α - 1) / α + 1` with `cs = ceilSqrt p` on `41`, `α` on `42`. -/
def ewE : Ex HS := .add (.ndiv (.add (.reg 41) (.add (.reg 42) (.lit (-1)))) (.reg 42)) (.lit 1)

/-- The environment of `exCore`: `GL` constants (20–27), `Glob` (5–18), `FwCtx` scalars. -/
def envL (K : ℕ) : List (Fin HS × Ex HS) :=
  [(20, .pow2 (.reg 43)), (21, .pow2 (.add (.reg 43) (.reg 46))),
    (22, .ndiv (.pow2 (.reg 43)) (.reg 31)), (23, .mul (.reg 45) (.reg 45)),
    (24, .mul (.mul (.reg 31) (.reg 31))
      (.pow2 (.add (.mul (.lit ((6 * K : ℕ) : ℤ)) (.mul (.reg 42) (.reg 42))) (.lit 1)))),
    (25, .pow2 (.add (.reg 43) (.lit 1))), (26, .reg 50), (27, .reg 45),
    (5, .reg 43), (6, .mul (.reg 42) (.reg 42)), (7, .mul (.reg 41) (.reg 42)),
    (8, .add (.mul (.lit 2) (.mul (.reg 41) (.reg 42))) (.lit 1)),
    (9, ewE), (10, .add (.mul (.lit 2) ewE) (.lit 1)),
    (11, .ndiv (.pow2 (.reg 43)) (.add (.reg 42) (.reg 42))),
    (12, .pow2 (.add (.reg 43) (.reg 43))), (13, .pow2 (.reg 43)), (14, .reg 2),
    (15, .lit (K : ℤ)), (16, .reg 49), (17, .reg 48), (18, .reg 47),
    (32, .pow2 (.reg 44)), (33, .pow2 (.reg 54)), (34, .reg 47),
    (52, .pow2 (.mul (.add (.reg 47) (.reg 47)) (.reg 44))),
    (53, .add (.pow2 (.reg 54)) (.lit 1)), (35, .pow2 (.reg 51)), (36, .reg 2),
    (37, .lit ((K : ℤ) - 1)), (38, .pow2 (.add (.reg 54) (.neg (.reg 51))))]

/-- `ceilSqrt p` onto `41` (`p` on `43`). -/
def csP : RM := .rs (CR.srch 41 19 (.reg 43) (CR.csE 43 41))

/-- The environment, `exCore`, and the environment pops. -/
def envP (K : ℕ) : RM :=
  RM.seqL [.rs (EX.pushes (envL K)), exCore, .rs (EX.pops ((envL K).map Prod.fst))]

/-- Between the temporaries: descriptors, environment, `exCore`, teardown. -/
def innerP (K : ℕ) : RM :=
  RM.seqL [csP, descLoop K, envP K, .rs (CR.dropN 39 19 (.lit ((8 * (K - 1) : ℕ) : ℤ))),
    .rs (.pop 41)]

def midCore (K : ℕ) : RM :=
  RM.seqL [.rs (.pop 1), .rs (mvList 41 1 19 (.lit (K : ℤ))), innerP K,
    .rs (CR.dropN 1 19 (.lit (K : ℤ))), .rs (.push 1 (.reg 45))]

def midP (K : ℕ) : RM :=
  RM.seqL [.rs (EX.pushes tmpL), midCore K, .rs (EX.pops (tmpL.map Prod.fst))]

def tailP : RM :=
  RM.seqL [.rs (CR.dropN 28 19 (.add (.reg 9) (.reg 9))), .rs CR.crtOutP,
    .rs (CR.dropN 3 19 (.reg 1)), .rs (.pop 1), .rs (.pop 2), GL.xferP 0 20 (.reg 33),
    .rs (.push 23 (.reg 31)), .rs (.push 26 (.reg 33)), CR.evalP, .rs (.pop 26), .rs (.pop 23),
    .rs (.push Top.XR (.reg 22)), .rs (.pop 22)]

/-- The parameter registers, in the order they are popped. -/
def parRegs : List (Fin HS) := [28, 26, 44, 17, 42, 33, 31, 39, 9, 4, 6, 5, 7, 8, 38, 37, 32, 36, 34, 35]

def popPar : RM := .rs (EX.pops parRegs)

/-- **The recursive step.** -/
def stepP (K : ℕ) : RM :=
  RM.seqL [fetchP, nbP, parPh K, keyPh K, chirpPh, crtPh, midP K, tailP, popPar]

end NLogN.ST

end

section
-- Source module: NLogN.HSt4
/-!
# The recursive step, part 4: generic helpers and the first phases (namespace `NLogN.ST`)
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unreachableTactic false
set_option linter.unusedTactic false

namespace NLogN.ST

open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref
open NLogN.FW (Spec)

/-! ## State helpers -/

/-! ## `fetchP` -/

/-! ## `nbP` -/

end NLogN.ST

namespace NLogN.ST

open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref
open NLogN.FW (Spec)

/-! ## `parPh` -/

/-! ## `keyPh` -/

def keyCost (K S B : ℕ) : ℕ :=
  2 * ((1 + 1) * 2000 * (B + 2) + 4 * K * (14000 * (B + 2) + 30) + 32) +
    (6 * 10 ^ 7 * (B + 2) ^ 2 + 1) + 10 ^ 6 * (S + 1) * (K + 1) * (B + 2) + (3 * (2 * B + 2) + 1) +
    (2 * 2000 * (B + 2) + K * (4000 * (B + 2) + 8 * B + 8 + 8000 * (B + 2) + 30) + 32)

/-! ## `chirpPh` -/

def chirpCost (q : Params) (kb B : ℕ) : ℕ :=
  4000 * (B + 2) +
    ((q.tdims.prod + 1) * (q.K + 6) * (2 * 10 ^ 9) * (B + 2) ^ 2 +
      (2 * q.r + 1) * (CR.twCost q.p (2 * q.r) + 3 * 10 ^ 9 * (B + 2) ^ 2) +
      10 ^ 7 * (kb + 1) * (2 * q.r + q.tdims.prod + 1) * (B + kb + 6)) +
    2 * ((3 + 1) * 2000 * (B + 2) + 2 * q.tdims.prod * (14000 * (B + 2) + 30) + 32)

/-! ## `crtPh` -/

def crtCost (S kb B : ℕ) : ℕ :=
  2 * (3 * 10 ^ 6 * (kb + 1) * (S + 1) * (B + kb + 5)) +
    2 * ((1 + 1) * 2000 * (B + 2) + S * (14000 * (B + 2) + 30) + 32)

end NLogN.ST

end

section
-- Source module: NLogN.HSt5
/-!
# The recursive step, part 5: the tail (`crtOut`, `evalDigits`, result) and the final pops
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unreachableTactic false
set_option linter.unusedTactic false

namespace NLogN.ST

open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref
open NLogN.FW (Spec)

def tailCost (T S Mo kb b B : ℕ) : ℕ :=
  ((3 + 1) * 2000 * (B + 2) + 2 * T * (8000 * (B + 2) + 2 * B + 40) + 32) +
  10 ^ 7 * (kb + 1) * (S + 1) * (B + kb + 5) +
  ((1 + 1) * 2000 * (B + 2) + S * (8000 * (B + 2) + 2 * B + 40) + 32) +
  2 * (2 * B + 2) +
  2 * ((1 + 1) * 2000 * (B + 2) + Mo * (14000 * (B + 2) + 30) + 32) +
  2 * (4000 * (B + 2)) +
  (40000 * (Mo + 1) * (B + 3) + 20000 * (b * Mo + B + 4) + 103) +
  2 * (2 * B + 2)

/-! ## Popping a list of distinct registers -/

/-- `t` with the stacks `l` replaced by `L r`. -/
def upds (t : IState HS) (L : Fin HS → List Item) : List (Fin HS) → IState HS
  | [] => t
  | r :: l => (upds t L l).upd r (L r)

end NLogN.ST

end

section
-- Source module: NLogN.HSt6
/-!
# The recursive step, part 6: the environment pushes of `envP` (namespace `NLogN.ST`)
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unreachableTactic false
set_option linter.unusedTactic false

namespace NLogN.ST

open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref
open NLogN.FW (Spec)

/-- The values pushed by `envL`. -/
def envV (q : Params) (kb : ℕ) : List (Fin HS × ℤ) :=
  [(20, 2 ^ q.p), (21, 2 ^ (q.p + q.logT)), (22, 2 ^ (q.p - q.b)), (23, (q.S : ℤ) ^ 2),
    (24, 2 ^ (GL.exC q + 1)), (25, 2 ^ (q.p + 1)), (26, (EX.TT q : ℤ)), (27, (q.S : ℤ)),
    (5, (q.p : ℤ)), (6, ((q.α ^ 2 : ℕ) : ℤ)), (7, (sWidth q.p q.α : ℤ)),
    (8, ((2 * sWidth q.p q.α + 1 : ℕ) : ℤ)), (9, (eWidth q.p q.α : ℤ)),
    (10, ((2 * eWidth q.p q.α + 1 : ℕ) : ℤ)), (11, betaT q.p q.α), (12, 2 ^ (2 * q.p)),
    (13, 2 ^ q.p), (14, (kb : ℤ)), (15, (q.K : ℤ)), (16, ((q.K - q.dh : ℕ) : ℤ)),
    (17, ((2 ^ (q.e - 1) : ℕ) : ℤ)), (18, ((2 ^ q.e : ℕ) : ℤ)),
    (32, 2 ^ q.P), (33, 2 ^ q.fn), (34, (q.r : ℤ)), (52, 2 ^ (2 * q.r * q.P)), (53, 2 ^ q.fn + 1),
    (35, ((2 ^ q.logOuter : ℕ) : ℤ)), (36, (kb : ℤ)), (37, ((q.K - 1 : ℕ) : ℤ)),
    (38, 2 ^ (q.fn - q.logOuter))]

/-- The registers `envL` reads, with their values. -/
structure EnvRegs (q : Params) (kb : ℕ) (w : IState HS) : Prop where
  r43 : ∃ L, w.G 43 = .int (q.p : ℤ) :: L
  r46 : ∃ L, w.G 46 = .int (q.logT : ℤ) :: L
  r31 : ∃ L, w.G 31 = .int ((2 ^ q.b : ℕ) : ℤ) :: L
  r45 : ∃ L, w.G 45 = .int (q.S : ℤ) :: L
  r42 : ∃ L, w.G 42 = .int (q.α : ℤ) :: L
  r50 : ∃ L, w.G 50 = .int (EX.TT q : ℤ) :: L
  r41 : ∃ L, w.G 41 = .int (ceilSqrt q.p : ℤ) :: L
  r2 : ∃ L, w.G 2 = .int (kb : ℤ) :: L
  r49 : ∃ L, w.G 49 = .int ((q.K - q.dh : ℕ) : ℤ) :: L
  r48 : ∃ L, w.G 48 = .int ((2 ^ (q.e - 1) : ℕ) : ℤ) :: L
  r47 : ∃ L, w.G 47 = .int ((2 ^ q.e : ℕ) : ℤ) :: L
  r44 : ∃ L, w.G 44 = .int (q.P : ℤ) :: L
  r54 : ∃ L, w.G 54 = .int (q.fn : ℤ) :: L
  r51 : ∃ L, w.G 51 = .int (q.logOuter : ℤ) :: L

/-- Size facts for the environment values (all values have at most `Bs` bits). -/
structure EnvN (q : Params) (kb Bs : ℕ) : Prop where
  K1 : 1 ≤ q.K
  α1 : 1 ≤ q.α
  bp : q.b ≤ q.p
  lo : q.logOuter ≤ q.fn
  e1 : 1 ≤ q.e
  p : 2 * q.p + q.logT + 2 ≤ Bs
  c : GL.exC q + 2 ≤ Bs
  P : q.P + 1 ≤ Bs
  fn : q.fn + 2 ≤ Bs
  rP : 2 * q.r * q.P + 1 ≤ Bs
  S2 : q.S * q.S < 2 ^ Bs
  T : EX.TT q < 2 ^ Bs
  sm : 6 * q.K * (q.α * q.α) + 2 * (ceilSqrt q.p * q.α) + 2 * q.α + ceilSqrt q.p + kb + q.K + 2 * 2 ^ q.e +
    2 * q.α + 2 < 2 ^ Bs

end NLogN.ST

end

section
-- Source module: NLogN.HSt7
/-!
# The recursive step, part 7: `envP` (environment + `exCore` + teardown)
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unreachableTactic false
set_option linter.unusedTactic false

namespace NLogN.ST

open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref
open NLogN.FW (Spec)

def exCost (q : Params) (kb CS CB Bx Q Φf Φm : ℕ) : ℕ :=
  3 * EX.fwdLCost q CS CB Bx (FWW.fwWCost q kb Φf) Q Φm + 5 * q.S * Φm + 1000000 * (q.S + 1) * (Q + 2)

end NLogN.ST

end

section
-- Source module: NLogN.HSt8
/-!
# The recursive step, part 8: `csP`, the descriptor bounds, `innerP`
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unreachableTactic false
set_option linter.unusedTactic false

namespace NLogN.ST

open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref
open NLogN.FW (Spec Desc descs enc8)

/-! ## The descriptor list -/

/-! ## `innerP` -/

def envRegL : List (Fin HS) := [43, 46, 31, 45, 42, 50, 41, 2, 49, 48, 47, 44, 54, 51]

/-- All the hypotheses `envP_spec` needs besides the machine state. -/
structure ExArgs (M : MulSpec) (q : Params) (kb Φf Φm m mm Φ Bacc Qa Bq Bx CS CB Q Bs mu : ℕ)
    (BS BB : ℕ → ℕ) (u v : List ℤ) : Prop where
  hMB : MulBnd M (q.fn + 1) Φf
  hP : 1 ≤ q.P
  hK : q.K ≤ q.fn
  hlo : q.logOuter ≤ q.fn
  hkb : q.logOuter ≤ kb
  hMm : MulBnd M m Φm
  hcfg : EX.FwdCfgX M q kb mm Φ Bacc Qa Bq Bx CS CB m Q BS BB
  hn : EnvN q kb Bs
  hul : u.length = q.S
  hvl : v.length = q.S
  hub : ∀ x ∈ u, zsz x ≤ mu
  hvb : ∀ x ∈ v, zsz x ≤ mu
  hmu : mu + (q.p - q.b) + 1 ≤ Q
  inU : EX.FwdInX q (FWW.FwPre q) BS BB m Q (GL.exU q u)
  inV : EX.FwdInX q (FWW.FwPre q) BS BB m Q (GL.exU q v)
  inW : EX.FwdInX q (FWW.FwPre q) BS BB m Q (GL.exW q u v)
  hS2 : zsz ((q.S : ℤ) ^ 2) ≤ m
  hBQ : 2 * m + GL.exC q + q.p + 6 ≤ Q
  hSQ : zsz ((2 * q.S : ℕ) : ℤ) ≤ Q

def envCost (q : Params) (kb Bs CS CB Bx Q Φf Φm : ℕ) : ℕ :=
  EX.pwt (envL q.K) * 10 ^ 7 * (Bs + 2) ^ 2 + 1 +
    (exCost q kb CS CB Bx Q Φf Φm + ((envV q kb).length * (2 * Bs + 2) + 1))

def innerCost (q : Params) (kb Bs CS CB Bx Q Φf Φm B : ℕ) : ℕ :=
  (q.p + 1) * 30 * 10 ^ 7 * (B + 2) ^ 2 + ((q.K + 1) * 10 ^ 10 * (B + 2) ^ 2 +
    (envCost q kb Bs CS CB Bx Q Φf Φm + (((Ex.lit (S := HS) ((8 * (q.K - 1) : ℕ) : ℤ)).size + 1) * 2000 * (B + 2) +
      (8 * (q.K - 1)) * (8000 * (B + 2) + 2 * B + 40) + 32 + (2 * B + 2))))

/-! ## `midCore` -/

def midCost (q : Params) (kb Bs CS CB Bx Q Φf Φm B : ℕ) : ℕ :=
  (2 * B + 2) + ((1 + 1) * 2000 * (B + 2) + q.K * (6000 * (B + 2) + 8000 * (B + 2) + 30) + 32 +
    (innerCost q kb Bs CS CB Bx Q Φf Φm B + ((1 + 1) * 2000 * (B + 2) +
      q.K * (8000 * (B + 2) + 2 * B + 40) + 32 + 4000 * (B + 2))))

/-! ## `midP` -/

def tmpV (q : Params) : List (Fin HS × ℤ) :=
  [(43, (q.p : ℤ)), (45, (q.S : ℤ)), (46, (q.logT : ℤ)), (47, ((2 ^ q.e : ℕ) : ℤ)),
    (48, ((2 ^ (q.e - 1) : ℕ) : ℤ)), (49, ((q.K - q.dh : ℕ) : ℤ)), (50, (EX.TT q : ℤ)),
    (51, (q.logOuter : ℤ)), (54, (q.fn : ℤ))]

def midPCost (q : Params) (kb Bs CS CB Bx Q Φf Φm B : ℕ) : ℕ :=
  EX.pwt tmpL * 10 ^ 7 * (B + 2) ^ 2 + 1 +
    (midCost q kb Bs CS CB Bx Q Φf Φm B + ((tmpV q).length * (2 * B + 2) + 1))

end NLogN.ST

end

section
-- Source module: NLogN.HSt9
/-!
# The recursive step, part 9: the whole program `stepP K` (generic in the numeric premises)
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unreachableTactic false
set_option linter.unusedTactic false

namespace NLogN.ST

open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref
open NLogN.FW (Spec)

/-- `crtIn` of the chunks of `x`. -/
def uOf (K N x : ℕ) : List ℤ := crtIn (mkParams K N).s (chunksL (mkParams K N).b (mkParams K N).L x)

/-- The values held by the parameter registers at the end (popped by `popPar`). -/
def parV (K N : ℕ) (r : Fin HS) : ℤ :=
  if r = 28 then ((mkParams K N).S : ℤ) else if r = 26 then ((mkParams K N).fn : ℤ)
  else if r = 44 then ((mkParams K N).P : ℤ) else if r = 17 then ((mkParams K N).p : ℤ)
  else if r = 42 then ((mkParams K N).α : ℤ) else if r = 33 then ((2 * (mkParams K N).L - 1 : ℕ) : ℤ)
  else if r = 31 then ((2 ^ (mkParams K N).b : ℕ) : ℤ) else if r = 39 then ((mkParams K N).logOuter : ℤ)
  else if r = 9 then ((mkParams K N).tdims.prod : ℤ) else if r = 4 then ((2 ^ ((mkParams K N).e + 1) : ℕ) : ℤ)
  else if r = 6 then ((2 ^ ((mkParams K N).e - 1) : ℕ) : ℤ) else if r = 5 then ((2 ^ (mkParams K N).e : ℕ) : ℤ)
  else if r = 7 then (((mkParams K N).K - (mkParams K N).dh : ℕ) : ℤ)
  else if r = 8 then ((mkParams K N).dh : ℤ) else if r = 38 then ((mkParams K N).e : ℤ)
  else if r = 37 then (CR.parEx K N : ℤ) else if r = 32 then ((mkParams K N).L : ℤ)
  else if r = 36 then ((mkParams K N).b : ℤ) else if r = 34 then (N : ℤ) else if r = 35 then zsz (N : ℤ)
  else 0

/-- All numeric premises of the step (for `q = mkParams K N`, inputs `a`, `b`). -/
structure StepArgs (M : MulSpec) (K N a b : ℕ) (Φf Φm m mm Φ Bacc Qa Bq Bx CS CB Q Bs mu Bc Bd : ℕ)
    (BS BB : ℕ → ℕ) : Prop where
  K1 : 1 ≤ K
  N1 : 1 ≤ N
  ha : a < 2 ^ N
  hb : b < 2 ^ N
  ex : ExArgs M (mkParams K N) ((mkParams K N).logT + 2) Φf Φm m mm Φ Bacc Qa Bq Bx CS CB Q Bs mu BS BB
    (uOf K N a) (uOf K N b)
  crt : CR.CrtOK (mkParams K N).s
  he : 2 ≤ (mkParams K N).e
  hdh : (mkParams K N).dh < K
  kb1 : 4 * (mkParams K N).r ≤ 2 ^ ((mkParams K N).logT + 2)
  kb2 : (mkParams K N).tdims.prod ≤ 2 ^ ((mkParams K N).logT + 2)
  kbS : (mkParams K N).S ≤ 2 ^ ((mkParams K N).logT + 2)
  LS : (mkParams K N).L ≤ (mkParams K N).S
  MoS : 2 * (mkParams K N).L - 1 ≤ (mkParams K N).S
  aL : a < 2 ^ ((mkParams K N).b * (mkParams K N).L)
  bL : b < 2 ^ ((mkParams K N).b * (mkParams K N).L)
  b1 : 1 ≤ (mkParams K N).b
  kB : 2 * (mkParams K N).S + 4 * K + 1 < 2 ^ Bc
  chB : CR.ChirpB (mkParams K N) Bc
  pB : (mkParams K N).p + 1 ≤ Bc
  bigB : 8 * (mkParams K N).r + 3 * (mkParams K N).tdims.prod + 4 < 2 ^ Bc
  kbB : (mkParams K N).logT + 4 ≤ Bc
  bB : (mkParams K N).b + 1 ≤ Bc
  dB : 2 * (mkParams K N).fn + (mkParams K N).logOuter + (mkParams K N).e + 2 * K + 4 ≤ Bd
  ppB : (mkParams K N).p * (mkParams K N).p + (mkParams K N).p + 2 < 2 ^ Bd
  KB : 8 * K < 2 ^ Bd
  slB : Bnd Bd (EX.sl (mkParams K N))
  TBd : (mkParams K N).tdims.prod < 2 ^ Bd
  SBd : (mkParams K N).S < 2 ^ Bd
  lTBd : (mkParams K N).logT + 1 ≤ Bd
  TB : 2 * (mkParams K N).tdims.prod < 2 ^ Bc
  SB : (mkParams K N).S < 2 ^ Bc
  cB : ∀ x ∈ crtOut (mkParams K N).s (2 * (mkParams K N).L - 1)
    (exactConvL (mkParams K N) (uOf K N a) (uOf K N b)), 0 ≤ x ∧ x < 2 ^ Bc
  wB : Bnd Bc (exactConvL (mkParams K N) (uOf K N a) (uOf K N b))
  wl : (exactConvL (mkParams K N) (uOf K N a) (uOf K N b)).length = (mkParams K N).S
  res : refStep (mkParams K N) a b = ((a * b : ℕ) : ℤ)
  popB : ∀ r ∈ parRegs, zsz (parV K N r) ≤ Bc + N

def stepCost (K N Φf Φm Bs CS CB Bx Q Bc Bd : ℕ) : ℕ :=
  (2 * (4000 * (N + 2)) + 2 * (2 * N + 2)) +
  ((3 * (4000 * (zsz (N : ℤ) + 2)) + Top.blenCost N + 2 * (2 * zsz (N : ℤ) + 2)) +
  (((CR.facN K + 2 * K + 5 * zsz (N : ℤ) + 102) * 10 ^ 9 * (Nat.size (CR.parBnd K N (zsz (N : ℤ))) + 2) ^ 2 +
      4 * 2000 * ((mkParams K N).logT + 5)) +
  (keyCost K (mkParams K N).s.prod Bc +
  (chirpCost (mkParams K N) ((mkParams K N).logT + 2) Bc +
  (crtCost (mkParams K N).S ((mkParams K N).logT + 2) Bc +
  (midPCost (mkParams K N) ((mkParams K N).logT + 2) Bs CS CB Bx Q Φf Φm Bd +
  ((tailCost (mkParams K N).tdims.prod (mkParams K N).S (2 * (mkParams K N).L - 1) ((mkParams K N).logT + 2)
      (mkParams K N).b Bc + (4000 * (2 * N + 2) + (2 * (2 * N) + 2))) +
  (parRegs.length * (2 * (Bc + N) + 2) + 1))))))))

end NLogN.ST

end

section
-- Source module: NLogN.HSt10
/-!
# The recursive step, part 10: parameter choices, the cost decomposition `lin`/`calls`
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unreachableTactic false
set_option linter.unusedTactic false

namespace NLogN.ST

open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref

/-! ## The derived quantities (explicit functions of `K` and `N`) -/

/-- Key width `kb = logT + 2`. -/
def kbK (K N : ℕ) : ℕ := (mkParams K N).logT + 2

/-- Bit bound of the `S̃` stage `k` inputs. -/
def BSf (K N k : ℕ) : ℕ :=
  Nat.size (BD.Bq (mkParams K N)) + k * Nat.size (BD.cS1 (mkParams K N).p (mkParams K N).α)

/-- Bit bound of the `B̃` stage `k` inputs. -/
def BBf (K N k : ℕ) : ℕ :=
  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)))

/-- The size of all small multiplications. -/
def mmK (K N : ℕ) : ℕ :=
  BSf K N K + BBf K N K + 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

/-- Accumulator bits of the axis transforms (also their scalar bound). -/
def BaccK (K N : ℕ) : ℕ :=
  2 * mmK K N + 2 * (mkParams K N).p + 2 * (mkParams K N).logT +
    2 * Nat.size (2 * eWidth (mkParams K N).p (mkParams K N).α + 2 * sWidth (mkParams K N).p (mkParams K N).α + 4) +
    64

/-- Table bits of the axis transforms. -/
def BqT (K N : ℕ) : ℕ :=
  2 * (mkParams K N).p + Nat.size (4 * (mkParams K N).p + 35) +
    24 * Nat.size ((mkParams K N).α ^ 2 + 2 * 2 ^ (mkParams K N).e + 2 * eWidth (mkParams K N).p (mkParams K N).α +
      2 * sWidth (mkParams K N).p (mkParams K N).α + 2) + 8

/-- Scalar bits of the axis loops. -/
def BxK (K N : ℕ) : ℕ := Nat.size (EX.Vx (mkParams K N) (kbK K N))

/-- Bits of the `fwdL` lists. -/
def QK (K N : ℕ) : ℕ := 2 * mmK K N + GL.exC (mkParams K N) + 2 * (mkParams K N).p + 2 * (mkParams K N).logT + 64

/-- Bits of the `exactLW` environment scalars. -/
def BsK (K N : ℕ) : ℕ :=
  2 * (mkParams K N).fn + 2 * (mkParams K N).p + 2 * (mkParams K N).logT + GL.exC (mkParams K N) + 64

/-- Bits of the CRT / chirp / tail values (`O(log N)`). -/
def BcK (K N : ℕ) : ℕ := 2 * (mkParams K N).p + 2 * (mkParams K N).logT + 2 * (mkParams K N).b + 4 * K + 64

/-- Bits of the descriptor values (`O(fn)`, only `O(K)` of them). -/
def BdK (K N : ℕ) : ℕ := 2 * (mkParams K N).fn + 2 * (mkParams K N).p + 2 * (mkParams K N).logT + 4 * K + 64

/-! ## The axis cost bounds, affine in `Φ` -/

def sapF (K N Φ k : ℕ) : ℕ :=
  AX.sapAxCost (mkParams K N).p (EX.sK (mkParams K N) k) (EX.tK (mkParams K N) k) (mkParams K N).α
    (EX.mS (mkParams K N) k) (kbK K N) (BSf K N k) (mmK K N) Φ (BaccK K N) (BaccK K N) (NLogN.ST.BqT K N)

def bapF (K N Φ k : ℕ) : ℕ :=
  AX.bapAxCost (mkParams K N).p (EX.sK (mkParams K N) k) (EX.tK (mkParams K N) k) (mkParams K N).α
    (EX.mB (mkParams K N) k) (kbK K N) (BBf K N k) (mmK K N) Φ (BaccK K N) (BaccK K N) (NLogN.ST.BqT K N)

def CS0 (K N : ℕ) : ℕ := (Finset.range K).sup (sapF K N 0)
def DS (K N : ℕ) : ℕ := (Finset.range K).sup (fun k => sapF K N 1 k - sapF K N 0 k)
def CB0 (K N : ℕ) : ℕ := (Finset.range K).sup (bapF K N 0)
def DB (K N : ℕ) : ℕ := (Finset.range K).sup (fun k => bapF K N 1 k - bapF K N 0 k)

def CSK (K N Φ : ℕ) : ℕ := CS0 K N + Φ * DS K N
def CBK (K N Φ : ℕ) : ℕ := CB0 K N + Φ * DB K N

/-! ## The total cost, `lin` and `calls` -/

/-- The cost bound of the step with Fermat-product cost `Φf` and small-product cost `Φm`. -/
def GK (K N Φf Φm : ℕ) : ℕ :=
  stepCost K N Φf Φm (BsK K N) (CSK K N Φm) (CBK K N Φm) (BxK K N) (QK K N) (BcK K N) (BdK K N)

/-- The non-multiplication part of the cost. -/
def lin (K N : ℕ) : ℕ := GK K N 0 0

/-- Number of Fermat-ring products (each of `fn + 1` bits). -/
def cntF (K N : ℕ) : ℕ := GK K N 1 0 - GK K N 0 0

/-- Number of small products (each of `mmK K N` bits). -/
def cntM (K N : ℕ) : ℕ := GK K N 0 1 - GK K N 0 0

/-- The multiplications performed on `N`-bit inputs: `(count, size)`. -/
def calls (K N : ℕ) : List (ℕ × ℕ) := [(cntF K N, (mkParams K N).fn + 1), (cntM K N, mmK K N)]

end NLogN.ST

end

section
-- Source module: NLogN.HStNum
/-!
# The recursive step: numeric facts about `mkParams K N` derived from the published lemmas
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.ST

open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref

/-- The threshold of `mkParams_step`. -/
def n0K (K : ℕ) : ℕ := 2 ^ 2 ^ (K * (64 * K ^ 2 * (256 * K ^ 2).factorial) + 4)

/-! ## Basic facts and the bit-size inequalities -/

/-- The facts used below (all from `HAsym.PF`, `mkParams_s_spec`, `T_eq`). -/
structure BF (K N : ℕ) : Prop where
  K20 : 20 ≤ K
  pf : Asym.PF K N
  S_le : (mkParams K N).S ≤ 2 ^ (mkParams K N).logT
  T_le : 2 ^ (mkParams K N).logT ≤ 2 * (mkParams K N).S
  TT : (mkParams K N).tdims.prod = 2 ^ (mkParams K N).logT
  r_eq : (mkParams K N).r = 2 ^ (mkParams K N).e
  e_le : (mkParams K N).e ≤ (mkParams K N).logT
  fn_eq : (mkParams K N).fn = 4 * 2 ^ (mkParams K N).e * (mkParams K N).P
  sl_le : ∀ x ∈ (mkParams K N).s, x ≤ 2 ^ (mkParams K N).e
  α_le : (mkParams K N).α ≤ (mkParams K N).p
  exC : GL.exC (mkParams K N) = 2 * (mkParams K N).b + 6 * K * (mkParams K N).α ^ 2

/-! ## The length of `exactConvL` -/

end NLogN.ST

end

section
-- Source module: NLogN.HSt11
/-!
# The recursive step, part 11: the numeric premises `NumOK` and the assembly of `StepArgs`
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unreachableTactic false
set_option linter.unusedTactic false

namespace NLogN.ST

open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref

/-- The arithmetic premises about `q = mkParams K N` that need the asymptotic analysis. -/
structure NumOK (K N : ℕ) : Prop where
  sax : ∀ k < K, EX.SAx (mkParams K N) (kbK K N) (mmK K N) (BaccK K N) (BaccK K N) (NLogN.ST.BqT K N) (BSf K N) k
  bax : ∀ k < K, EX.BAx (mkParams K N) (kbK K N) (mmK K N) (BaccK K N) (BaccK K N) (NLogN.ST.BqT K N) (BBf K N) k
  inU : ∀ a < 2 ^ N, 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))
  inW : ∀ a < 2 ^ N, ∀ b < 2 ^ N, 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))
  smallF : (mkParams K N).fn + 1 < N
  smallM : mmK K N < N

end NLogN.ST

end

section
-- Source module: NLogN.HSt12
/-!
# The recursive step, part 12: `StepOK (stepP K) n₀ (lin K) (calls K)`
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.ST

open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref

/-! ## Procedure calls -/

/-- `true` iff the program contains no procedure call. -/
def noPrc : RM → Bool
  | .prc .. => false
  | .seq a b => noPrc a && noPrc b
  | .ite _ a b => noPrc a && noPrc b
  | .rep _ _ b => noPrc b
  | _ => true

/-! ## The main theorem -/

/-- A multiplication oracle that allows everything for free (used for the functional `run`). -/
def M0 : MulSpec := ⟨fun _ _ => 0, fun _ _ => True⟩

end NLogN.ST

end

section
-- Source module: NLogN.HNk1
/-!
# Task K, part 1: basic facts about `mkParams K N` and the per-axis conditions `SAx`, `BAx`

Everything here is proved from `Asym.pf_of_large` and the explicit definitions (no use of the
stubbed published lemmas).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.NK

open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref NLogN.ST

/-! ## Generic size lemmas -/

/-! ## The source lengths -/

/-- The basic facts. -/
structure KF (K N : ℕ) : Prop where
  K20 : 20 ≤ K
  big : 2 ^ (2 ^ (8 * K) + 1) ≤ N
  pf : Asym.PF K N
  sl : (mkParams K N).s.length = K
  e_le : (mkParams K N).e ≤ (mkParams K N).logT
  TT : EX.TT (mkParams K N) = 2 ^ (mkParams K N).logT
  hJ : BD.HJ (mkParams K N)
  s0 : ∀ k < K, 0 < EX.sK (mkParams K N) k
  st : ∀ k < K, EX.sK (mkParams K N) k < EX.tK (mkParams K N) k
  co : ∀ k < K, Nat.Coprime (EX.sK (mkParams K N) k) (EX.tK (mkParams K N) k)
  t2 : ∀ k < K, 2 ≤ EX.tK (mkParams K N) k
  te : ∀ k < K, EX.tK (mkParams K N) k ≤ 2 ^ (mkParams K N).e
  jJ : ∀ k < K, jIter (mkParams K N).p (EX.sK (mkParams K N) k) (EX.tK (mkParams K N) k)
    (mkParams K N).α ≤ BD.Jm (mkParams K N)
  p5 : (mkParams K N).p ≤ 5 * (mkParams K N).b
  bp : 2 * (mkParams K N).b ≤ (mkParams K N).p

/-! ## Monotonicity of the stage bounds -/

/-! ## The table bound `BqT` -/

/-- The quantity inside `BqT`. -/
def GT (K N : ℕ) : ℕ := (mkParams K N).α ^ 2 + 2 * 2 ^ (mkParams K N).e +
  2 * eWidth (mkParams K N).p (mkParams K N).α + 2 * sWidth (mkParams K N).p (mkParams K N).α + 2

/-! ## Abstract versions of the hypothesis structures -/

/-! ## `SAx` -/

/-! ## `BAx` -/

end NLogN.NK

end

section
-- Source module: NLogN.HNk2
/-!
# Task K, part 2: the input conditions `FwdInX`, `smallF`, `smallM` and `NumOK`
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.NK

open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref NLogN.ST

/-! ## Lengths -/

/-! ## From `LB` to `GB` -/

/-! ## `FwdInX` -/

/-- The `M`-independent part of `fermatW_facts`. -/
def M00 : MulSpec := ⟨fun _ _ => 0, fun _ _ => True⟩

/-! ## `smallF`, `smallM` -/

/-! ## The main statement -/

/-- The threshold (the same as that of `stepOK`). -/
def n1K (K : ℕ) : ℕ := n0K K

end NLogN.NK

end

section
-- Source module: NLogN.HFin3
/-!
# Final assembly, part 3: the cost of the step for `q = mkParams K N`, under explicit bounds
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option maxHeartbeats 8000000
set_option maxRecDepth 100000

namespace NLogN.FIN

open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref NLogN.ST

/-- The bounds on the parameters used by the cost estimate: `β` bounds all bit sizes,
`W` bounds the band widths (and is much smaller than `β`). -/
structure HB (K N β W : ℕ) : Prop where
  kf : NK.KF K N
  ts : ∀ k < K, EX.tK (mkParams K N) k ≤ 2 * EX.sK (mkParams K N) k
  Ws : ∀ k < K, W ≤ EX.sK (mkParams K N) k
  sW : 2 * sWidth (mkParams K N).p (mkParams K N).α + 1 ≤ W
  eJ : (BD.Jm (mkParams K N) + 1) * (2 * eWidth (mkParams K N).p (mkParams K N).α + 1 + 1) ≤ W
  Wβ : W ≤ β
  p : (mkParams K N).p ≤ β
  P : (mkParams K N).P ≤ β
  kb : kbK K N ≤ β
  mm : mmK K N ≤ β
  Bacc : BaccK K N ≤ β
  BqT : NLogN.ST.BqT K N ≤ β
  Bx : BxK K N ≤ β
  Q : QK K N ≤ β
  Bc : BcK K N ≤ β
  α : 2 * (mkParams K N).α ^ 2 ≤ β
  b : (mkParams K N).b ≤ β
  par : Nat.size (CR.parBnd K N (zsz (N : ℤ))) ≤ β
  Kβ : K ≤ β
  Bs : BsK K N ≤ 16 * 2 ^ (mkParams K N).e * β
  Bd : BdK K N ≤ 16 * 2 ^ (mkParams K N).e * β

/-! ## Abstract pieces of the final estimate -/

end NLogN.FIN

end

section
-- Source module: NLogN.HFin4
/-!
# Final assembly, part 4: the bounds `HB` hold for huge `N`
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option maxHeartbeats 8000000
set_option maxRecDepth 100000

namespace NLogN.FIN

open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref NLogN.ST

/-- `γ = ⌈√⌈√b⌉⌉`, a fourth root of `b`. -/
def gam (b : ℕ) : ℕ := ceilSqrt (ceilSqrt b)

/-- The arithmetic facts about `q = mkParams K N` for huge `N`. -/
structure PB (K N : ℕ) : Prop where
  kf : NK.KF K N
  hN : n0K K ≤ N
  hP : 10 ^ 60 * (K + 1) ^ 12 * (Nat.size (mkParams K N).b + 20) ^ 12 ≤ (mkParams K N).b

/-- Simple facts. -/
structure SB (K N : ℕ) : Prop where
  b1 : 1 ≤ (mkParams K N).b
  Kb : K ≤ (mkParams K N).b
  p5 : (mkParams K N).p ≤ 5 * (mkParams K N).b
  bp : 2 * (mkParams K N).b ≤ (mkParams K N).p
  lT : (mkParams K N).logT ≤ (mkParams K N).b + 3
  e_le : (mkParams K N).e ≤ (mkParams K N).logT
  P : (mkParams K N).P = 2 * (mkParams K N).p + (mkParams K N).logT + 8
  α2 : 384 * K * (mkParams K N).α ^ 2 ≤ (mkParams K N).b
  sW : 2 * sWidth (mkParams K N).p (mkParams K N).α + 1 ≤ 200 * (mkParams K N).b
  eW : 2 * eWidth (mkParams K N).p (mkParams K N).α + 1 ≤ 200 * (mkParams K N).b
  B20 : 100 * (Nat.size (mkParams K N).b + 20) ≤ (mkParams K N).b
  bB : (mkParams K N).b < 2 ^ Nat.size (mkParams K N).b
  K20 : 20 ≤ K
  mm : mmK K N ≤ 30 * (mkParams K N).b
  T : 2 ^ (mkParams K N).logT ≤ 2 ^ ((mkParams K N).b + 3)

end NLogN.FIN

end

section
-- Source module: NLogN.HFin5
/-!
# Final assembly, part 5: the `O(n log n)` theorem

For `K ≥ 10^4` and `N` huge, `HB K N (200 b) (1000 K γ³)` holds (part 4), so `GK_le` bounds the
non-multiplication cost `lin` by `O(N log N)` and the two recursive-call families by a quarter of
`TT' N` each.  `Top.hv_mulTimeBound` with `D = 2` then gives `MulTimeBound (n log n)`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option maxHeartbeats 8000000
set_option maxRecDepth 100000

namespace NLogN.FIN

open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref NLogN.ST NLogN.Top

/-! ## Polynomial vs exponential -/

/-! ## Counts of the recursive calls -/

/-- The additive constant of `GK_le`. -/
def Jc (K N β : ℕ) : ℕ :=
  10 ^ 22 * ((K + 1) ^ 2 * ((2 ^ (mkParams K N).logT + 1) * (β + 2) ^ 2)) +
    10 ^ 64 * ((K + 1) ^ 2 * ((2 ^ (mkParams K N).e + 1) ^ 3 * (β + 2) ^ 12)) +
    10 ^ 7 * ((N + 1) * (β + 2))

/-! ## The small products cost at most a quarter -/

/-! ## The linear part -/

/-! ## The final theorem -/

/-- The threshold. -/
def nF (K B0 : ℕ) : ℕ := max (n0K K) (max (2 ^ (2 ^ (8 * K) + 1)) (2 ^ 2 ^ B0))

end NLogN.FIN

end
Source
D. Harvey, J. van der Hoeven, Integer multiplication in time O(n log n), Ann. of Math. 193 (2021), 563–617 (Theorem 1.1: multitape Turing machine multiplication in O(n log n)). Definitions of the Lean development NLogN, written for the prove2.me integer-multiplication campaign.

View graph