recognition_work_constraint_cert
plain-language theorem explainer
This definition builds the master certificate that bundles the recognition-work axioms for any cost function on a configuration space. Researchers formalizing the T-1 to T0 bridge would cite it to turn the recognition-work primitive into an explicit quantitative constraint. The construction is a direct record builder that wires the input cost function into the four required fields using prior lemmas on zero cost, positivity, additivity, and uniqueness.
Claim. Let $C$ be a cost function on a configuration space satisfying the dichotomy axiom ($C(Γ)=0$ precisely when $Γ$ is consistent) and the independent-additivity axiom. The recognition-work constraint certificate for $C$ is the structure whose cost component is $C$, whose empty-configuration cost is zero, whose cost is positive exactly on inconsistent configurations, whose cost is additive over independent joins, and whose values are uniquely determined on independent decompositions.
background
The module formalizes the T-1 to T0 bridge paper by introducing recognition work as the unit cost of performing a single distinction. A configuration space carries consistency, join, and independence relations. A cost function is a map $C$ from configurations to non-negative reals obeying two axioms: dichotomy (cost zero if and only if consistent) and independent additivity (cost of a join equals sum of costs when the summands share no predicates). The master certificate RecognitionWorkConstraintCert packages these properties together with the immediate consequences for the empty configuration and for uniqueness on decompositions.
proof idea
The definition is a record constructor. It sets the cost component to the supplied function and fills the remaining fields by direct application of the lemmas emp_cost_zero, cost_pos_iff_inconsistent, the additivity field already present in the cost function, and uniqueness_on_indep_decomposition.
why it matters
This definition supplies the concrete witness used by the recognition-work constraint theorem, which asserts that the certificate type is non-empty for any cost function obeying the two bridge axioms. It operationalizes the recognition-work primitive by enforcing independent additivity, ensuring cost factors through the independent-decomposition structure of the configuration space. In the broader framework it closes the gap between the algebra of distinguishability and the quantitative cost structure required for later steps in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.