ledgerComparison_forces_jcost
plain-language theorem explainer
A reciprocal, normalized, calibrated continuous cost on positive reals, whose symmetric combination factors through a primitive ledger-posting combiner with per-slice monotone or antitone regularity, equals the recognition cost J(x)=(x+1/x)/2-1. Phase 3 ledger-to-J closure cites this: the combiner is ledger-supplied, composition follows, and logic-forcing finishes with no analytic composition-law hypothesis. Proof is a one-line re-export of the composition-forcing theorem.
Claim. Let $F:\mathbb{R}\to\mathbb{R}$ be reciprocal ($F(x)=F(x^{-1})$ for $x>0$), normalized ($F(1)=0$), calibrated ($G''(0)=1$ where $G(t)=F(e^t)$), and continuous on $(0,\infty)$. Let $P$ satisfy primitive ledger-posting semantics and, for each fixed first argument, be monotone or antitone in the second. If $F$ composes through $P$ (i.e. $F(xy)+F(x/y)=P(F(x),F(y))$), then $F(x)=J(x)$ for all $x>0$, where $J(x)=(x+x^{-1})/2-1$.
background
Recognition cost on a positive ratio is $J(x)=(x+x^{-1})/2-1$. The functional-equation package packages the standing side conditions: reciprocal symmetry $F(x)=F(1/x)$, normalization $F(1)=0$, and calibration $G''(0)=1$ for $G(t)=F(e^t)$ (equivalently $\lim_{t\to 0}2F(e^t)/t^2=1$), plus continuity on the positive ray.
This module finishes two Phase 3 gaps left after the composition-to-$J$ bridge: the comparison object is the positive ratio of a closed-observable reading (swap-reciprocal, self-comparison unital), and factorization existence is not an analytic extra but the ledger-native well-definedness condition that the symmetric combination $F(xy)+F(x/y)$ depends only on the pair of single-point costs. That condition is exactly existence of a combiner $P$ with cost composition through $P$.
Upstream, composition-through-$P$ plus primitive ledger-posting semantics and per-slice directional regularity already force $F=J$ via the composition-forcing theorem; the present declaration is the comparison-side packaging of that fact.
proof idea
One-line term wrapper: apply the upstream composition-forcing theorem to the same $F$, $P$, and the full hypothesis bundle (reciprocal, normalized, calibrated, continuous on $(0,\infty)$, primitive ledger-posting semantics, per-slice monotone-or-antitone regularity, and cost composition through $P$). No extra rewriting or case split.
why it matters
Phase 3 composite on the ledger path to $J$-uniqueness (forcing-chain T5): a comparison cost meeting the standard analytic side conditions, with symmetric combination realized by a ledger-posting combiner rather than by an assumed analytic composition law, is forced to $J$. The doc-comment states the route: the factorization combiner is ledger-supplied (hence forced to the RCL combiner), the composition law follows, and the logic-forcing theorem finishes.
Together with the module equivalences (multiplicative consistency iff the combination is cost-determined; existence of a composing $P$), this closes honest derivation of positive-ratio comparison and factorization from the ledger, so the Recognition Composition Law input is no longer an external analytic hypothesis. No downstream consumers are recorded yet; the declaration is the named Phase 3 certificate endpoint for comparison-side forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.