Round-six lemma `swGUP_spec`
ProvedIntMul.Kappa.R6.IL.swGUP_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.swGUP_spec (hτ : 0 ≤ τ) (h : L12Canon tab l12 τ) :
∃ K : ℝ, 0 ≤ K ∧
∀ (u w : ℕ) (sh : Shape) (p q : ℕ), 1 ≤ u → (∀ a ∈ sh, 1 ≤ a) → p < q → q < sh.length →
sh.getD p 0 = 2 ^ u → sh.getD q 0 = 2 ^ u →
∀ (I : List Sym) (s : IState HS) (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ),
(∀ j, j ≠ 0 → j ≠ dS → f j = []) → f dS = KFM.descSw w u p q sh →
f 0 = gflat zs ++ l → zs.length = vol sh → GB w zs →
∃ c : ℕ, IRuns I tab (swGUP l12) (encK s f)
(encK s (Function.update f 0 (gflat (pull sh sh (swapPos p q) 0 zs) ++ l))) c ∧
(c : ℝ) ≤ K * (((w : ℝ) + 1) * ((vol sh : ℝ) + 1) * (u : ℝ) ^ τ +
(((sh.length + 1) * (Nat.size (vol sh) + w + u + 1) ^ 2 : ℕ) : ℝ))
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.swGUP_spec (hτ : 0 ≤ τ) (h : L12Canon tab l12 τ) :
∃ K : ℝ, 0 ≤ K ∧
∀ (u w : ℕ) (sh : Shape) (p q : ℕ), 1 ≤ u → (∀ a ∈ sh, 1 ≤ a) → p < q → q < sh.length →
sh.getD p 0 = 2 ^ u → sh.getD q 0 = 2 ^ u →
∀ (I : List Sym) (s : IState HS) (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ),
(∀ j, j ≠ 0 → j ≠ dS → f j = []) → f dS = KFM.descSw w u p q sh →
f 0 = gflat zs ++ l → zs.length = vol sh → GB w zs →
∃ c : ℕ, IRuns I tab (swGUP l12) (encK s f)
(encK s (Function.update f 0 (gflat (pull sh sh (swapPos p q) 0 zs) ++ l))) c ∧
(c : ℝ) ≤ K * (((w : ℝ) + 1) * ((vol sh : ℝ) + 1) * (u : ℝ) ^ τ +
(((sh.length + 1) * (Nat.size (vol sh) + w + u + 1) ^ 2 : ℕ) : ℝ)) := by sorry