HvdH machine lemma AX.eTab_flatten_length (One resampling axis, part 8: the `B̃` axis program `bapAxP`)

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

theorem NLogN.AX.eTab_flatten_length (p s t α : ℕ) :
    (eTab p s t α).flatten.length = s * (2 * HvdH.eWidth p α + 1)

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 $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|$.