IsRegular
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not specify the topology or neighborhood basis on the configuration space.
- Does not prove that any particular recognizer satisfies the property.
- Does not address global connectivity or path-connectedness outside neighborhoods.
- Does not incorporate J-cost, defect distance, or the phi-ladder explicitly.
Lean usage
example (L : LocalConfigSpace C) (r : Recognizer C E) : Prop := IsRegular L rformal statement (Lean)
86def IsRegular (L : LocalConfigSpace C) (r : Recognizer C E) : Prop :=
proof body
Definition body.
87 ∀ c : C, IsLocallyRegular L r c
88
89/-- **RG5**: Local Regularity Axiom.
90
91 A recognition geometry satisfies RG5 if every recognizer is locally regular.
92 This ensures that resolution cells form coherent "blobs" within neighborhoods,
93 not scattered fragments. -/