OAI/Combinatorics/EditApproximation/Binary/BinaryBandReads.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Representative bands with charged child-table reads in every score and prefix predicate over the materialized wide grid.

  1. theorem OAI.EditApproximation.BinaryFraction.bandFromActionsReadWithWork_eq_cost line 17
  2. def OAI.EditApproximation.BinaryFraction.representativeReadOverhead line 45
  3. theorem OAI.EditApproximation.BinaryFraction.representativeFromActionsReadWithWork_eq_cost line 48
  4. theorem OAI.EditApproximation.BinaryFraction.preparedRepresentativeReadWithWork_eq_cost line 86