constant_recognizer_regular
plain-language theorem explainer
Constant recognizers satisfy local regularity (RG5) at every configuration. Researchers on recognition geometry cite this when checking that uniform maps yield coherent resolution cells. The proof obtains a neighborhood from the local configuration space nonempty axiom and applies the constancy hypothesis directly to pairs inside it.
Claim. If a recognizer $r$ satisfies $r.R(c_1)=r.R(c_2)$ for all configurations $c_1,c_2$, then $r$ is locally regular everywhere: for every $c$ there exists a neighborhood $U$ of $c$ such that $r$ takes the same value on all points of $U$.
background
The module introduces recognition connectivity and the RG5 axiom. IsRegular is defined as the universal quantification over all configurations of IsLocallyRegular, which requires that recognizer preimages remain connected inside neighborhoods; this prevents resolution cells from fragmenting into Cantor-like sets. LocalConfigSpace supplies the neighborhood structure via its nonempty axiom. The module states that RG5 makes resolution cells the coherent atoms from which smooth geometry can emerge.
proof idea
Term-mode proof. Introduce arbitrary configuration $c$, obtain a neighborhood $U$ from the nonempty axiom of the local configuration space, then discharge the local regularity condition by applying the constancy hypothesis to any pair of points inside $U$.
why it matters
The result shows constant recognizers obey RG5 and is invoked by the connectivity_status definition that summarizes the connected-set properties. It fills the base case for the claim that RG5 produces blob-like resolution cells, supporting the transition from discrete recognition to smooth structure. It sits inside the T5-T8 forcing chain by guaranteeing regularity for the simplest recognizers before more complex phi-ladder constructions are considered.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.