A chunk round, uniform (round six, `layerU_chunk6`)
ProvedNLogN.KFV.R6P.layerU_chunk6A chunk round, uniform, from the uniform Proposition 14.
The following holds (Lean statement, in the scope of module Solutions.R6P18Chunk):
theorem NLogN.KFV.R6P.layerU_chunk6 (hK : 0 < K) (hℓ : 1 ≤ ℓ) {e14 : Fin Pp} {Ew : ℕ → ℕ} {lamp : ℝ} {K₀ : ℕ}
{C₀ : ℝ} (HP : IntMul.Kappa.R6.IL3.P14NeedH' I iprog e14 dD Ew lamp K₀ C₀) {h p W Z B : ℕ} (hb : bb ℓ K ≤ h) (hh : h < ℓ - 1)
(hW : p + 1 ≤ W) (hB : (tgtL D ℓ K long).length + ℓ + 3 ≤ B) (hpB : p ≤ B) (hWB : W ≤ B)
(hZB : Z ≤ B)
(c1 : 6 ≤ K) (c3 : 80 * Z * (Z + 2) ≤ 2 ^ K)
(c4 : zsz ((32 * (2 ^ nB D ℓ K long * 2 ^ ℓ) : ℕ) : ℤ) ≤ Z)
(cp : zsz (p : ℤ) ≤ Z)
(c6 : Ew D ≤ W + 1) (c7 : W + Ew D + 2 < 2 ^ Z) (c8 : 2 * (2 * Z + 4) ^ 3 + 2 ≤ 2 ^ ℓ)
(c9 : (K * D + 2 ^ nB D ℓ K long + 10) * (Z + 2) ≤ 2 ^ nB D ℓ K long * 2 ^ ℓ)
(n1 : zsz ((2 ^ nB D ℓ K long * 2 ^ ℓ + W + Ew D : ℕ) : ℤ) ≤ p) (n2 : (p + K₀) ^ 5 ≤ 2 ^ K)
(n3 : ((K₀ * D * (zsz (p : ℤ) + 1) : ℕ) : ℝ) ≤ K * (D : ℝ) ^ lamp) :
LayerU (r := 2 ^ ℓ) I iprog (fun s => RCtx (pLP D ℓ K long) (flOf D long) h s ∧ XR s p W Z)
(chunkC e14) (layerQc p (paperSel D ℓ K long hK hℓ h)) (2 ^ nB D ℓ K long) p W
(cChunk6 D ℓ K long W B C₀ lamp p)
Context. Round six, Proposition 18: the chunk rounds through P14NeedH'
KFV.layerU_chunk with the uniform Proposition 14 of round six (IL3.P14NeedH': guard Ew,
exponent lamp, per-call factor (zsz p + 1) D^lamp, the three size hypotheses n1 n2 n3, no
bound on K). layerU_chunk6, chunkU_of6; the cost of a chunk round is cChunk6.
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_Defs70
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open NLogN NLogN.KFV NLogN.KFV.R6P
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.R6P.layerU_chunk6 (hK : 0 < K) (hℓ : 1 ≤ ℓ) {e14 : Fin Pp} {Ew : ℕ → ℕ} {lamp : ℝ} {K₀ : ℕ}
{C₀ : ℝ} (HP : IntMul.Kappa.R6.IL3.P14NeedH' I iprog e14 dD Ew lamp K₀ C₀) {h p W Z B : ℕ} (hb : bb ℓ K ≤ h) (hh : h < ℓ - 1)
(hW : p + 1 ≤ W) (hB : (tgtL D ℓ K long).length + ℓ + 3 ≤ B) (hpB : p ≤ B) (hWB : W ≤ B)
(hZB : Z ≤ B)
(c1 : 6 ≤ K) (c3 : 80 * Z * (Z + 2) ≤ 2 ^ K)
(c4 : zsz ((32 * (2 ^ nB D ℓ K long * 2 ^ ℓ) : ℕ) : ℤ) ≤ Z)
(cp : zsz (p : ℤ) ≤ Z)
(c6 : Ew D ≤ W + 1) (c7 : W + Ew D + 2 < 2 ^ Z) (c8 : 2 * (2 * Z + 4) ^ 3 + 2 ≤ 2 ^ ℓ)
(c9 : (K * D + 2 ^ nB D ℓ K long + 10) * (Z + 2) ≤ 2 ^ nB D ℓ K long * 2 ^ ℓ)
(n1 : zsz ((2 ^ nB D ℓ K long * 2 ^ ℓ + W + Ew D : ℕ) : ℤ) ≤ p) (n2 : (p + K₀) ^ 5 ≤ 2 ^ K)
(n3 : ((K₀ * D * (zsz (p : ℤ) + 1) : ℕ) : ℝ) ≤ K * (D : ℝ) ^ lamp) :
LayerU (r := 2 ^ ℓ) I iprog (fun s => RCtx (pLP D ℓ K long) (flOf D long) h s ∧ XR s p W Z)
(chunkC e14) (layerQc p (paperSel D ℓ K long hK hℓ h)) (2 ^ nB D ℓ K long) p W
(cChunk6 D ℓ K long W B C₀ lamp p) := by sorry