Fine Lemma 12 from `ILProp11` (round six, `l12R_fine`)

Fine Lemma 12 from ILProp11, with the row-padding base W ^ cW.

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

theorem IntMul.Kappa.R6.IL.l12R_fine (C : Bit.QHNet (ZMod 2) W T m) (hm : 2 ≤ m) (hruns : C.RunsOK) {τ : ℝ}
    (hτ0 : 0 < τ) (hτ1 : τ ≤ 1) (hmom : histMoment C.hist m τ < W)
    {cW : ℕ} (hcW : ∀ k, Bit.depH m (m ^ k) ≤ cW * k) {q : ℕ} (hq : q.Prime)
    (hOK : ∀ f, C.OK (q ^ f)) {tab : Fin 1 → IStmt HS 1} {T₀ c₁ : ℕ} {K₁ K₂ : ℝ}
    (hK₁ : 0 ≤ K₁) (hK₂ : 0 ≤ K₂) (hIL : ILProp11 tab C q T₀ c₁ K₁ K₂) :
    ∃ K : ℝ, 0 ≤ K ∧
      ∀ (u : ℕ) (Pre G Suf : Shape) (Bb : ℕ), 1 ≤ u →
      (∀ a ∈ Pre, 1 ≤ a) → (∀ a ∈ G, 1 ≤ a) → (∀ a ∈ Suf, 1 ≤ a) →
      zsz (((8 + m + W ^ cW + 4 * T₀) * (q ^ 2 * vol (binShape Pre G Suf (2 ^ u)) + 1) ^ 2 : ℕ) :
        ℤ) ≤ Bb → 1 ≤ Bb →
      ∀ (I : List Sym) (s : IState HS) (F : Fin HS → List ℤ) (xs : List (ZMod 2))
        (LP LG LS LU : List ℤ),
      F KIL.kP = (vol Pre : ℤ) :: LP → F KIL.kG = (vol G : ℤ) :: LG →
      F KIL.kS = (vol Suf : ℤ) :: LS → F KIL.aU = (u : ℤ) :: LU → F 0 = enc2 xs →
      F 8 = [] → F 9 = [] → F 10 = [] → F 11 = [] → F 15 = [] → F 20 = [] → F 21 = [] →
      F 23 = [] → F 24 = [] →
      xs.length = vol (binShape Pre G Suf (2 ^ u)) →
      ∃ c : ℕ, IRuns I tab (l12F q m (W ^ cW)) (encK s F)
        (encK s (Function.update F 0 (enc2 (pull (binShape Pre G Suf (2 ^ u))
          (binShape Pre G Suf (2 ^ u)) (swapPos Pre.length (Pre.length + 1 + G.length)) 0 xs))))
        c ∧
        (c : ℝ) ≤ K * (((vol (binShape Pre G Suf (2 ^ u)) : ℝ) + 1) * (u : ℝ) ^ τ +
          ((u : ℝ) + 1) ^ (c₁ + 1) * ((Bb : ℝ) + 2) ^ 2)

Context. Round six, item language: fine Lemma 12 for any bit network, from the item-language Prop. 11

The frozen Lemma 12 wrapper KFE.l12F q m W (binary embedding, min (W·Kp) e high-digit swaps, row padding to a multiple of W ^ Kp, the Prop. 11 oracle on the base-m pieces of the remaining digits, extraction) is generic in its procedure table: it only needs CallSpec for the oracle calls at the levels m ^ j. Here it is used with

• the table tab of an item-language Prop. 11 for the round-six network C (ILProp11 tab C q T₀ c₁ K₁ K₂: at every level k, with the KIL5 calling convention DescIn, tab 0 computes progH C q (m ^ k) at cost ⌈K₁ costH C (m^k) V + K₂ (m^k + 1)^c₁ (Bb + 2)²⌉), and
• the row-padding base W' = W ^ cW, where depH m (m ^ k) ≤ cW k (depH_pow_le), so that the padded rows are divisible by W ^ depH as progH_correct requires.

Results.

• l12R_fine: ILProp11 → fine Lemma 12 with cost K ((V+1) u^τ + (u+1)^(c₁+1) (Bb+2)²).
• l12Canon_of_IL: ILProp11 → L12Canon tab (l12F q m W') τ (canonical item size).
• l12Canon_of_net': from ilProp11_of_net (R6ILProp).

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