LocalRecognizer
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not construct an explicit example of the map R.
- Does not specify the topology or metric on the local configuration space.
- Does not derive event cardinality from the phi-ladder or J-cost.
- Does not prove existence of recognizers beyond the inherited axiom.
formal statement (Lean)
41structure LocalRecognizer (C : Type*) (E : Type*) extends
42 LocalConfigSpace C, Recognizer C E
43
44/-! ## Basic Properties -/
45
46variable {C E : Type*}
47
48/-- The image of a recognizer has at least 2 elements -/
49theorem Recognizer.image_nontrivial (r : Recognizer C E) :
50 ∃ e₁ e₂ : E, e₁ ∈ Set.range r.R ∧ e₂ ∈ Set.range r.R ∧ e₁ ≠ e₂ := by
proof body
Definition body.
51 obtain ⟨c₁, c₂, hne⟩ := r.nontrivial
52 exact ⟨r.R c₁, r.R c₂, ⟨c₁, rfl⟩, ⟨c₂, rfl⟩, hne⟩
53
54/-- A trivial recognizer maps everything to the same event -/
55def Recognizer.isTrivial (r : Recognizer C E) : Prop :=
56 ∀ c₁ c₂ : C, r.R c₁ = r.R c₂
57
58/-- No recognizer is trivial (by definition) -/
59theorem Recognizer.not_trivial (r : Recognizer C E) : ¬r.isTrivial := by
60 intro h
61 obtain ⟨c₁, c₂, hne⟩ := r.nontrivial
62 exact hne (h c₁ c₂)
63
64/-! ## Local Image -/
65
66/-- The local image of a recognizer on a neighborhood -/
67def Recognizer.localImage (r : Recognizer C E) (U : Set C) : Set E :=
68 r.R '' U
69
70/-- Local image is subset of full image -/
71theorem Recognizer.localImage_subset_range (r : Recognizer C E) (U : Set C) :
72 r.localImage U ⊆ Set.range r.R :=
73 Set.image_subset_range r.R U
74
75/-! ## Preimage Structure -/
76
77/-- The preimage (fiber) of an event under a recognizer -/
78def Recognizer.fiber (r : Recognizer C E) (e : E) : Set C :=
79 r.R ⁻¹' {e}
80
81/-- A configuration is in the fiber of its event -/
82theorem Recognizer.mem_fiber_self (r : Recognizer C E) (c : C) :
83 c ∈ r.fiber (r.R c) := by
84 simp [fiber]
85
86/-- Fibers partition the configuration space -/
87theorem Recognizer.fibers_partition (r : Recognizer C E) :
88 ∀ c : C, ∃! e : E, c ∈ r.fiber e := by
89 intro c
90 use r.R c
91 constructor
92 · exact r.mem_fiber_self c
93 · intro e he
94 simp [fiber] at he
95 exact he.symm
96
97/-! ## Event Lifting -/
98
99/-- An event is realized by some configuration if it's in the image -/
100def Recognizer.isRealized (r : Recognizer C E) (e : E) : Prop :=
101 e ∈ Set.range r.R
102
103/-- Every event in the image has a witness configuration -/
104noncomputable def Recognizer.witness (r : Recognizer C E) (e : E)
105 (he : r.isRealized e) : C :=
106 he.choose
107
108theorem Recognizer.witness_spec (r : Recognizer C E) (e : E)
109 (he : r.isRealized e) : r.R (r.witness e he) = e :=
110 he.choose_spec
111
112/-! ## Constant Recognizer (Trivial Event Space) -/
113
114/-- A constant function is NOT a valid recognizer (it's trivial) -/