Jcost_forced_by_monotonicity
plain-language theorem explainer
The recognition cost J lies in the forced scale family costLambda for some real c: on positives, J(x) equals costLambda(c,x). Anyone using the order-only (monotonicity) route to J-uniqueness cites this non-vacuity check. The proof is a direct application of the monotone composition-law forcing lemma, discharging reciprocal symmetry, unit normalization, the d'Alembert form of the composition law, and monotonicity of J's log-transform.
Claim. There exists $c \in \mathbb{R}$ such that for all $x > 0$, the recognition cost $J(x) = \frac{x+x^{-1}}{2}-1$ equals the scaled cost $\mathrm{costLambda}(c,x)$.
background
In Recognition Science the load-bearing cost is $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. Its shift $H(x)=J(x)+1=\frac12(x+x^{-1})$ turns the Recognition Composition Law into the classical d'Alembert equation $H(xy)+H(x/y)=2H(x)H(y)$.
The module develops a completeness-free uniqueness route: any reciprocal-symmetric, normalized cost obeying the composition law whose log-transform is monotone on $[0,\infty)$ must lie in a one-parameter scale family $\mathrm{costLambda},c$. The continuum argument uses continuity; here monotonicity of the log-transform replaces that hypothesis.
This result is the non-vacuity check: the actual recognition cost $J$ meets every hypothesis of the monotone forcing lemma, so $J$ itself sits in the forced family on $(0,\infty)$.
proof idea
Term-mode one-shot application of composition_law_monotone_forces_costLambda to $J$. Four side conditions are discharged in place:
- Reciprocal symmetry $J(x^{-1})=J(x)$, by simplification and ring.
- Normalization $J(1)=0$, by
norm_num. - Composition law, by transporting the known cosh-addition identity for $J$ through the equivalence between the composition law and the cosh-add form.
- Monotonicity of the log-transform, via the named lemma
H_Jcost_monotoneOn.
No calibration step appears here; existence of some scale $c$ is the whole claim.
why it matters
Non-vacuity capstone for the order-only forcing of $J$, the completeness-free analogue of the continuity-based law-of-logic result. It anchors the T5 landmark (J-uniqueness) on monotonicity rather than continuum hypotheses: no completeness, no continuity, and no derivative-of-a-limit on $\mathbb{R}$.
Downstream, costLambda_successor_increment_tendsto generalizes the discrete $\delta$-act ladder asymptotics from the pure-$J$ case to the whole forced scale family, showing the leading per-step coefficient tends to $c^2/2$. That argument needs $J$ as a family member so the calibration invariant is well-defined on the actual recognition cost.
Together these close the "order forces the load-bearing joint" branch of the primitive recognition calculus without topological completeness of the reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.