Recognizer
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not construct an explicit R for any concrete C and E.
- Does not prove existence of a recognizer in any model.
- Does not impose continuity, linearity, or other structure on R.
- Does not reference J-cost, defect distance, or the φ-ladder.
formal statement (Lean)
34structure Recognizer (C : Type*) (E : Type*) where
35 /-- The recognition function mapping configurations to events -/
36 R : C → E
37 /-- The recognizer is nontrivial: at least two distinct events are produced -/
38 nontrivial : ∃ c₁ c₂ : C, R c₁ ≠ R c₂
39
40/-- A local recognizer is a recognizer on a local configuration space -/