IsRegular
plain-language theorem explainer
IsRegular defines global regularity of a recognizer r on local configuration space L to mean local regularity holds at every configuration c. Recognition-geometry researchers cite it when stating the RG5 axiom for coherent resolution cells. The declaration is a direct universal quantification with no separate proof steps.
Claim. A recognizer $r$ is regular on local configuration space $L$ when it is locally regular at every configuration $c$.
background
The module develops recognition connectivity: two configurations are connected when a path stays inside one resolution cell. Key sibling notions are IsRecognitionConnected (a set is connected when all its points are equivalent under the recognizer), IsLocallyRegular (preimages remain connected inside neighborhoods), and SatisfiesRG5 (the full axiom that every recognizer satisfies local regularity). MODULE_DOC states that RG5 prevents resolution cells from fragmenting into Cantor-like sets and thereby lets smooth geometric structure emerge from discrete recognition steps.
proof idea
One-line definition that expands directly to the universal quantifier over the sibling predicate IsLocallyRegular.
why it matters
IsRegular supplies the predicate inside the structure SatisfiesRG5 and is invoked by constant_recognizer_regular and connectivity_status. It encodes the RG5 local-regularity step that keeps resolution cells blob-like rather than scattered, directly supporting the emergence of smooth physics from the recognition process described in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.