Binary cut-response rank on seven vertices
ProvedConway99Formal.FiniteFields.cut_response_rankfinite-fieldsgraph-theorylinear-algebra
For any simple graph on seven labeled vertices, including isolated vertices, the binary vertex-edge incidence matrix has rank equal to seven minus the number of connected components. This is an independent cut-response identity; it does not assume a Conway graph or prove one exists.
Preamble
import Mathlib set_option autoImplicit false open Matrix SimpleGraph
Formal statement
theorem Conway99Formal.FiniteFields.cut_response_rank (H : SimpleGraph (Fin 7)) [DecidableRel H.Adj] : (H.incMatrix (ZMod 2)).rank + Nat.card H.ConnectedComponent = 7 := by sorry
Source
C04finitefieldranks.lean:777 (SHA-256 dd4045131b6d6eeddb8be571417bf9208ddaac2bc8d6a4019c50313d381c884b); self-contained proof SHA-256 091911ccbbb7a34b048c7c71f5a9e4d8fbe5d9f0c54d6d4bc9f314d4b82ca73b. Exact rank equation only; other cut-space subclaims remain open.
Human review
Confirmed by the mission captain (proposal self-audit).