LocalConfigSpace
plain-language theorem explainer
LocalConfigSpace augments any configuration space C with a neighborhood assignment N(c) obeying containment, nonemptiness, intersection closure, and refinement. Recognition-geometry work cites this as the precise statement of axiom RG1. The declaration is a direct structure definition whose fields encode the four axioms; the listed theorems are one-line projections of those fields.
Claim. A local configuration space on a type $C$ is a configuration space over $C$ equipped with a map $N:C→𝒫(𝒫(C))$ such that (i) $c∈U$ for every $U∈N(c)$, (ii) $N(c)$ is nonempty for each $c$, (iii) any two neighborhoods $U,V∈N(c)$ admit a common refinement $W∈N(c)$ with $W⊆U∩V$, and (iv) if $U∈N(c)$ and $c'∈U$ then some $V∈N(c')$ satisfies $V⊆U$.
background
Recognition geometry opens with axiom RG1: recognition is always performed inside finite neighborhoods of configurations rather than globally. The module therefore extends the base ConfigSpace (imported from RecogGeom.Core) by a neighborhood map N that assigns to each point c a collection of subsets of C. The four listed axioms are the minimal conditions that let one speak of “varying a configuration a little” without choosing a metric or topology.
proof idea
The structure is declared directly by listing the four neighborhood axioms as fields. The four theorems that follow (has_neighborhood, self_mem_neighborhood, common_refinement, sub_neighborhood) are one-line wrappers that simply project the corresponding fields of an instance L. The neighborhoodFilterBase and neighborhoodFilter definitions are likewise direct constructions from those fields.
why it matters
LocalConfigSpace supplies the locality interface RG1 that every later recognition-geometry construction must respect. It is the point at which discrete configuration spaces acquire the ability to talk about nearby states, preparing the ground for the neighborhood-filter constructions that appear immediately below. The definition closes the basic locality layer; no further scaffolding is required.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.