OAI/Combinatorics/EditApproximation/Geometry/RefinementBufferRanges.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual earlier-history gather projects into the child-initial gather. Consequently its default-zero word table retains the required history bounds, even at coordinates absent from both finite buffers.

  1. theorem OAI.EditApproximation.queryEarlierInputCover_initial line 12
  2. theorem OAI.EditApproximation.BinaryFraction.gatheredRefinementHistory_range line 29