OAI/Combinatorics/EditApproximation/Geometry/StateGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The finite domain of valid target states

The endpoint domain is enumerated by actual bounded natural loops. A state's true cost and signed length gap use the stored target substring.

  1. theorem OAI.EditApproximation.targetStates_complete line 22
  2. theorem OAI.EditApproximation.natural_distance_cast line 31
  3. def OAI.EditApproximation.stateEditCost line 39
  4. def OAI.EditApproximation.stateLengthGap line 42
  5. theorem OAI.EditApproximation.stateLengthGap_actual line 45
  6. theorem OAI.EditApproximation.stateEditCost_length_lower line 53
  7. theorem OAI.EditApproximation.stateEditCost_spatial line 59
  8. theorem OAI.EditApproximation.stateLengthGap_spatial line 73