IndisputableMonolith.Foundation.LedgerCompositionToJCost
Equates the recognition composition law for a cost F with matching the RCL combiner 2uv+2u+2v on values F(x), F(y), then shows ledger composition forces the unique J-cost of T5. Phase-3 foundation work and anyone citing the ledger-to-J bridge land here. The argument is algebraic rearrangement plus the upstream functional-equation uniqueness stack.
claimA cost $F$ satisfies the recognition composition law iff $F(xy)+F(x/y)$ equals the combiner $2uv+2u+2v$ at $u=F(x)$, $v=F(y)$. Under ledger composition hypotheses, $F$ is forced to be the unique $J$-cost $J(x)=(x+x^{-1})/2-1$.
background
The Recognition Composition Law (RCL) is the two-point identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. This module treats the right-hand side as a pure combiner on cost values, $\mathrm{rclCombiner}(u,v)=2uv+2u+2v$, and records that $F$ obeys RCL exactly when its symmetric two-point combination matches that combiner (a pure rearrangement of the same identity).
Upstream, LedgerToFactorization isolates the remaining algebraic condition after free-ledger additivity: a two-variable combiner with ledger-linear response in its second argument. FunctionalEquation and AczelProof supply the T5 stack: continuous solutions of d'Alembert's equation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ are analytic, and $J$ is the unique normalized cost.
The local setting is Phase 3 of the foundation chain: derive the T4-to-T5 bridge from the recognition ledger rather than assume it as an analytic input.
proof idea
The module opens with the iff that composition-law satisfaction is exactly matching the RCL combiner on values. It introduces a "composes through" predicate for a cost relative to a two-variable combiner, then lifts ledger composition to composition through the RCL combiner. From there it applies the T5 uniqueness route (ledger composition forces $J$) and packages the result as a certificate for downstream import. Most steps are algebraic rearrangements or one-line transfers of upstream lemmas; no new analytic work is done here.
why it matters in Recognition Science
Downstream LedgerComparisonToComposition imports this module and states that it discharged the Phase-3 checklist item "apply law_of_logic_forces_jcost". The remaining checklist items there are positive-ratio comparison (the object $J$ acts on is a positive ratio with reciprocal symmetry) and factorization existence from the ledger.
In the forcing chain this closes the algebraic half of T5 from ledger axioms: once composition is ledger-linear, the cost is forced to $J(x)=\cosh(\log x)-1$. That uniqueness is the gateway to T6 ($\phi$ as self-similar fixed point) and T7 (eight-tick octave). Without this bridge, T5 would remain an analytic assumption rather than a ledger consequence.
scope and limits
- Does not prove continuity or analyticity of F; that lives in AczelProof.
- Does not derive positive-ratio comparison or reciprocal symmetry; next module.
- Does not construct the free ledger; assumes ledger-composition hypotheses.
- Does not address T6 phi-forcing, T7 eight-tick structure, or T8 dimension.
- Does not compute numerical constants (alpha band, mass ladder, G, hbar).
used by (1)
depends on (3)
declarations in this module (10)
-
theorem
satisfiesCompositionLaw_iff_rclCombiner -
def
CostComposesThrough -
theorem
satisfiesCompositionLaw_of_composesThrough_rcl -
theorem
satisfiesCompositionLaw_of_ledgerComposes -
theorem
ledgerComposition_forces_jcost -
theorem
jcost_composesThrough_rclCombiner -
theorem
jcost_satisfiesCompositionLaw -
theorem
of -
structure
LedgerCompositionCertificate -
theorem
ledgerCompositionCertificate