Adjacency images have even binary self-pairing
ProvedConway99Formal.BinaryCode.image_evenV is the finite vertex set, G is its graph, and adjacency G is its matrix over ZMod 2; x, y, and u are binary words indexed by V. weight is Hamming weight. Rooted matrices are the source-defined blocks at the chosen root. The exact type records which results assume SRG parameters (99,14,1,2) and which are general binary linear algebra.
Variable guide: V is the finite vertex set, G is its graph, and adjacency G is its matrix over ZMod 2; x, y, and u are binary words indexed by V. weight is Hamming weight. Rooted matrices are the source-defined blocks at the chosen root. The exact type records which results assume SRG parameters (99,14,1,2) and which are general binary linear algebra.
The source declaration has the exact hypotheses and variable types preserved in variables_and_premises. Under those assumptions, it concludes:
This is a binary-code or rooted-matrix consequence under exactly the assumptions in the source declaration. SRG parameters are retained where stated; the result is conditional and does not assert graph existence.
import Definitions.Def_QaAlgebra_BinaryCode
import Mathlib
namespace Conway99Formal.BinaryCode
end Conway99Formal.BinaryCode
set_option autoImplicit false
/-!
Binary adjacency-code identities for an actual SRG(99,14,1,2).
Sources: Conway99/Conway99/Claims/C01srgcorealgebra.lean §4;
Conway99/Conway99/Claims/C04finitefieldranks.lean §1;
Conway99/results/R003_enriched_binary_code_odd_cross_rank.md §1;
Conway99/results/R017_binary_genus2_smith_weight60.md §1.
-/
open Conway99Formal.BinaryCode
open Matrix SimpleGraph Finset
variable {V : Type*} [Fintype V] [DecidableEq V]
variable (G : SimpleGraph V) [DecidableRel G.Adj]
theorem Conway99Formal.BinaryCode.image_even (h : G.IsSRGWith 99 14 1 2) (x : V → ZMod 2) :
(adjacency G).mulVec x ⬝ᵥ (adjacency G).mulVec x = 0 := by sorry