substitutivity_forces_factorization
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.
claimAssume $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 in Recognition Science
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.
scope and limits
- Does not derive the explicit polynomial form of the combiner P.
- Does not incorporate regrouping invariance.
- Does not address the specific value of J at 1 beyond the given hypothesis.
- Does not extend to non-positive arguments.
formal statement (Lean)
57def substitutivity_forces_factorization
58 (J : ℝ → ℝ) (hJ0 : J 1 = 0)
59 (hSym : ∀ x : ℝ, 0 < x → J x = J x⁻¹)
60 (P : ℝ → ℝ → ℝ)
61 (hComp : ∀ x y : ℝ, 0 < x → 0 < y →
62 J (x * y) + J (x / y) = P (J x) (J y)) :
63 ContextualSubstitutivity J :=
proof body
Definition body.
64 ⟨P, hComp⟩
65
66/-- Symmetry of the combiner follows from commutativity of `(ℝ₊, ×)`:
67`J(xy) + J(x/y) = J(yx) + J(y/x)` because `xy = yx` and
68`J(x/y) = J(y/x)` by reciprocal symmetry. -/