OneStepDynamics
plain-language theorem explainer
OneStepDynamics packages an abstract discrete dynamical system on type α together with a real-valued defect that is nonincreasing under iteration. Lattice Navier-Stokes researchers cite the structure when constructing 8-tick stability certificates and window propagations. It is introduced directly as a three-field record with no computational obligations or lemmas.
Claim. A one-step dynamics on a set $α$ consists of a map $s:α→α$ and a defect function $d:α→ℝ$ satisfying $d(s(x))≤d(x)$ for all $x∈α$.
background
The module treats time as discrete so that an 8-step window becomes the natural stability unit for the Navier-Stokes lattice program. Certificates over one window then propagate to later windows by iteration. The defect functional is taken from LawOfExistence, where defect(x) equals J(x) for positive x and J is the recognition cost. The step operation is taken from CellularAutomata, where step applies a local rule globally to produce the successor tape.
proof idea
The declaration is a structure definition that directly records the three components: the step function, the defect map, and the monotonicity condition. No lemmas or tactics are invoked; the record serves as the interface for all downstream 8-tick constructions.
why it matters
OneStepDynamics supplies the abstract interface used by EightTickCertificate to certify single 8-step windows and by windowDynamics to lift the dynamics to the 8-tick level. It connects to the eight-tick octave (T7) in the forcing chain and supports the discrete treatment of Navier-Stokes evolution. The structure closes the gap between single-step cellular automata and multi-tick certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.