hasMultiplicativeConsistency_iff_exists_composesThrough
plain-language theorem explainer
Multiplicative consistency of a real cost F is definitionally the same as existence of a binary combiner through which F composes. Anyone wiring the d'Alembert factorization gate to the ledger composition interface cites this bridge. The proof is pure definitional reflexivity: the two propositions unfold to the same existential.
Claim. For any $F : \mathbb{R} \to \mathbb{R}$, the statement that $F$ is multiplicatively consistent (there exists a binary map $P$ with $F(xy)+F(x/y)=P(F(x),F(y))$ for all $x,y>0$) is equivalent to the existence of a combiner $P$ through which $F$ composes in the ledger sense.
background
Phase 3 of the ledger comparison program asks two things of a recognition cost on a closed observable framework: the comparison object must be a positive ratio of observables, and the d'Alembert factorization input must be derived rather than assumed. The second item is the existence of a binary combiner $P$ such that the symmetric two-point combination equals $P$ at the single-point costs.
In the Ultimate d'Alembert layer, multiplicative consistency of $F$ is defined as existence of some $P$ with $F(xy)+F(x/y)=P(Fx,Fy)$ on the positive ray. Independently, CostComposesThrough packages the same equation as the ledger composition interface: the cost composes through a combiner when that identity holds. The canonical RCL combiner $P(u,v)=2uv+2u+2v$ is the target law once uniqueness is forced.
The module therefore treats factorization existence as a well-definedness condition: the symmetric combination depends only on the pair of costs, matching the ledger-native hypothesis already used in closed-framework reconstruction.
proof idea
One-line term proof by definitional reflexivity (Iff.rfl). Unfolding the Ultimate multiplicative-consistency predicate yields exactly $\exists P,,\mathrm{CostComposesThrough},F,P$, so the biconditional is an identity of propositions. No lemmas are applied.
why it matters
Closes the bookkeeping gap between the d'Alembert Ultimate gate and the ledger composition interface used by LedgerCompositionToJCost. Once the two names are interchangeable, the module can restate factorization existence as cost-determined combination and feed the RCL combiner path that forces $F=J$ (T5 J-uniqueness, Recognition Composition Law). Downstream siblings such as the cost-determined equivalence and the ledger-comparison certificate rely on this identification being literal, not merely isomorphic. No external used-by edges yet; the declaration is internal glue for Phase 3 honesty rather than a new forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.