OAI/Combinatorics/EditApproximation/Geometry/UnskippedBands.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Literal unskipped-band tests

The finite representative band, rational child envelopes and canonical rounded action are tested directly. A successful result carries exactly the facts checked by the algorithm; inaccurate seeds still produce a finite list of such tested records.

  1. theorem OAI.EditApproximation.UnskippedBand.envelope_pos line 35