Jcost_nonincreasing
plain-language theorem explainer
If a real-valued sequence on the naturals satisfies J_{n+1} ≤ J_n at every step, then the entire sequence remains bounded above by its initial term. This monotonicity fact is invoked inside the master lattice regularity theorem for discrete Navier-Stokes on the RS lattice. The argument is a direct induction that applies only reflexivity and transitivity of the order relation.
Claim. Let $(J_n)_{n∈ℕ}$ be a sequence of real numbers such that $J_{n+1}≤J_n$ for every natural number $n$. Then $J_n≤J_0$ for all $n$.
background
The Discrete Maximum Principle module establishes that the sub-Kolmogorov condition is self-improving under discrete Navier-Stokes evolution on the finite RS lattice, rendering the regularity result unconditional. The J-cost is the cumulative quantity whose monotonicity controls the discrete gradient energy and thereby excludes vorticity blow-up. The module documentation states that bounded J-cost follows once the initial sub-Kolmogorov condition holds and the one-step contraction is verified by the discrete operator. Upstream, the proof relies only on the basic order lemmas le_refl and le_trans imported from ArithmeticFromLogic, which supply reflexivity and transitivity for the real numbers.
proof idea
The proof proceeds by induction on the time index n. The base case n=0 is immediate from reflexivity of ≤. The successor case applies the given one-step inequality at k and then uses transitivity to chain the result back to the initial value.
why it matters
This lemma is applied directly by master_lattice_regularity, the theorem that concludes unconditional regularity on the RS lattice by propagating the sub-Kolmogorov condition and obtaining a uniform bound on J-cost. It supplies the monotonicity step required to convert the discrete maximum principle into a global bound that prevents blow-up, consistent with the self-improving property described in the module. In the Recognition framework it supports the discrete analogue of the maximum principle that leads to D=3 regularity without external hypotheses beyond finite initial energy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.