Edge certificate (round six, `pair_of_cert`)

Edge certificate. SV is a nondegenerate subspace of dimension kU + kR containing U and R; U has a dual family; R is orthonormal and orthogonal to U.

The following holds (Lean statement, in the scope of module Solutions.R6ChkF2):

theorem R6Chk.pair_of_cert {kU kR : ℕ} {SV : Submodule (ZMod 2) (Fin n → ZMod 2)} {u eu : Fin kU → (Fin n → ZMod 2)} {r : Fin kR → (Fin n → ZMod 2)}
    (hV : NondegF SV) (hVd : finrank (ZMod 2) SV = kU + kR)
    (huV : ∀ i, u i ∈ SV) (hrV : ∀ i, r i ∈ SV)
    (hUE : ∀ j i, u j ⬝ᵥ eu i = if i = j then 1 else 0)
    (hRU : ∀ j i, r j ⬝ᵥ u i = 0) (hRR : ∀ j i, r j ⬝ᵥ r i = if i = j then 1 else 0) :
    spanF u ≤ SV ∧ finrank (ZMod 2) (spanF u) = kU ∧ NondegF (spanF u) ∧
      (spanF u = SV ∨ ∃ w ∈ SV, w ⬝ᵥ w = 1 ∧ ∀ z ∈ spanF u, z ⬝ᵥ w = 0)

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