additive_emp_right
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.
claimLet $κ$ 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 in Recognition Science
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.
scope and limits
- Does not establish additivity for joins lacking the independence hypothesis.
- Does not derive explicit numerical cost values for any configuration.
- Does not address joins involving more than two configurations.
- Does not prove uniqueness of cost functions on its own.
formal statement (Lean)
235theorem additive_emp_right (κ : CostFunction Config) (Γ : Config) :
236 κ.C (join Γ emp) = κ.C Γ := by
proof body
Term-mode proof.
237 rw [join_emp]
238
239/-! ### The Recognition-Work Constraint Theorem -/
240
241/--
242**Recognition-Work Constraint Theorem (uniqueness on independent
243decompositions).**
244
245If two cost functions `κ₁` and `κ₂` on the same configuration space
246agree on a set `S` of configurations, and if a configuration `Γ`
247decomposes as the join of two `S`-elements that are independent of
248each other, then `κ₁` and `κ₂` agree at `Γ`.
249
250This is the substantive content of the recognition-work primitive:
251once cost is constrained to be additive over independent joins, the
252cost function is uniquely determined by its restriction to a
253generating set of "indecomposable" configurations. Recognition work
254is therefore not just a binary stipulation; it forces the cost
255function to factor through the independent-decomposition structure of
256the configuration space.
257-/