constant_recognizer_regular
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.
claimIf 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 in Recognition Science
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.
scope and limits
- Does not establish local regularity for non-constant recognizers.
- Does not prove global connectivity of the entire configuration space.
- Does not derive the full SatisfiesRG5 axiom from weaker assumptions.
- Does not address empirical calibration of the recognizer map.
formal statement (Lean)
115theorem constant_recognizer_regular (L : LocalConfigSpace C) (r : Recognizer C E)
116 (hconst : ∀ c₁ c₂, r.R c₁ = r.R c₂) :
117 IsRegular L r := by
proof body
Term-mode proof.
118 intro c
119 obtain ⟨U, hU⟩ := L.N_nonempty c
120 use U, hU
121 intro c₁ c₂ _ _
122 exact hconst c₁ c₂
123
124/-! ## The Role of RG5 in Geometry -/
125
126/-- **Intuition**: RG5 ensures that "resolution cells don't fragment".
127
128 Without RG5, a resolution cell could look like a Cantor set:
129 infinitely fragmented within any neighborhood. With RG5, resolution
130 cells are locally "blob-like"—they stay together coherently.
131
132 This is what allows smooth geometric structure to emerge:
133 resolution cells become the "atoms" of recognition geometry,
134 and RG5 ensures these atoms are well-behaved. -/
135
136/-! ## Module Status -/
137