fundamental_theorem
The theorem states that two configurations belong to the same recognition quotient class precisely when the recognizer maps them to identical events. Modelers of observation in geometry or information theory cite it to equate observable distinctions with recognizer outputs. The proof is a direct one-line application of the quotient equality lemma from the quotient construction.
claimLet $C$ be a nonempty configuration space and $E$ a nontrivial event space. For any recognizer $r$ from $C$ to $E$ and any configurations $c_1, c_2$ in $C$, the equivalence classes satisfy $[c_1]_r = [c_2]_r$ if and only if $r(c_1) = r(c_2)$, where the quotient is taken with respect to the recognizer's event assignment.
background
A configuration space is a nonempty type of possible world states; recognizers receive only events, never the configurations themselves. An event space is a type containing at least two distinct observable outcomes. The recognition quotient is formed by identifying configurations that produce the same event under a given recognizer. The module states the three pillars of recognition geometry, with this result realizing the first: the quotient captures exactly the observable distinctions. Upstream results supply the ConfigSpace and EventSpace classes that parametrize the theorem.
proof idea
The proof is a one-line wrapper that applies the quotientMk_eq_iff lemma from the quotient module. That lemma directly equates membership in the recognition quotient to equality of the recognizer's event values, discharging the biconditional without further tactics.
why it matters in Recognition Science
This result is the cornerstone of recognition geometry and feeds the complete summary of all modules. It justifies the identification of observable space with the quotient by recognizer events, closing the first pillar. The statement aligns with the framework's emphasis on finite resolution and indistinguishability under recognition, though it leaves composite recognizers to the extended version.
scope and limits
- Does not define the internal structure or construction of any recognizer.
- Does not treat composite or multiple recognizers.
- Does not establish existence or uniqueness of the quotient beyond the stated equivalence.
- Does not connect to cost, spectral, or forcing structures from other modules.
formal statement (Lean)
98theorem fundamental_theorem {C E : Type*} [ConfigSpace C] [EventSpace E]
99 (r : Recognizer C E) (c₁ c₂ : C) :
100 recognitionQuotientMk r c₁ = recognitionQuotientMk r c₂ ↔ r.R c₁ = r.R c₂ :=
proof body
Term-mode proof.
101 quotientMk_eq_iff r
102
103/-- **Extended Fundamental Theorem** for composite recognizers. -/