discreteLocalConfigSpace
plain-language theorem explainer
discreteLocalConfigSpace equips any nonempty type C with the discrete locality structure in which every subset containing a point c counts as a neighborhood of c. Recognition geometers cite this as the finest possible neighborhood system satisfying RG1. The definition proceeds by direct construction of the neighborhood family as all containing sets and verification of the four required axioms by set-theoretic reasoning.
Claim. For a nonempty type $C$, the discrete local configuration space is the instance of LocalConfigSpace $C$ in which $N(c)$ consists of all subsets $Usubseteq C$ such that $c in U$, with membership, nonemptiness, intersection closure, and refinement holding by construction.
background
LocalConfigSpace $C$ extends ConfigSpace $C$ by a neighborhood assignment $N:Cto Set(Set C)$ together with the axioms that every $Uin N(c)$ contains $c$, that $N(c)$ is nonempty, that intersections of neighborhoods contain a neighborhood, and that neighborhoods admit refinement around nearby points. The module RecogGeom.Locality presents this structure as Axiom RG1, ensuring that recognition is always performed from within a finite neighborhood rather than globally. Upstream definitions such as Configuration in InitialCondition supply the underlying spaces of ledger entries on which the neighborhood structure is imposed.
proof idea
The definition directly sets $N(c)$ to the collection of all subsets containing $c$. It verifies mem_of_mem_N by the membership condition in the set comprehension, N_nonempty by exhibiting the full set $C$, intersection_closed by exhibiting the intersection of two such sets, and refinement by reusing the same neighborhood.
why it matters
This definition supplies the canonical example of the finest locality structure compatible with RG1. It serves as a basic building block for Recognition Geometry, allowing subsequent developments to instantiate locality in the discrete case before considering coarser structures. It directly realizes the neighborhood axioms without additional assumptions on the configuration space or appeal to the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.