OAI/Combinatorics/EditApproximation/Binary/BinaryInitialReads.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Inline initial-cone evaluation reads the gathered previous-pass seed words explicitly. Each query seed is loaded once per routine and each visited center load contributes its measured lookup cost.

  1. def OAI.EditApproximation.BinaryFraction.initialGridPlainWithWork line 18
  2. theorem OAI.EditApproximation.BinaryFraction.initialGridReadWithWork_eq_cost line 26
  3. theorem OAI.EditApproximation.BinaryFraction.initialCentersReadWithWork_eq_cost line 45
  4. theorem OAI.EditApproximation.BinaryFraction.initialConeReadWithWork_eq_cost line 68
  5. theorem OAI.EditApproximation.BinaryFraction.initialMinimumReadWithWork_eq_cost line 85
  6. theorem OAI.EditApproximation.BinaryFraction.initialProgramReadWithWork_eq_cost line 122
  7. theorem OAI.EditApproximation.BinaryFraction.finishCachedWithWork_read_factor line 140
  8. theorem OAI.EditApproximation.BinaryFraction.cachedInitialProgramReadWithWork_eq_cost line 155