Documentation

LeanPool.Erdos97ConvexOctagon.PairCompatibility

Pair-sparsity guard for direct incidence-table search #

source
def Erdos97Octagon.RawIncidence.pairCount (assignments : List (Vertex × UInt64)) (a b : Vertex) :
ℕ

Number of processed row masks containing both vertices.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Erdos97Octagon.RawIncidence.pairCompatibleB (assignments : List (Vertex × UInt64)) (row : UInt64) :
    Bool

    Boolean guard that prevents a new row from making any pair occur three times.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Erdos97Octagon.RawIncidence.pairCount_le_pairMultiplicity (Q : OctagonIncidence) (assignments : List (Vertex × UInt64)) (a b : Vertex) (hcentres : (List.map Prod.fst assignments).Nodup) (hrows : ∀ (centre : Vertex) (row : UInt64), (centre, row) ∈ assignments → Q.targets centre = packedRow row) :
      pairCount assignments a b ≤ Q.pairMultiplicity a b

      The processed-row count of a pair is bounded by its full incidence multiplicity.

      source
      theorem Erdos97Octagon.RawIncidence.pairCompatibleB_of_pairSparse (Q : OctagonIncidence) (hSparse : Q.PairSparse) (assignments : List (Vertex × UInt64)) (nextCentre : Vertex) (nextMask : UInt64) (hcentres : (nextCentre :: List.map Prod.fst assignments).Nodup) (hrows : ∀ (centre : Vertex) (row : UInt64), (centre, row) ∈ assignments → Q.targets centre = packedRow row) (hnext : Q.targets nextCentre = packedRow nextMask) :
      pairCompatibleB assignments nextMask = true

      Pair sparsity makes the direct-search pair guard accept the actual next row.

      source
      theorem Erdos97Octagon.RawIncidence.pairCompatibleB_of_pairSparse_prefix (Q : OctagonIncidence) (hSparse : Q.PairSparse) (assignments : List (Vertex × UInt64)) (nextCentre : Vertex) (remaining : List Vertex) (nextMask : UInt64) (hcentres : List.map Prod.fst assignments ++ nextCentre :: remaining = List.finRange 8) (hrows : ∀ (centre : Vertex) (row : UInt64), (centre, row) ∈ assignments → Q.targets centre = packedRow row) (hnext : Q.targets nextCentre = packedRow nextMask) :
      pairCompatibleB assignments nextMask = true

      The pair guard accepts the next row of a prefix partitioning all eight centres.