OAI/NumberTheory/DukePrimeDegree/Entropy/WholeFutureStationarity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Global stationarity of the actual whole-future kernel

The countable family of genuine quotient boxes covers each bounded future fiber. Local mass-containment events therefore cover almost every point, and their stationary restrictions glue to the ambient measure.

  1. theorem OAI.DukePrimeDegree.RootPrefixCoordinates.wholeFutureKernel_stationary line 26