Jcost_le_self_of_one_le
plain-language theorem explainer
For real x at least 1 the J-cost satisfies J(x) ≤ x, where J is the canonical recognition cost (x + x inverse)/2 minus 1. Workers on finite-volume FRC bounds inside the Recognition Science treatment of Navier-Stokes regularity cite this estimate to close the lattice-to-conditional-completion bridge. The proof unfolds the definition of Jcost, invokes the reciprocal bound x inverse ≤ 1, applies transitivity to obtain x inverse ≤ x, and concludes by linear arithmetic.
Claim. For every real number $x$ with $x ≥ 1$, $J(x) ≤ x$ where $J(x) = (x + x^{-1})/2 - 1$.
background
The module Lattice FRC Bridge supplies the exact logical link between the lattice φ-ladder cutoff theorem and the hypothesis required by any conditional-completion route of the form FRC → injection damping → direction constancy → rigid rotation veto → regularity. Jcost is the recognition cost of an event, defined as the J-cost of its state; the upstream cost definitions in MultiplicativeRecognizerL4 and ObserverForcing both reduce to this same derivedCost on positive ratios. The normalizedRatio of a FiniteVolumeProfile is the quantity to which the bound is applied downstream.
proof idea
Term-mode proof that unfolds Jcost, obtains x inverse ≤ 1 from the standard reciprocal inequality for x ≥ 1, chains it with the hypothesis via le_trans from ArithmeticFromLogic, and finishes with linarith.
why it matters
This supplies the elementary comparison Jcost y ≤ y needed inside finiteVolume_Jcost_bound to reach the explicit lattice bound Jcost(normalizedRatio s) ≤ sqrt(siteCount). It therefore closes the finite-volume recognition-cost step that the module doc-comment identifies as the bridge from the φ-ladder cutoff to the Navier-Stokes conditional-completion hypothesis. The result sits inside the eight-tick octave and D = 3 setting of the overall forcing chain but adds no new structural content beyond the half-line estimate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.