Slot swap `i` on the geometry (round six, `swE_geo`)
ProvedIntMul.Kappa.R6.IL2.swE_geoSlot swap i on the geometry with expression parameters.
The following holds (Lean statement, in the scope of module Solutions.R6IL2Sw):
theorem IntMul.Kappa.R6.IL2.swE_geo (hτ : 0 ≤ τ) (hL : L12Canon tab l12 τ) :
∃ K : ℝ, 0 ≤ K ∧
∀ (i : Fin 3) (g : Geo), g.Pos → ∀ u : ℕ, 1 ≤ u → g.Q = 2 ^ u →
∀ (I : List Sym) (t : IState HS) (zs : List ℤ) (R : List Item),
KFL.Bits zs → t.G 0 = ints zs ++ R → zs.length = g.V →
∀ (eP eG eS eU : Ex HS) (Bb : ℕ), Bb ≤ zsz (g.V : ℤ) + 3 →
eP.size + eG.size + eS.size + eU.size ≤ 50 →
NoK eP → NoK eG → NoK eS → NoK eU →
ESp eP t Bb (svP g i : ℤ) → ESp eG t Bb (svG g i : ℤ) → ESp eS t Bb (svS g i : ℤ) →
ESp eU t Bb (u : ℤ) →
∃ c : ℕ, IRuns I tab (swE l12 eP eG eS eU) t
(t.upd 0 (ints (rixT g (swT i) zs) ++ R)) c ∧
(c : ℝ) ≤ K * ((g.V : ℝ) + 1) * (u : ℝ) ^ τ
Context. Round six, item language (I2): the register-driven Lemma 13 core over any Lemma 12 table
Parametric copy of KFX.swE/swE_spec/swE_geo (KFX1Sw), KFL.coreCost/coreCost_le
(KFLMain) and the tail of KFX4Core (optA … l13U_body) with the OpenAI Lemma 12
(KFL.l12prog, KFL.l12C q, τ = 1 - 2^-50) replaced by any table tab, code l12 and
exponent τ satisfying IL.L12Canon tab l12 τ (0 ≤ τ ≤ 1).
l13U_body: L12Canon tab l12 τ → ∃ Kc > 0, (Lemma 13 for the code l13U l12).
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*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.
import Definitions.Def_IntMul_Kappa_R6_Defs13
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL2
open IntMul NLogN NLogN.RS NLogN.KIL NLogN.KFD NLogN.KFE NLogN.KFB NLogN.KFL NLogN.KFW NLogN.KFH NLogN.KFX AModel AModelL12 NetProp7 Butterfly IntMul.Kappa.R6.IL
variable {tab : Fin 1 → IStmt HS 1} {l12 : IStmt HS 1} {τ : ℝ}
theorem IntMul.Kappa.R6.IL2.swE_geo (hτ : 0 ≤ τ) (hL : L12Canon tab l12 τ) :
∃ K : ℝ, 0 ≤ K ∧
∀ (i : Fin 3) (g : Geo), g.Pos → ∀ u : ℕ, 1 ≤ u → g.Q = 2 ^ u →
∀ (I : List Sym) (t : IState HS) (zs : List ℤ) (R : List Item),
KFL.Bits zs → t.G 0 = ints zs ++ R → zs.length = g.V →
∀ (eP eG eS eU : Ex HS) (Bb : ℕ), Bb ≤ zsz (g.V : ℤ) + 3 →
eP.size + eG.size + eS.size + eU.size ≤ 50 →
NoK eP → NoK eG → NoK eS → NoK eU →
ESp eP t Bb (svP g i : ℤ) → ESp eG t Bb (svG g i : ℤ) → ESp eS t Bb (svS g i : ℤ) →
ESp eU t Bb (u : ℤ) →
∃ c : ℕ, IRuns I tab (swE l12 eP eG eS eU) t
(t.upd 0 (ints (rixT g (swT i) zs) ++ R)) c ∧
(c : ℝ) ≤ K * ((g.V : ℝ) + 1) * (u : ℝ) ^ τ := by sorry