IsRegular
plain-language theorem explainer
A definition stating that a recognizer r on local configuration space L is regular exactly when it is locally regular at every configuration c. Recognition geometry researchers cite it when stating the RG5 axiom that guarantees resolution cells remain coherent blobs inside neighborhoods. The definition is a direct universal quantification over the local regularity predicate IsLocallyRegular.
Claim. Let $L$ be a local configuration space over configurations $C$ and let $r$ be a recognizer. Then $r$ is regular on $L$ if and only if for every configuration $c$ the recognizer $r$ is locally regular at $c$.
background
The module develops recognition connectivity: two configurations are connected when a path between them stays inside one resolution cell. Core notions are IsRecognitionConnected (a set is connected when all its points are equivalent), IsLocallyRegular (preimages under the recognizer remain connected inside neighborhoods), and SatisfiesRG5 (the axiom that every recognizer satisfies local regularity). The physical reading is that nearby configurations must cluster coherently rather than fragment, which is required for smooth geometric structure to emerge from discrete recognition steps.
proof idea
This is a definition whose body is the universal statement that local regularity holds at every configuration. It functions as a one-line wrapper that expands directly to the forall quantifier over IsLocallyRegular.
why it matters
IsRegular supplies the predicate used to state the RG5 local regularity axiom. It is invoked inside the structure SatisfiesRG5 (locally_regular : IsRegular L r) and inside the theorem constant_recognizer_regular that shows constant recognizers are regular. In the broader framework it closes the connectivity step that lets resolution cells act as the atoms of geometry, supporting the emergence of D = 3 spatial dimensions and the eight-tick octave from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.