OAI/Combinatorics/EditApproximation/Geometry/RoundedComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual rounded comparison actions

An optimal balanced alignment at the rounded representative is rounded on the same integer grid. This produces a shared-endpoint wide action and the manuscript's multiplicative cost growth, with all empty children retained as labeled coordinates.

  1. theorem OAI.EditApproximation.rounded_comparison_action line 20