OAI/Combinatorics/EditApproximation/Binary/BinaryCellReads.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Reader-aware whole-cell construction. Every eligibility test reads its initial word, and every accepted band and selected action uses the counted reader kernels.

  1. theorem OAI.EditApproximation.filterMapWithWork_extra line 15
  2. theorem OAI.EditApproximation.BinaryFraction.cellCentersReadWithWork_eq_cost line 38
  3. def OAI.EditApproximation.BinaryFraction.preparedCellGroupReadWithWork line 71
  4. theorem OAI.EditApproximation.BinaryFraction.preparedCellGroupReadWithWork_eq line 83