OAI/Combinatorics/LowSpaceSubsetSum/Search/PreparedReaderContext.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Preparing one shared-array reader context

Generation and sorting execute once. Row initialization captures the returned right array, and the context retains that same immutable array with its measured tournament state. Proof transports do not regenerate either array.

  1. structure OAI.LowSpaceSubsetSum.PreparedReaderContext.Context line 19
  2. theorem OAI.LowSpaceSubsetSum.PreparedReaderContext.context_ext line 24
  3. theorem OAI.LowSpaceSubsetSum.PreparedReaderContext.rekey_tree line 34
  4. theorem OAI.LowSpaceSubsetSum.PreparedReaderContext.key_eq line 40
  5. def OAI.LowSpaceSubsetSum.PreparedReaderContext.fromArrays line 49

    Source documentation

    The initializer takes array values, so every row closure shares right.

    def fromArrays (I : Instance n) (F : IndexedMask n) (left right : Array (LeafRecord n))
    (p P c : ℤ)
    (hs : FilteredRow.PrimarySorted right (fun x => (RepresentationKeys.leafWeight I F x).1) p)
    (ht : FilteredRow.SecondarySorted right (fun x => (RepresentationKeys.leafWeight I F x).1) p P)
    (hP : 0 < P) (mode : FilteredStream.Mode) : Context I F P mode × ℕ :=
…

    Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.LeafRecord, OAI.LowSpaceSubsetSum.FilteredRow.PrimarySorted, OAI.LowSpaceSubsetSum.RepresentationKeys.leafWeight, OAI.LowSpaceSubsetSum.FilteredRow.SecondarySorted, OAI.LowSpaceSubsetSum.FilteredStream.Mode, OAI.LowSpaceSubsetSum.PreparedReaderContext.Context

  6. theorem OAI.LowSpaceSubsetSum.PreparedReaderContext.fromArrays_tree line 57
  7. theorem OAI.LowSpaceSubsetSum.PreparedReaderContext.dep_heq line 67
  8. theorem OAI.LowSpaceSubsetSum.PreparedReaderContext.state_heq line 72
  9. def OAI.LowSpaceSubsetSum.PreparedReaderContext.source line 82
  10. theorem OAI.LowSpaceSubsetSum.PreparedReaderContext.record_key_eq line 88
  11. theorem OAI.LowSpaceSubsetSum.PreparedReaderContext.fromArrays_source line 97
  12. theorem OAI.LowSpaceSubsetSum.PreparedReaderContext.parent_primary line 135
  13. theorem OAI.LowSpaceSubsetSum.PreparedReaderContext.parent_secondary line 148
  14. theorem OAI.LowSpaceSubsetSum.PreparedReaderContext.prepared_primary line 161
  15. theorem OAI.LowSpaceSubsetSum.PreparedReaderContext.prepared_secondary line 170
  16. def OAI.LowSpaceSubsetSum.PreparedReaderContext.build line 180

    Source documentation

    One complete preparation and initialization; a is evaluated once.

    def build (D : RepresentationParentData n) (F : IndexedMask n) (P : StoredRestriction n)
    (hF : F.semantic = D.signs) (j : Fin 2) : Context D.input F D.modulus (D.pair j).mode × ℕ :=
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationParentData, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.StoredRestriction, OAI.LowSpaceSubsetSum.PreparedReaderContext.Context

  17. theorem OAI.LowSpaceSubsetSum.PreparedReaderContext.build_value line 187
  18. theorem OAI.LowSpaceSubsetSum.PreparedReaderContext.build_work line 195