OAI/Combinatorics/LowSpaceSubsetSum/Counting/MaskRestriction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Testing a partial indexed mask before generating raw streams

  1. structure OAI.LowSpaceSubsetSum.MaskRestriction line 9
  2. def OAI.LowSpaceSubsetSum.MaskRestriction.empty line 17
  3. def OAI.LowSpaceSubsetSum.MaskRestriction.Compatible line 21

    Source documentation

    A leaf checks only forced-one indices in its own top block. Forced zeros can be tested against its selected top mask directly.

    def Compatible (domain selected : Finset (Fin n)) : Prop :=
…
  4. instance OAI.LowSpaceSubsetSum.MaskRestriction.(instance at line 24) line 24
  5. def OAI.LowSpaceSubsetSum.MaskRestriction.accept line 27
  6. theorem OAI.LowSpaceSubsetSum.MaskRestriction.accept_eq_true line 29
  7. theorem OAI.LowSpaceSubsetSum.MaskRestriction.empty_compatible line 32
  8. theorem OAI.LowSpaceSubsetSum.MaskRestriction.union_compatible line 35
  9. theorem OAI.LowSpaceSubsetSum.MaskRestriction.left_compatible line 48

    Source documentation

    A compatible full mask yields a compatible leaf restriction because the other leaf cannot contain an index in this leaf's disjoint top domain.

    theorem left_compatible {A B S T : Finset (Fin n)}
    (hd : Disjoint A B) (hT : T ⊆ B) (h : P.Compatible (A ∪ B) (S ∪ T)) :
    P.Compatible A S := by
…
  10. theorem OAI.LowSpaceSubsetSum.MaskRestriction.right_compatible line 60