OAI/Combinatorics/EditApproximation/Binary/BinaryBufferInputBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A refinement continuation has a separate current-index buffer. Only the earlier-history buffer enters the online objective, so its range invariant does not require any relation at unused current keys.

  1. theorem OAI.EditApproximation.BinaryFraction.PreparedKernelNumericBounds.with_independent_cached_values line 13