Erdős 97 convex-octagon formalization: Finite Model

@[reducible, inline]

abbrev Erdos97Octagon.RawIncidence : Type

An unbundled eight-row incidence table used by the finite certificate.

Equations

• Erdos97Octagon.RawIncidence = (Erdos97Octagon.Vertex → Finset Erdos97Octagon.Vertex)

@[reducible, inline]

abbrev Erdos97Octagon.RawIncidence.SearchRow : Type

A four-entry row used by the finite certificate.

Equations

• Erdos97Octagon.RawIncidence.SearchRow = Finset Erdos97Octagon.Vertex

def Erdos97Octagon.RawIncidence.rowOptions (v : Vertex) : List SearchRow

All four-element rows available at a specified centre.

Equations

• Erdos97Octagon.RawIncidence.rowOptions v = List.map List.toFinset (List.sublistsLen 4 (List.filter (fun (x : Erdos97Octagon.Vertex) => decide (x ≠ v)) (List.finRange 8)))

theorem Erdos97Octagon.RawIncidence.target_row_mem_rowOptions (Q : OctagonIncidence) (v : Vertex) : Q.targets v ∈ rowOptions v

Every row of an octagon incidence system occurs in the finite row list.

def Erdos97Octagon.RawIncidence.varIndex (centre target : Vertex) : ℕ

The zero-based SAT variable representing one directed incidence.

Equations

• Erdos97Octagon.RawIncidence.varIndex centre target = 8 * ↑centre + ↑target

def Erdos97Octagon.RawIncidence.bitSetB (code : UInt64) (index : ℕ) : Bool

Test one bit of a packed 64-bit incidence table.

Equations

• Erdos97Octagon.RawIncidence.bitSetB code index = (code >>> UInt64.ofNat index &&& 1 != 0)

def Erdos97Octagon.RawIncidence.decodeMap (code : UInt64) (vertex : Vertex) : Vertex

Decode one three-bit entry of a packed permutation.

Equations

• Erdos97Octagon.RawIncidence.decodeMap code vertex = Fin.ofNat 8 (code >>> UInt64.ofNat (3 * ↑vertex) &&& 7).toNat

def Erdos97Octagon.RawIncidence.packedRow (mask : UInt64) : Finset Vertex

Decode an eight-bit row mask as a set of octagon vertices.

Equations

• Erdos97Octagon.RawIncidence.packedRow mask = {target : Erdos97Octagon.Vertex | Erdos97Octagon.RawIncidence.bitSetB mask ↑target = true}

@[simp]

theorem Erdos97Octagon.RawIncidence.mem_packedRow (mask : UInt64) (target : Vertex) : target ∈ packedRow mask ↔ bitSetB mask ↑target = true

def Erdos97Octagon.RawIncidence.vertexPairs : List (List Vertex)

Vertex pairs in the lexicographic order used by the finite search.

Equations

• Erdos97Octagon.RawIncidence.vertexPairs = (List.sublistsLen 2 (List.finRange 8)).reverse

def Erdos97Octagon.RawIncidence.packedSelectsB (code : UInt64) (centre target : Vertex) : Bool

Read one directed incidence from a packed table.

Equations

• Erdos97Octagon.RawIncidence.packedSelectsB code centre target = Erdos97Octagon.RawIncidence.bitSetB code (Erdos97Octagon.RawIncidence.varIndex centre target)

def Erdos97Octagon.RawIncidence.packedIncidence (code : UInt64) : RawIncidence

Decode a packed table to the mathematical finite-set model.

Equations

• Erdos97Octagon.RawIncidence.packedIncidence code centre = {target : Erdos97Octagon.Vertex | Erdos97Octagon.RawIncidence.packedSelectsB code centre target = true}

@[simp]

theorem Erdos97Octagon.RawIncidence.mem_packedIncidence (code : UInt64) (centre target : Vertex) : target ∈ packedIncidence code centre ↔ packedSelectsB code centre target = true

def Erdos97Octagon.RawIncidence.rowMask (row : SearchRow) : UInt64

Pack one finite row into its eight-bit position.

Equations

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

def Erdos97Octagon.RawIncidence.systemCode (R : RawIncidence) : UInt64

Pack all eight rows into one 64-bit key.

Equations

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