OAI/Combinatorics/EditApproximation/Geometry/ConeLocality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The numerical locality test for initial cones

Any globally minimizing cone at a positive-cost query lies in the algorithm's finite local scale interval and search radius. The inequalities below use the actual seed factor and cone slope from Section 4.

  1. theorem OAI.EditApproximation.initial_cone_locality_numeric line 15