Round-six lemma `rowUC_of_canon`

rowUC_of from the output of IL.swapNeedτ_of_bitNetR6 (round six: m = 576).

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

theorem IntMul.Kappa.R6.IL2.rowUC_of_canon (hτ0 : 0 ≤ τ) (hτ1 : τ ≤ 1)
    (h : ∃ (tab : Fin 1 → IStmt HS 1) (l12 : IStmt HS 1), L12Canon tab l12 τ ∧ SwapNeedτ tab τ) :
    ∃ tab : Fin 1 → IStmt HS 1, RowUCP 576 τ tab ∧ SwapNeedτ tab τ

Context. Round six, item language (I2): RowUC, uniform row additions for any m, τ and Lemma 12 table

RowUC m τ Isym tbl rowC Kc is the frozen KFW.RowU (KFWRowIface) with the label dimension mC = 100^3 replaced by m and τ50 = 1 - 2^-50 by τ: the single fixed code rowC implements the row addition Pm i j on the bits Fin m × Fin (m^k) laid out at posR m K e k, parameters [m^k, K, e, t, S0, B, r, H, i, j] in the background registers 36 … 45, at cost ≤ (Kc (K+2) + 1) · n · (r (H+1) (m^k + 1)^τ + PsiR r Z H).

RowUCP m τ tab: a fixed list of procedures and a code with RowUC in every extension IL.kTableP tab ext.

rowUC_of: 16 ≤ m ≤ 10^6 → 0 ≤ τ ≤ 1 → IL.L12Canon tab l12 τ → RowUCP m τ tab (code (rowCodeU l12).ren id (gL E), no extra procedures).

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