of
plain-language theorem explainer
Phase 3 endpoint certificate: the composition-law hypothesis of the Law of Logic cost theorem reduces to bare cost composability through a primitive ledger-posting combiner, which forces any such cost equal to J, and J itself is a consistent fixed point. Cite when replacing an analytic RCL assumption by a ledger-side posting statement. The declaration packages that reduction, the forcing, and the non-vacuity check.
Claim. A certificate records three facts: (i) the composition law $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ is equivalent to $F$ composing through a primitive ledger-posting combiner; (ii) under reciprocity, normalization, calibration, and continuity this forces $F=J$; (iii) $J$ itself composes through the RCL combiner $u,v\mapsto 2uv+2u+2v$, so the fixed point is attained.
background
Phase 3 of the foundation chain applies the Law of Logic cost theorem: the unique reciprocal, normalized, calibrated, continuous cost satisfying the Recognition Composition Law (RCL)
$$F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$$
is the J-cost $J(x)=(x+x^{-1})/2-1$. That theorem previously took SatisfiesCompositionLaw F as an analytic hypothesis.
This module rewrites that hypothesis ledger-side. Termwise, the composition law says the two-point combiner $(x,y)\mapsto F(xy)+F(x/y)$ equals the RCL combiner rclCombiner at the costs $(F x, F y)$. The directional ledger theorem already forces any primitive ledger-posting combiner with per-slice directional regularity to equal rclCombiner. So if $F$ composes through some combiner $P$ and $P$ is a primitive ledger-posting combiner, then $P=$ rclCombiner, hence the composition law holds, hence $F=J$.
The residual input is bare composability (CostComposesThrough F P for some $P$). The "combiner is RCL" half is now a ledger theorem, not a hypothesis. Non-vacuity: $J$ itself composes through rclCombiner.
proof idea
Certificate constructor packaging three already-proved pieces rather than a fresh analytic argument.
- Equivalence: composition law iff the cost composes through
rclCombiner(sibling iff and the twosatisfiesCompositionLaw_of_*directions). - Forcing: feed ledger composability into the ledger-posting directional theorem to obtain the composition law, then apply
law_of_logic_forces_jcostwith the remaining reciprocal/normalized/calibrated hypotheses (and the internal Aczél smoothness package) to conclude $F=J$ (ledgerComposition_forces_jcost). - Fixed-point check:
jcost_composesThrough_rclCombinerandjcost_satisfiesCompositionLawshow $J$ saturates the setup.
No new functional-equation work; the proof is assembly of those lemmas into the certificate record.
why it matters
Closes the Phase 3 checklist gap flagged in the module doc: law_of_logic_forces_jcost existed, but its composition-law hypothesis was assumed rather than derived from the recognition ledger. After this certificate, that hypothesis is replaced by "the cost composes through a ledger-posting combiner," with the RCL identification discharged by the ledger.
In the forcing chain this is the structural bridge into T5 J-uniqueness: once ledger posting plus bare composability are granted, the unique cost is $J(x)=\cosh(\log x)-1$. It also confirms the construction is inhabited ($J$ is a fixed point), so the ledger-composition story is not vacuous.
No downstream uses are recorded yet (used_by_count = 0); the natural consumers are any master or bridge theorems that still list SatisfiesCompositionLaw as an open hypothesis and want a ledger-native discharge path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.