OAI/Combinatorics/EditApproximation/Binary/BinaryGeometrySpace.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Endpoint geometry and actual finite score/minimum scans retain all arithmetic scratch and all callback read invocations.

  1. theorem OAI.EditApproximation.BinaryFraction.distanceAllocation_le_work line 15
  2. theorem OAI.EditApproximation.BinaryFraction.connectionTermsAllocation_le_work line 24
  3. theorem OAI.EditApproximation.BinaryFraction.connectionAllocation_le_work line 44
  4. theorem OAI.EditApproximation.BinaryFraction.endpointDistanceAllocation_le_work line 55
  5. theorem OAI.EditApproximation.BinaryFraction.endpointConnectionAllocation_le_work line 67
  6. theorem OAI.EditApproximation.BinaryFraction.stateGapAllocation_le_work line 77
  7. theorem OAI.EditApproximation.BinaryFraction.endpointScoreReadAllocation_le_work line 87
  8. theorem OAI.EditApproximation.BinaryFraction.wideMinimumReadAllocation_le_work line 105
  9. def OAI.EditApproximation.BinaryFraction.distanceInvocations line 121
  10. theorem OAI.EditApproximation.BinaryFraction.distanceInvocations_le_work line 123
  11. def OAI.EditApproximation.BinaryFraction.connectionTermsInvocations line 130
  12. theorem OAI.EditApproximation.BinaryFraction.connectionTermsInvocations_le_work line 136
  13. def OAI.EditApproximation.BinaryFraction.connectionInvocations line 152
  14. theorem OAI.EditApproximation.BinaryFraction.connectionInvocations_le_work line 157
  15. def OAI.EditApproximation.BinaryFraction.endpointDistanceInvocations line 166
  16. theorem OAI.EditApproximation.BinaryFraction.endpointDistanceInvocations_le_work line 171
  17. def OAI.EditApproximation.BinaryFraction.endpointConnectionInvocations line 181
  18. theorem OAI.EditApproximation.BinaryFraction.endpointConnectionInvocations_le_work line 185
  19. def OAI.EditApproximation.BinaryFraction.stateGapInvocations line 193
  20. theorem OAI.EditApproximation.BinaryFraction.stateGapInvocations_le_work line 197
  21. def OAI.EditApproximation.BinaryFraction.endpointScoreReadInvocations line 205
  22. theorem OAI.EditApproximation.BinaryFraction.endpointScoreReadInvocations_le_work line 213
  23. def OAI.EditApproximation.BinaryFraction.wideMinimumReadInvocations line 229
  24. theorem OAI.EditApproximation.BinaryFraction.wideMinimumReadInvocations_le_work line 239