Erdős 97 convex-octagon formalization: Residual Obstructions

theorem Erdos97Octagon.residualRepresentative_not_convex_realises (classIndex : Fin 13) {p : Vertex → Plane} (hC : ConvexIndependent ℝ p) : ¬Realises p (residualRepresentative classIndex)

None of the thirteen explicit candidate systems has a convex-independent realisation. This statement does not assert that the family is exhaustive.