substitutivity_forces_factorization
plain-language theorem explainer
Substitutivity of the J-cost under equivalent mismatches forces the compound cost to factor through the pair of J-values. A researcher deriving the Recognition Composition Law from primitive ledger axioms would cite this construction to establish the combiner P. The proof is a direct packaging of the supplied combiner and composition equation into the ContextualSubstitutivity structure.
Claim. Assume $J : ℝ → ℝ$ satisfies $J(1) = 0$ and $J(x) = J(x^{-1})$ for $x > 0$. Suppose there exists $P : ℝ → ℝ → ℝ$ such that $J(xy) + J(x/y) = P(J(x), J(y))$ for all $x, y > 0$. Then the compound cost of a pair depends only on the values of $J$ at each factor.
background
ContextualSubstitutivity is the structure asserting that the compound cost $J(xy) + J(x/y)$ equals some combiner applied to $(J x, J y)$. This is the minimal invariance of a comparison ledger: equivalent mismatch costs are interchangeable. The module establishes that factorization and hence the Recognition Composition Law follow from contextual substitutivity together with regrouping invariance. Upstream results include the reciprocal automorphism in CostAlgebra and the definition of J-cost structures in PhiForcingDerived.
proof idea
The definition is a one-line wrapper that constructs the ContextualSubstitutivity instance by supplying the given combiner P and the hypothesis hComp that encodes the factorization equation.
why it matters
This definition establishes that the factorization property is a direct consequence of the ledger's substitutivity under cost-equivalent replacements. It supplies the combiner needed for subsequent steps that derive the Recognition Composition Law via the FactorizationAssociativityGate. In the framework, this closes the path from primitive comparison properties to the RCL polynomial.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.