zero_pos_dist
plain-language theorem explainer
The sign recognizer on the integers maps each number to one of three classes: negative, zero, or positive. This theorem shows that zero and one fall into distinct classes and are therefore distinguishable. It is cited when verifying that the sign example produces exactly three equivalence classes. The proof is a direct simplification that reduces the claim to the case distinction in the sign function.
Claim. Let $r$ be the sign recognizer on the integers, where $r(n)$ equals negative if $n<0$, zero if $n=0$, and positive otherwise. Then $0$ and $1$ are distinguishable under $r$: they do not produce the same recognition event.
background
Recognition geometry equips a configuration space with a recognizer that maps each configuration to an event; two configurations are indistinguishable precisely when they map to the same event. The sign recognizer is built from the auxiliary function that returns Sign.neg for negative integers, Sign.zero for zero, and Sign.pos otherwise. The module supplies concrete examples to show how the induced equivalence classes behave: the discrete case yields a quotient isomorphic to the original space, while the sign case yields three classes.
proof idea
The term proof applies simp to the definitions of Indistinguishable, the sign recognizer, and the sign function. This reduces the negated equality to the observation that signOf 0 equals Sign.zero while signOf 1 equals Sign.pos.
why it matters
The result confirms the module claim that the sign recognizer on integers produces exactly three equivalence classes. It supplies a concrete partition used to illustrate how recognition refines distinctions, consistent with the Recognition Composition Law and the construction of recognizers that feed into the forcing chain deriving three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.