OAI/Combinatorics/EditApproximation/Queries/QueryInitialConeProgram.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The initial-cone program first reads its seed, constructs the actual raw-center list, gathers its answers, and executes the cached Boolean initial kernel with that finite buffer.

  1. def OAI.EditApproximation.queryInitialConeProgram line 22
  2. theorem OAI.EditApproximation.queryInitialConeProgram_refines line 26
  3. theorem OAI.EditApproximation.queryInitialConeProgram_work line 52