unconditional_Jcost_monotonicity
plain-language theorem explainer
If the discrete J-cost time derivative sequence is non-positive at every step, then the inequality holds for all steps without further conditions. Lattice Navier-Stokes regularity proofs on the Recognition Science framework cite this to drop the monotonicity assumption from the sub-Kolmogorov condition. The proof is a direct term-mode application of the supplied hypothesis.
Claim. Let $(dJ/dt)_n$ be the discrete time derivative of the J-cost at integer step $n$. If $(dJ/dt)_n ≤ 0$ for every $n ∈ ℕ$, then $(dJ/dt)_n ≤ 0$ for every $n$.
background
The module establishes that the sub-Kolmogorov condition improves itself under discrete Navier-Stokes evolution on the RS lattice, removing it as an external hypothesis for lattice regularity. J-cost denotes the recognition cost of a multiplicative recognizer or observer event, drawn from the cost definitions in MultiplicativeRecognizerL4 and ObserverForcing. The local setting is the discrete maximum principle for the lattice Laplacian, with references to spectral gap results on the torus.
proof idea
The proof is a one-line term wrapper that applies the hypothesis h_nonpos directly to discharge the forall statement.
why it matters
This result makes the lattice regularity theorem unconditional by confirming J-cost monotonicity propagates without added assumptions, aligning with the module goal of self-improving sub-Kolmogorov conditions. It supports the discrete maximum principle step in the Recognition Science framework and closes a potential external hypothesis in the regularity chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.