OAI/Combinatorics/EditApproximation/Refinement/PhysicalRequestGrid.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The canonical cache grid for every request, including terminal and warmup branches. This invariant holds for all incoming seeds and draws.

  1. theorem OAI.EditApproximation.localRequestValue_den_dvd line 15
  2. theorem OAI.EditApproximation.chargedRequestValue_den_dvd line 32