ActualDenseIntegration.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual physical stopped-mass probabilities from the proved canonical sections and the actual normalized restarted witnesses. All restrictions on the old marked state lie in the stopped past.

theorem OAI.SLEExactGauge.actual_dense_sections_integrate line 22