Documentation

LeanPool.Erdos97ConvexOctagon.PairStateExactness

Exactness of packed pair-occurrence states #

source
def Erdos97Octagon.RawIncidence.StaticDirectCoverage.PairState.Exact (state : PairState) (assignments : List RowAssignment) :
Prop

A packed pair state exactly records whether each vertex pair has occurred once or twice.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.PairState.empty_exact :
    empty.Exact []

    The empty packed pair state exactly represents the empty assignment list.

    source
    theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.PairState.Exact.add {state : PairState} {assignments : List RowAssignment} (hexact : state.Exact assignments) (centre : Vertex) (row pairMask : UInt64) (hmask : pairMask = rowPairMask row) :
    (state.add pairMask).Exact ((centre, row) :: assignments)

    Adding an audited row mask preserves exact packed pair counts.

    source
    theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.PairState.Exact.perm {state : PairState} {assignments assignments' : List RowAssignment} (hexact : state.Exact assignments) (hperm : assignments.Perm assignments') :
    state.Exact assignments'

    Exact pair states are invariant under reordering the semantic assignment list.

    source
    theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.PairState.compatible_of_exact {state : PairState} {assignments : List RowAssignment} {row pairMask : UInt64} (hexact : state.Exact assignments) (hmask : pairMask = rowPairMask row) (hcompatible : pairCompatibleB assignments row = true) :
    state.compatible pairMask = true

    Exact packed pair state makes its constant-time guard complete for a compatible row.