PacketDataParentStoppedBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Parent-cone version of the stopped physical path estimate. The two literal physical reference events discharge the square and variation inputs of the stopped path estimate. The propagated unary residual and mass power estimates follow from the active mass path itself. The remaining local hypotheses concern marking and off-child amplitudes.

def OAI.LipschitzHilbert.PacketLatticeData.physicalParentStoppedBoundAt line 27
Source documentation
The exact physical stopped-path statement at one manuscript scale.
```
def physicalParentStoppedBoundAt (q D Cmass qoff A_M L : ℝ) (Klocal Hlocal : ℕ) : Prop :=
…
```
theorem OAI.LipschitzHilbert.PacketLatticeData.eventually_physical_parent_stopped_bound line 127