config_exists
plain-language theorem explainer
The theorem guarantees that any type C carrying a ConfigSpace instance is nonempty by exhibiting an explicit witness element drawn from the class. Researchers formalizing recognition axioms or building event spaces from RG0 would cite it to replace vacuous existence with a constructive starting state. The proof is a one-line term that applies the witness accessor and reflexivity.
Claim. Let $C$ be a type equipped with a ConfigSpace structure. Then there exists an element $c$ in $C$ such that $c$ equals the witness configuration extracted from the structure.
background
Recognition Geometry derives space from recognition maps. The module defines ConfigSpace as a type of possible world states whose only required property is nonemptiness (RG0). The class supplies a Nonempty instance; the witness function extracts an element from it as the canonical starting configuration.
proof idea
The proof is a one-line term that constructs the existential witness by pairing ConfigSpace.witness C with the reflexivity proof that the element equals itself.
why it matters
The result discharges the constructive form of axiom RG0 in the Recognition Geometry core. It supplies the nonempty starting point required by sibling declarations such as EventSpace and RecognitionTriple. In the larger framework it anchors the transition from abstract configurations to geometric structure without invoking external models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.