The entry bounds from one volume bound (`entB_of`)
ProvedIntMul.Kappa.R6.IL.entB_ofThe entry bounds from one volume bound.
The following holds (Lean statement, in the scope of module Solutions.R6ILGen):
theorem IntMul.Kappa.R6.IL.entB_of {q e P L M : ℕ} {A B Cs : Shape} (hm : 2 ≤ m) (hq : 2 ≤ q)
(hP : 1 ≤ P) (hL : 1 ≤ L) (hA : ∀ x ∈ A, 1 ≤ x) (hB : ∀ x ∈ B, 1 ≤ x) (hC : ∀ x ∈ Cs, 1 ≤ x)
(hKM : (m + q + T + W + 16) * (vol (P :: L :: hdShape A B Cs e q) + 1) ≤ M) :
EntB m q W T e P L (vol A) (vol B) (vol Cs) M ∧ (q ^ (e / m) + 1) ^ 3 ≤ M ∧
vol (P :: L :: hdShape A B Cs e q) ≤ M
Context. Round six, item language: the general procedure and its correctness
genP C q (entry genE, level branch genL C, tail genTail q) is run by tabG C q ad 0 when
the descriptor register dJ holds -1 (generic mode, descriptor DescG). gen_correct: by strong
induction on the width e, tabG C q ad 0 computes progH C q e at cost costN C q Bb e V.
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.entB_of {q e P L M : ℕ} {A B Cs : Shape} (hm : 2 ≤ m) (hq : 2 ≤ q)
(hP : 1 ≤ P) (hL : 1 ≤ L) (hA : ∀ x ∈ A, 1 ≤ x) (hB : ∀ x ∈ B, 1 ≤ x) (hC : ∀ x ∈ Cs, 1 ≤ x)
(hKM : (m + q + T + W + 16) * (vol (P :: L :: hdShape A B Cs e q) + 1) ≤ M) :
EntB m q W T e P L (vol A) (vol B) (vol Cs) M ∧ (q ^ (e / m) + 1) ^ 3 ≤ M ∧
vol (P :: L :: hdShape A B Cs e q) ≤ M := by sorry