uniqueness_three_indep
plain-language theorem explainer
Two cost functions that agree on a generating set S of configurations agree on the cost of any three-way independent join drawn from S. Recognition scientists working on the cost-from-distinction bridge would cite this when extending pairwise uniqueness to finite decompositions. The proof is a direct term-mode reduction that invokes the three-way additivity lemma on each cost function and substitutes the component costs via the agreement hypothesis.
Claim. Let $κ_1$ and $κ_2$ be cost functions on a configuration space. Let $S$ be a set of configurations such that $κ_1(Γ) = κ_2(Γ)$ for all $Γ ∈ S$. Then for any $Γ_1, Γ_2, Γ_3 ∈ S$ that are pairwise independent with $Γ_1$ independent of the join of $Γ_2$ and $Γ_3$, one has $κ_1(Γ_1 ∨ (Γ_2 ∨ Γ_3)) = κ_2(Γ_1 ∨ (Γ_2 ∨ Γ_3))$.
background
CostFunction is a structure on a ConfigSpace that assigns a non-negative real cost C to each configuration, obeying the dichotomy axiom (C(Γ) = 0 iff Γ is consistent) and the independent-additivity axiom (C(join(Γ1, Γ2)) = C(Γ1) + C(Γ2) whenever Γ1 and Γ2 are independent). The module CostFromDistinction formalizes the recognition-work constraint by adding independent additivity to the satisfiability dichotomy, yielding quantitative structure on costs of independent decompositions. This theorem relies on the upstream result additive_three, which establishes additivity of cost over three pairwise-independent configurations.
proof idea
The proof proceeds by rewriting the target equality using the additive_three lemma applied separately to κ₁ and to κ₂, then substituting the three component costs via the agreement hypothesis h_agree on each of Γ₁, Γ₂, and Γ₃.
why it matters
This three-way uniqueness result extends the basic uniqueness theorem to support induction over finite independent decompositions in the recognition-work constraint theorem. It contributes to the T-1 to T0 bridge by showing that cost is uniquely determined on all configurations expressible as independent joins from a generating set. The result sits inside the CostFromDistinction module that supplies the quantitative content of the recognition-work primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.