Pith. sign in
module module high

IndisputableMonolith.Foundation.LedgerCompositionToJCost

show as:
view Lean formalization →

Ledger composition forces the recognition cost onto the unique J-cost of T5. A cost F obeys the recognition composition law exactly when F(xy)+F(x/y) equals the RCL combiner 2uv+2u+2v on (F x, F y). Phase-3 and T4-to-T5 bridge work cite this module. The argument is algebraic rearrangement plus the existing Aczél/T5 uniqueness pipeline once ledger-linear response is assumed.

claimA cost $F$ satisfies the recognition composition law if and only if $F(xy)+F(x/y)=\mathrm{rclCombiner}(F(x),F(y))$ with $\mathrm{rclCombiner}(u,v)=2uv+2u+2v$. When $F$ arises from ledger composition (ledger-linear response in the second argument), this law holds, and the T5 uniqueness pipeline forces $F=J$ with $J(x)=\frac{x+x^{-1}}{2}-1$.

background

Recognition Science isolates the cost functional by a forcing chain. T5 asserts uniqueness of the J-cost $J(x)=\cosh(\log x)-1=\frac{x+x^{-1}}{2}-1$ among solutions of the recognition composition law (RCL) $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. The right-hand side is exactly the bilinear combiner $\mathrm{rclCombiner}(u,v)=2uv+2u+2v$ evaluated at $(u,v)=(J(x),J(y))$.

Phase 3 of the foundation work asks that the T4-to-T5 bridge be derived from the recognition ledger rather than postulated analytically. The free ledger already supplies unconditional additivity. The remaining algebraic condition, isolated in LedgerToFactorization, is that a two-variable combiner respond linearly to the ledger in its second argument.

Upstream, FunctionalEquation supplies the T5 helper lemmas, and AczelProof shows that continuous solutions of the related d'Alembert equation are real-analytic, closing the smoothness step of uniqueness.

proof idea

The module is organized as a short bridge, not a single deep proof.

First, satisfiesCompositionLaw_iff_rclCombiner is pure rearrangement: the RCL identity is rewritten as equality of the symmetric two-point combination against rclCombiner on the values of F.

CostComposesThrough and the of_composesThrough / of_ledgerComposes lemmas then show that any cost whose two-variable combiner has the ledger-linear response of LedgerToFactorization satisfies that rearranged law.

Separately, jcost_composesThrough_rclCombiner and jcost_satisfiesCompositionLaw verify that the concrete J-cost meets the same law.

The capstone ledgerComposition_forces_jcost feeds the composition law into the existing T5 uniqueness pipeline (FunctionalEquation helpers plus Aczél smoothness) and packages the result as a LedgerCompositionCertificate.

why it matters in Recognition Science

This module discharges the Phase-3 checklist item "apply law_of_logic_forces_jcost" from the ledger side. Downstream, LedgerComparisonToComposition imports it and continues the remaining Phase-3 work: deriving positive-ratio comparison (the object to which J is applied) and reciprocal symmetry under state swap, again from ledger structure rather than analytic postulate.

In the forcing chain it sits at the T4-to-T5 interface: ledger composition supplies the RCL, and T5 J-uniqueness then pins the cost to $J(x)=\frac{x+x^{-1}}{2}-1$. Without this bridge the uniqueness theorem would remain an external analytic input; with it the cost is forced by ledger algebra plus the already-proved Aczél/T5 pipeline.

The certificate form (LedgerCompositionCertificate) is the stable interface later foundation modules consume when they need "composition has already forced J".

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (10)