HvdH machine lemma AX.expPos_zsz (One resampling axis, part 8: the `B̃` axis program `bapAxP`)
ProvedNLogN.AX.expPos_zszThe following holds (Lean statement, in the scope of module NLogN.HAx8):
theorem NLogN.AX.expPos_zsz (p K2 j g Bq : ℕ) (h : (4 * p + 35) * 2 ^ (2 * p) < 2 ^ Bq) :
zsz (HvdH.expPos p K2 j g) ≤ Bq
Context. The lemma belongs to the part One resampling axis, part 8: the B̃ axis program bapAxP: bapAxP on gD = gints L ++ R (with L of dims t :: rest, m = rest.prod) computes
gints (tensorGo [(s, bapL p s t α)] (t :: rest) L) ++ R: it pushes the derived scalars
e, s², 2α²-2, builds the seven tables of bapP (layout: HAx5), pops the derived scalars,
runs GL.axisP with the slice program bapSl, and pops the seven tables again. Every stack
except gD is restored.
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 open NLogN open NLogN.AX open IntMul NLogN IntMul.HvdH.Ref NLogN.GL NLogN.Rsp
theorem NLogN.AX.expPos_zsz (p K2 j g Bq : ℕ) (h : (4 * p + 35) * 2 ^ (2 * p) < 2 ^ Bq) :
zsz (HvdH.expPos p K2 j g) ≤ Bq := by sorry