Quadratic forms over 𝔽₂ on bit strings

Reading the bits of x : ι → Bool as a vector v over 𝔽₂ = ZMod 2 (BitString.bitVal), a square matrix Q over 𝔽₂ defines the Boolean function x ↦ v ⬝ᵥ Q *ᵥ v (BitString.quadForm), the quadratic form of Q as in Matrix.toQuadraticForm'. Every quadratic form over 𝔽₂ in the variables x arises so. The inner product function x ↦ ∑ᵢ xᵢ yᵢ is the quadratic form of the matrix with the identity in the block of rows x and columns y; more generally, a matrix carrying R on a block of rows x and columns y and vanishing elsewhere has the bilinear form xᵀ R y as its quadratic form (BitString.quadForm_eq_of_submatrix).

Main definitions

• Cslib.BitString.quadForm Q: the quadratic form of Q over 𝔽₂, as a Boolean function.

Main results

• Cslib.BitString.neg_one_pow_val_eq: the sign (-1) ^ (v ⬝ᵥ Q *ᵥ v) of a quadratic form.
• Cslib.BitString.quadForm_eq_of_submatrix: bilinear forms are quadratic forms.

theorem Cslib.BitString.bitVal_zmod_two_injective : Function.Injective (bitVal (ZMod 2))

Reading bits in 𝔽₂ is injective.

theorem Cslib.BitString.bitVal_zmod_two_surjective : Function.Surjective (bitVal (ZMod 2))

Every element of 𝔽₂ is a bit.

def Cslib.BitString.quadForm {ι : Type u_1} [Fintype ι] (Q : Matrix ι ι (ZMod 2)) (x : ι → Bool) : Bool

The quadratic form of a square matrix Q over 𝔽₂ as a Boolean function: reading the bits of x as a vector v over 𝔽₂, it is true when v ⬝ᵥ Q *ᵥ v = 1.

theorem Cslib.BitString.quadForm_eq_true_iff {ι : Type u_1} [Fintype ι] (Q : Matrix ι ι (ZMod 2)) (x : ι → Bool) : quadForm Q x = true ↔ ((fun (i : ι) => bitVal (ZMod 2) (x i)) ⬝ᵥ Q.mulVec fun (i : ι) => bitVal (ZMod 2) (x i)) = 1

The quadratic form of Q is true at x exactly when v ⬝ᵥ Q *ᵥ v = 1 for the vector v over 𝔽₂ of the bits of x.

theorem Cslib.BitString.neg_one_pow_val_eq {ι : Type u_1} [Fintype ι] {R : Type u_2} [Ring R] (Q : Matrix ι ι (ZMod 2)) (x : ι → Bool) : (-1) ^ ((fun (i : ι) => bitVal (ZMod 2) (x i)) ⬝ᵥ Q.mulVec fun (i : ι) => bitVal (ZMod 2) (x i)).val = if quadForm Q x = true then -1 else 1

The sign of a quadratic form: (-1) ^ (v ⬝ᵥ Q *ᵥ v) is -1 where the form is true and 1 where it is false.

theorem Cslib.BitString.quadForm_eq_of_submatrix {ι : Type u_1} [Fintype ι] {κ : Type u_2} {κ' : Type u_3} [Fintype κ] [Fintype κ'] {R : Matrix κ κ' (ZMod 2)} {M : Matrix ι ι (ZMod 2)} {f : κ → ι} {g : κ' → ι} (hf : Function.Injective f) (hg : Function.Injective g) (hMR : M.submatrix f g = R) (hM : ∀ (i j : ι), i ∉ Set.range f ∨ j ∉ Set.range g → M i j = 0) (x : ι → Bool) : quadForm M x = decide (((fun (a : κ) => bitVal (ZMod 2) (x (f a))) ⬝ᵥ R.mulVec fun (b : κ') => bitVal (ZMod 2) (x (g b))) = 1)

Bilinear forms are quadratic forms. If M carries R on the rows f and the columns g, both injective, and vanishes elsewhere, its quadratic form is the bilinear form (x ∘ f)ᵀ R (x ∘ g).