step8
The step8 definition supplies the eight-fold iteration of any one-step defect-nonincreasing dynamics on an abstract state space. Lattice modelers working on discrete Navier-Stokes or cellular automata cite it to access the natural eight-tick stability window. It is realized as a direct abbreviation applying the iteration operator to the step component of the supplied OneStepDynamics record.
claimLet $dyn$ be a one-step dynamics on a state space $α$, consisting of a step map $s:α→α$ and a defect map $d:α→ℝ$ that is nonincreasing under $s$. The eight-step evolution operator is then $step8(dyn):=s^{[8]}$, the eight-fold composition of $s$.
background
The module formalizes the temporal side of the Navier-Stokes lattice program. Time is treated as discrete, making an 8-step window the natural stability unit; certificates over one window propagate to later windows by iteration. OneStepDynamics is an abstract structure packaging a step function, a defect functional, and the proof that defect is nonincreasing under one application of step. The defect functional originates from the LawOfExistence module where it equals the J-cost for positive arguments. Upstream results include the global step operation from CellularAutomata and the basic one constants from integer and rational constructions.
proof idea
This is a one-line definition that applies the iteration operator ^[8] directly to the step field of the input OneStepDynamics record.
why it matters in Recognition Science
This definition supplies the core operator for the eight-tick dynamics in the Navier-Stokes module. It feeds the EightTickCertificate structure and the propagation theorem eight_tick_certificate_propagates, which shows that one-window defect bounds extend to all later windows. It realizes the T7 eight-tick octave landmark of the Recognition Science forcing chain, where period 2^3 emerges as the stability unit in D=3.
scope and limits
- Does not specify the concrete state space or step rule for any particular dynamics.
- Does not prove that the defect remains bounded over infinite time.
- Does not connect to continuous Navier-Stokes equations.
- Does not establish existence of fixed points or cycles.
Lean usage
theorem example (dyn : OneStepDynamics α) (s : α) : dyn.defect (step8 dyn s) ≤ dyn.defect s := step8_defect_nonincreasing dyn sformal statement (Lean)
28def step8 {α : Type} (dyn : OneStepDynamics α) : α → α :=
proof body
Definition body.
29 dyn.step^[8]
30
31/-- Iterating a one-step defect-nonincreasing map preserves defect monotonicity. -/