Exhaustive coverage contradiction #
The compact kernel-checked coverage certificate excludes all seven canonical first rows.
theorem
Erdos97Octagon.RawIncidence.canonicalBranch_impossible
{p : Vertex → Plane}
{Q : OctagonIncidence}
(hC : ConvexIndependent ℝ p)
(hR : Realises p Q)
(hN : Q.Normalized)
(hSparse : Q.PairSparse)
(hBalanced : Q.Balanced)
(rowOneIndex : Fin 7)
(hrowOne : Q.targets 1 = packedRow (canonicalRowMask rowOneIndex))
:
Every normalized counterexample with a canonical first row contradicts the exhaustive coverage certificate.