The scaling slab pass (pass 1) (round six, `slabSc_runs`)

The scaling slab pass (pass 1).

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

theorem J6Seg.Slab.slabSc_runs (s : IState HS) (F : Fin HS → List ℤ) {n n' post pre : ℕ} (hnp : 0 < n * post)
    {src : ℕ → Option ℕ} (hs : MonoSrc n n' src) (p P' : ℕ) (L : List GI) (l : List ℤ)
    (hL : L.length = pre * (n * post)) {Bu : ℕ} (hBu : ∀ u ∈ gflat L, zsz u ≤ Bu)
    (hF0 : F 0 = gflat L ++ l) (hA : F lA = []) (hC : F lC = []) (hD : F lD = []) (RC : List ℤ)
    (hFC : F rC = flatC (ctlOf n n' src (fun _ => 2 ^ (P' - p - 1))) ++ RC) (hACC : F rACC = [])
    {LM : List ℤ} (hM : F rM = ((2 * post : ℕ) : ℤ) :: LM) {LN : List ℤ}
    (hN : F rNC = ((ctlOf n n' src (fun _ => 2 ^ (P' - p - 1))).length : ℤ) :: LN) {LB : List ℤ}
    (hB : F rNB = (pre : ℤ) :: LB) {LT : List ℤ}
    (hT : F rTOT = ((pre * (n' * (2 * post)) : ℕ) : ℤ) :: LT) :
    IRuns I iprog (J6Seg.Slab.passP (.op (.drop 0)) (.op (.mv 0 J6Seg.Slab.rT)) itS (.op (.mv J6Seg.Slab.rT 0))) (encK s F)
      (encK s (update F 0 (gflat (slabPass n n' post src (J6Seg.selH p P') L) ++ l)))
      (passC pre (ctlOf n n' src (fun _ => 2 ^ (P' - p - 1))).length (2 * post) (P' - p + 1)
        (2 * Bu + 2 + (2 * moveCost Bu + 19) + (300 * (Bu + 1) + 200 * (P' - p - 1 + 1)) +
          (2 * moveCost Bu + 19))
        (pre * (n' * (2 * post))) (Bu + (P' - p + 1)))

Context. B-line IL, B1 (streaming slab pass) §8: the slab passes of axisPipe on GI arrays

The three IL slab passes, on gflat arrays (post GI entries = m = 2 post integers per slab):

• slabId_runs (passes 3, 5: h = fun _ z => z; control ctlOf n n' src (fun _ => 0)),
• slabSc_runs (pass 1: h = selH p P; control ctlOf n n' src (fun _ => 2^(P-p-1))),
• slabOut_runs (pass 7: h = outH p P s t α on zip Y Y₂, source some l; control ctlOf N N some argO with argO l = d̃_l for l < s, else 0; the two arrays on stacks 0 and rZ; constants 2^(P-p), 2^p on rK1, rK2; multiplication MulOK pM).

Each takes the skeleton inputs (rC = flatC cs ++ RC, rACC = [], rNB = pre, rNC = |cs|, rM = 2 post, rTOT = pre · n' · 2 post, the rptX counters empty) and leaves gflat (slabPass …) ++ l on stack 0, everything else unchanged. The cost is passC …; with passC_le and |cs| ≤ n + n' (length_ctlOf_le) it is, per block, O((n + n' + 1) (post + 1) (cu + Ba + 1)) with cu = O(Bu + 1) (identity), O(Bu + P + 1) (scale), O(cU (Bu + Ba + 2) + P) (output: one multiplication per entry).

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