additive_emp_right
plain-language theorem explainer
The result shows that cost remains unchanged when any configuration is joined on the right with the empty configuration. Researchers formalizing the recognition-work bridge would cite it to confirm the empty element acts as a cost identity. The proof reduces directly to a single rewrite using the upstream join-identity lemma.
Claim. Let $κ$ be a cost function on a configuration space obeying the dichotomy axiom (cost zero exactly on consistent configurations) and the independent-additivity axiom. For any configuration $Γ$, the cost of the join of $Γ$ with the empty configuration equals the cost of $Γ$.
background
This declaration belongs to the module that encodes the recognition-work constraint theorem from the T-1 to T0 bridge paper. The central object is a cost function, defined as a map from configurations to non-negative reals that satisfies two axioms: cost vanishes if and only if the configuration is consistent, and cost adds exactly when two configurations are independent (share no predicates). The module documentation states that these axioms together force the cost function to be uniquely determined by its values on indecomposable inconsistent configurations. The upstream lemma join_emp supplies the algebraic identity that the join of any configuration with the empty one recovers the original configuration.
proof idea
The proof is a one-line wrapper that applies the join-identity lemma join_emp to replace the joined term with the original configuration, after which equality is immediate.
why it matters
It supplies the right-identity case needed for the additive structure that the recognition-work constraint imposes on cost functions. The module documentation positions such identities as prerequisites for the uniqueness theorem on independent decompositions, which states that two cost functions agreeing on a generating set agree everywhere on configurations built by independent joins. The result therefore closes a basic case in the chain from the dichotomy and additivity axioms to the claim that recognition work forces quantitative structure on the configuration space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.