uniqueness_on_indep_decomposition
plain-language theorem explainer
If two cost functions agree on a set S of configurations, they agree on the join of any two independent elements from S. Researchers formalizing the recognition-work bridge cite this to establish that cost is uniquely determined by its values on indecomposable generators. The proof is a direct algebraic reduction that invokes independent additivity for each function and substitutes the agreement hypothesis.
Claim. Let $κ_1$ and $κ_2$ be cost functions on a configuration space satisfying the dichotomy and independent-additivity axioms. Let $S$ be a subset of configurations such that $κ_1(Γ) = κ_2(Γ)$ for all $Γ ∈ S$. Then for any independent pair $Γ_1, Γ_2 ∈ S$, $κ_1( join(Γ_1, Γ_2) ) = κ_2( join(Γ_1, Γ_2) )$.
background
The module formalizes the T-1 to T0 bridge by adding independent additivity to the cost framework. A cost function is a map C from configurations to non-negative reals obeying two axioms: dichotomy (C(Γ) = 0 if and only if Γ is consistent) and independent additivity (C(join(Γ₁, Γ₂)) = C(Γ₁) + C(Γ₂) whenever Γ₁ and Γ₂ share no predicates). The ConfigSpace typeclass supplies the join operation and the Independent predicate. This theorem shows that agreement on a generating set S propagates to any independent decomposition of elements from S.
proof idea
The proof is a one-line wrapper. It introduces the two configurations and the independence hypothesis, then rewrites the cost of the join using the additivity axiom from each cost function and substitutes the given pointwise agreement on S.
why it matters
This uniqueness result feeds the recognition-work constraint certificate constructed later in the module, which packages the dichotomy and additivity axioms into a single certificate. It supplies the substantive content of the recognition-work primitive in RS_Cost_From_Distinction.tex by showing that cost factors through the independent-decomposition structure, consistent with the forcing chain from T0 onward where recognition work enforces quantitative structure on the configuration space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.