`SwapNeedτ` from fine Lemma 12 (round six, `swapNeedtau_of_l12Canon`)
ProvedIntMul.Kappa.R6.IL.swapNeedtau_of_l12CanonSwapNeedτ from fine Lemma 12: the table kTableP tab with the one extra procedure
(swGUP l12).ren id (gL 1) (entry 7) and the descriptor on dS.
The following holds (Lean statement, in the scope of module Solutions.R6ILSwapU):
theorem IntMul.Kappa.R6.IL.swapNeedtau_of_l12Canon (hτ : 0 ≤ τ) (h : L12Canon tab l12 τ) : SwapNeedτ tab τ
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.swapNeedtau_of_l12Canon (hτ : 0 ≤ τ) (h : L12Canon tab l12 τ) : SwapNeedτ tab τ := by sorry