constant_not_recognizer
plain-language theorem explainer
Constant functions from a nonempty configuration space C to a single event e fail to qualify as recognizers because their image has cardinality one. Workers formalizing recognition maps under axiom RG2 cite this to exclude trivial cases. The tactic proof negates the existential quantifier over distinct outputs and reduces the resulting equality to reflexivity.
Claim. Let $C$ be a nonempty type and $e$ an element of the event space $E$. Then the constant map $f: C → E$ with $f(c) = e$ for all $c$ satisfies $¬∃ c_1,c_2 ∈ C$ such that $f(c_1) ≠ f(c_2)$.
background
Recognition Geometry defines a recognizer as a map $R: C → E$ whose image contains at least two distinct events, per axiom RG2. Configurations represent world states while events are the observable outputs of the map. The upstream definition E counts edges of the D-cube via $|E| = D × 2^{D-1}$, supplying the geometric cardinality of the event space.
proof idea
The term-mode proof first applies push_neg to the negated existential, then intros to obtain two configuration variables, and finally invokes rfl to witness that the constant function returns identical values.
why it matters
The result directly implements the nontriviality clause of axiom RG2 by excluding constant maps. It sits at the base of the Recognition Geometry module and ensures that only maps producing observable distinctions qualify as recognizers. No downstream theorems depend on it, confirming its role as a filter rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.