RecognitionWorkConstraintCert
plain-language theorem explainer
The RecognitionWorkConstraintCert structure packages a cost function on a configuration space with the properties that the empty configuration has zero cost, positive cost precisely signals inconsistency, costs add over independent joins, and the function is uniquely determined by its values on independent components. Researchers studying the recognition-work bridge in Recognition Science would cite this certificate when invoking the quantitative structure forced by independent additivity. The definition is assembled directly from the CostFunc-
Claim. A recognition-work constraint certificate on a configuration space $Config$ consists of a cost function $κ:Config→ℝ_{≥0}$ such that $κ(∅)=0$, $0<κ(Γ)↔¬IsConsistent(Γ)$ for all $Γ$, $κ(Γ_1∨Γ_2)=κ(Γ_1)+κ(Γ_2)$ whenever $Γ_1,Γ_2$ are independent, and $κ$ is the unique cost function agreeing with any other on a set closed under independent joins.
background
The module formalizes the T-1 to T0 bridge by introducing recognition work as the unit cost of a single distinction above the algebra of distinguishability. A configuration space abstracts an empty element, a commutative join monoid, a consistency predicate, and an independence relation (no shared predicates). A cost function maps configurations to non-negative reals and obeys the dichotomy (zero cost exactly on consistent configurations) together with independent additivity (cost of join equals sum of costs).
proof idea
The structure is defined by direct bundling of the cost function field with four properties: empty cost zero from the emp_cost_zero lemma, positivity characterization from cost_pos_iff_inconsistent, additivity taken from the CostFunction additivity axiom, and uniqueness on independent decompositions. No tactics appear; it is a pure structure declaration packaging the axioms and immediate corollaries.
why it matters
This certificate is the master packaging for the recognition-work constraint theorem, which asserts existence of such a certificate for any cost function obeying the bridge axioms. It fills the T-1 to T0 step in RS_Cost_From_Distinction.tex by making explicit that independent additivity constrains costs on all independent extensions. In the Recognition Science framework it supplies the cost structure that later feeds phi-ladder mass formulas and the eight-tick octave. The downstream recognition_work_constraint_theorem invokes it to prove nonemptiness of the certificate type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.