The entry procedure (round six, `p14QH`)

The entry procedure.

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

theorem IntMul.Kappa.R6.IL3H.p14QH {c : IntMul.Kappa.R6.IL3H.Cfg} (hc : CfgOK c) (cW : ℕ) (hWc : c.W ≤ 2 ^ cW)
    (jZ jG jD jK jL : Fin Pp) (rowC : IStmt HS Pp)
    (hZt : tbl jZ = zloopC c jZ (zcontC jG)) (hGt : tbl jG = gloopC czH jG (gcontC jD))
    (hDt : tbl jD = dloopC c.m c.W jD (coreCH c cW (bodyCH c jK jL)))
    (hK : tbl jK = kerLoopC jK jL) (hL : tbl jL = levCH c jL rowC)
    {K r Z Zr P D S ρ p w Bz : ℕ} {CB : ℕ → ℝ}
    (L1 : LvH c Isym tbl jL rowC K r (chV c cW P K D S r w).Zl Zr (chV c cW P K D S r w).H
      (chV c cW P K D S r w).G CB 1)
    (hρ : ρ < K) (hK1 : 1 ≤ K) (hS : 1 ≤ S) (hP : 1 ≤ P) (hr : 1 ≤ r) (hD : 1 ≤ D)
    (hKW : cW * (chV c cW P K D S r w).d + 2 * (D / c.m * (chV c cW P K D S r w).G) ≤ K * D)
    (hGm : (chV c cW P K D S r w).G + c.m ≤ P * 2 ^ (K * D) * S * r)
    (hZ32 : zsz ((32 * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Z)
    (hHZ : zsz ((chV c cW P K D S r w).H : ℤ) ≤ Z)
    (hV1 : zsz ((VbH c K (K * D) S r (chV c cW P K D S r w).H 1 (ρ + K * (D - 1)) P : ℕ) : ℤ) ≤ Zr)
    (hMb : zsz ((MbChain c cW P K D S r w : ℕ) : ℤ) ≤ Bz)
    (pre : (chV c cW P K D S r w).q0 + (chV c cW P K D S r w).qB < D →
      MidPre c Isym tbl jL rowC CB K S r (chV c cW P K D S r w).H P D ρ (chV c cW P K D S r w).q0
        (chV c cW P K D S r w).Bp (chV c cW P K D S r w).qB (chV c cW P K D S r w).Zl Z Zr
        (chV c cW P K D S r w).G)
    (hEZ : zsz ((Etot c D (chV c cW P K D S r w).q0 (chV c cW P K D S r w).qB : ℕ) : ℤ) ≤ Z)
    (hH : w + (dwCL c D (chV c cW P K D S r w).q0 (chV c cW P K D S r w).qB + 2) ≤
      (chV c cW P K D S r w).H)
    (hp : zsz (p : ℤ) ≤ Z) (hwZ : w < 2 ^ Z)
    (st : IState HS) (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ)
    (xs : List (Fin r → ℂ)) (hx : RecRep r p zs xs)
    (hl : xs.length = vol (Butterfly.layerShape P K D S)) (h0 : f 0 = gflat zs ++ l)
    (h36 : f 36 = [(P : ℤ), (K : ℤ), (D : ℤ), (S : ℤ), (ρ : ℤ), (r : ℤ), (p : ℤ), (w : ℤ), (Z : ℤ)])
    (hfree : ∀ j : Fin HS, j ≠ 0 → j ≠ 36 → j.val < 50 → f j = [])
    (hb : GB w zs) (hdisk : ∀ j (h : j < xs.length), ‖xs[j]‖ ≤ 1)
    (hex : ∃ zs', RecRep r p zs' (Butterfly.prop14Proc (P := P) (S := S) hρ p
        (Butterfly.tens Butterfly.Cm : Butterfly.Op (Fin D)) xs)) :
    IRuns Isym tbl (p14CH jZ) (encK st f)
      (encK st (Function.update f 0 (gflat (Classical.choose hex) ++ l)))
      (8 * (2 * moveCost Z + 19) + (cChainH c CB cW P K D S r w Z Zr Bz +
        8 * (2 * moveCost Z + 19)))

Context. Round six, item language (I3): the entry procedure of the uniform Proposition 14

p14CH jZ = dIn ; mainCH jZ ; dOut (the frozen descriptor moves of KFWC15).

p14QH: on encK st f with the descriptor [P, K, D, S, ρ, r, p, w, Z] on stack 36, the array on stack 0 and the stacks 1 … 49 (but 36) empty, p14CH jZ leaves gflat zs* ++ l on stack 0 and restores every other stack.

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