jcost_combinationCostDetermined
plain-language theorem explainer
The recognition cost J has a cost-determined symmetric combination: J(xy)+J(x/y) is a function of the pair (J x, J y) alone. Phase 3 ledger-comparison work cites this to show the factorization-existence side of the d'Alembert input is non-vacuous for J. The proof is a one-line mp application of the equivalence between multiplicative consistency and cost-determined combination, witnessed by composition through the RCL combiner.
Claim. The recognition cost $J(x)=\frac{x+x^{-1}}{2}-1$ has cost-determined symmetric combination: for all $x_i,y_i>0$, if $J(x_1)=J(x_2)$ and $J(y_1)=J(y_2)$, then $J(x_1 y_1)+J(x_1/y_1)=J(x_2 y_2)+J(x_2/y_2)$.
background
This module finishes two Phase 3 checklist items left after the ledger-to-J composition step: positive-ratio comparison from a closed observable framework, and factorization existence from the ledger rather than as an analytic assumption.
A cost $F$ is cost-determined when the symmetric combination $F(xy)+F(x/y)$ depends only on the pair of single-point values $(F x, F y)$. By definition that property is equivalent to multiplicative consistency (existence of a binary combiner $P$ with $F(xy)+F(x/y)=P(F x, F y)$), the d'Alembert factorization input. The module treats the combiner as a ledger-native well-definedness condition, not an external hypothesis.
The recognition cost is $J(x)=(x+x^{-1})/2-1$. Upstream, the law-of-logic theorem states that $J$ is the unique reciprocal, normalized, calibrated, continuous cost satisfying the Recognition Composition Law (RCL). Composition of $J$ through the RCL combiner is already available from the ledger-composition path.
proof idea
One-line term proof. Apply the forward direction of the in-module equivalence between multiplicative consistency and cost-determined combination at $F=J$. The witness pair is the RCL combiner together with the already-proved fact that $J$ composes through that combiner; the equivalence turns that composition into cost-determinedness of the symmetric combination.
why it matters
Feeds the Phase 3 comparison/factorization certificate, which packages positive-ratio comparison facts, the consistency-iff-cost-determined equivalence, and this non-vacuity result for $J$. Downstream the certificate records that $J$'s combination is cost-determined, so the factorization side of the ledger reconstruction is inhabited rather than empty.
In the forcing chain this sits under T5 ($J$-uniqueness) and the RCL $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Combined with the ledger-composition path and law_of_logic_forces_jcost, a comparison cost whose combination is cost-determined through a ledger-posting combiner is forced to be $J$, with no free analytic composition-law hypothesis. Closes the honest derivation of factorization existence from the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.