OAI/Combinatorics/EditApproximation/Geometry/SourceErasure.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Removing already fixed source answers is a proof operation on a query. It preserves the table trace and separates source/table charges; the implementation continues to cache and sample explicit source keys.

  1. def OAI.EditApproximation.FiniteQuery.eraseSources line 13
  2. theorem OAI.EditApproximation.FiniteQuery.eraseSources_value line 18
  3. theorem OAI.EditApproximation.FiniteQuery.eraseSources_cost line 29
  4. theorem OAI.EditApproximation.FiniteQuery.eraseSources_keys_all line 40
  5. theorem OAI.EditApproximation.FiniteQuery.cost_add_weights line 62
  6. theorem OAI.EditApproximation.FiniteQuery.cost_mul_weight line 70
  7. theorem OAI.EditApproximation.FiniteQuery.cost_source_table line 78