ContextualSubstitutivity
Contextual substitutivity packages a combiner P such that the compound J-cost J(xy) + J(x/y) equals P(J(x), J(y)) for all positive x and y. Ledger theorists deriving the Recognition Composition Law cite it as the minimal invariance allowing mismatch costs to substitute without changing totals. The declaration is a bare structure definition with no proof obligations.
claimLet $J : ℝ → ℝ$. A combiner $P : ℝ → ℝ → ℝ$ satisfies contextual substitutivity for $J$ when $J(xy) + J(x/y) = P(J(x), J(y))$ for all $x, y > 0$.
background
The module proves the factorization property, and hence the Recognition Composition Law, from two primitive ledger properties. Contextual substitutivity is the first: compound comparison cost depends only on the J-mismatches of the subcomparisons. J is the cost function fixed by T5 uniqueness, satisfying J(x) = (x + x^{-1})/2 - 1 with J(1) = 0. The second property, regrouping invariance, is introduced in the sibling structure that extends this one.
proof idea
This declaration is a structure definition that introduces the combiner field and the factorization equation; it carries no proof steps or tactic applications.
why it matters in Recognition Science
The structure is extended by RegroupingInvariance, which adds symmetry, zero_boundary, unit_diagonal and right_affine conditions. It is invoked directly in substitutivity_forces_factorization to descend the compound cost to a function of the J-values. The pair of structures supplies the two primitives that force the FactorizationAssociativityGate and thereby deliver the RCL polynomial via gate_forces_rcl. It occupies the first step in the ledger-to-RCL chain inside the T5 J-uniqueness setting.
scope and limits
- Does not impose symmetry on the combiner.
- Does not specify boundary conditions such as combiner(u,0) = 2u.
- Does not derive the explicit polynomial form of the combiner.
- Does not reference the phi-ladder or spatial dimension D=3.
formal statement (Lean)
35structure ContextualSubstitutivity (J : ℝ → ℝ) where
36 combiner : ℝ → ℝ → ℝ
37 factors : ∀ x y : ℝ, 0 < x → 0 < y →
38 J (x * y) + J (x / y) = combiner (J x) (J y)
39
40/-- Regrouping invariance: the combiner is symmetric and satisfies the
41boundary and normalization conditions forced by the abelian group