Round-six lemma `allL_spec`
ProvedR6Chk.allL_specAn 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.R6ChkCx):
theorem R6Chk.allL_spec {α : Type} {p : α → Bool} : ∀ {l : List α}, allL p l = true → ∀ a ∈ l, p a = true
Context. Reflective checker for nested nondegenerate F₂ label pairs (complex round six)
Data: a list of groups. A group is one natural number read as 32-bit fields (LSB first):
kV, cnt, B (kV rows), H (n-kV), D (kV), E (n-kV), then cnt entries kU, U (kU), EU (kU), R (kV-kU). Rows are vectors of F₂^n (n ≤ 24).
grpChk n bad G : Bool— two packed products for the labelV = span B(H·[B;E]ᵀ = [0 | I],D·[H;B]ᵀ = [0 | I]) and two per entry (U·[H;EU]ᵀ = [0 | I],R·[H;U;R]ᵀ = [0 | 0 | I]), plus row range checks.grpChk_sound: ifgrpChk n (BADf n) G = truethenVis nondegenerate of dimensionkV, and for every entry(U, kU),PairOK n U kU V kV:span U ≤ span V,dim span U = kU,span Unondegenerate, andspan U = span Vor somew ∈ span Vhasw·w = 1,w ⊥ U(i.e.NetComplexP8.Up (span U) (span V)withFd = kV - kU; seeR6ChkCxBridge).
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_Defs9 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open R6Chk open Matrix Matrix.Module Module
theorem R6Chk.allL_spec {α : Type} {p : α → Bool} : ∀ {l : List α}, allL p l = true → ∀ a ∈ l, p a = true := by sorry