H_Jcost_monotoneOn
plain-language theorem explainer
The shifted recognition cost attached to J coincides with cosh and is therefore monotone on the nonnegative reals. Anyone running the completeness-free monotone forcing route for the native cost cites this regularity fact. The proof rewrites the shifted cost to cosh and inherits monotonicity from the standard strict increase of cosh on [0, ∞).
Claim. The log-coordinate transform $H(J)$ of the recognition cost $J(x)=\frac{x+x^{-1}}{2}-1$ is monotone on $[0,\infty)$. Equivalently, $H(J)$ agrees with $\cosh$ on that ray, so $0\le a\le b$ implies $H(J)(a)\le H(J)(b)$.
background
In Recognition Science the native cost is $J(x)=\frac{x+x^{-1}}{2}-1$ on positive reals (forcing landmark T5). The shifted cost $H=J+1$ rewrites the Recognition Composition Law as d'Alembert's equation $H(xy)+H(x/y)=2H(x)H(y)$. Upstream, CostAlgebra records $H(x)=J(x)+1=\frac12(x+x^{-1})$ and notes that under $H$ the RCL becomes the standard d'Alembert equation.
The FunctionalEquation layer presents $H\circ J$ in a log coordinate, where it becomes ordinary $\cosh$. Monotonicity of this transform on $[0,\infty)$ is exactly the completeness-free regularity hypothesis demanded by the monotone forcing theorems in this module.
The local setting is PRCNativeCostUniqueness: show that algebraic identities plus order regularity alone force the native recognition cost, without analytic completeness assumptions.
proof idea
Short term-mode argument. Introduce $a,b\ge 0$ with $a\le b$. Rewrite both occurrences of the shifted cost via the identity that $H(J)$ equals $\cosh$. The goal reduces to monotonicity of $\cosh$ on $[0,\infty)$, which is the monotone-on projection of Real.cosh_strictMonoOn.
why it matters
Discharges the monotonicity hypothesis of the non-vacuity capstone that forces $J$ by monotonicity. That parent applies the completeness-free theorem placing any cost with reciprocal symmetry, normalization, the composition law, and log-transform monotonicity into the scale family $\mathrm{costLambda},c$; calibration $c=1$ recovers $J$ exactly. As its doc-comment puts it: the order-only forcing route is therefore not merely abstract, it forces the actual recognition cost.
Also feeds the successor-increment limit for the whole scale family, which shows the discrete $\delta$-act ladder sees exactly the calibration invariant $c^2$. In the forcing chain this underwrites T5 (J-uniqueness via $J(x)=\cosh(\log x)-1$) and confirms the RCL-plus-order route is inhabited by the genuine native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.