OAI/Combinatorics/EditApproximation/Binary/BinaryLocalGroupReads.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The physical query's outer whole-cell loops use the same dyadic scales and exact Fin-count draws, with explicit initial-table lookups.

  1. def OAI.EditApproximation.BinaryFraction.preparedComputedCellReadWithWork line 21
  2. theorem OAI.EditApproximation.BinaryFraction.preparedComputedCellReadWithWork_eq line 31
  3. def OAI.EditApproximation.BinaryFraction.preparedLocalGroupScaleReadWithWork line 45
  4. theorem OAI.EditApproximation.BinaryFraction.preparedLocalGroupScaleReadWithWork_eq line 60
  5. def OAI.EditApproximation.BinaryFraction.preparedLocalCellGroupsReadWithWork line 78
  6. theorem OAI.EditApproximation.BinaryFraction.preparedLocalCellGroupsReadWithWork_eq line 93