OAI/Combinatorics/EditApproximation/Queries/QueryInitialConeCenters.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The initial-cone gather uses the unfiltered center list: a seed at a center must be read before the eligibility test at that center is known.

  1. theorem OAI.EditApproximation.BinaryFraction.queryInitialConeCentersWithWork_value line 15
  2. theorem OAI.EditApproximation.BinaryFraction.queryInitialSeedReadWithWork_value line 34
  3. theorem OAI.EditApproximation.BinaryFraction.cachedInitialProgramReadWithWork_value_only line 45