First-row symmetry reduction

The normalized zeroth row splits the remaining labels into {2,3,4} and {5,6,7}. Permuting within those blocks reduces the 35 possible first rows to seven canonical orbits. The small table below records an explicit forward and inverse permutation for every row.

theorem Erdos97Octagon.RawIncidence.exists_rowOneIndex (Q : OctagonIncidence) : ∃ (index : Fin 35), Q.targets 1 = packedRow (rowOneMask index)

Every legal first row has one of the 35 explicit masks.

theorem Erdos97Octagon.RawIncidence.exists_rowTwoIndex (Q : OctagonIncidence) : ∃ (index : Fin 35), Q.targets 2 = packedRow (rowTwoMask index)

Every legal second row has one of the 35 explicit masks.

structure Erdos97Octagon.RawIncidence.RowSymmetryCertificate : Type

One explicit permutation taking a first row to a canonical orbit.

• orbit : Fin 7

  Index of the canonical first-row orbit.

• forwardCode : UInt64

  Packed code for the forward vertex permutation.

• inverseCode : UInt64

  Packed code for the inverse vertex permutation.

def Erdos97Octagon.RawIncidence.RowSymmetryCertificate.Valid (certificate : RowSymmetryCertificate) (sourceMask : UInt64) : Prop

Mathematical validity of a row-symmetry certificate.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Erdos97Octagon.RawIncidence.instDecidableRowSymmetryCertificateValid (certificate : RowSymmetryCertificate) (sourceMask : UInt64) : Decidable (certificate.Valid sourceMask)

Equations

• Erdos97Octagon.RawIncidence.instDecidableRowSymmetryCertificateValid certificate sourceMask = id inferInstance

def Erdos97Octagon.RawIncidence.rowSymmetryCertificate : Fin 35 → RowSymmetryCertificate

The 35 explicit orbit certificates, aligned with rowOneMask.

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos97Octagon.RawIncidence.rowSymmetryCertificate_valid (index : Fin 35) : (rowSymmetryCertificate index).Valid (rowOneMask index)

Kernel audit of all 35 explicit symmetry certificates.

def Erdos97Octagon.RawIncidence.RowSymmetryCertificate.toEquiv (certificate : RowSymmetryCertificate) {sourceMask : UInt64} (hvalid : certificate.Valid sourceMask) : Vertex ≃ Vertex

Decode a valid row-symmetry certificate as a vertex equivalence.

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos97Octagon.RawIncidence.canonicalize_rowOne {p : Vertex → Plane} {Q : OctagonIncidence} (hC : ConvexIndependent ℝ p) (hR : Realises p Q) (hN : Q.Normalized) (index : Fin 35) (hrow : Q.targets 1 = packedRow (rowOneMask index)) : ∃ (orbit : Fin 7) (p' : Vertex → Plane) (Q' : OctagonIncidence), ConvexIndependent ℝ p' ∧ Realises p' Q' ∧ Q'.Normalized ∧ Q'.PairSparse ∧ Q'.Balanced ∧ Q'.targets 1 = packedRow (canonicalRowMask orbit)

Relabel a normalized system so that row one is one of seven canonical rows.