PhysicalProgramStateAccuracy.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Expected excess at every original physical table entry, under the same query-filtered global stream law.

theorem OAI.EditApproximation.rooted_refinement_budget_mono line 14
theorem OAI.EditApproximation.physicalProgram_expected_state_excess line 59
Source documentation
A pass of the actual rational recurrence has expected positive root error at most the actual edit cost divided by the computed small logarithm.
```
theorem physicalProgram_expected_state_excess :
    (∫ draw : Draw, max ((physicalRefinement source target U N P ell A T delta (choices draw)
      root S rootQ : ℝ) -
        stateEditCost (physicalSource source root) target rootQ) 0 ∂globalLaw) ≤
      (1 / (ell : ℝ)) * stateEditCost (physicalSource source root) target rootQ := by
…
```
Mentions: OAI.EditApproximation.physicalRefinement, OAI.EditApproximation.stateEditCost, OAI.EditApproximation.physicalSource