hasMultiplicativeConsistency_iff_costDetermined
plain-language theorem explainer
A comparison cost F admits a binary combiner P with F(xy)+F(x/y)=P(Fx,Fy) exactly when that symmetric combination depends only on the pair of single-point costs. Anyone deriving d'Alembert factorization from ledger well-definedness cites this equivalence. Forward direction rewrites through P; reverse builds P by classical choice of witnessing ratio pairs, with cost-determinedness making the choice irrelevant.
Claim. For any $F:\mathbb{R}\to\mathbb{R}$, the following are equivalent: (i) there exists a binary map $P$ such that $F(xy)+F(x/y)=P(F(x),F(y))$ for all $x,y>0$; (ii) whenever $x_1,y_1,x_2,y_2>0$ satisfy $F(x_1)=F(x_2)$ and $F(y_1)=F(y_2)$, one has $F(x_1 y_1)+F(x_1/y_1)=F(x_2 y_2)+F(x_2/y_2)$.
background
In the Recognition Science foundation, the d'Alembert factorization input asks that a cost $F$ on positive reals factor its symmetric two-point combination through some binary combiner $P$: $F(xy)+F(x/y)=P(Fx,Fy)$. Ultimate packages multiplicative consistency as existence of such a $P$; CostComposesThrough is the same relation with $P$ fixed.
This module closes Phase 3 of the ledger comparison story. After LedgerCompositionToJCost discharged the apply-law-of-logic step, two items remained: derive positive-ratio comparison from the ledger, and derive factorization existence rather than assume it. CombinationCostDetermined is the ledger-native well-definedness condition: $F(xy)+F(x/y)$ depends only on the pair $(Fx,Fy)$. It is the joint form of the hJ_suff field of ClosedFramework.ledger_reconstruction.
The theorem equates the analytic factorization assumption with this ledger condition, so the combiner is not an arbitrary extra hypothesis.
proof idea
Term-mode constructor proof of the biconditional.
Forward: given a witness $P$ for multiplicative consistency, if $Fx_1=Fx_2$ and $Fy_1=Fy_2$ then both combination sides equal $P(Fx_i,Fy_i)$, so they agree. Two rewrites through the consistency equation and the cost equalities.
Reverse: from cost-determinedness, construct $P(u,v)$ by classical choice. If there exists a positive pair $(p,q)$ with $Fp=u$ and $Fq=v$, set $P(u,v)=F(pq)+F(p/q)$ via choose; otherwise set $0$. For any positive $x,y$, the pair $(x,y)$ itself witnesses the existential, so the if-branch fires. Cost-determinedness then shows the chosen pair yields the same combination as $(x,y)$, giving $F(xy)+F(x/y)=P(Fx,Fy)$.
why it matters
This equivalence turns factorization from an analytic assumption into a ledger well-definedness condition. Downstream, jcost_combinationCostDetermined applies the forward direction to Jcost with the RCL combiner, showing J's combination is cost-determined and factorization existence is non-vacuous. The Phase 3 composite ledgerComparisonCertificate packages the equivalence as factorization_iff_cost_determined, together with the positive-ratio comparison facts and J's cost-determinedness.
Combined with LedgerCompositionToJCost, a comparison cost whose combination is cost-determined through a ledger-posting combiner is forced to be J. That lands near T5 (J-uniqueness) and the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. The module goal is explicit: factorization existence is no longer assumed; it is equivalent to cost-determined combination.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.