derivedCost_jcostComparison
plain-language theorem explainer
The one-argument cost obtained by fixing the second argument of the canonical J-comparison at the multiplicative identity equals the standard recognition cost J. Anyone wiring J into the continuous Law of Logic, or citing T5 uniqueness in the forcing chain, needs this identification. The proof is function extensionality plus simp unfolding of both definitions.
Claim. Let $C_J$ be the canonical J-comparison operator on positive ratios. Its derived one-argument cost, $r \mapsto C_J(r,1)$, equals the recognition cost $J(r) = \frac{r + r^{-1}}{2} - 1$ pointwise on $\mathbb{R}$.
background
This module builds the complete inevitability chain T-1 through T8 from the cost foundation (Recognition Composition Law, normalization $F(1)=0$, calibration $F''(1)=1$). Logic, discreteness, the ledger, unique $J$, $\varphi$, the eight-tick octave, and $D=3$ are treated as forced, not assumed.
A comparison operator is a two-argument cost on positive ratios. The derived cost of such an operator is the one-argument map obtained by fixing the second slot at the multiplicative identity: $r \mapsto C(r,1)$. Under scale invariance this is well-defined on the multiplicative group of positive ratios.
The standard recognition cost is $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$). It is the unique continuous solution pinned by d'Alembert structure plus normalization and calibration (T5). The canonical J-comparison is the two-argument lift of that $J$ used when stating the continuous positive-ratio Law of Logic.
proof idea
Term-mode proof by function extensionality. After funext x, both sides are definitionally the same once jcostComparison and derivedCost are unfolded: the right-hand side is Cost.Jcost, and the left-hand side is the comparison applied to (x, 1), which is definitionally $J(x)$. A single simp closes the goal. No lemmas beyond the two definitions are required.
why it matters
This is the bridge that lets the canonical J-comparison inherit the continuous Law of Logic. The sole downstream consumer is jcostComparison_satisfies_laws, whose doc-comment states that the canonical J comparison satisfies that law; the identity, non-contradiction, and related clauses are checked after this equality is in hand.
In the forcing chain it sits under T0 (logic from cost) and feeds T5 (unique $J$). Once derived cost equals $J$, the Aristotelian constraints on the comparison become constraints on $J$ itself, so the RCL-normalized calibrated cost is available as a logic-satisfying comparison without a separate axiomatic choice. Constants and the later $\varphi$-ladder steps inherit that uniqueness rather than re-proving it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.