The level branch computes `levelH` (round six, `gen_level`)

The level branch computes levelH.

The following holds (Lean statement, in the scope of module Solutions.R6ILGenL):

theorem IntMul.Kappa.R6.IL.gen_level {I : List Sym} {tab : Fin 1 → IStmt HS 1} (C : Bit.QHNet (ZMod 2) W T m)
    (s0 : IState HS) {q e P L M Bb : ℕ} {A B Cs : Shape} (hm : 2 ≤ m) (hq : q.Prime)
    (hqB : qBound C < q) (hOK : ∀ f, C.EdgesOK (q ^ f)) (hruns : C.RunsOK)
    (hM : zsz (M : ℤ) ≤ Bb) (hEB : EntB m q W T e P L (vol A) (vol B) (vol Cs) M)
    (hP : 1 ≤ P) (hL : 1 ≤ L) (hA : ∀ x ∈ A, 1 ≤ x) (hB : ∀ x ∈ B, 1 ≤ x)
    (hC : ∀ x ∈ Cs, 1 ≤ x) (hWL : m ≤ e → W ∣ L) (hN3 : (q ^ (e / m) + 1) ^ 3 ≤ M)
    (child : ℕ × ℕ × ℕ → List (ZMod 2) → List (ZMod 2)) (c0 : ℕ × ℕ × ℕ → ℕ)
    (hchL : ∀ ρ ∈ runsL C, ∀ ys : List (ZMod 2),
      ys.length = vol (P :: (L / W) :: hdShape A (List.replicate (e % m) q ++ B)
        (List.replicate (e % m) q ++ Cs) m (q ^ (e / m))) →
      (child ρ ys).length = vol (P :: (L / W) :: hdShape A (List.replicate (e % m) q ++ B)
        (List.replicate (e % m) q ++ Cs) m (q ^ (e / m))))
    (hch : m ≤ e → ∀ ρ ∈ runsL C, ∀ (t' : IState HS) (R' : List Item) (ys : List (ZMod 2)),
      DescG t' (ρ.2.2 * (e / m)) P (L / W)
        (chDesc m (q ^ (e / m)) (vol A) (q ^ (e % m) * vol B) (q ^ (e % m) * vol Cs) ρ).1
        (chDesc m (q ^ (e / m)) (vol A) (q ^ (e % m) * vol B) (q ^ (e % m) * vol Cs) ρ).2.1
        (chDesc m (q ^ (e / m)) (vol A) (q ^ (e % m) * vol B) (q ^ (e % m) * vol Cs) ρ).2.2 →
      ys.length = vol (P :: (L / W) :: hdShape A (List.replicate (e % m) q ++ B)
        (List.replicate (e % m) q ++ Cs) m (q ^ (e / m))) →
      IRuns I tab (tab 0) (t'.upd 0 (ints (enc2 ys) ++ R')) (t'.upd 0 (ints (enc2 (child ρ ys)) ++ R'))
        (c0 ρ))
    (R : List Item) (xs : List (ZMod 2)) (hxs : xs.length = vol (P :: L :: hdShape A B Cs e q)) :
    IRuns I tab (genL C)
      (encK (s0.upd 0 (ints (enc2 xs) ++ R))
        (regState (fDesc e P L (vol A) (vol B) (vol Cs))
          (vEnt m q W T e P L (vol A) (vol B) (vol Cs)) genD))
      (encK (s0.upd 0 (ints (enc2 (if m ≤ e then Bit.levelH C (q ^ (e / m)) P (L / W) A
          (List.replicate (e % m) q ++ B) (List.replicate (e % m) q ++ Cs) child xs else xs)) ++ R))
        (regState (fDesc e P L (vol A) (vol B) (vol Cs))
          (vEnt m q W T e P L (vol A) (vol B) (vol Cs)) genD))
      (cGenL C e (vol (P :: (L / W) :: hdShape A (List.replicate (e % m) q ++ B)
        (List.replicate (e % m) q ++ Cs) m (q ^ (e / m)))) Bb c0)

Context. Round six, item language: the level branch of the general procedure

genL C: if f = e / m = 0 nothing; otherwise push -N on sNQ (N = q ^ f), run the level body levBody C (the level registers are those of the entry file), pop sNQ. gen_level: given a specification of the child calls, it computes levelH with the child of progH.

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).