OAI/Combinatorics/EditApproximation/Geometry/GatheredInputs.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

One local calculation gathers its distinct recursive inputs once. Subsequent scoring and optimizer iterations use the binary dictionary. The counters record oracle calls and actual persistent node writes.

  1. structure OAI.EditApproximation.GatheredInputs line 11
  2. def OAI.EditApproximation.gatherInputs line 16
  3. theorem OAI.EditApproximation.gatherInputs_calls line 24
  4. theorem OAI.EditApproximation.gatherInputs_writes line 30
  5. theorem OAI.EditApproximation.gatherInputs_lookup line 39
  6. theorem OAI.EditApproximation.gatherInputs_nodes line 58