Label certificate (round six, `label_of_cert`)

Label certificate.

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

theorem R6Chk.label_of_cert {k m : ℕ} {b d : Fin k → (Fin n → ZMod 2)} {h e : Fin m → (Fin n → ZMod 2)} (hmk : m + k = n)
    (hHB : ∀ i j, h i ⬝ᵥ b j = 0) (hHE : ∀ i j, h i ⬝ᵥ e j = if i = j then 1 else 0)
    (hDH : ∀ j i, d j ⬝ᵥ h i = 0) (hDB : ∀ j i, d j ⬝ᵥ b i = if i = j then 1 else 0) :
    (∀ x, x ∈ spanF b ↔ ∀ i, h i ⬝ᵥ x = 0) ∧ finrank (ZMod 2) (spanF b) = k ∧
      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*).