EightTickCertificate
plain-language theorem explainer
EightTickCertificate bundles a one-step dynamics record, an initial state, and the single inequality that defect after the 8-step operator is at most the starting defect. Discrete Navier-Stokes workers cite it to record the minimal data that lets one-window bounds iterate forward. The declaration is a pure structure definition that assembles the three fields without further computation.
Claim. An $8$-tick certificate on a state space $X$ consists of a one-step dynamics (a map $s:Xto X$ together with a defect map $d:Xtomathbb{R}$ satisfying $d(s(x))leq d(x)$ for all $x$), an initial state $x_0in X$, and the bound $d(s^8(x_0))leq d(x_0)$.
background
The module treats time as discrete with the fundamental tick $tau_0=1$ taken from Constants, making one octave exactly eight ticks. OneStepDynamics abstracts any discrete evolution equipped with a defect functional that is nonincreasing under a single step; the defect itself is the J-cost from LawOfExistence, which equals the hyperbolic expression for positive arguments. The local setting is therefore a lattice-time Navier-Stokes program in which an eight-tick window serves as the natural stability unit before certificates are propagated by iteration.
proof idea
The declaration is a pure structure definition with no computational body; it simply records the three fields (dynamics, initial state, and one-window inequality) that the downstream propagation theorem consumes.
why it matters
This structure supplies the input type for eight_tick_certificate_propagates, which lifts the one-window bound to every later window by repeated application of the step operator. It directly encodes the eight-tick octave (T7) of the forcing chain and anchors the temporal side of the Navier-Stokes lattice program. No open scaffolding is closed; the definition merely packages the minimal data required for forward propagation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.