ledgerCompositionCertificate
plain-language theorem explainer
The Phase 3 ledger-composition certificate packages four proved facts: the recognition composition law is exactly composition through the RCL combiner; ledger-posting combiners force that law on any cost that composes through them; those hypotheses plus reciprocity, normalization, calibration, and continuity force the cost to equal J; and J itself is a fixed point. Anyone discharging the composition-law hypothesis of the uniqueness theorem for J would cite this bundle. The proof is pure structure assembly of four prior theorems.
Claim. There is a ledger-composition certificate asserting four facts: (i) a real map $F$ satisfies the recognition composition law iff $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ for all positive $x,y$; (ii) if $F$ composes through a primitive ledger-posting combiner $P$ with per-slice directional regularity, then $F$ satisfies that law; (iii) under reciprocity, normalization, calibration, and continuity on the positive ray, such ledger composition forces $F=J$ on positives; (iv) the recognition cost $J(x)=\frac12(x+x^{-1})-1$ itself composes through the RCL combiner $(u,v)\mapsto 2uv+2u+2v$.
background
The Recognition Composition Law (RCL) is the functional equation $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ on positive reals. In Recognition Science this is not an independent analytic axiom: it is exactly the claim that the cost's two-point combiner equals the RCL combiner evaluated at the costs. Under reciprocity, normalization, calibration, and continuity the unique solution is $J(x)=\frac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$), the T5 landmark of the forcing chain.
This module is the Phase 3 endpoint that closes a structural gap. The uniqueness theorem for $J$ previously took the composition law as an assumed hypothesis. Phase 3's directional ledger theorem already forces any primitive ledger-posting combiner with per-slice directional regularity to equal the RCL combiner. Composing that with bare cost composability yields the composition law, and thence $F=J$. The residual input is only bare composability through some combiner $P$; the "combiner is RCL" half is now a ledger theorem.
The construction is non-vacuous: $J$ itself composes through the RCL combiner, so $J$ is a genuine fixed point of the whole ledger-composition setup.
proof idea
Term-mode construction of the certificate structure. Each field is filled by a named theorem of the same module: the pure rearrangement equating the composition law with the RCL-combiner identity on costs; the implication from ledger-posting plus directional regularity plus composability to the composition law; the full forcing theorem that ledger composition plus reciprocity, normalization, calibration, and continuity yield $F=J$ on positives; and the direct verification that $J$ itself composes through the RCL combiner. No new analytic steps: the proof is a one-shot packaging of those four prior results into a single Prop-valued certificate.
why it matters
This is the Phase 3 closure certificate for the ledger-to-$J$ pipeline. It records that the composition-law hypothesis of the uniqueness theorem for $J$ reduces to a ledger-posting combiner plus bare composability, that this forces $J$, and that $J$ is a consistent fixed point. In the forcing chain it sits at T5 (J-uniqueness) and the RCL landmark: the composition law is no longer an external analytic input but a theorem of ledger posting.
No downstream consumers are wired yet, so the certificate is presently a terminal packaging object. Its role is structural and documentary: anyone discharging "apply uniqueness of $J$ from ledger data" cites this bundle rather than four separate lemmas. The residual open surface isolated by the module is bare composability of the cost through some combiner; everything else on the composition-law side is discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.