OAI/Combinatorics/EditApproximation/Geometry/ChargedTerminalCost.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Warmup and terminal queries have no same-index requests. Their charged seed reads strictly decrease the pass index, including coarse entries at pass zero.

  1. theorem OAI.EditApproximation.chargedWarmupQuery_same_cost_zero line 13
  2. theorem OAI.EditApproximation.chargedInitialQuery_same_cost_zero line 23