constant_recognizer_regular
plain-language theorem explainer
Constant recognizers satisfy local regularity at every configuration. Researchers building recognition geometry from RG5 axioms cite this to guarantee coherent resolution cells under uniform maps. The proof extracts a neighborhood from the local config space at each point and applies the constancy hypothesis to verify preimage connectedness.
Claim. If the recognition map of recognizer $r$ is constant, then $r$ is locally regular everywhere with respect to local configuration space $L$.
background
Recognition geometry examines when configurations remain connected inside resolution cells. LocalConfigSpace supplies a neighborhood predicate N for each configuration c. IsRegular L r holds when IsLocallyRegular L r c is true for every c, which requires that preimages under the recognizer map stay connected inside those neighborhoods. The module states that this is the RG5 axiom ensuring resolution cells form coherent blobs rather than scattered fragments, allowing smooth structure to emerge from discrete recognition. Upstream results supply the nonempty neighborhood property from RecognitionLatticeFromRecognizer and the basic recognizer structure from PhiForcingDerived.
proof idea
Fix arbitrary configuration c. Obtain a nonempty neighborhood U from L.N_nonempty c. Use U to witness local regularity at c. For any c1, c2 inside U the constancy hypothesis supplies the required equality of recognizer values, closing the connectedness check.
why it matters
The result supplies the constant-recognizer case of RG5 and is referenced by the module's connectivity_status summary. It supports the claim that RG5 prevents pathological fragmentation of resolution cells, enabling coherent geometric structure consistent with the forcing chain landmarks T7 (eight-tick octave) and T8 (D=3). No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.