CombinationCostDetermined
plain-language theorem explainer
A real cost F is cost-determined when the symmetric combination F(xy)+F(x/y) depends only on the pair of values (F x, F y), not on which positive ratios realize those values. Anyone working the Phase 3 ledger-to-d'Alembert bridge cites this as the ledger-native well-definedness condition. It is a pure Prop definition: four positive reals, equal single-point costs, equal combinations.
Claim. A function $F:\mathbb{R}\to\mathbb{R}$ has cost-determined combination if, for all $x_1,y_1,x_2,y_2>0$ with $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)$. Equivalently, the map $(x,y)\mapsto F(xy)+F(x/y)$ factors through the pair of single-point costs $(F x, F y)$.
background
Phase 3 of the foundation closes two gaps left after the ledger-to-$J$ composition step: that the comparison object is a positive ratio of observables, and that the d'Alembert factorization input is not an extra analytic assumption.
Multiplicative consistency (from the d'Alembert modules) asserts existence of a binary combiner $P$ with $F(xy)+F(x/y)=P(Fx,Fy)$ on positive reals. That is the classical factorization form of the Recognition Composition Law skeleton. The present predicate isolates the well-definedness half of that statement: the combination value is constant on level sets of $(F,F)$.
In the closed-observable setting, comparison ratios $r(s_1)/r(s_2)$ are strictly positive and invert under state swap, so reciprocal-symmetric normalized costs become swap-invariant and vanish on self-comparison. Cost-determinedness is the joint form of the sufficiency field already present in ledger reconstruction: posting depends only on the costs of the compared states.
proof idea
No proof: this is a Prop-valued definition. The body quantifies over four positive reals, assumes equality of the two single-point costs, and demands equality of the two symmetric combinations $F(x_i y_i)+F(x_i/y_i)$. Downstream, the forward half of the equivalence to multiplicative consistency rewrites both combinations via a witnessing $P$; the reverse half builds $P$ by choosing any preimage pair in the image of $F$ and invokes this predicate to show the choice is irrelevant.
why it matters
This predicate is the ledger-native restatement of factorization existence. The sibling theorem hasMultiplicativeConsistency_iff_costDetermined proves it equivalent to d'Alembert multiplicative consistency, so the combiner $P$ is no longer an arbitrary analytic input: it exists exactly when the combination is a function of costs alone.
It feeds three local consumers: the iff with multiplicative consistency, the witness that $J$ itself is cost-determined (via composition through the RCL combiner), and the Phase 3 LedgerComparisonCertificate that packages positive-ratio comparison with factorization closure. Together with the earlier ledger-composition-to-$J$ result, a comparison cost whose combination is cost-determined through a ledger-posting combiner is forced to be the unique $J$ of the forcing chain (T5 J-uniqueness, RCL). That is the honest discharge of the Phase 3 checklist item "derive factorization from the ledger."
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.