additive_three
plain-language theorem explainer
Cost is additive over three pairwise-independent configurations, providing the base case for finite induction on independent decompositions in the recognition-work framework. Researchers extending uniqueness results or building cost functions from distinction axioms would cite this when proving additivity for larger finite sets. The proof is a one-line wrapper that applies the independent additivity axiom twice to the nested joins and simplifies the resulting expression with ring.
Claim. Let $κ$ be a cost function on configurations satisfying dichotomy and independent additivity. For configurations $Γ_1, Γ_2, Γ_3$ with $Γ_1$ independent of $Γ_2$, $Γ_1$ independent of $Γ_3$, $Γ_2$ independent of $Γ_3$, and $Γ_1$ independent of the join of $Γ_2$ and $Γ_3$, the cost of the triple join equals the sum of the separate costs: $κ.C( join(Γ_1, join(Γ_2, Γ_3)) ) = κ.C(Γ_1) + κ.C(Γ_2) + κ.C(Γ_3)$.
background
The module formalizes the T-1 to T0 bridge by equipping a ConfigSpace with a CostFunction structure. This structure encodes two axioms: dichotomy (cost zero exactly on consistent configurations) and independent additivity (cost of a join equals the sum of costs when the configurations share no predicates). The join operation and Independent relation come from the ConfigSpace typeclass. Upstream results include the CostFunction definition itself, which supplies the additivity field used here, and related structures such as LedgerFactorization that calibrate the underlying J-cost.
proof idea
The proof applies the additivity field of κ first to the outer join Γ1 with (join Γ2 Γ3) under the hypothesis that Γ1 is independent of that join. It then applies the same field to the inner join Γ2 with Γ3 under their independence hypothesis. The ring tactic collects the three cost terms on the right-hand side.
why it matters
This result is the immediate predecessor of uniqueness_three_indep, which lifts the same argument to show that two cost functions agreeing on a generating set agree on any three-way independent decomposition. It directly implements the independent-additivity axiom of the recognition-work constraint theorem described in the module doc and the paper RS_Cost_From_Distinction.tex. In the broader framework it supplies the quantitative structure needed for costs on finite independent decompositions, feeding into the phi-ladder mass formulas and the T0 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.