join_emp
plain-language theorem explainer
Joining any configuration with the empty configuration on the right returns the original configuration. Researchers formalizing the recognition-work constraint would cite this when reducing expressions that contain empty components in cost calculations. The proof is a one-line rewrite applying commutativity of join followed by the left-identity lemma.
Claim. For any configuration $Γ$, $Γ ∨ ∅ = Γ$, where $∨$ denotes the join operation on configurations and $∅$ is the empty configuration.
background
The module CostFromDistinction formalizes the T-1 to T0 bridge by introducing recognition work as the unit cost of a distinction. Configurations live in a space abstracted by the ConfigSpace typeclass, which equips them with a consistency predicate, a join operation combining independent parts, and an independence relation. The empty configuration emp serves as the identity element for this join. Upstream results supply the join operation from PrimitiveDistinction and the J-cost structure from PhiForcingDerived, together with the independent semantics from LNALSemantics.
proof idea
One-line wrapper that applies join_comm followed by emp_join.
why it matters
This identity is invoked by additive_emp_right to show that cost is invariant under right-joining with empty. It supports the recognition-work constraint theorem by guaranteeing that the cost function respects the independent-additivity axiom and is uniquely determined on indecomposable inconsistent components. The result closes part of the algebraic structure required for the cost framework in the RS cost-from-distinction paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.