Round-six lemma `rowCodeU_runs`
ProvedIntMul.Kappa.R6.IL2.rowCodeU_runsAn auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.
The following holds (Lean statement, in the scope of module Solutions.R6IL2Run):
theorem IntMul.Kappa.R6.IL2.rowCodeU_runs {Kc : ℝ} (H13 : L13U tab l12 τ Kc) {I : List Sym}
{k K e T S0 B r H : ℕ} {i j : Fin m} (hij : (i : ℕ) ≠ j) (hK : 6 ≤ K)
(hp : PF m k K e T S0 B r) {u : IState HS} (hA : Agree (rowσ m k K e T S0 B r H i j) u)
(zs : List GI) (R0 : List Item) (hg0 : u.G 0 = ints (gflat zs) ++ R0)
(hl : zs.length = B * 2 ^ T * S0 * r) (hGB : GB H zs) :
∃ c, IRuns I tab (rowCodeU l12) u
(u.upd 0 (ints (gflat (permRecs (rect (N0R m k K e T B i j) (N1R m k K e i j) (N2R m k K e i j)
(N3R m k K e S0 i j) (m ^ k * K)) (rowAddAddr K (e % K) (m ^ k) (pxR i j) (pyR i j)) r zs))
++ R0)) c ∧
(c : ℝ) ≤ bnd τ Kc K (m ^ k) (B * 2 ^ T * S0) r H +
(cHd (zsz ((VbR T S0 B r H : ℕ) : ℤ)) : ℝ)
Context. Round six, item language (I2): the run of the uniform row addition (any m, tab, l12, τ)
Parametric copy of the tainted part of KFX6Run: L13U tab l12 τ Kc (the Lemma 13 core as a
hypothesis), l13U_L13U (from L12Canon), the code rowCodeU l12, the row geometry σF,
posR_he, shR_eq, vol_rowRect for label dimension m, and rowCodeU_runs.
The bit-length loop, the header pushes and cHd are the frozen ones.
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*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.
import Definitions.Def_IntMul_Kappa_R6_Defs13
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL2
open IntMul NLogN NLogN.RS NLogN.KIL NLogN.KFD NLogN.KFE NLogN.KFB NLogN.KFL NLogN.KFW NLogN.KFH NLogN.KFX AModel Butterfly IntMul.Kappa.R6.IL
variable {tab : Fin 1 → IStmt HS 1} {l12 : IStmt HS 1} {τ : ℝ} {m : ℕ}
theorem IntMul.Kappa.R6.IL2.rowCodeU_runs {Kc : ℝ} (H13 : L13U tab l12 τ Kc) {I : List Sym}
{k K e T S0 B r H : ℕ} {i j : Fin m} (hij : (i : ℕ) ≠ j) (hK : 6 ≤ K)
(hp : PF m k K e T S0 B r) {u : IState HS} (hA : Agree (rowσ m k K e T S0 B r H i j) u)
(zs : List GI) (R0 : List Item) (hg0 : u.G 0 = ints (gflat zs) ++ R0)
(hl : zs.length = B * 2 ^ T * S0 * r) (hGB : GB H zs) :
∃ c, IRuns I tab (rowCodeU l12) u
(u.upd 0 (ints (gflat (permRecs (rect (N0R m k K e T B i j) (N1R m k K e i j) (N2R m k K e i j)
(N3R m k K e S0 i j) (m ^ k * K)) (rowAddAddr K (e % K) (m ^ k) (pxR i j) (pyR i j)) r zs))
++ R0)) c ∧
(c : ℝ) ≤ bnd τ Kc K (m ^ k) (B * 2 ^ T * S0) r H +
(cHd (zsz ((VbR T S0 B r H : ℕ) : ℤ)) : ℝ) := by sorry