OAI/Combinatorics/EditApproximation/Geometry/InitialInputBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The local initial cone uses a bounded number of preceding-seed queries on every clamped seed, independently of an accuracy event.

  1. theorem OAI.EditApproximation.localTargetStates_length_from_scale line 11
  2. theorem OAI.EditApproximation.localInitialConeCenters_length line 27