OAI/Combinatorics/EditApproximation/Geometry/ChargedGlobalQuery.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The global lazy program exposes coarse entries as ordinary memo requests. Warmup uses these explicit seed reads; positive internal refinement uses the proved finite table query, whose data reads are all earlier table entries.

  1. def OAI.EditApproximation.chargedRequestValue line 27
  2. theorem OAI.EditApproximation.chargedSeedQuery_localValue line 32
  3. theorem OAI.EditApproximation.chargedWarmupQuery_value line 52
  4. def OAI.EditApproximation.chargedGlobalQuery line 87
  5. theorem OAI.EditApproximation.localRequestValue_terminal line 107
  6. theorem OAI.EditApproximation.chargedGlobalQuery_value line 126
  7. def OAI.EditApproximation.chargedMemoEvaluate line 157
  8. theorem OAI.EditApproximation.chargedMemoEvaluate_value line 164