Erdős 97 convex-octagon formalization: Certificates

inductive Erdos97Octagon.RawIncidence.Certificate : Type

A finite witness emitted by the obstruction classifier.

• k4 (root : Vertex) (component : List Vertex) (a b c d : Vertex) : Certificate
• hubPentagon (root : Vertex) (component : List Vertex) (o a b c d e : Vertex) : Certificate
• sharedThree (a b q1 q2 q3 : Vertex) : Certificate
• cycleStrip (root : Vertex) (component : List Vertex) (o x1 x2 x3 x4 x5 x6 : Vertex) : Certificate
• residual (payload : UInt64) : Certificate

@[instance_reducible]

instance Erdos97Octagon.RawIncidence.instDecidableEqCertificate : DecidableEq Certificate

Equations

• Erdos97Octagon.RawIncidence.instDecidableEqCertificate = Erdos97Octagon.RawIncidence.instDecidableEqCertificate.decEq

def Erdos97Octagon.RawIncidence.instDecidableEqCertificate.decEq (x✝ x✝¹ : Certificate) : Decidable (x✝ = x✝¹)

Equations

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

inductive Erdos97Octagon.RawIncidence.PrefixCertificate : Type

The two obstruction shapes that remain valid when incidences are added.

• k4 (root : Vertex) (component : List Vertex) (a b c d : Vertex) : PrefixCertificate
• sharedThree (a b q1 q2 q3 : Vertex) : PrefixCertificate

def Erdos97Octagon.RawIncidence.instDecidableEqPrefixCertificate.decEq (x✝ x✝¹ : PrefixCertificate) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Erdos97Octagon.RawIncidence.instDecidableEqPrefixCertificate : DecidableEq PrefixCertificate

Equations

• Erdos97Octagon.RawIncidence.instDecidableEqPrefixCertificate = Erdos97Octagon.RawIncidence.instDecidableEqPrefixCertificate.decEq

def Erdos97Octagon.RawIncidence.PrefixCertificate.toCertificate : PrefixCertificate → Certificate

Regard a monotone prefix witness as a general obstruction certificate.

Equations

• (Erdos97Octagon.RawIncidence.PrefixCertificate.k4 root component a b c d).toCertificate = Erdos97Octagon.RawIncidence.Certificate.k4 root component a b c d
• (Erdos97Octagon.RawIncidence.PrefixCertificate.sharedThree a b q1 q2 q3).toCertificate = Erdos97Octagon.RawIncidence.Certificate.sharedThree a b q1 q2 q3

def Erdos97Octagon.RawIncidence.extendsTreeB (R : RawIncidence) (reached : Finset Vertex) : List Vertex → Bool

Validate the tail of an ordered mutual-edge spanning tree.

Equations

• R.extendsTreeB reached [] = true
• R.extendsTreeB reached (v :: todo) = (decide (v ∉ reached) && decide (∃ u ∈ reached, v ∈ R u ∧ u ∈ R v) && R.extendsTreeB (insert v reached) todo)

def Erdos97Octagon.RawIncidence.componentTreeB (R : RawIncidence) (root : Vertex) : List Vertex → Bool

Check that the listed vertices form an ordered mutual-edge spanning tree.

Equations

• R.componentTreeB root [] = false
• R.componentTreeB root (v :: todo) = (decide (v = root) && R.extendsTreeB {root} todo)

def Erdos97Octagon.RawIncidence.TreeLabelledEdge (R : RawIncidence) (component : List Vertex) (a b : Vertex) : Prop

A selected edge whose selecting endpoint occurs in a validated tree.

Equations

• R.TreeLabelledEdge component a b = (a ∈ component ∧ b ∈ R a ∨ b ∈ component ∧ a ∈ R b)

def Erdos97Octagon.RawIncidence.payloadClass (payload : UInt64) : ℕ

The class number stored in a residual-isomorphism payload.

Equations

• Erdos97Octagon.RawIncidence.payloadClass payload = (payload &&& 15).toNat

def Erdos97Octagon.RawIncidence.payloadForwardCode (payload : UInt64) : UInt64

The forward permutation stored in a residual-isomorphism payload.

Equations

• Erdos97Octagon.RawIncidence.payloadForwardCode payload = payload >>> 4 &&& 16777215

def Erdos97Octagon.RawIncidence.payloadInverseCode (payload : UInt64) : UInt64

The inverse permutation stored in a residual-isomorphism payload.

Equations

• Erdos97Octagon.RawIncidence.payloadInverseCode payload = payload >>> 28 &&& 16777215

def Erdos97Octagon.RawIncidence.Certificate.Valid (R : RawIncidence) : Certificate → Prop

The mathematical proposition checked for each emitted finite witness.

Equations

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

def Erdos97Octagon.RawIncidence.Certificate.validB (R : RawIncidence) : Certificate → Bool

Kernel-check the mathematical content of an emitted witness.

Equations

• One or more equations did not get rendered due to their size.
• Erdos97Octagon.RawIncidence.Certificate.validB R (Erdos97Octagon.RawIncidence.Certificate.residual payload) = Erdos97Octagon.RawIncidence.residualValidB✝ R payload

theorem Erdos97Octagon.RawIncidence.Certificate.valid_of_validB {R : RawIncidence} {certificate : Certificate} (hvalid : validB R certificate = true) : Valid R certificate

The Boolean validator implies the mathematical certificate predicate.

def Erdos97Octagon.RawIncidence.Extends (R S : RawIncidence) : Prop

One incidence table extends another when it contains every selected edge.

Equations

• R.Extends S = ∀ (centre target : Erdos97Octagon.Vertex), target ∈ R centre → target ∈ S centre

theorem Erdos97Octagon.RawIncidence.PrefixCertificate.valid_mono {R S : RawIncidence} {certificate : PrefixCertificate} (hRS : R.Extends S) (hvalid : Certificate.Valid R certificate.toCertificate) : Certificate.Valid S certificate.toCertificate

A prefix certificate remains valid in every incidence extension.

theorem Erdos97Octagon.RawIncidence.componentTree_sameComponent (Q : OctagonIncidence) {root : Vertex} {component : List Vertex} (htree : componentTreeB Q.targets root component = true) {v : Vertex} (hv : v ∈ component) : Q.SameComponent root v

Every vertex in a validated ordered tree belongs to the root component.

theorem Erdos97Octagon.RawIncidence.treeLabelledEdge_sound (Q : OctagonIncidence) {root : Vertex} {component : List Vertex} (htree : componentTreeB Q.targets root component = true) {a b : Vertex} (h : TreeLabelledEdge Q.targets component a b) : Q.LabelledEdge root a b

Every tree-labelled checker edge is a genuine component-radius edge.

theorem Erdos97Octagon.RawIncidence.Certificate.not_convex_realises {Q : OctagonIncidence} (certificate : Certificate) (hvalid : Valid Q.targets certificate) {p : Vertex → Plane} (hC : ConvexIndependent ℝ p) (hR : Realises p Q) : False

Every validated finite witness contradicts a convex planar realisation.