The call wrapper of a run (round six, `callR_runs`)

The call wrapper of a run. The registers gF, rLp, gA, sQQ, rVB, rVC, dP hold f, L', vol A, N, vol B, vol Cs, P; if procedure j0 maps every state with the child descriptor to the child's array, then callR does so on the level's state.

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

theorem IntMul.Kappa.R6.IL.callR_runs (j0 : Fin Pp) (m : ℕ) (ρ : ℕ × ℕ × ℕ) (hρ : ρ.1 + ρ.2.2 ≤ m)
    (hρ' : ρ.2.1 + ρ.2.2 ≤ m) {f N P L' a b c : ℕ}
    (ch : List (ZMod 2) → List (ZMod 2)) (c0 V : ℕ)
    (hrec : ∀ (t' : IState HS) (R' : List Item) (ys : List (ZMod 2)),
      DescG t' (ρ.2.2 * f) P L' (a * N ^ ρ.1) (N ^ (m - ρ.1 - ρ.2.2) * (b * N ^ ρ.2.1))
        (N ^ (m - ρ.2.1 - ρ.2.2) * c) →
      ys.length = V →
      IRuns I iprog (iprog j0) (t'.upd 0 (ints (enc2 ys) ++ R'))
        (t'.upd 0 (ints (enc2 (ch ys)) ++ R')) c0)
    {M Bb : ℕ} (hM : zsz (M : ℤ) ≤ Bb) (hM1 : 1 ≤ M) (hN : 1 ≤ N) (hNM : N ≤ M) (hfM : f ≤ M)
    (hbA : a * N ^ ρ.1 ≤ M) (hbB : N ^ (m - ρ.1 - ρ.2.2) * (b * N ^ ρ.2.1) ≤ M)
    (hbC : N ^ (m - ρ.2.1 - ρ.2.2) * c ≤ M) (hbE : ρ.2.2 * f ≤ M) (hbL : L' ≤ M)
    (ha1 : 1 ≤ a) (hb1 : 1 ≤ b) (hc1 : 1 ≤ c) (hrM : ρ.2.2 ≤ M)
    (t : IState HS) {L1 L2 L3 L4 L5 L6 L7 : List Item}
    (hF : t.G gF = .int (f : ℤ) :: L1) (hLp : t.G rLp = .int (L' : ℤ) :: L2)
    (hA : t.G gA = .int (a : ℤ) :: L3) (hQQ : t.G sQQ = .int (N : ℤ) :: L4)
    (hB : t.G rVB = .int (b : ℤ) :: L5) (hC : t.G rVC = .int (c : ℤ) :: L6)
    (hP : t.G dP = .int (P : ℤ) :: L7)
    (R : List Item) (ys : List (ZMod 2)) (hys : ys.length = V) :
    IRuns I iprog (callR j0 m ρ) (t.upd 0 (ints (enc2 ys) ++ R))
      (t.upd 0 (ints (enc2 (ch ys)) ++ R)) (cCallR m ρ Bb c0)

Context. Round six, item language: the code of one edge (shift templates and one child call per run)

• the general descriptor DescG t e P L a b c (dJ = -1, dT = e, dP, dL, dA, dB, dC);
• npow and the natural-expression push lists (pushOK_NE);
• callR m ρ: push the child descriptor of the run ρ = (i, j, r) (width r f, shapes A ++ [N]^i, [N]^(m-i-r) ++ B ++ [N]^j, [N]^(m-j-r) ++ Cs), call procedure 0, pop; callR_runs;
• tplE E: the rational shift templates of the lower triangular E (tplE_eval: they denote shiftSteps (redM N E));
• edgeR m e: shifts of E₂, the child calls, shifts of E₁; edgeR_runs: it computes realEdge (R6BitLevel).

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*).