with
The recognition work constraint theorem establishes that cost on a configuration equals the sum of costs on its independent inconsistent components and is uniquely fixed by values on indecomposable inconsistencies. Researchers formalizing the T-1 to T0 bridge in Recognition Science cite it to justify quantitative structure beyond the mere consistency dichotomy. The argument combines the dichotomy axiom with independent additivity to reduce arbitrary configurations to base cases via finite decompositions.
claimLet $C$ be a cost function on a configuration space satisfying the dichotomy ($C=0$ precisely on consistent configurations) and independent additivity ($C$ of an independent join equals the sum of the $C$ values). Then for any finite collection of pairwise independent configurations, $C$ of their join equals the sum of the individual $C$ values, and $C$ is uniquely determined by its restriction to indecomposable inconsistent configurations.
background
The module formalizes the substantive content of the T-1 to T0 bridge paper RS_Cost_From_Distinction.tex by adding one operational primitive: recognition work as the unit cost of performing a single distinction. ConfigSpace is the typeclass abstracting configuration spaces equipped with consistency, joining, and independence. CostFunction is the structure satisfying the dichotomy axiom together with independent additivity over configurations that share no predicates. The local theoretical setting is that the recognition-work narrative supplies no formal content without this additivity constraint; the proofs then use only the satisfiability dichotomy plus the stipulation that cost vanishes on consistent configurations.
proof idea
The proof is a one-line wrapper that applies the independent-additivity axiom to finite pairwise-independent joins and invokes uniqueness on indecomposable decompositions. It first records that the empty configuration has cost zero, then shows that any configuration decomposes into independent inconsistent components whose costs sum, reducing the general case to the base inconsistent configurations.
why it matters in Recognition Science
This is the main constraint result of the CostFromDistinction module and directly fills the gap identified in RS_Cost_From_Distinction.tex by enforcing independent additivity. It supplies the quantitative structure required for the cost framework in the Foundation layer and feeds into downstream derivations of the forcing chain. The result touches the open calibration question of assigning a specific positive cost to the base inconsistent configuration. In the Recognition Science framework it operationalizes the T-1 to T0 bridge by turning the recognition-work primitive into a genuine additive cost function.
scope and limits
- Does not assign a numerical value to the base cost on indecomposable inconsistencies.
- Does not apply when configurations share predicates.
- Does not derive the explicit J-cost formula or phi-ladder.
- Does not treat infinite or continuous joins.
formal statement (Lean)
350theorem with its immediate consequences.
351
352This certificate makes precise what the recognition-work primitive
353adds above the algebra of distinguishability. It is non-vacuous: the
354calibration component picks out a specific inconsistent
355configuration with a specific positive cost, and the additivity
356component constrains the cost on all independent extensions of that
357configuration.
358-/