CostComposesThrough
plain-language theorem explainer
A cost F composes through a binary combiner P when the symmetric two-point combination F(xy)+F(x/y) equals P applied to the single-point costs, for all positive x,y. This is the bare factorization/composability input used throughout Phase 3. Anyone citing ledger-to-J forcing or d'Alembert multiplicative consistency will use it. The body is a one-line Prop abbreviation, not a proved statement.
Claim. A real function $F$ composes through a binary combiner $P:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ when, for all $x,y>0$, $$F(xy)+F(x/y)=P(F(x),F(y)).$$
background
Phase 3 of the foundation chain aims to force the recognition cost $J(x)=\frac12(x+x^{-1})-1$ from ledger structure rather than from an analytic composition-law hypothesis. The Recognition Composition Law (RCL) reads $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$, i.e. the two-point combination equals the RCL combiner $\mathrm{rclCombiner}(u,v)=2uv+2u+2v$ at the costs.
The module isolates bare composability: the left-hand side is some function $P$ of the two costs alone. Separately, the directional ledger theorem already forces any primitive ledger-posting combiner with per-slice directional regularity to equal $\mathrm{rclCombiner}$. Composing the two halves replaces $\mathrm{SatisfiesCompositionLaw},F$ by a ledger-side pair.
Upstream cost notions (observer J-cost on events, multiplicative-recognizer derived cost, rung-coarsen weighted sums) all supply candidate $F$'s; this definition is the common composability interface they feed into.
proof idea
Definitional Prop, not a theorem. The body is the universal quantification over positive reals equating the symmetric two-point combination of $F$ with $P$ at the image costs. No tactics, no lemmas: pure type-level abbreviation of the factorization input.
why it matters
This is the residual composability atom after Phase 3 splits the old analytic hypothesis. Downstream, hasMultiplicativeConsistency_iff_exists_composesThrough identifies d'Alembert multiplicative consistency with existence of some $P$ through which $F$ composes; hasMultiplicativeConsistency_iff_costDetermined equates that to cost-determined combination. The forcing theorems ledgerComposition_forces_jcost and ledgerComparison_forces_jcost take a concrete $P$ that is primitive ledger-posting with directional regularity, deduce $P=\mathrm{rclCombiner}$, obtain the composition law, and finish with law_of_logic_forces_jcost to get $F=J$ on positives (under reciprocity, normalization, calibration, continuity).
Non-vacuity is recorded by jcost_composesThrough_rclCombiner: $J$ itself composes through the RCL combiner, so $J$ is a fixed point of the setup it forces. The LedgerCompositionCertificate packages the whole closure. Framework landmark: this is the structural discharge of T5-adjacent J-uniqueness input from the ledger rather than from an independent functional equation assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.