SourceAssignedParentVertexIntegral.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual simplex vertices satisfy the physical plane hypotheses. The original per-top packet integrals consequently hold on one common measurable good set, with only that top's bad event removed, and with the common terminal count used by finite-tree interpolation.

theorem OAI.LipschitzHilbert.SourceLabeledLattice.eventually_assigned_parent_vertex_integral line 17