OAI/Combinatorics/EditApproximation/Geometry/InitialCones.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Rational scaled seeds and the actual cone lower invariant

Ceilings preserve the upper bound because F*c is an integer. Cone lower bounds use the actual edit-distance and signed-length geometry, rather than an assumed lower-bound-preserving cone oracle.

  1. theorem OAI.EditApproximation.rationalStateGap_cast line 20
  2. theorem OAI.EditApproximation.scaledSeedValue_bounds line 27
  3. theorem OAI.EditApproximation.scaledSeedValue_zero line 44
  4. theorem OAI.EditApproximation.initialConeValue_actual_lower line 49