Recognizer
plain-language theorem explainer
The Recognizer structure defines a function R from a configuration space C to an event space E such that at least two configurations map to distinct events. Researchers in recognition geometry cite it as the direct implementation of axiom RG2. The declaration is a structure definition that packages the map and its nontriviality witness with no separate proof steps.
Claim. A recognizer consists of a function $R : C → E$ together with a witness that there exist $c_1, c_2 ∈ C$ satisfying $R(c_1) ≠ R(c_2)$.
background
The Recognition Geometry module introduces recognition maps as the objects that connect configurations (what the world does) to events (what is observed), per axiom RG2 requiring at least one map whose image has size at least 2. The structure Recognizer packages the recognition function R with the explicit nontriviality condition. Upstream results supply concrete nontriviality witnesses, including the seven nontrivial kinship systems from anthropology and the nuclear density tiers from astrophysics that realize discrete φ-scaled structures.
proof idea
This declaration is a structure definition that directly specifies the two fields: the recognition function R and the existential witness for nontriviality. No lemmas or tactics are invoked beyond the built-in structure constructor.
why it matters
The definition realizes axiom RG2, establishing the basic object that links configurations to observable events in the Recognition Geometry layer. It supplies the foundation for sibling constructions such as LocalRecognizer. In the broader framework it marks the transition from the forcing chain to the event world, where recognition maps begin to generate the observable physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.