IsLocallyRegular
plain-language theorem explainer
Local regularity at a configuration point means the set of nearby configurations sharing the same recognition output forms a connected cluster inside some neighborhood. Researchers establishing conditions for smooth geometry to emerge from discrete recognition cite this definition when verifying the RG5 axiom. It is expressed as a direct existential statement quantifying over a neighborhood and applying the connectivity predicate to the relevant preimage intersection.
Claim. Let $L$ be a local configuration space, $r$ a recognizer, and $c$ a configuration. The recognizer $r$ is locally regular at $c$ if there exists a neighborhood $U$ of $c$ in $L$ such that the preimage of the event $r(c)$ intersected with $U$ is recognition-connected.
background
The Recognition Geometry module develops connectivity to determine when discrete recognition structures can support smooth physics. Recognition-connected sets are those in which all points are equivalent under paths that remain inside a single resolution cell. Neighborhoods are supplied by the local configuration space structure around each point, while recognizers map configurations to events via their recognition function.
proof idea
This is a direct definition that packages the local connectivity requirement as an existential quantification over a neighborhood drawn from the local configuration space and the recognition-connected predicate applied to the preimage intersection. No lemmas are applied; the body is the primitive statement of the condition.
why it matters
This definition supplies the local half of the RG5 axiom and is invoked by the full regularity predicate that requires the property at every configuration. It appears in the connectivity status summary as the property that keeps resolution cells coherent rather than fragmented. In the Recognition Science framework it corresponds to the local regularity step that permits continuous structure to arise, consistent with the forcing chain through T8 and the emergence of D=3 dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.