sign_indistinguishable
plain-language theorem explainer
The sign recognizer on the integers induces an equivalence relation whose classes are exactly the negative integers, zero, and the positive integers. Researchers working with recognition geometries cite this to confirm that the quotient under signRecognizer has precisely three cells. The proof is a one-line wrapper that applies rfl because Indistinguishable is defined directly in terms of equality of the recognizer map.
Claim. For integers $n$ and $m$, $n$ is indistinguishable from $m$ under the sign recognizer if and only if signOf$(n)$ equals signOf$(m)$, where signOf maps each integer to its class in the three-element set of negative, zero, and positive.
background
The Recognition Geometry module supplies concrete examples that illustrate how recognizers induce equivalence relations on configuration spaces. The sign recognizer is built from the function signOf, which sends negative integers to Sign.neg, zero to Sign.zero, and positive integers to Sign.pos. Indistinguishability under a recognizer holds exactly when the recognizer map sends both configurations to the same event, as defined in the Indistinguishable module.
proof idea
The proof is a one-line wrapper that applies rfl. By the definition of Indistinguishable, the left side holds precisely when signOf n equals signOf m, which is the right side, so the biconditional follows immediately by reflexivity.
why it matters
This result verifies the sign-recognizer example referenced in the examples_status definition, which later uses it to illustrate that sign and magnitude together refine distinctions on nonzero integers. It supplies a finite three-class quotient that demonstrates the basic recognition geometry construction before composition principles are examined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.