step8_defect_nonincreasing
plain-language theorem explainer
The theorem shows that the eight-step evolution map on any one-step dynamics never increases the defect measure. Lattice fluid models cite it to treat an eight-tick window as a stable unit whose certificates carry forward. The proof is a one-line wrapper that invokes the general iteration lemma after unfolding the definition of the eight-step operator.
Claim. Let $d$ be the defect functional of a one-step dynamics whose single step is defect-nonincreasing. Then $d(s_8) ≤ d(s)$ for every state $s$, where $s_8$ denotes the state obtained by applying the step operator eight times.
background
OneStepDynamics is the structure consisting of a step map $α → α$, a defect map $α → ℝ$, and the axiom that defect(step s) ≤ defect s for all s. The defect functional itself is the J-cost from the Law of Existence, which equals zero at unity. The module treats time as discrete for the Navier-Stokes lattice program, taking the eight-tick window (period $2^3$) as the natural stability unit whose certificates propagate by iteration.
proof idea
One-line wrapper that applies iterate_defect_nonincreasing dyn 8 s after the simpa tactic unfolds the definition of step8.
why it matters
The result supplies the defect_nonincreasing field inside the windowDynamics definition, so the eight-step map itself becomes a OneStepDynamics. It realizes the eight-tick octave (T7) of the forcing chain and ensures that defect certificates remain valid across repeated windows in the discrete Navier-Stokes setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.