recognition_work_constraint_theorem
plain-language theorem explainer
Any cost function on a configuration space that obeys the dichotomy axiom (zero cost exactly on consistent configurations) and independent additivity (cost of an independent join equals the sum of the costs) admits a master certificate bundling those properties with their immediate consequences. Researchers formalizing the recognition-work bridge in Recognition Science cite this result to establish the quantitative structure forced by the recognition-work primitive above the algebra of distinguishability. The proof is a one-line term that feeds
Claim. Let $Config$ be a configuration space and let $κ$ be a cost function on $Config$ satisfying the dichotomy axiom ($κ(Γ)=0$ if and only if $Γ$ is consistent) and independent additivity ($κ(Γ_1 ∨ Γ_2)=κ(Γ_1)+κ(Γ_2)$ whenever $Γ_1$ and $Γ_2$ are independent). Then the type of master certificates for $κ$ is nonempty.
background
The module formalizes the T-1 to T0 bridge paper by adding one operational primitive, recognition work, above the algebra of distinguishability. A configuration space carries consistency, a join operation, and an independence relation. A cost function is a map from configurations to non-negative reals obeying two axioms: the dichotomy (cost vanishes exactly on consistent configurations) and independent additivity (cost of an independent join equals the sum of the costs). The upstream definition recognition_work_constraint_cert packages any such cost function together with the derived facts that the empty configuration has zero cost and that cost is positive precisely on inconsistent configurations.
proof idea
The proof is a term-mode one-liner that applies the constructor recognition_work_constraint_cert directly to the input cost function κ. That constructor in turn invokes the lemmas emp_cost_zero κ and cost_pos_iff_inconsistent κ to populate the remaining fields of the certificate.
why it matters
This is the headline theorem of the CostFromDistinction module and supplies the formal content of the recognition-work constraint in the T-1 to T0 bridge. It guarantees that any cost function obeying the two axioms carries additive structure over independent decompositions and is uniquely determined by its values on indecomposable generators. In the Recognition Science framework the result anchors the cost primitive required for the forcing chain from T0 through T8 and for the subsequent derivation of the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.