OAI/Combinatorics/EditApproximation/Geometry/ChargedSeedQuery.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A pass-zero seed read requests a cached coarse entry. Later seed reads request the previous pass's final table value in each distinct copy. Thus neither kind of seed value enters the charged program as a free oracle.

  1. theorem OAI.EditApproximation.chargedSeedQuery_value line 20
  2. theorem OAI.EditApproximation.chargedSeedQuery_cost line 36