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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Conditional scalar construction with a quantitative bound along every actual recorder prefix. The sole analytic assumption is the stated published scalar existence input.

  1. theorem OAI.ForcedComputation.ExpandingDetector.expanding_scalar_retention line 16