LedgerCompositionCertificate
plain-language theorem explainer
Phase 3 ledger-composition certificate: a Prop bundle of four statements equating the recognition composition law with composability through the RCL combiner, deriving that law from primitive ledger-posting combiners with directional regularity, forcing F = J under reciprocal/normalized/calibrated/continuous hypotheses, and recording that J itself is a fixed point. Cited when reducing the composition hypothesis of the uniqueness theorem for J to ledger data. Pure structure definition; the companion inhabitant fills each field.
Claim. A certificate (as a proposition) with four fields: (1) for all $F:\mathbb{R}\to\mathbb{R}$, $F$ satisfies the composition law iff $F(xy)+F(x/y)=\mathrm{rcl}(F x,F y)$ for all $x,y>0$; (2) if $F$ composes through a primitive ledger-posting combiner $P$ that is monotone or antitone in each fixed-$u$ slice, then $F$ satisfies the composition law; (3) if moreover $F$ is reciprocal, normalized, calibrated, and continuous on $(0,\infty)$, then $F(x)=J(x)$ for all $x>0$; (4) $J$ composes through the RCL combiner.
background
The recognition cost is $J(x)=(x+x^{-1})/2-1$ on positives (also written $\cosh(\log x)-1$). The Recognition Composition Law (RCL) is the two-argument identity $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$, equivalently $F(xy)+F(x/y)=\mathrm{rcl}(F x,F y)$ with $\mathrm{rcl}(u,v)=2uv+2u+2v$.
This module sits at the Phase 3 endpoint: the uniqueness theorem that forces $F=J$ still took "satisfies the composition law" as an analytic hypothesis. Here that hypothesis is rewritten as bare composability. Cost composes through a combiner $P$ when $F(xy)+F(x/y)=P(Fx,Fy)$ for $x,y>0$. Upstream, any primitive ledger-posting combiner with per-slice monotone/antitone regularity equals the RCL combiner, so composability through such a $P$ yields the composition law automatically.
Standard side conditions on $F$ are normalization $F(1)=0$, calibration (second derivative of $t\mapsto F(e^t)$ at $0$ equals $1$), reciprocity, and continuity on $(0,\infty)$.
proof idea
No proof body: this is a structure of four Prop fields, not a theorem. Each field is a named interface to a proved lemma in the same module. The companion inhabitant ledgerCompositionCertificate assigns: composition-law iff RCL-composability; ledger posting plus directional regularity plus composability implies the composition law; those plus reciprocal/normalized/calibrated/continuous force $F=J$; and $J$ composes through the RCL combiner (non-vacuity). The structure only packages the interface.
why it matters
Closes the Phase 3 checklist gap flagged in the module doc: uniqueness of $J$ no longer assumes the composition law as an independent analytic input. That law is exactly "the cost composes through the RCL combiner," and the ledger already forces any primitive directional posting combiner to be RCL. The residual hypothesis is bare composability of $F$ through some ledger-side $P$.
Downstream, the single inhabitant theorem fills every field, so callers can project ledger_composition_forces_jcost (or the weaker composition-law fields) without re-assembling the chain. In the forcing chain this is the ledger-side route into T5 J-uniqueness: reciprocal, normalized, calibrated continuous costs that compose through ledger postings must be $J$. Non-vacuity (jcost_composes) shows $J$ is a genuine fixed point of the whole setup, not an empty interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.