Exhaustive normalized-incidence classification #
The 35 possible first rows reduce to seven symmetry orbits. A kernel-audited finite search excludes every completion of those canonical rows using checked geometric obstruction witnesses.
theorem
Erdos97Octagon.normalized_convex_realisation_impossible
{p : Vertex → Plane}
{Q : OctagonIncidence}
(hC : ConvexIndependent ℝ p)
(hR : Realises p Q)
(hN : Q.Normalized)
:
No normalized octagon incidence table has a convex planar realisation.
theorem
Erdos97Octagon.erdos97_convex_octagon
{p : Vertex → Plane}
(hC : ConvexIndependent ℝ p)
:
∃ (vertex : Vertex), ¬HasFourEquidistant p vertex
A convex-independent labelled octagon has a vertex that does not have four other labelled vertices at one common distance.