Round-six lemma `jsize_ax`

An 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.J6SegJCost5):

theorem J6Seg.Side.jsize_ax (hc : Val.ValCond6 ap) :
    let wd := axwd6 P n src k ap; let kJ := axkJ6 P n src k ap
    let pre := axpre6 P n D k; let post := axpost6 P n D k; let fJ := axfJ6 P n src k
    let NJ := 2 * (pre * 1 * post * 2 ^ fJ)
    let TJ := tabsT (fun _ => axTJ6 P n src k ap) 1
    let BkJ := BkJ6 P n src k ap; let Lj := (axTJ6 P n src k ap).length
    1 ≤ BkJ ∧ wd ≤ BkJ ∧ zsz (wd : ℤ) ≤ BkJ ∧ zsz (fJ : ℤ) ≤ BkJ ∧
    zsz ((pre * 1 : ℕ) : ℤ) ≤ BkJ ∧ zsz (post : ℤ) ≤ BkJ ∧ zsz (pre : ℤ) ≤ BkJ ∧
    zsz ((1 : ℕ) : ℤ) ≤ BkJ ∧ zsz ((2 * 2 ^ fJ : ℕ) : ℤ) ≤ BkJ ∧ zsz (NJ : ℤ) ≤ BkJ ∧
    zsz (TJ.length : ℤ) ≤ BkJ ∧ zsz (Lj : ℤ) ≤ BkJ ∧
    Bnd BkJ (axTJ6 P n src k ap)

Context. J cost 5: the size facts of the J pass at BkJ = wd + kJ + Bc + p + 10

• bc_ax: Bc ≤ Q + bcC and Bc ≤ 2ℓ + 6 + bcC (Bc = axBc6);
• partD_ax: PartD of the line streams at Xb = Xb0 Q w 0, Bc = axBc6, k = kJ (plan);
• jsize_ax: the kerW size facts and the table bound of the J pass.

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