StageComparisonEnergy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual averaged warmup supplies the local mass and energy charges.

theorem OAI.EditApproximation.stateLengthGap_difference line 12
theorem OAI.EditApproximation.stageComparison_positive_movement line 40
Source documentation
The rounded representative has positive true cost, and its movement is smaller than the actual parent averaged warmup mass.
```
theorem stageComparison_positive_movement
    (hscale : 2 * (refinementFactor A F : ℝ) ≤ P) :
    let b := 2 ^ Nat.log 2 (stateEditCost (physicalSource source node) target q)
…
```
Mentions: OAI.EditApproximation.refinementFactor, OAI.EditApproximation.stateEditCost, OAI.EditApproximation.physicalSource
theorem OAI.EditApproximation.stageComparison_energy line 83
Source documentation
No local energy or discrepancy hypothesis is assumed: these are the charges of the input-determined comparison children and the actual warmup.
```
theorem stageComparison_energy
    (hleaf : ¬ (physicalSourceInterval source.length node).hi -
      (physicalSourceInterval source.length node).lo ≤ 1)
    (hscale : 2 * (refinementFactor A F : ℝ) ≤ P) :
    let parent := physicalSourceInterval source.length node
…
```
Mentions: OAI.EditApproximation.physicalSourceInterval, OAI.EditApproximation.refinementFactor