windowDynamics
plain-language theorem explainer
windowDynamics packages any one-step defect-nonincreasing dynamics into an equivalent eight-step operator by setting its step field to the eight-fold iteration of the original step map. Lattice researchers modeling discrete Navier-Stokes would cite it to treat the eight-tick window as the primitive time unit. The definition is a direct structure constructor that re-uses the input defect map and the already-established monotonicity lemma for the iterated step.
Claim. Let $D$ be a one-step dynamics on a state space with step map $s$, defect functional $d$, and the property that $d(s(x)) ≤ d(x)$ for every state $x$. The window dynamics $W(D)$ is the one-step dynamics whose step map is the eight-fold composition $s^{(8)}$, whose defect remains $d$, and which inherits the nonincreasing property from the eight-step iteration.
background
The module formalizes discrete-time evolution for the Navier-Stokes lattice program, taking the fundamental time quantum to be one tick in RS-native units. OneStepDynamics is the abstract carrier structure that bundles a step map, a real-valued defect, and the guarantee that each application of the step does not increase defect. The eight-tick window is the natural stability unit because the Recognition Science forcing chain identifies an eight-tick octave as the fundamental evolution period.
proof idea
The definition is a direct structure constructor. It sets the step field to the already-defined step8 operator applied to the input dynamics, copies the original defect field, and supplies the defect_nonincreasing field by direct appeal to step8_defect_nonincreasing.
why it matters
This definition supplies the eight-step operator iterated inside window_certificate_extends to obtain defect bounds over arbitrary numbers of windows. It therefore realizes the eight-tick octave as a concrete dynamics object, allowing certificates to propagate across repeated windows. In the broader framework it supplies the temporal side of the Navier-Stokes program by making the eight-tick cycle the primitive evolution unit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.