OAI/Combinatorics/LowSpaceSubsetSum/Streams/PrefixAccounting.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Deterministic accounting for right-prefix refinement

The tree depends on distinct entries for overflow, while raw tuple occurrences are charged separately. The finite sets in this mathematical accounting are ambient analysis sets, not arrays that the implementation is allowed to store. The resulting combinatorial bounds give the accounting in lem:prefix.

  1. abbrev OAI.LowSpaceSubsetSum.MaskBits line 21

    Source documentation

    Labels of the successive mask bits, in the fixed processing order.

    abbrev MaskBits (α : Type*) := ℕ → α → Bool
  2. def OAI.LowSpaceSubsetSum.bitPart line 23
  3. theorem OAI.LowSpaceSubsetSum.bitPart_card_add line 26
  4. def OAI.LowSpaceSubsetSum.overflowNodes line 33

    Source documentation

    Overflow count includes an overflowing full-prefix node that is dropped.

    def overflowNodes (C : ℕ) (bits : MaskBits α) (depth : ℕ) : ℕ → Finset α → ℕ
  | 0, U => if C < U.card then 1 else 0
  | fuel + 1, U => if C < U.card then
      1 + overflowNodes C bits (depth + 1) fuel (bitPart bits depth false U) +
        overflowNodes C bits (depth + 1) fuel (bitPart bits depth true U)
    else 0

/-- The task count includes empty completed tasks and dropped full prefixes. -/

    Mentions: OAI.LowSpaceSubsetSum.MaskBits, OAI.LowSpaceSubsetSum.bitPart

  5. def OAI.LowSpaceSubsetSum.prefixTasks line 41

    Source documentation

    The task count includes empty completed tasks and dropped full prefixes.

    def prefixTasks (C : ℕ) (bits : MaskBits α) (depth : ℕ) : ℕ → Finset α → ℕ
  | 0, _ => 1
  | fuel + 1, U => if C < U.card then
      1 + prefixTasks C bits (depth + 1) fuel (bitPart bits depth false U) +
        prefixTasks C bits (depth + 1) fuel (bitPart bits depth true U)
    else 1

/-- Sum of the lengths of all completed right dictionaries. -/

    Mentions: OAI.LowSpaceSubsetSum.MaskBits, OAI.LowSpaceSubsetSum.bitPart

  6. def OAI.LowSpaceSubsetSum.completedEntries line 49

    Source documentation

    Sum of the lengths of all completed right dictionaries.

    def completedEntries (C : ℕ) (bits : MaskBits α) (depth : ℕ) : ℕ → Finset α → ℕ
  | 0, U => if C < U.card then 0 else U.card
  | fuel + 1, U => if C < U.card then
      completedEntries C bits (depth + 1) fuel (bitPart bits depth false U) +
        completedEntries C bits (depth + 1) fuel (bitPart bits depth true U)
    else U.card

/-- The sum of ambient entry counts over all task nodes, for charging by depth. -/

    Mentions: OAI.LowSpaceSubsetSum.MaskBits, OAI.LowSpaceSubsetSum.bitPart

  7. def OAI.LowSpaceSubsetSum.potentialVisits line 57

    Source documentation

    The sum of ambient entry counts over all task nodes, for charging by depth.

    def potentialVisits (C : ℕ) (bits : MaskBits α) (depth : ℕ) : ℕ → Finset α → ℕ
  | 0, U => U.card
  | fuel + 1, U => if C < U.card then
      U.card + potentialVisits C bits (depth + 1) fuel (bitPart bits depth false U) +
        potentialVisits C bits (depth + 1) fuel (bitPart bits depth true U)
    else U.card

/-- Raw occurrences are a separate type and retain all multiplicities. Task
branching is decided by `U`, the distinct entries, rather than by `T`. -/

    Mentions: OAI.LowSpaceSubsetSum.MaskBits, OAI.LowSpaceSubsetSum.bitPart

  8. def OAI.LowSpaceSubsetSum.rawVisits line 66

    Source documentation

    Raw occurrences are a separate type and retain all multiplicities. Task branching is decided by U, the distinct entries, rather than by T.

    def rawVisits {β : Type*} (C : ℕ) (bits : MaskBits α) (rawBits : MaskBits β)
    (depth : ℕ) : ℕ → Finset α → Finset β → ℕ
  | 0, _, T => T.card
  | fuel + 1, U, T => if C < U.card then
      T.card + rawVisits C bits rawBits (depth + 1) fuel
          (bitPart bits depth false U) (bitPart rawBits depth false T) +
        rawVisits C bits rawBits (depth + 1) fuel
          (bitPart bits depth true U) (bitPart rawBits depth true T)
    else T.card

