LocalRecognizer
plain-language theorem explainer
LocalRecognizer is the structure that pairs a local configuration space on C with a recognition map R: C → E obeying the nontriviality axiom. Recognition-geometry researchers cite it when localizing the RG2 existence statement. The declaration is a direct structure extension carrying no separate proof obligations.
Claim. A local recognizer on configuration space $C$ and event space $E$ is any structure that extends both a local configuration space on $C$ and a recognizer $R: C → E$ satisfying $∃ c_1,c_2 ∈ C$ with $R(c_1) ≠ R(c_2)$.
background
The module RecogGeom.Recognizer implements axiom RG2: there exists at least one map $R: C → E$ whose image contains at least two distinct events. The sibling structure Recognizer packages exactly this data: the function $R$ together with the witness that its image is nontrivial. LocalConfigSpace supplies the locality constraint on the domain $C$. Upstream results on spectral emergence and phi-forcing supply the broader setting in which such recognizers are later embedded, but are not invoked inside this definition.
proof idea
The declaration is a structure definition that performs a direct extension of LocalConfigSpace C and Recognizer C E; no tactics or lemmas are applied.
why it matters
It supplies the localized version of the recognizer required by RG2 and is referenced by the module-status definition recognizer_status, which records that locality and recognition have been combined. The construction sits inside the Recognition Geometry layer that precedes any appeal to the forcing chain T0–T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.