theorem Q2Presentation.Quadratic.nonsingular_even_finrank {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] [Finite V] (q : QuadF2 V) (hns : q.Nonsingular) : Even (Module.finrank (ZMod 2) V)

A nonsingular 𝔽₂ quadratic space has even dimension (F-E1). Dickson.gaussSum_sq gives D² = |V| = 2^d; then |D| is a power of two (Nat.dvd_prime_pow) whose square has exponent d, so d = k·2 (Nat.pow_right_injective). Mirrors the banked dickson_arith arithmetic verbatim.