TimeStep
plain-language theorem explainer
A structure supplying a positive real time increment Δt (default 1) for discrete fluid approximations. Researchers building Recognition Science to Navier-Stokes bridges cite it when assembling the minimal interface that later links to LNAL execution and CPM defect accounting. The declaration is a direct structure with an accompanying positivity predicate.
Claim. A time step is a real number $Δt > 0$, defaulting to 1.
background
The module supplies the minimal interface for a discrete Navier-Stokes approximation without committing to Galerkin or grid methods. It introduces TimeStep as the basic time unit to be related downstream to LNAL spatial semantics and CPM instantiations of defect and energy. The module doc states the file deliberately avoids choosing a discretization family so that concrete models can be added later.
proof idea
Direct structure definition that introduces the field Δt with default value 1, followed by the one-line predicate TimeStep.Valid asserting positivity.
why it matters
Supplies the time discretization parameter to RSNSBridgeSpec and DiscreteModel. It completes the discrete-time slot in the classical-bridge interface, connecting to the eight-tick octave and J-cost structures from the foundation. It leaves open the concrete choice of spatial discretization (e.g., Galerkin on 𝕋²).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.