The item-language Prop. 11 program for a round-six bit network (round six, `ilProp11_of_net`)
ProvedIntMul.Kappa.R6.IL.ilProp11_of_netThe item-language Prop. 11 program for a round-six bit network.
The following holds (Lean statement, in the scope of module Solutions.R6ILProp):
theorem IntMul.Kappa.R6.IL.ilProp11_of_net (C : Bit.QHNet (ZMod 2) W T m) (hC : NetIL C) :
∃ q₀ : ℕ, ∀ q, q.Prime → q₀ < q → ∃ (tab : Fin 1 → IStmt HS 1) (T₀ c₁ : ℕ) (K₁ K₂ : ℝ),
0 ≤ K₁ ∧ 0 ≤ K₂ ∧ ILProp11 tab C q T₀ c₁ K₁ K₂
Context. Round six, item language: the item-language Prop. 11 for a round-six bit network
ilProp11_of_net: the table tabG C q (adS m) (generic procedure genP C q, adapter adS m
from the KIL5 descriptor) satisfies ILProp11 with T₀ = m + q + T + W + 16,
K₁ = 2 cq q + Kv C, K₂ = KA C q + KAd m and c₁ = 1 + (S + 1) c (S runs, c the
depH slope of depH_pow_le).
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.KFE AModel AModelL12 Finset
variable {W T m : ℕ} [NeZero W]
theorem IntMul.Kappa.R6.IL.ilProp11_of_net (C : Bit.QHNet (ZMod 2) W T m) (hC : NetIL C) :
∃ q₀ : ℕ, ∀ q, q.Prime → q₀ < q → ∃ (tab : Fin 1 → IStmt HS 1) (T₀ c₁ : ℕ) (K₁ K₂ : ℝ),
0 ≤ K₁ ∧ 0 ≤ K₂ ∧ ILProp11 tab C q T₀ c₁ K₁ K₂ := by sorry