jcostComparison
plain-language theorem explainer
Defines the canonical two-argument comparison on positive reals by feeding the ratio into the T5 J-cost: C(x,y) = J(x/y). Anyone citing the T4→T5 cost bridge or the continuous Law of Logic uses this object. The body is a one-line lambda, not a proof.
Claim. Let $J(t) = (t + t^{-1})/2 - 1$ on positive reals. The canonical continuous positive-ratio comparison is the map $C:\mathbb{R}_{>0}\times\mathbb{R}_{>0}\to\mathbb{R}$ given by $C(x,y) = J(x/y)$.
background
The Unified Forcing Chain module aims to force every landmark T−1 through T8 from the Recognition Composition Law plus normalization and calibration. T5 is the uniqueness of the cost functional $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$).
A comparison operator is any map $\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ that scores the cost of comparing two positive quantities. Under scale invariance one recovers a one-argument cost by fixing the second slot at $1$: the derived cost is $x\mapsto C(x,1)$. The four Aristotelian constraints (identity, symmetry, positivity off the diagonal, and the composition law) are the structural content of a well-posed comparison.
Upstream, Cost.Jcost (and its cosmology twin) is exactly that $J$. The present definition packages $J$ as a two-argument operator so it can sit in the Law-of-Logic interface used by the T4→T5 bridge.
proof idea
Definitional, not a proof. The body is the lambda $x,y\mapsto \mathrm{Jcost}(x/y)$. No lemmas are applied; noncomputable is inherited from real division and the closed form of $J$.
why it matters
This is the concrete comparison that the T4→T5 cost bridge installs as the continuous positive-ratio realization of recognition. Downstream, derivedCost_jcostComparison shows the derived one-argument cost collapses exactly to $J$, and jcostComparison_satisfies_laws verifies the Law of Logic (identity, symmetry, positivity, RCL surface).
Those facts feed T4_To_T5_Cost_Bridge and t4_to_t5_cost_bridge_holds, which package T5 cost-uniqueness so the complete forcing chain no longer treats T5 as a free sibling of T4. Framework landmark: T5 J-uniqueness and the Recognition Composition Law. Honesty note on the bridge: the uniqueness proof itself does not consume T−1..T4 data; this definition is the comparison object the packaging layer names.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.