A context for a size (round six, `ctx_exists6`)

A context for a size.

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

theorem IntMul.Kappa.R6.ctx_exists6 {E : ℕ} (P : Prm) (ix : Ix6 (7 + E)) (tab : Fin 1 → IStmt HS 1)
    (extM : Fin E → IStmt HS (7 + E))
    (ext₂ : Fin ix.P₂ → IStmt HS (7 + ix.P₂))
    (hp₂ : ∀ j, IL.kTableP tab extM (ix.g₂ j) = (IL.kTableP tab ext₂ j).ren id ix.g₂)
    (ext₃ : Fin ix.P₃ → IStmt HS (7 + ix.P₃))
    (hp₃ : ∀ j, IL.kTableP tab extM (ix.g₃ j) = (IL.kTableP tab ext₃ j).ren id ix.g₃)
    (ext₄ : Fin ix.P₄ → IStmt HS (7 + ix.P₄))
    (hp₄ : ∀ j, IL.kTableP tab extM (ix.g₄ j) = (IL.kTableP tab ext₄ j).ren id ix.g₄)
    (CΦ CL CC : ℝ) (AΦ AL AC n₁Φ n₁L n₁C : ℕ)
    (hdΦ : ix.dSΦ ≠ 0) (hdL : ix.dSL ≠ 0) (hdC : ix.dSC ≠ 0)
    (HΦ : ∀ (Isym : List Sym) (n : ℕ), n₁Φ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src →
      phiG6 Isym (IL.kTableP tab ext₂) ix.eF ix.eI ix.dSΦ CΦ AΦ ⟨P, n, src⟩)
    (HL : ∀ n, n₁L ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 →
      ∀ [∀ i, NeZero (sD6 src D i)] [∀ i, NeZero (tD6 P n D i)],
      ∃ M : AxisMaps6 (αN6 P n) (sD6 src D) (tD6 P n D),
        ∀ Isym, lineG6 Isym (IL.kTableP tab ext₃) ix.eA ix.eB ix.dSL CL AL ⟨P, n, src⟩ D M)
    (HC : ∀ (Q : Q6), Q.P = P → QOk Q → n₁C ≤ Q.n → ∀ (D : ℕ), Q.d = D + 1 →
      ∀ [∀ i, NeZero (Q.tB D i)],
      ∃ (θt θit at' bt : ((i : Fin (D + 1)) → ZMod (Q.tB D i)) → ℂ) (ζ : ℂ),
        ζ ^ Q.tB D (Fin.last D) = -1 ∧
        Phases Q.p (twX (Q.tB D) ζ) θt ∧
        Phases Q.p (fun j => (twX (Q.tB D) ζ j)⁻¹) θit ∧
        Phases Q.p (fun j => (starRingEnd ℂ) (chirp (Q.sB D) (Q.tB D) j)) at' ∧
        Phases Q.p (chirp (Q.sB D) (Q.tB D)) bt ∧
        Grid Q.p bt ∧
        ∀ Isym, chirpG6 Isym (IL.kTableP tab ext₄) ix.eC ix.dSC CC AC Q D θt θit at' bt)
    (n : ℕ) (src : ℕ → ℕ) (hQ : QOk ⟨P, n, src⟩) (h1 : n₁Φ ≤ n) (h2 : n₁L ≤ n) (h3 : n₁C ≤ n)
    (D : ℕ) (hD : dP6 P n = D + 1) :
    ∃ (iS : ∀ i, NeZero (sD6 src D i)) (iT : ∀ i, NeZero (tD6 P n D i)), ∀ Isym,
      ∃ C : BigCtx6 ix Isym tab extM ⟨P, n, src⟩ D, C.CΦ = CΦ ∧ C.AΦ = AΦ ∧
        C.BΦ = dzB (descPhi6 P n src) ∧ C.CL = CL ∧ C.AL = AL ∧ C.BL = dzB (descLine6 P n src) ∧
        C.CC = CC ∧ C.AC = AC ∧ C.BC = dzB (descChirp6 P n src)

Context. Round-six machine: the merged table, the contexts and BigSpec

The frozen KFMBig11 at the round-six parameters.

• ixM6: the index data of the merged table mExt4 ext₁ ext₂ ext₃ ext₄ [bigP6] (setup, Φ, lines, chirp; chirp descriptor stack cS).
• ctx_exists6: from the per-size guarantees of Φ (CrtBody6), the lines (LineBody6) and the chirp (chirp_of_P18), a BigCtx6 exists for every admissible size and every Isym, with the fixed constants and the canonical descriptor bounds dzB.
• bigSpec_of6: contexts and setup runs for all n ≥ N₁ give BigSpec.

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