HvdH machine lemma EX.exactLP_all (The full `fwdL` / `exactConvL` programs, part 10: `exactLP`)
ProvedNLogN.EX.exactLP_allThe following holds (Lean statement, in the scope of module NLogN.HEx10):
theorem NLogN.EX.exactLP_all (fw : LProg2 M Ctx PreW (fermatW q) CW) (hfw : FwOK fw) {m Φm : ℕ}
(hM : MulBnd M m Φm) {kb mm Φ Bacc Qa Bq Bx CS CB Q : ℕ} {BS BB : ℕ → ℕ}
(hcfg : FwdCfgX M q kb mm Φ Bacc Qa Bq Bx CS CB m Q BS BB) (s : IState HS)
(hE : FwdEnvX q kb Ctx s)
(u v : List ℤ) (R RV LM LS LQ LC LR : List Item) (mu : ℕ)
(hu : s.G gD = ints u ++ R) (hv : s.G gV = ints v ++ RV)
(hul : u.length = q.S) (hvl : v.length = q.S)
(hPM : s.G gPM = .int q.S :: LM) (hPS : s.G gPS = .int (2 ^ (q.p - q.b)) :: LS)
(hPQ : s.G gPQ = .int ((q.S : ℤ) ^ 2) :: LQ)
(hPC : s.G gPC = .int (2 ^ (NLogN.GL.exC q + 1)) :: LC)
(hPR : s.G gPR = .int (2 ^ (q.p + 1)) :: LR)
(hub : ∀ x ∈ u, zsz x ≤ mu) (hvb : ∀ x ∈ v, zsz x ≤ mu) (hmu : mu + (q.p - q.b) + 1 ≤ Q)
(inU : FwdInX q PreW BS BB m Q (exU q u)) (inV : FwdInX q PreW BS BB m Q (exU q v))
(inW : FwdInX q PreW BS BB m Q (exW q u v))
(hS2 : zsz ((q.S : ℤ) ^ 2) ≤ m) (hBQ : 2 * m + NLogN.GL.exC q + q.p + 6 ≤ Q)
(hSQ : zsz ((2 * q.S : ℕ) : ℤ) ≤ Q) :
(exactLP fw).run s = (s.upd gV RV).upd gD (ints (exactConvL q u v) ++ R) ∧
(exactLP fw).ok M s ∧
(exactLP fw).cost M s ≤
3 * fwdLCost q CS CB Bx CW Q Φm + 5 * q.S * Φm + 1000000 * (q.S + 1) * (Q + 2)
Context. The lemma belongs to the part The full fwdL / exactConvL programs, part 10: exactLP: exactLP fw follows GL.exactP (scale u, fwdL, park, scale v, fwdL, pointwise
mulConj, fwdL, round) with fwdLP fw in place of GL.fwdP.
Formalization Note. This is a lemma of the Lean development NLogN, a multitape-Turing-machine implementation of the Harvey–van der Hoeven 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 .
-- Harvey–van der Hoeven multitape-TM development (NLogN), generated by skeleton subtraction.
import Definitions.Def_IntMul_HvdH_M_Defs8
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
open NLogN
open NLogN.EX
open IntMul NLogN IntMul.HvdH IntMul.HvdH.Ref NLogN.GL NLogN.AX NLogN.Rsp
variable {M : MulSpec} {Ctx : IState HS → Prop} {PreW : List (ℤ × ℤ) → List (ℤ × ℤ) → Prop}
{q : Params} {CW : ℕ}
set_option maxHeartbeats 8000000
theorem NLogN.EX.exactLP_all (fw : LProg2 M Ctx PreW (fermatW q) CW) (hfw : FwOK fw) {m Φm : ℕ}
(hM : MulBnd M m Φm) {kb mm Φ Bacc Qa Bq Bx CS CB Q : ℕ} {BS BB : ℕ → ℕ}
(hcfg : FwdCfgX M q kb mm Φ Bacc Qa Bq Bx CS CB m Q BS BB) (s : IState HS)
(hE : FwdEnvX q kb Ctx s)
(u v : List ℤ) (R RV LM LS LQ LC LR : List Item) (mu : ℕ)
(hu : s.G gD = ints u ++ R) (hv : s.G gV = ints v ++ RV)
(hul : u.length = q.S) (hvl : v.length = q.S)
(hPM : s.G gPM = .int q.S :: LM) (hPS : s.G gPS = .int (2 ^ (q.p - q.b)) :: LS)
(hPQ : s.G gPQ = .int ((q.S : ℤ) ^ 2) :: LQ)
(hPC : s.G gPC = .int (2 ^ (NLogN.GL.exC q + 1)) :: LC)
(hPR : s.G gPR = .int (2 ^ (q.p + 1)) :: LR)
(hub : ∀ x ∈ u, zsz x ≤ mu) (hvb : ∀ x ∈ v, zsz x ≤ mu) (hmu : mu + (q.p - q.b) + 1 ≤ Q)
(inU : FwdInX q PreW BS BB m Q (exU q u)) (inV : FwdInX q PreW BS BB m Q (exU q v))
(inW : FwdInX q PreW BS BB m Q (exW q u v))
(hS2 : zsz ((q.S : ℤ) ^ 2) ≤ m) (hBQ : 2 * m + NLogN.GL.exC q + q.p + 6 ≤ Q)
(hSQ : zsz ((2 * q.S : ℕ) : ℤ) ≤ Q) :
(exactLP fw).run s = (s.upd gV RV).upd gD (ints (exactConvL q u v) ++ R) ∧
(exactLP fw).ok M s ∧
(exactLP fw).cost M s ≤
3 * fwdLCost q CS CB Bx CW Q Φm + 5 * q.S * Φm + 1000000 * (q.S + 1) * (Q + 2) := by sorry