Round-six lemma `chunkArith`
ProvedNLogN.KFV.chunkArithAn 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.KFV22Chunk):
theorem NLogN.KFV.chunkArith {h Lst n : ℕ} (hK : 0 < K) (hD : 1 ≤ D) (hb : bb ℓ K ≤ h) (hh : h < ℓ - 1)
(hn : n = Lst + D * qq ℓ K * K) :
1 ≤ qq ℓ K ∧ qq ℓ K * K ≤ n ∧ qq ℓ K ≤ n ∧ K ≤ n ∧ D ≤ n ∧ bb ℓ K ≤ ℓ ∧ Lst ≤ n ∧
eIdx ℓ K h + 1 + (h - bb ℓ K) = qq ℓ K * K ∧ eIdx ℓ K h ≤ n ∧
eIdx ℓ K h / K < qq ℓ K ∧ eIdx ℓ K h / K ≤ n ∧ eIdx ℓ K h / K * D ≤ n ∧
eIdx ℓ K h / K * D * K ≤ n ∧ Lst + eIdx ℓ K h / K * D * K + 1 ≤ n ∧
(qq ℓ K - 1 - eIdx ℓ K h / K) * D ≤ n ∧ (qq ℓ K - 1 - eIdx ℓ K h / K) * D * K + 1 ≤ n
Context. KFV §26: the chunk rounds through the uniform Proposition 14
A chunk round b ≤ h < ℓ - 1 pushes the descriptor
desc14 (2^A) K D (2^B) ρ r p W Z on stack 36 (A = |Lst| + j₀ D K, B = (q - 1 - j₀) D K,
j₀ = (qK - 1 - (h - b)) / K, ρ = (h - b) mod K, r = 2^ℓ; p, W, Z from the registers
gPp, gWw, gZz of the base), calls the Proposition 14 entry e14, and pops the descriptor.
layerU_chunk: given P14Need for e14 (the uniform Proposition 14 of KFW), this is the
computed layer of round h.
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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_HvdH_Numeric
import Definitions.Def_IntMul_HvdH_ExpApprox
import Definitions.Def_IntMul_HvdH_RealExp
import Definitions.Def_IntMul_HvdH_Twiddle
import Definitions.Def_IntMul_HvdH_MachineRef
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open NLogN NLogN.KFV
open IntMul NLogN.RS NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFH AModel Butterfly
variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}
open Synth GlueLayout GlueP14 GlueError
variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)
theorem NLogN.KFV.chunkArith {h Lst n : ℕ} (hK : 0 < K) (hD : 1 ≤ D) (hb : bb ℓ K ≤ h) (hh : h < ℓ - 1)
(hn : n = Lst + D * qq ℓ K * K) :
1 ≤ qq ℓ K ∧ qq ℓ K * K ≤ n ∧ qq ℓ K ≤ n ∧ K ≤ n ∧ D ≤ n ∧ bb ℓ K ≤ ℓ ∧ Lst ≤ n ∧
eIdx ℓ K h + 1 + (h - bb ℓ K) = qq ℓ K * K ∧ eIdx ℓ K h ≤ n ∧
eIdx ℓ K h / K < qq ℓ K ∧ eIdx ℓ K h / K ≤ n ∧ eIdx ℓ K h / K * D ≤ n ∧
eIdx ℓ K h / K * D * K ≤ n ∧ Lst + eIdx ℓ K h / K * D * K + 1 ≤ n ∧
(qq ℓ K - 1 - eIdx ℓ K h / K) * D ≤ n ∧ (qq ℓ K - 1 - eIdx ℓ K h / K) * D * K + 1 ≤ n := by sorry