eight_tick_certificate_propagates
plain-language theorem explainer
If a one-step dynamics admits an 8-tick certificate (a single window where defect after step8 is at most the initial defect), then the defect remains non-increasing after any number of further 8-tick iterations. Lattice-model researchers working on discrete Navier-Stokes would cite the result to obtain long-term stability from a one-window check. The proof is a direct one-line application of the window-certificate extension theorem to the certificate's dynamics and initial state.
Claim. Let cert be an 8-tick certificate consisting of a one-step dynamics dyn, initial state s, and the bound defect(step8(dyn,s)) ≤ defect(s). Then for every natural number n, defect(((step8 dyn)^n)(s)) ≤ defect(s), where defect(x) := J(x) is the Recognition Science cost functional and step8 denotes the eight-fold iteration of the one-step map.
background
The Eight-Tick Discrete-Time Dynamics 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 all later windows by iteration. The defect functional is defined by defect(x) := J(x), the Recognition Science cost (zero at unity). An EightTickCertificate for type α packages a OneStepDynamics dyn, an initial state, and the one-window bound defect(step8 dyn initial) ≤ defect initial. The upstream theorem window_certificate_extends asserts that repeated 8-tick windows remain defect-nonincreasing: for any dyn, ∀ n s, defect(((step8 dyn)^[n]) s) ≤ defect(s), obtained by applying iterate_defect_nonincreasing to windowDynamics.
proof idea
The proof is a one-line wrapper: introduce the natural number n and apply the upstream theorem window_certificate_extends directly to cert.dyn, n, and cert.initial.
why it matters
The result guarantees that a single-window defect bound extends indefinitely, supporting the eight-tick octave (T7) in the forcing chain and the temporal side of the Navier-Stokes discretization. It closes the propagation step required once a finite-window certificate is obtained, feeding the broader claim that 8-tick stability units suffice for the lattice model. No downstream theorems are listed yet, but the declaration directly realizes the module's stated purpose that certificates propagate by iteration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.