Erdős 97 convex-octagon formalization: Relabelling

def Erdos97Octagon.standardTargets : Finset Vertex

The canonical first witness row used by the finite classification.

Equations

• Erdos97Octagon.standardTargets = {1, 2, 3, 4}

@[simp]

theorem Erdos97Octagon.card_standardTargets : standardTargets.card = 4

The canonical witness row has four vertices.

@[simp]

theorem Erdos97Octagon.zero_notMem_standardTargets : 0 ∉ standardTargets

The canonical witness row does not contain its centre.

def Erdos97Octagon.OctagonIncidence.relabel (Q : OctagonIncidence) (e : Vertex ≃ Vertex) : OctagonIncidence

Simultaneously relabel the centres and every entry of their witness rows.

Equations

• Q.relabel e = { targets := fun (v : Erdos97Octagon.Vertex) => Finset.map e.toEmbedding (Q.targets (e.symm v)), card_targets := ⋯, centre_not_mem := ⋯ }

def Erdos97Octagon.OctagonIncidence.Normalized (Q : OctagonIncidence) : Prop

A system is normalized when row zero is the canonical four-set.

Equations

• Q.Normalized = (Q.targets 0 = Erdos97Octagon.standardTargets)

theorem Erdos97Octagon.OctagonIncidence.exists_normalized_relabel (Q : OctagonIncidence) : ∃ (e : Vertex ≃ Vertex), (Q.relabel e).Normalized

Every octagon incidence system is isomorphic to one with canonical row zero.

def Erdos97Octagon.relabelPoints (p : Vertex → Plane) (e : Vertex ≃ Vertex) : Vertex → Plane

Relabel a planar configuration contragrediently with its incidence system.

Equations

• Erdos97Octagon.relabelPoints p e = p ∘ ⇑e.symm

theorem Erdos97Octagon.realises_relabel {p : Vertex → Plane} {Q : OctagonIncidence} (hR : Realises p Q) (e : Vertex ≃ Vertex) : Realises (relabelPoints p e) (Q.relabel e)

Equal-distance realisability is invariant under simultaneous relabelling.

theorem Erdos97Octagon.convexIndependent_relabel {p : Vertex → Plane} (hC : ConvexIndependent ℝ p) (e : Vertex ≃ Vertex) : ConvexIndependent ℝ (relabelPoints p e)

Convex independence is invariant under relabelling.

theorem Erdos97Octagon.normalized_reduction_of_all_hasFour {p : Vertex → Plane} (hC : ConvexIndependent ℝ p) (h : ∀ (v : Vertex), HasFourEquidistant p v) : ∃ (p' : Vertex → Plane) (Q : OctagonIncidence), ConvexIndependent ℝ p' ∧ Realises p' Q ∧ Q.Normalized ∧ Q.PairSparse ∧ Q.Balanced

A failed convex octagon has a normalized balanced pair-sparse realisation.