Documentation

LeanPool.Erdos97ConvexOctagon.CoverageSearchRowChoiceSoundness

Soundness and completeness of lightweight legal-row search data #

source
def Erdos97Octagon.RawIncidence.searchRowChoiceAt (centre : Vertex) (index : Fin 35) :
SearchRowChoice

The lightweight choice at one legal-row index.

Equations
Instances For
    source
    theorem Erdos97Octagon.RawIncidence.searchRowChoices_size (centre : Vertex) :
    (searchRowChoices.getD ↑centre #[]).size = 35

    Each centre has exactly the expected 35 legal rows.

    source
    theorem Erdos97Octagon.RawIncidence.searchRowChoiceAt_mem (centre : Vertex) (index : Fin 35) :
    searchRowChoiceAt centre index ∈ searchRowChoices.getD ↑centre #[]

    Indexed lookup returns a member of the corresponding centre's row table.

    source
    theorem Erdos97Octagon.RawIncidence.searchRowChoices_complete (centre : Vertex) :
    (rowOptions centre).reverse = List.ofFn fun (index : Fin 35) => packedRow (searchRowChoiceAt centre index).rowMask

    The generated table is the complete legal-row enumeration, in search order.

    source
    theorem Erdos97Octagon.RawIncidence.exists_searchRowChoiceIndex (Q : OctagonIncidence) (centre : Vertex) :
    ∃ (index : Fin 35), Q.targets centre = packedRow (searchRowChoiceAt centre index).rowMask

    Every mathematical incidence row occurs at one lightweight search index.

    source
    theorem Erdos97Octagon.RawIncidence.searchRowChoiceAt_pairMask (centre : Vertex) (index : Fin 35) :
    (searchRowChoiceAt centre index).pairMask = rowPairMask (searchRowChoiceAt centre index).rowMask

    Every stored unordered-pair mask is exactly computed from its row mask.

    source
    theorem Erdos97Octagon.RawIncidence.searchRowChoiceAt_two_mask (index : Fin 35) :
    (searchRowChoiceAt 2 index).rowMask = rowTwoMask index

    The centre-two row table uses exactly the public fixed-branch ordering.

    source
    theorem Erdos97Octagon.RawIncidence.searchRowChoice_pairMask_of_mem (centre : Vertex) {choice : SearchRowChoice} (hchoice : choice ∈ searchRowChoices.getD ↑centre #[]) :
    choice.pairMask = rowPairMask choice.rowMask

    Every member of a centre's row table carries the exact computed pair mask.

    source
    theorem Erdos97Octagon.RawIncidence.searchRowChoice_pairMask (centre : Vertex) (index : ℕ) (hindex : index < 35) :
    have choice := (searchRowChoices.getD ↑centre #[]).getD index { rowMask := 0, pairMask := 0 }; choice.pairMask = rowPairMask choice.rowMask

    Natural-number indexed lookup has the same audited pair-mask guarantee.

    source
    theorem Erdos97Octagon.RawIncidence.searchChoiceForRow_spec (centre : Vertex) (row : UInt64) (hexists : ∃ choice ∈ searchRowChoices.getD ↑centre #[], choice.rowMask = row) :
    searchChoiceForRow centre row ∈ searchRowChoices.getD ↑centre #[] ∧ (searchChoiceForRow centre row).rowMask = row

    Lookup by row mask returns the matching audited table entry when it exists.

    source
    theorem Erdos97Octagon.RawIncidence.searchChoiceForRow_pairMask (centre : Vertex) (row : UInt64) (hexists : ∃ choice ∈ searchRowChoices.getD ↑centre #[], choice.rowMask = row) :
    (searchChoiceForRow centre row).pairMask = rowPairMask row

    Successful row-mask lookup also returns its exactly computed pair mask.

    source
    theorem Erdos97Octagon.RawIncidence.searchChoiceForRow_zero_spec :
    (searchChoiceForRow 0 30).rowMask = 30

    Lookup finds the normalized zeroth row.

    source
    theorem Erdos97Octagon.RawIncidence.searchChoiceForRow_zero_pairMask :
    (searchChoiceForRow 0 30).pairMask = rowPairMask 30

    The normalized zeroth-row lookup carries its exact pair mask.

    source
    theorem Erdos97Octagon.RawIncidence.searchChoiceForRow_canonical_spec (orbit : Fin 7) :
    (searchChoiceForRow 1 (canonicalRowMask orbit)).rowMask = canonicalRowMask orbit

    Lookup finds every public canonical first-row mask.

    source
    theorem Erdos97Octagon.RawIncidence.searchChoiceForRow_canonical_pairMask (orbit : Fin 7) :
    (searchChoiceForRow 1 (canonicalRowMask orbit)).pairMask = rowPairMask (canonicalRowMask orbit)

    Every canonical first-row lookup carries its exact pair mask.

    source
    theorem Erdos97Octagon.RawIncidence.searchChoiceForRow_two_spec (index : Fin 35) :
    (searchChoiceForRow 2 (rowTwoMask index)).rowMask = rowTwoMask index

    Lookup finds every public second-row mask in the same indexed order.

    source
    theorem Erdos97Octagon.RawIncidence.searchChoiceForRow_two_pairMask (index : Fin 35) :
    (searchChoiceForRow 2 (rowTwoMask index)).pairMask = rowPairMask (rowTwoMask index)

    Every indexed second-row lookup carries its exact pair mask.