OAI/Combinatorics/EditApproximation/Binary/BinaryRoundedReads.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Rounded canonical actions and their acceptance guards retain the literal initial-table reads used by each child-envelope computation.

  1. theorem OAI.EditApproximation.BinaryFraction.roundedBandReadWithWork_eq_cost line 16
  2. theorem OAI.EditApproximation.BinaryFraction.unskippedGuardReadWithWork_eq_cost line 37