Round-six lemma `nondeg_of_dual`

Proved

R6Chk.nondeg_of_dual

by xuanji · Oct 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplicationkappa-improvement

An 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.R6ChkF2):

theorem R6Chk.nondeg_of_dual {k : ℕ} {b d : Fin k → (Fin n → ZMod 2)} (hd : ∀ j, d j ∈ spanF b)
    (hdb : ∀ j i, d j ⬝ᵥ b i = if i = j then 1 else 0) : NondegF (spanF b)

Context. F₂ linear algebra from packed certificates

Semantics: vr n X i : Fin n → ZMod 2 is row i of the packed number X (bit t of the 32-bit field i). Certificates are lists of rows; all checks are dotsP products compared with target patterns (R6ChkPack).

dot_of_dotsP: a dotsP equation gives every inner product vr A j ⬝ᵥ vr B i.
indep_of_dual: rows with a dual family (e_j ⬝ v_i = δ) are independent.
mem_iff_of_cert (label certificate): B (k rows), H (n-k rows) with H Bᵀ = 0, H Eᵀ = I, D Hᵀ = 0, D Bᵀ = I ⟹ span B = ker H, dim = k, nondegenerate.
pair_of_cert (edge certificate): U ⊆ V, a dual of U, and an orthonormal basis R of the residual (R ⊥ U, R ⊆ V, |R| = dim V − |U|) ⟹ span U nondegenerate of dim |U|, and U = V or a norm-one w ∈ V orthogonal to U exists.

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*).

Preamble

-- 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
variable {n : ℕ}

Formal statement

theorem R6Chk.nondeg_of_dual {k : ℕ} {b d : Fin k → (Fin n → ZMod 2)} (hd : ∀ j, d j ∈ spanF b)
    (hdb : ∀ j i, d j ⬝ᵥ b i = if i = j then 1 else 0) : NondegF (spanF b) := by sorry

Source

S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean declaration `R6Chk.nondeg_of_dual`, Solutions/R6ChkF2.lean (lines 132–141) of the round-six development.

View graph