join_emp
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove the left-identity property without invoking commutativity.
- Does not address consistency or independence predicates.
- Does not extend to joins of multiple non-empty components.
Lean usage
rw [join_emp]formal statement (Lean)
112theorem join_emp (Γ : Config) : join Γ emp = Γ := by
proof body
Term-mode proof.
113 rw [join_comm, emp_join]
114
115/-- Independence on the right: `emp` is independent of everything from
116both sides by symmetry. -/