OAI/Combinatorics/EditApproximation/Geometry/LocalGrid.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Direct enumeration of a local grid square

The algorithm enumerates bounded ranges of grid indices. It does not scan the unrelated target positions. The completeness theorem includes boundary states and intervals with equal endpoints.

  1. theorem OAI.EditApproximation.gridPointsBetween_complete line 20
  2. theorem OAI.EditApproximation.gridPointsBetween_sound line 30
  3. theorem OAI.EditApproximation.gridPointsBetween_length line 39
  4. theorem OAI.EditApproximation.gridPointsBetween_length_le line 43
  5. theorem OAI.EditApproximation.localTargetStates_complete line 68
  6. theorem OAI.EditApproximation.localTargetStates_length_le line 84