Explicit row masks for the finite incidence-table search

def Erdos97Octagon.RawIncidence.canonicalRowMask : Fin 7 → UInt64

The seven canonical first-row masks, in certificate order.

Equations

• Erdos97Octagon.RawIncidence.canonicalRowMask = ![29, 45, 101, 225, 60, 108, 228]

def Erdos97Octagon.RawIncidence.rowOneMask : Fin 35 → UInt64

All first-row masks in the lexicographic search order.

Equations

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

def Erdos97Octagon.RawIncidence.rowTwoMask : Fin 35 → UInt64

All second-row masks in the lexicographic search order.

Equations

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

def Erdos97Octagon.RawIncidence.searchCentres : List Vertex

Order in which the direct audit assigns the five noncanonical rows.

Equations

• Erdos97Octagon.RawIncidence.searchCentres = [3, 4, 7, 6, 5]