OAI/Combinatorics/LowSpaceSubsetSum/Search/ComputedParentFuels.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Computed and cached parent loop limits

Only domain scans, two multiplicative binomial loops, and a doubling loop are run per leaf. No subset list is enumerated to obtain a loop limit.

  1. def OAI.LowSpaceSubsetSum.ComputedParentFuels.lengthAcc line 16
  2. theorem OAI.LowSpaceSubsetSum.ComputedParentFuels.lengthAcc_eq line 20
  3. def OAI.LowSpaceSubsetSum.ComputedParentFuels.powerAcc line 26
  4. theorem OAI.LowSpaceSubsetSum.ComputedParentFuels.powerAcc_eq line 30
  5. def OAI.LowSpaceSubsetSum.ComputedParentFuels.leaf line 38
  6. theorem OAI.LowSpaceSubsetSum.ComputedParentFuels.leaf_value line 52
  7. theorem OAI.LowSpaceSubsetSum.ComputedParentFuels.leaf_formula line 58

    Source documentation

    Closed form for the leaf count and its charged scalar-loop work.

    theorem leaf_formula (L : RepresentationLeaf (Fin n)) :
    leaf L =
      (L.top.card.choose L.topCount * L.mixer.card.choose L.localCount * 2^L.background.card,
        (RepresentationLeaf.domainSort L.top).2 + (RepresentationLeaf.domainSort L.mixer).2 +
        (RepresentationLeaf.domainSort L.background).2 + (2*L.top.card+1) +
        (2*L.mixer.card+1) + (2*L.background.card+1) +
        8*(CountedBinomial.run L.top.card L.topCount).steps +
        8*(CountedBinomial.run L.mixer.card L.localCount).steps +
        (3*L.background.card+1) + 12) := by
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationLeaf, OAI.LowSpaceSubsetSum.ComputedParentFuels.leaf, OAI.LowSpaceSubsetSum.RepresentationLeaf.domainSort, OAI.LowSpaceSubsetSum.CountedBinomial.run

  8. theorem OAI.LowSpaceSubsetSum.ComputedParentFuels.leaf_work line 70
  9. theorem OAI.LowSpaceSubsetSum.ComputedParentFuels.leaf_bound line 83
  10. structure OAI.LowSpaceSubsetSum.ComputedParentFuels.Values line 97
  11. def OAI.LowSpaceSubsetSum.ComputedParentFuels.run line 103

    Source documentation

    The four scalar counts are retained long enough to form both limits.

    def run (D : RepresentationParentData n) : Values × ℕ :=
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationParentData, OAI.LowSpaceSubsetSum.ComputedParentFuels.Values

  12. theorem OAI.LowSpaceSubsetSum.ComputedParentFuels.run_restrict line 112
  13. theorem OAI.LowSpaceSubsetSum.ComputedParentFuels.run_congr_leaves line 115
  14. theorem OAI.LowSpaceSubsetSum.ComputedParentFuels.lengthBound_eq line 119
  15. theorem OAI.LowSpaceSubsetSum.ComputedParentFuels.first_value line 123
  16. theorem OAI.LowSpaceSubsetSum.ComputedParentFuels.second_value line 128
  17. theorem OAI.LowSpaceSubsetSum.ComputedParentFuels.control_value line 133
  18. theorem OAI.LowSpaceSubsetSum.ComputedParentFuels.run_bounds line 138
  19. theorem OAI.LowSpaceSubsetSum.ComputedParentFuels.run_work line 152
  20. theorem OAI.LowSpaceSubsetSum.ComputedParentFuels.run_scale line 162