ContextualSubstitutivity
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.