TimeStep
TimeStep supplies the positive real time increment for discrete Navier-Stokes approximations in the Recognition Science classical bridge. Researchers assembling RSNSBridgeSpec or DiscreteModel cite it to fix the time discretization parameter before relating the model to LNAL semantics or CPM tests. The declaration is a bare structure with default value 1 together with a separate positivity predicate.
claimA time step is a structure containing a real number $Δt$ (default value 1) required to satisfy $Δt > 0$.
background
The module ClassicalBridge.Fluids.Discrete supplies a minimal interface for discrete Navier-Stokes approximations without committing to Galerkin or grid methods. It prepares the connection to LNAL spatial execution semantics and CPM defect/energy tests. TimeStep is the time-increment object in that interface.
proof idea
The declaration is a direct structure definition with a single field carrying default value 1. The associated Valid predicate is introduced as the proposition 0 < h.Δt.
why it matters in Recognition Science
TimeStep populates the dt field inside RSNSBridgeSpec and is referenced by DiscreteModel. It supplies the time component of the discrete model interface that later links to the Recognition Science forcing chain (T5–T8) and the eight-tick octave. Downstream files are expected to instantiate a concrete discretization family.
scope and limits
- Does not prescribe any numerical value for Δt beyond positivity.
- Does not select a spatial discretization method (Galerkin versus grid).
- Does not impose stability or CFL-type restrictions on Δt.
- Does not embed Δt into the phi-ladder or J-cost formulas.
formal statement (Lean)
32structure TimeStep where
33 Δt : ℝ := 1
proof body
Definition body.
34
35def TimeStep.Valid (h : TimeStep) : Prop := 0 < h.Δt
36
37/-- High-level choice of discretization family. -/