Round-six lemma `swIUP_spec`
ProvedIntMul.Kappa.R6.IL.swIUP_specAn 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.R6ILSwapU):
theorem IntMul.Kappa.R6.IL.swIUP_spec (hτ : 0 ≤ τ) (h : L12Canon tab l12 τ) :
∃ K : ℝ, 0 ≤ K ∧
∀ (u : ℕ) (Pre G Suf : Shape), 1 ≤ u →
(∀ a ∈ Pre, 1 ≤ a) → (∀ a ∈ G, 1 ≤ a) → (∀ a ∈ Suf, 1 ≤ a) →
∀ (I : List Sym) (t : IState HS) (xs : List (ZMod 2)) (R : List Item),
t.G 0 = ints (enc2 xs) ++ R →
xs.length = vol (binShape Pre G Suf (2 ^ u)) →
∀ {L1 L2 L3 L4 : List Item}, t.G sP = .int (vol Pre : ℤ) :: L1 →
t.G sG = .int (vol G : ℤ) :: L2 → t.G sS = .int (vol Suf : ℤ) :: L3 →
t.G sU = .int (u : ℤ) :: L4 →
∃ c : ℕ, IRuns I tab (swIUP l12) t
(t.upd 0 (ints (pull (binShape Pre G Suf (2 ^ u)) (binShape Pre G Suf (2 ^ u))
(swapPos Pre.length (Pre.length + 1 + G.length)) 0 (enc2 xs)) ++ R)) c ∧
(c : ℝ) ≤ K * ((vol (binShape Pre G Suf (2 ^ u)) : ℝ) + 1) * (u : ℝ) ^ τ
Context. Round six, item language: SwapNeedτ from fine Lemma 12 (parametric copy of KFW's chain)
KFW.swIU_spec, KFW.swWU_spec, KFW.swGU_spec and KFW.swapNeed with the OpenAI Lemma 12
(KFB.lemma12_fine_canon, table KFL.l12prog, code KFL.l12C q, τS) replaced by any
L12Canon tab l12 τ. The register programs (toBitsU, fromBitsU, descP, popP) are the
frozen ones.
swapNeedτ_of_l12Canon : L12Canon tab l12 τ → SwapNeedτ tab τ (0 ≤ τ).
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.IL
open IntMul NLogN NLogN.RS NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFS NLogN.KFL NLogN.KFW AModel AModelL12
variable {tab : Fin 1 → IStmt HS 1} {l12 : IStmt HS 1} {τ : ℝ}
theorem IntMul.Kappa.R6.IL.swIUP_spec (hτ : 0 ≤ τ) (h : L12Canon tab l12 τ) :
∃ K : ℝ, 0 ≤ K ∧
∀ (u : ℕ) (Pre G Suf : Shape), 1 ≤ u →
(∀ a ∈ Pre, 1 ≤ a) → (∀ a ∈ G, 1 ≤ a) → (∀ a ∈ Suf, 1 ≤ a) →
∀ (I : List Sym) (t : IState HS) (xs : List (ZMod 2)) (R : List Item),
t.G 0 = ints (enc2 xs) ++ R →
xs.length = vol (binShape Pre G Suf (2 ^ u)) →
∀ {L1 L2 L3 L4 : List Item}, t.G sP = .int (vol Pre : ℤ) :: L1 →
t.G sG = .int (vol G : ℤ) :: L2 → t.G sS = .int (vol Suf : ℤ) :: L3 →
t.G sU = .int (u : ℤ) :: L4 →
∃ c : ℕ, IRuns I tab (swIUP l12) t
(t.upd 0 (ints (pull (binShape Pre G Suf (2 ^ u)) (binShape Pre G Suf (2 ^ u))
(swapPos Pre.length (Pre.length + 1 + G.length)) 0 (enc2 xs)) ++ R)) c ∧
(c : ℝ) ≤ K * ((vol (binShape Pre G Suf (2 ^ u)) : ℝ) + 1) * (u : ℝ) ^ τ := by sorry