OAI/Combinatorics/EditApproximation/Geometry/InitialConeGrid.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A rounded eligible center for each positive-cost query

This uses the actual natural division grid and the dyadic scale selected from the integer edit cost. It supplies a finite-family witness for the initial cone minimum.

  1. theorem OAI.EditApproximation.cost_dyadicScale line 22
  2. theorem OAI.EditApproximation.rounded_seedGrid_error line 33
  3. theorem OAI.EditApproximation.roundInterval_on_grid line 53
  4. theorem OAI.EditApproximation.rounded_initial_center_numeric line 57
  5. theorem OAI.EditApproximation.stateEditCost_distance_abs line 71
  6. theorem OAI.EditApproximation.rounded_initial_cone_witness line 86