LocalRecognizer
plain-language theorem explainer
LocalRecognizer pairs a local configuration space on C with a recognition map R: C to E that produces at least two distinct events. Researchers formalizing axiom RG2 in Recognition Geometry cite this structure when defining how underlying configurations generate observable events. The definition works by direct extension of the Recognizer structure, inheriting its nontriviality condition with no separate proof required.
Claim. A local recognizer on configuration space $C$ and event space $E$ is a structure extending the local configuration space on $C$ together with a map $R: C → E$ such that there exist distinct $c_1, c_2 ∈ C$ with $R(c_1) ≠ R(c_2)$.
background
The Recognition Geometry module defines recognition maps under axiom RG2: there exists a map $R: C → E$ whose image has at least two elements. The sibling Recognizer structure supplies the function $R$ and the nontriviality witness. LocalRecognizer augments this with locality constraints via the LocalConfigSpace extension. Upstream results from SpectralEmergence supply the event-space cardinality $|E| = D × 2^{D-1}$ and the gauge content forced by the Q3 cube.
proof idea
The declaration is a structure definition that extends LocalConfigSpace C and Recognizer C E. It inherits the recognition function R and the nontriviality existential directly; no separate tactic steps or lemmas are applied beyond the extension mechanism.
why it matters
This structure supplies the basic object used by the downstream recognizer_status definition that verifies the RG2 axiom implementation. It realizes the module insight that configurations are what the world does while events are what recognizers see. In the Recognition Science framework it bridges the forcing chain (T5 J-uniqueness through T8 D=3) to geometric recognition, consistent with the eight-tick octave and the RCL composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.