then
plain-language theorem explainer
Cost functions obeying the dichotomy and independent additivity axioms are uniquely determined by their values on any chosen generating set of indecomposable inconsistent configurations. A researcher deriving the quantitative cost structure from recognition work would cite this result to establish that the assignment is rigid once the generators are fixed. The argument reduces equality on composite configurations to equality on the generators by repeated application of additivity over independent joins.
Claim. Let $C$ be a configuration space equipped with consistency, join, and independence. Let $κ, κ' : C → ℝ$ be cost functions satisfying the dichotomy (zero on consistent configurations, positive on inconsistent ones) and independent additivity. Let $α$ be any set of indecomposable inconsistent configurations. If $κ(γ) = κ'(γ)$ for every $γ ∈ α$, then $κ(c) = κ'(c)$ for every configuration $c$ expressible as an independent join of elements of $α$.
background
The module formalizes the T-1 to T0 bridge by adding independent additivity to the algebra of distinguishability. A configuration space abstracts consistency, joining, and an independence relation allowing decomposition into non-overlapping parts. The cost function must vanish on consistent configurations and be positive on inconsistent ones, with additivity over independent unions. Upstream results identify cost with J-cost (the cost of a recognition event equals the J-cost of its state) and structure J-cost via the phi-forcing derivation.
proof idea
The declaration states the uniqueness result with no attached proof body. The intended argument decomposes any target configuration into its indecomposable inconsistent components via the independence relation, then invokes additivity (including the three-way case) to reduce the equality to the generators where agreement is given by hypothesis.
why it matters
This uniqueness result shows that the cost function carries no free parameters beyond the choice of values on the indecomposable generators. It supports the main recognition_work_constraint_theorem by guaranteeing that independent additivity plus the dichotomy fixes the entire cost assignment. In the Recognition Science chain it closes the T-1 to T0 bridge, where recognition work plus additivity yields a rigid quantitative structure determined by the generators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.