OAI/Analysis/LipschitzHilbert/Packets/PacketDataAssignedParentPhysicalPlane.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Literal physical reference events imply the original per-top plane bound. The stopped-path comparison and all inhabited-model transports are proved before applying the plane integral theorem.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.eventually_assigned_parent_physical_plane_integral line 15