Documentation

LeanPool.Erdos97ConvexOctagon.CodeStateExactness

Exactness of packed incidence-table prefixes #

source
def Erdos97Octagon.RawIncidence.StaticDirectCoverage.CodeMatches (code : UInt64) (assignments : List RowAssignment) :
Prop

A packed table code exactly records all selected bits in its assignment list.

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

    The zero code exactly represents the empty assignment list.

    source
    theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.CodeMatches.add {code : UInt64} {assignments : List RowAssignment} (hexact : CodeMatches code assignments) (rowCentre : Vertex) (row : UInt64) :
    CodeMatches (addRowCode code row rowCentre) ((rowCentre, row) :: assignments)

    Adding a masked row preserves exact packed-code semantics.

    source
    theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.CodeMatches.perm {code : UInt64} {assignments assignments' : List RowAssignment} (hexact : CodeMatches code assignments) (hperm : assignments.Perm assignments') :
    CodeMatches code assignments'

    Exact code semantics are invariant under reordering the assignment list.

    source
    theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.CodeMatches.selected_of_subset {code mask : UInt64} {assignments : List RowAssignment} (hexact : CodeMatches code assignments) (hsubset : (mask &&& code == mask) = true) {centre target : Vertex} (hselected : bitSetB mask (varIndex centre target) = true) :
    selectedByAssignmentsB assignments centre target = true

    A subset mask selects only bits selected by an exact prefix code.

    source
    theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.CodeMatches.extends_of_subset {code mask : UInt64} {assignments : List RowAssignment} {table : Vertex → Finset Vertex} (hexact : CodeMatches code assignments) (hsound : ∀ (centre target : Vertex), selectedByAssignmentsB assignments centre target = true → target ∈ table centre) (hsubset : (mask &&& code == mask) = true) :
    (packedIncidence mask).Extends table

    A subset of an exact prefix code extends any table matched by its assignments.

    source
    theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.CodeMatches.table_eq_of_code_eq {code exactCode : UInt64} {assignments : List RowAssignment} {table : Vertex → Finset Vertex} (hexact : CodeMatches code assignments) (hsound : ∀ (centre target : Vertex), selectedByAssignmentsB assignments centre target = true → target ∈ table centre) (hcomplete : ∀ (centre target : Vertex), target ∈ table centre → selectedByAssignmentsB assignments centre target = true) (hequal : (exactCode == code) = true) :
    table = packedIncidence exactCode

    Equality with a complete exact prefix code identifies the entire incidence table.

    source
    theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.CodeMatches.patternExtendsAssignmentsB {code : UInt64} {assignments : List RowAssignment} (hexact : CodeMatches code assignments) (summary : PatternSummary) (hsubset : (summary.mask &&& code == summary.mask) = true) :
    StaticDirectCoverage.patternExtendsAssignmentsB assignments summary = true

    Packed subset validation implies the full semantic prefix extension check.

    source
    theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.CodeMatches.hardEqualsAssignmentsB {code : UInt64} {assignments : List RowAssignment} (hexact : CodeMatches code assignments) (summary : HardSummary) (hequal : (summary.code == code) = true) :
    StaticDirectCoverage.hardEqualsAssignmentsB assignments summary = true

    Equality with an exact prefix code implies the full semantic table-code check.