ledgerComposition_forces_jcost
plain-language theorem explainer
Any reciprocal, normalized, calibrated cost continuous on positives that composes through a primitive ledger-posting combiner with per-slice directional regularity must equal the recognition cost J(x)=(x+x^{-1})/2-1 on the positive ray. Phase-3 auditors cite this as the ledger-side discharge of the composition-law hypothesis in the uniqueness theorem for J. The proof derives the composition law from ledger posting, then applies the existing functional-equation uniqueness result.
Claim. Let $F:\mathbb{R}_{>0}\to\mathbb{R}$ be reciprocal ($F(x)=F(x^{-1})$), normalized ($F(1)=0$), calibrated ($G''(0)=1$ for $G(t)=F(e^t)$), and continuous on $(0,\infty)$. Let $P$ be a binary combiner with primitive ledger-posting semantics and, for each fixed first argument, monotone or antitone in the second. If $F$ composes through $P$ in the sense that $F(xy)+F(x/y)=P(F(x),F(y))$ for all $x,y>0$, then $F(x)=J(x):=\frac{x+x^{-1}}{2}-1$ for every $x>0$.
background
Recognition Science identifies the cost of a positive ratio with $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Uniqueness of $J$ among reciprocal, normalized, calibrated continuous costs is already proved as law_of_logic_forces_jcost, but that theorem takes the Recognition Composition Law
$$F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$$
as an analytic hypothesis (SatisfiesCompositionLaw). Phase 3 of the foundation chain asks that this hypothesis be derived from ledger structure rather than assumed.
The module isolates the residual composability input as CostComposesThrough F P: the symmetric two-point combination of $F$ equals some binary combiner $P$ evaluated at the single-point costs. Upstream, the directional ledger theorem forces any primitive ledger-posting combiner with per-slice monotone/antitone regularity to equal the RCL combiner $u,v\mapsto 2uv+2u+2v$. Thus ledger posting plus composability yields the composition law, and the remaining reciprocal/normalized/calibrated/continuous package feeds the uniqueness theorem.
Calibration is the second-derivative condition $G''(0)=1$ (limit form $\lim_{t\to 0}2F(e^t)/t^2=1$). Normalization is $F(1)=0$. Reciprocity is $F(x)=F(x^{-1})$.
proof idea
Two-line term proof. First apply satisfiesCompositionLaw_of_ledgerComposes to the triple (primitive ledger-posting semantics of $P$, per-slice directional regularity, and CostComposesThrough F P) to obtain SatisfiesCompositionLaw F. That intermediate lemma uses the directional ledger factorization theorem to identify $P$ with the RCL combiner, which is exactly the composition law. Then feed reciprocity, normalization, the derived composition law, calibration, and continuity into law_of_logic_forces_jcost, which returns pointwise equality $F=J$ on positives.
why it matters
This is the Phase 3 endpoint that closes the gap flagged in the module doc: the composition-law hypothesis of the J-uniqueness theorem (T5 in the forcing chain) is no longer an independent analytic input. It is replaced by a ledger-side statement (cost composes through a primitive posting combiner), and the identification of that combiner with the RCL combiner is a theorem of ledger factorization.
Downstream, ledgerComparison_forces_jcost packages the same argument for comparison costs, and ledgerCompositionCertificate records the four structural facts (composition law iff RCL combiner; ledger composability forces the law; this uniqueness theorem; and non-vacuity that $J$ itself composes through the RCL combiner). The residual open surface is bare composability of the cost through some $P$; the "combiner is RCL" half is discharged. Framework landmark: T5 J-uniqueness via the Recognition Composition Law, now ledger-derived rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.