H_jcost_monotoneOn
plain-language theorem explainer
The shifted recognition cost built from J is nondecreasing on [0, ∞). Anyone running the order-based uniqueness argument for J cites this as the non-vacuity witness: without it the monotone class would be empty. The proof identifies the shifted cost with cosh and invokes the standard cosh monotonicity lemma on the nonnegative ray.
Claim. Let $J(x)=\frac{x+x^{-1}}{2}-1$ be the recognition cost and let $H$ be its log-domain shift (so that $H(J)(t)=\cosh t$). Then $t\mapsto H(J)(t)$ is monotone on $[0,\infty)$.
background
In the Recognition Composition Law setting the raw cost is $J(x)=\frac{x+x^{-1}}{2}-1$. The shifted cost $H=J+1$ converts the RCL into d'Alembert's functional equation $H(xy)+H(x/y)=2H(x)H(y)$. In log coordinates $x=e^t$ one has $H(J)(t)=\cosh t$.
The module develops a monotone-only route to the cosh family: additive monotone maps are linear, d'Alembert solutions that are monotone on $[0,\infty)$ are forced into the cosh shape, and composition-law costs with a monotone log transform are thereby pinned down. The present lemma simply checks that the canonical $J$ itself meets that monotone hypothesis.
Upstream, H is defined as the shift $J\mapsto J+1$ (equivalently $\frac12(x+x^{-1})$ on the multiplicative side), and Jcost is the standard RS recognition cost of a positive ratio.
proof idea
One algebraic identification plus a library lemma. First rewrite: pointwise, $H(Jcost)=t\mapsto\cosh(1\cdot t)$, via the existing identity H_jcost_eq_cosh and one_mul. After substituting that equality, the claim reduces to monotonicity of $t\mapsto\cosh(c t)$ on $[0,\infty)$ for $c=1>0$, which is cosh_mul_monotoneOn discharged by norm_num.
why it matters
This is the non-vacuity witness for the entire order route. Downstream, jcost_forced_by_order takes reciprocal symmetry, normalization, the composition law, unit calibration, and monotone-on-$[0,\infty)$ of the shifted cost, and concludes the cost equals $J$ on the positives, with no continuity or lub argument. The doc-comment on that parent theorem states it is "the theorem the forcing chain's T5 rung now cites."
T5 in the UnifiedForcingChain is J-uniqueness: $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). The older scale-family proof law_of_logic_forces_jcost_monotone already gave the same conclusion but could not be named from below the completion layer; this monotone package fixes that layering. Without the present lemma the monotone hypothesis class would be empty and T5's order route would be vacuous.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.