OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationParentStream.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Executable bounded parent tasks with early leaf restrictions

  1. instance OAI.LowSpaceSubsetSum.(instance at line 12) line 12
  2. structure OAI.LowSpaceSubsetSum.RepresentationParentData line 19

    Source documentation

    Data available to a parent task: input, signs, leaf domains, moduli, residues, capacity, and the current partial top mask. No solution is stored.

    structure RepresentationParentData (n : ℕ) where
…
  3. def OAI.LowSpaceSubsetSum.RepresentationParentData.weights line 35
  4. def OAI.LowSpaceSubsetSum.RepresentationParentData.pair line 37
  5. abbrev OAI.LowSpaceSubsetSum.RepresentationParentData.Child line 49
  6. abbrev OAI.LowSpaceSubsetSum.RepresentationParentData.Parent line 50
  7. def OAI.LowSpaceSubsetSum.RepresentationParentData.key line 52
  8. def OAI.LowSpaceSubsetSum.RepresentationParentData.emit line 57

    Source documentation

    All top and background validity checks are redundant on the intended layout, but keep the subset-witness invariant explicit on arbitrary data.

    def emit (x y : Child (n := n)) : Option (Entry (Fin n)) :=
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationParentData.Child, OAI.LowSpaceSubsetSum.Entry

  9. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.emit_some_iff line 61
  10. def OAI.LowSpaceSubsetSum.RepresentationParentData.collect line 67
  11. def OAI.LowSpaceSubsetSum.RepresentationParentData.entries line 74
  12. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.collect_invariant line 76
  13. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.storage line 83

    Source documentation

    All outcomes, including overflow, retain at most one rejected entry.

    theorem storage (B : ℕ) :
    (D.entries B).size ≤ D.capacity + 1 ∧
      BinaryTrie.nodes (D.collect B).state.user.keys.tree ≤
        (WeightEncoding.entryWidth D.input + 1) * (D.capacity + 1) :=
…

    Mentions: OAI.LowSpaceSubsetSum.BinaryTrie.nodes, OAI.LowSpaceSubsetSum.WeightEncoding.entryWidth

  14. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.streams_parent line 89
  15. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.streams_compatible line 98
  16. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.entries_provenance line 113

    Source documentation

    Every retained record comes from a valid raw four-leaf occurrence, even if this task overflows. Compatible masks were filtered before the streams.

    theorem entries_provenance (B : ℕ) (e : Entry (Fin n)) (he : e ∈ (D.entries B).toList) :
    ∃ x ∈ RepresentationUniverse.parents D.leaves, RepresentationUniverse.Valid x ∧
      RepresentationUniverse.entry D.weights x = e ∧
        D.maskRestriction.Compatible (RepresentationUniverse.topDomain D.leaves) e.mask := by
…

    Mentions: OAI.LowSpaceSubsetSum.Entry, OAI.LowSpaceSubsetSum.RepresentationUniverse.parents, OAI.LowSpaceSubsetSum.RepresentationUniverse.Valid, OAI.LowSpaceSubsetSum.RepresentationUniverse.entry, OAI.LowSpaceSubsetSum.RepresentationUniverse.topDomain