OAI/Combinatorics/EditApproximation/Binary/BitMemoStorage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Storage of the actual binary-word memo. Node paths are identical to the rational evaluator, while stored numerator/denominator bits are bounded using the deterministic returned-word invariant.

  1. theorem OAI.EditApproximation.BinaryMemo.fractionStorage_le line 18
  2. theorem OAI.EditApproximation.rankedBitMemoEvaluate_widths line 46
  3. theorem OAI.EditApproximation.rankedBitMemoEvaluate_nodes_bound line 96