ConfigSpace
plain-language theorem explainer
ConfigSpace supplies the abstract typeclass for configuration spaces used throughout the recognition-work constraint development, consisting of an empty element, commutative associative join, consistency predicate, and independence relation obeying monoid laws plus preservation of consistency and inconsistency under independent joins. Researchers citing the T-1 to T0 bridge or constructing cost functions with independent additivity would reference this structure as the required algebraic substrate. The declaration is a direct class definition;
Claim. Let $C$ be a type. A configuration space on $C$ is given by an element $e$, a binary operation $+$ , a predicate $K$ for consistency, and a binary relation $I$ for independence, such that $+$ is commutative and associative with identity $e$, $I$ is symmetric, $e$ is independent of every element and is consistent, the join of two independent consistent elements is consistent, and the join of an independent pair remains inconsistent whenever either factor is inconsistent.
background
The module formalizes the recognition-work constraint theorem from the T-1 to T0 bridge paper by adding the independent-additivity axiom to the satisfiability dichotomy. ConfigSpace is the opening typeclass that abstracts any natural configuration system (predicate constraints, multisets of formulas, typed assertions) so that the subsequent cost axioms can be stated uniformly. It equips a carrier with an empty configuration, a join operation forming a commutative monoid, a consistency predicate, and an independence relation that is symmetric and satisfies the listed preservation properties.
proof idea
This is the base class definition; the structure is introduced directly by listing the fields and axioms with no reduction steps or tactic applications required.
why it matters
ConfigSpace is the parent structure for CostFunction (which encodes dichotomy and independent additivity) and for RecognitionWorkConstraintCert (the master certificate bundling the constraint theorem). It also appears in Modal.Possibility and RecogGeom.Core. The declaration supplies the algebraic substrate for the recognition-work bridge, ensuring cost is additive over independent inconsistent components and uniquely determined on indecomposable generators. In the Recognition Science setting it supports the T-1 to T0 step by turning the recognition-work primitive into a quantitative constraint without further stipulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.