ConfigSpace
plain-language theorem explainer
ConfigSpace is a type class requiring a configuration space C to be nonempty, serving as axiom RG0 that guarantees underlying states exist before events or recognizers are introduced. Physicists building recognition-based models cite it to anchor the domain for cost functions and geometry derivations. The definition is a minimal one-field class whose witness extractor is a direct application of the Nonempty instance.
Claim. A configuration space is a type $C$ such that $C$ is nonempty.
background
Recognition Geometry treats configuration spaces as the primitive collection of possible world states; recognizers observe only derived events. The module RecogGeom.Core opens with this minimal structure to reverse the usual geometric order, letting space emerge from recognition maps rather than being presupposed. Upstream results supply a richer ConfigSpace in CostFromDistinction that adds an empty element, commutative join, consistency predicate, and independence relation, but the present declaration isolates the single nonemptiness requirement stated in RG0.
proof idea
The class is introduced directly by its nonempty field of type Nonempty C. The witness definition is a one-line wrapper that invokes the supplied Nonempty instance and extracts an element via .some.
why it matters
This declaration supplies the base axiom RG0 that every subsequent Recognition Geometry construction presupposes. It is invoked by the config_exists theorem to produce an explicit witness and by RecognitionTriple and CostFunction to ensure the recognition-work bridge and cost additivity are stated over a nonempty domain. In the larger framework it precedes the J-uniqueness and phi-ladder steps by guaranteeing a carrier set on which the Recognition Composition Law can act.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.