/-- The bucket reached by following a designated entry's complete prefix. -/

    Mentions: OAI.LowSpaceSubsetSum.MaskBits, OAI.LowSpaceSubsetSum.bitPart

  9. def OAI.LowSpaceSubsetSum.fullPrefixBucket line 77

    Source documentation

    The bucket reached by following a designated entry's complete prefix.

    def fullPrefixBucket (bits : MaskBits α) (depth : ℕ) (e : α) : ℕ → Finset α → Finset α
  | 0, U => U
  | fuel + 1, U => fullPrefixBucket bits (depth + 1) e fuel
      (bitPart bits depth (bits depth e) U)

/-- The actual refinement path stops at the first dictionary that fits. -/

    Mentions: OAI.LowSpaceSubsetSum.MaskBits, OAI.LowSpaceSubsetSum.bitPart

  10. def OAI.LowSpaceSubsetSum.reachesCompleted line 83

    Source documentation

    The actual refinement path stops at the first dictionary that fits.

    def reachesCompleted (C : ℕ) (bits : MaskBits α) (depth : ℕ) (e : α) :
    ℕ → Finset α → Prop
  | 0, U => U.card ≤ C
  | fuel + 1, U => U.card ≤ C ∨ reachesCompleted C bits (depth + 1) e fuel
      (bitPart bits depth (bits depth e) U)

    Mentions: OAI.LowSpaceSubsetSum.MaskBits, OAI.LowSpaceSubsetSum.bitPart

  11. theorem OAI.LowSpaceSubsetSum.mem_fullPrefixBucket line 89
  12. theorem OAI.LowSpaceSubsetSum.reachesCompleted_of_fullPrefix_fits line 100

    Source documentation

    A fitting full-prefix bucket ensures that the designated path completes, even if larger ancestors overflow.

    theorem reachesCompleted_of_fullPrefix_fits (C : ℕ) (bits : MaskBits α)
    (depth fuel : ℕ) (e : α) (U : Finset α)
    (hfit : (fullPrefixBucket bits depth e fuel U).card ≤ C) :
    reachesCompleted C bits depth e fuel U := by
…

    Mentions: OAI.LowSpaceSubsetSum.MaskBits, OAI.LowSpaceSubsetSum.fullPrefixBucket, OAI.LowSpaceSubsetSum.reachesCompleted

  13. theorem OAI.LowSpaceSubsetSum.overflowNodes_capacity_bound line 110
  14. theorem OAI.LowSpaceSubsetSum.prefixTasks_le_overflowNodes line 127
  15. theorem OAI.LowSpaceSubsetSum.prefixTasks_capacity_bound line 141

    Source documentation

    Division-free version of the right task-start bound.

    theorem prefixTasks_capacity_bound (C : ℕ) (bits : MaskBits α)
    (depth fuel : ℕ) (U : Finset α) :
    C * prefixTasks C bits depth fuel U ≤ C + 2 * (fuel + 1) * U.card := by
…

    Mentions: OAI.LowSpaceSubsetSum.MaskBits, OAI.LowSpaceSubsetSum.prefixTasks

  16. theorem OAI.LowSpaceSubsetSum.completedEntries_le_card line 148
  17. theorem OAI.LowSpaceSubsetSum.potentialVisits_le_depth_mul_card line 164

    Source documentation

    Every occurrence has exactly one prefix at a fixed depth. The total potential work is charged by depth, even for occurrences later rejected.

    theorem potentialVisits_le_depth_mul_card (C : ℕ) (bits : MaskBits α)
    (depth fuel : ℕ) (U : Finset α) :
    potentialVisits C bits depth fuel U ≤ (fuel + 1) * U.card := by
…

    Mentions: OAI.LowSpaceSubsetSum.MaskBits, OAI.LowSpaceSubsetSum.potentialVisits

  18. theorem OAI.LowSpaceSubsetSum.rawVisits_le_depth_mul_card line 179

    Source documentation

    The occurrence bound is independent of deduplication and validity tests.

    theorem rawVisits_le_depth_mul_card {β : Type*}
    (C : ℕ) (bits : MaskBits α) (rawBits : MaskBits β)
    (depth fuel : ℕ) (U : Finset α) (T : Finset β) :
    rawVisits C bits rawBits depth fuel U T ≤ (fuel + 1) * T.card := by
…

    Mentions: OAI.LowSpaceSubsetSum.MaskBits, OAI.LowSpaceSubsetSum.rawVisits

  19. theorem OAI.LowSpaceSubsetSum.checkInputs_le line 198

    Source documentation

    Even charging the left array at every task bounds all actual final-check inputs. This includes every reuse of the same retained left array.

    theorem checkInputs_le (C L : ℕ) (hL : L ≤ C) (bits : MaskBits α)
    (depth fuel : ℕ) (U : Finset α) :
    completedEntries C bits depth fuel U + L * prefixTasks C bits depth fuel U ≤
      L + (2 * fuel + 3) * U.card := by
…

    Mentions: OAI.LowSpaceSubsetSum.MaskBits, OAI.LowSpaceSubsetSum.completedEntries, OAI.LowSpaceSubsetSum.prefixTasks