HvdH machine lemma Rsp.JP_okc (`Japprox` on a slice: the `E` pass (`gresP` against the `E` tables) it)

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

theorem NLogN.Rsp.JP_okc (M : MulSpec) (mm Φ B : ℕ) (hM : MulBnd M mm Φ) (p s t α n : ℕ) (hs : 0 < s)
    (u : List (ℤ × ℤ)) (hu : u.length = s)
    (s0 : IState HS) (RU LL LN : List Item) (hE : EParams s0 p s t α)
    (hU : s0.G CU = gints u ++ RU)
    (hL : s0.G JL = .int ((2 * s : ℕ) : ℤ) :: LL) (hN : s0.G JN = .int (n : ℤ) :: LN)
    (hub : ∀ z ∈ u, zsz z.1 ≤ B ∧ zsz z.2 ≤ B)
    (hv : ∀ j ≤ n, ∀ z ∈ vL p s t α u j, zsz z.1 ≤ mm ∧ zsz z.2 ≤ mm)
    (hac : ∀ j ≤ n, ∀ z ∈ accL p s t α u j, zsz z.1 ≤ B ∧ zsz z.2 ≤ B)
    (hWB : ∀ W ∈ eTab p s t α, ∀ y ∈ W, zsz y ≤ mm)
    (hAcc : (2 * HvdH.eWidth p α + 2) * 2 ^ (2 * mm) ≤ 2 ^ B) (hmB : 2 * mm ≤ B)
    (hLB : zsz ((s + (2 * HvdH.eWidth p α + 1) : ℕ) : ℤ) ≤ B) (hpB : p + 1 ≤ B)
    (hnB : zsz ((s * (2 * HvdH.eWidth p α + 1) : ℕ) : ℤ) ≤ B) (hsB : zsz (s : ℤ) ≤ B)
    (h2s : zsz ((2 * s : ℕ) : ℤ) ≤ B) (hnN : zsz (n : ℤ) ≤ B) (h2B : 2 ≤ B) :
    JP.ok M s0 ∧ JP.cost M s0 ≤ jCost s (2 * HvdH.eWidth p α + 1) n mm Φ B

Context. The lemma belongs to the part Japprox on a slice: the E pass (gresP against the E tables) iterated with signed.

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