OAI/Combinatorics/EditApproximation/Geometry/ComparisonLift.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual physical tables on the stopped comparison tree. Stopped states retain their exact cost while the complete-tree representation carries them forward.

  1. def OAI.EditApproximation.stoppedComparisonValue line 15
  2. def OAI.EditApproximation.comparisonPhysicalLift line 23
  3. theorem OAI.EditApproximation.stoppedComparisonValue_physical line 33
  4. theorem OAI.EditApproximation.comparisonPhysicalLift_root line 47
  5. theorem OAI.EditApproximation.comparisonPhysicalLift_step_active line 60
  6. theorem OAI.EditApproximation.stoppedComparisonValue_step_stopped line 91
  7. theorem OAI.EditApproximation.comparisonPhysicalLift_terminal line 108