OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/ExpandingFiniteRetention.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Successive concentration estimates compose along every finite recorder execution. Only the proved per-stage diffusion losses accumulate.

  1. theorem OAI.ForcedComputation.ExpandingDetector.recorder_steps_mass_retention line 13