Erdős 97 convex-octagon formalization: Incidence

@[reducible, inline]

abbrev Erdos97Octagon.Vertex : Type

The labelled vertex set of an octagon.

Equations

• Erdos97Octagon.Vertex = Fin 8

structure Erdos97Octagon.OctagonIncidence : Type

Four selected equidistant witnesses around every labelled octagon vertex.

• targets : Vertex → Finset Vertex

  The four selected witnesses associated with a centre.

• card_targets (v : Vertex) : (self.targets v).card = 4

  Every witness row has exactly four vertices.

• centre_not_mem (v : Vertex) : v ∉ self.targets v

  A centre is not one of its own positive-radius witnesses.

theorem Erdos97Octagon.OctagonIncidence.ext {Q R : OctagonIncidence} (h : Q.targets = R.targets) : Q = R

theorem Erdos97Octagon.OctagonIncidence.ext_iff {Q R : OctagonIncidence} : Q = R ↔ Q.targets = R.targets

def Erdos97Octagon.OctagonIncidence.indegree (Q : OctagonIncidence) (a : Vertex) : ℕ

The number of witness rows containing a.

Equations

• Q.indegree a = ∑ v : Erdos97Octagon.Vertex, if a ∈ Q.targets v then 1 else 0

def Erdos97Octagon.OctagonIncidence.pairMultiplicity (Q : OctagonIncidence) (a b : Vertex) : ℕ

The number of witness rows containing both a and b.

Equations

• Q.pairMultiplicity a b = ∑ v : Erdos97Octagon.Vertex, if a ∈ Q.targets v ∧ b ∈ Q.targets v then 1 else 0

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

No distinct pair occurs together in more than two witness rows.

Equations

• Q.PairSparse = ∀ ⦃a b : Erdos97Octagon.Vertex⦄, a ≠ b → Q.pairMultiplicity a b ≤ 2

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

Every vertex occurs in exactly four witness rows.

Equations

• Q.Balanced = ∀ (a : Erdos97Octagon.Vertex), Q.indegree a = 4

theorem Erdos97Octagon.OctagonIncidence.sum_pairMultiplicity (Q : OctagonIncidence) (a : Vertex) : ∑ b ∈ Finset.univ.erase a, Q.pairMultiplicity a b = 3 * Q.indegree a

Double-count pairs in the witness rows containing a fixed vertex.

theorem Erdos97Octagon.OctagonIncidence.indegree_le_four (Q : OctagonIncidence) (hQ : Q.PairSparse) (a : Vertex) : Q.indegree a ≤ 4

Every vertex has indegree at most four when pair multiplicities are at most two.

theorem Erdos97Octagon.OctagonIncidence.sum_indegree (Q : OctagonIncidence) : ∑ a : Vertex, Q.indegree a = 32

There are exactly 32 selected incidences in an octagon witness system.

theorem Erdos97Octagon.OctagonIncidence.balanced_of_pairSparse (Q : OctagonIncidence) (hQ : Q.PairSparse) : Q.Balanced

Pair sparsity forces the four-in/four-out balanced incidence condition.