OAI/Combinatorics/EditApproximation/Binary/BinaryCellCentersWork.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Complete work for a whole-cell representative scan, including both endpoint grids and every initial-value eligibility test.

  1. theorem OAI.EditApproximation.BinaryFraction.flatMap_length_bound line 13
  2. theorem OAI.EditApproximation.BinaryFraction.cellStatesWithWork_length line 25
  3. def OAI.EditApproximation.BinaryFraction.cellCentersBitBudget line 37
  4. theorem OAI.EditApproximation.BinaryFraction.cellCentersWithWork_cost line 42
  5. theorem OAI.EditApproximation.BinaryFraction.cellCentersBitBudget_mono_count line 95
  6. theorem OAI.EditApproximation.BinaryFraction.cellCentersWithWork_uniform_cost line 100