Jcost_nonincreasing
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.
claimLet $(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 in Recognition Science
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.
scope and limits
- Does not derive the one-step inequality Jcost(n+1)≤Jcost(n); that must be supplied by the discrete NS operator.
- Applies only to sequences indexed by natural numbers and does not address continuous-time limits.
- Uses only the standard order on the reals; no RS-specific constants or phi-ladder structure appear.
- Does not establish boundedness of the J-cost sequence, only monotonicity under the step hypothesis.
Lean usage
have hmono : ∀ n, Jcosts n ≤ Jcosts 0 := Jcost_nonincreasing Jcosts h_Jcost_stepformal statement (Lean)
151theorem Jcost_nonincreasing
152 (Jcost_seq : ℕ → ℝ)
153 (h_step : ∀ n, Jcost_seq (n + 1) ≤ Jcost_seq n) :
154 ∀ n, Jcost_seq n ≤ Jcost_seq 0 := by
proof body
Term-mode proof.
155 intro n
156 induction n with
157 | zero => exact le_refl _
158 | succ k ih => exact le_trans (h_step k) ih
159
160/-- Master theorem: unconditional regularity on the RS lattice.
161
162Given a discrete NS flow on the finite lattice:
1631. The initial velocity gradient is finite (automatic on a finite lattice).
1642. The discrete maximum principle ensures viscous contraction dominates
165 advection growth whenever the sub-Kolmogorov condition holds.
1663. The sub-Kolmogorov condition at t=0 follows from (1) and the fact
167 that nu/(C*h^2) is astronomically large on the RS lattice.
1684. The self-improving property propagates (2) to all future times.
1695. Therefore the J-cost is monotonically non-increasing for all time.
1706. Bounded J-cost excludes vorticity blow-up.
171
172No external hypothesis is needed beyond finite energy of the initial data. -/