Jcost
plain-language theorem explainer
Jcost defines the recognition cost as half the sum of a positive real and its reciprocal minus one. Researchers formalizing Navier-Stokes regularity via the phi-ladder cutoff cite it as the base cost function. The definition is a direct abbreviation that implements the T5 uniqueness condition from the forcing chain.
Claim. $J(x) := (x + x^{-1})/2 - 1$ for $x > 0$.
background
The module formalizes the algebraic core of the argument that the phi-ladder supplies an ultraviolet cutoff terminating the Navier-Stokes energy cascade on the RS discrete lattice. Main results listed include J non-negativity, J vanishing only at unity, positive strictly monotone phi-rungs, and monotone cascade depth in Reynolds number. The J-cost is introduced as the canonical recognition cost satisfying the normalization axiom J(1) = 0.
proof idea
The declaration is the direct definition of the cost function as the given algebraic expression. No lemmas are invoked; it functions as the primitive from which sibling results such as non-negativity and the zero-equivalence are derived.
why it matters
This supplies the J-cost used throughout the phi-ladder cutoff argument in the Navier-Stokes regularity paper. It realizes the T5 J-uniqueness step of the unified forcing chain, fixing J in the form required for the Recognition Composition Law and the eight-tick octave. It anchors the energy decay statements such as subDissipationDecayFactor_lt_one and the finite-rung count below any scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.