`AKCond` of one `A` axis (round six, `akCond_at`)

AKCond of one A axis.

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

theorem J6Seg.AC.akCond_at (P : Prm) {n : ℕ} {src : ℕ → ℕ} {D k : ℕ} (h : AxANum P n src D k)
    (hp64 : 64 ≤ pP6 P n) :
    let p := pP6 P n; let s := src k; let t := tF6 P n k; let α := αN6 P n; let H := HA6 P n
    let pk := pkA6 8 16 p; let b := bA6 17 40 p; let w := p + 2
    let f := Nat.log 2 (IntMul.HvdH.sWidth p α) + 3
    let pre := preT P n D k; let post := postT P n D k
    let WA := J6A.WA p α H
    AKCond p s t α H pk b w f pre post (mulSup (2 * (20 * p + 60)))
      (mulSup (2 * (b * (2 * (2 * WA + 2 * H)) + 2))) (20 * p + 60) (b + 2) (b + 2)
      (17 + 2 * WA + (2 * WA + 2 * H) + 2 * H) (aK0 p) (aK0 p) (aK0 p) (2 ^ (p + 2))

Context. A-axis costs 4: the numeric side conditions AKCond of the A kernel v2

For p ≥ 64 (eventually true) and an A axis with the facts AxANum, akCond_at gives AKCond at

• B = 20p + 60, BH = Bk = b + 2, Lmax = 17 + 2W + (2W + 2H) + 2H (the row length),
• φ₁ = mulSup (2B), φ₂ = mulSup (2 (b · 2n + 2)) with n = 2W + 2H,
• Ka = Kr = Kc = (8p + 35) 2^{2p} (J6AILTab12), X₀ = 2^{p+2}.

The exponential facts come from 2^16 p^4 ≤ 2^p (pow4_big, p ≥ 64).

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