trivialLocalConfigSpace
plain-language theorem explainer
The trivialLocalConfigSpace supplies the coarsest locality structure on any nonempty configuration space C, with N(c) always equal to the singleton containing the full set C. Researchers modeling minimal recognition geometry cite it as the base case satisfying axiom RG1 without metric or topology assumptions. The definition proceeds by direct field assignment for N together with four short verifications that substitute singleton membership and apply Set.univ and inter_self.
Claim. Let $C$ be a nonempty type. The trivial local configuration space on $C$ is the structure whose neighborhood family satisfies $N(c) = {C}$ for every $c$, with the membership, nonemptiness, intersection-closure, and refinement axioms of a local configuration space holding by direct substitution into the universal set.
background
A local configuration space on a type $C$ augments the plain configuration space with a neighborhood assignment $N : C → Set (Set C)$. The structure requires that every $U ∈ N(c)$ contains $c$, that $N(c)$ is nonempty, that intersections of neighborhoods contain a neighborhood, and that every neighborhood admits refinements. These are the minimal axioms of RG1 in recognition geometry, allowing statements about nearby configurations without committing to a metric or topology. The module sets this structure as the foundation for all subsequent locality arguments in the Recognition framework.
proof idea
The definition is a direct structure instance. It sets $N$ to the constant function returning the singleton containing the universal set. Membership follows by rewriting singleton membership to the universal set and applying mem_univ. Nonemptiness is immediate from the singleton. Intersection closure and refinement are obtained by substitution of the two singleton hypotheses followed by Set.inter_self and Subset.rfl.
why it matters
This supplies the canonical coarsest model of RG1 locality, serving as the base case before any refinement or discrete structure is imposed. It demonstrates that the neighborhood axioms can be satisfied with a single global neighborhood, providing a minimal anchor for recognition geometry. In the broader Recognition Science setting it precedes constructions that introduce the phi-ladder, J-cost, or eight-tick octave, and illustrates the separation between locality and the later emergence of spatial dimension D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.