OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationMatchingWork.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Raw matching-occurrence charges through the executable prefix tree

Invalid tuples are included: the join must report them before the callback can reject them. Early prefix filtering partitions this larger universe too.

  1. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.matchingUniverse_mem line 18
  2. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.matching_restriction line 27
  3. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.matchingUniverse_restriction line 69
  4. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.matchingUniverse_force line 84
  5. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.matchingUniverse_force_card_add line 101
  6. def OAI.LowSpaceSubsetSum.RepresentationParentData.matchingVisits line 116

    Source documentation

    A proof view of all matching occurrences visited if YES checks are ignored. The runtime does not build this tree or its list of occurrences.

    def matchingVisits (B : ℕ) : List (Fin n) → MaskRestriction n → ℕ
  | [], P => ({ D with maskRestriction := P }).matchingUniverse.card
…

    Mentions: OAI.LowSpaceSubsetSum.MaskRestriction

  7. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.matchingVisits_le line 124
  8. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.pair_outputUniverse_subset_unrestricted line 147

    Source documentation

    Early leaf restrictions only remove child stream occurrences.

    theorem pair_outputUniverse_subset_unrestricted (P : MaskRestriction n) (j : Fin 2) :
    ({ D with maskRestriction := P }.pair j).outputUniverse ⊆
…

    Mentions: OAI.LowSpaceSubsetSum.MaskRestriction, OAI.LowSpaceSubsetSum.RepresentationParentData.pair

  9. def OAI.LowSpaceSubsetSum.RepresentationParentData.unrestrictedChildCount line 166
  10. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.restricted_collect_queries_le line 170
  11. def OAI.LowSpaceSubsetSum.RepresentationParentData.queryVisits line 182

    Source documentation

    Actual reader calls summed over the hypothetical full prefix execution.

    def queryVisits (B : ℕ) : List (Fin n) → MaskRestriction n → ℕ
  | [], P => ({ D with maskRestriction := P }.collect B).state.queries
…

    Mentions: OAI.LowSpaceSubsetSum.MaskRestriction, OAI.LowSpaceSubsetSum.RepresentationParentData.collect

  12. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.queryVisits_le_tasks_matching line 190
  13. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.queryVisits_le line 207