The cost of the compact Lemma 13 code (round six, `cL13_le`)

The cost of the compact Lemma 13 code (no factor K).

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

theorem IntMul.Kappa.R6.IL2C.cL13_le {Ksw τ : ℝ} (hKsw : 0 ≤ Ksw) (hτ0 : 0 ≤ τ) (hτ1 : τ ≤ 1)
    {N0 N1 N2 N3 K f ρ G R w Z : ℕ} {px py : Fin 3}
    (hp : IntMul.Kappa.R6.IL2C.RP N0 N1 N2 N3 K f ρ G px py) (hR : 1 ≤ R) (hfZ : f ≤ Z)
    (hZG : 4 * Z * (Z + 2) ≤ 2 ^ G) (hGK : 16 * Z * (Z + 2) * 2 ^ G ≤ 2 ^ K)
    (hzV : zsz ((vol (rect N0 N1 N2 N3 (f * K)) * (R * (2 * (w + 1))) : ℕ) : ℤ) ≤
      Z + zsz ((w : ℤ) + 1)) :
    cL13 Ksw τ N0 N1 N2 N3 K f ρ G R w px py ≤ (10 ^ 31 + 100 * Ksw) * ((G : ℝ) + 2) *
      ((vol (rect N0 N1 N2 N3 (f * K)) : ℝ) *
        ((R : ℝ) * (w + 1) * ((f : ℝ) + 1) ^ τ + (KFR.PsiR R Z w : ℝ)))

Context. Round six, compact controls (I2C): the cost of the compact Lemma 13 code

Polynomial bounds of the cost units (cR_le, cXorU_le', cCo_le) and cL13_le: the cost of l13C is at most (10^31 + 100 Ksw) (G + 2) · n (r (H+1) (F+1)^τ + PsiR r Z H) under the round-six guards 4 Z (Z+2) ≤ 2^G, 16 Z (Z+2) 2^G ≤ 2^K (no factor K).

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