independent_emp
plain-language theorem explainer
The theorem shows that the empty configuration is independent of any configuration Γ from both sides. Researchers formalizing the cost function via independent additivity in Recognition Science cite this when proving that emp contributes zero to any decomposition. The proof is a one-line term that invokes symmetry on the base independence fact for emp.
Claim. For every configuration $Γ$, the empty configuration $emp$ is independent of $Γ$ (and symmetrically $Γ$ is independent of $emp$).
background
The module CostFromDistinction supplies the recognition-work constraint by adding independent additivity to the consistency dichotomy: cost is zero on consistent configurations and positive on inconsistent ones, with additivity holding precisely when components share no predicates. ConfigSpace is the typeclass that packages consistency, join, and independence operations on configurations. The empty configuration $emp$ acts as the identity element for join.
proof idea
The term applies the symmetry lemma for independence to the already-established fact that $emp$ is independent of $Γ$, producing the two-sided independence statement.
why it matters
This fills the right-hand independence case needed for the uniqueness theorem on independent decompositions and for the recognition-work constraint theorem in the same module. It directly supports the T-1 to T0 bridge by ensuring the zero-cost identity behaves correctly under the independent-additivity axiom. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.