magnitude_indistinguishable
plain-language theorem explainer
The magnitude recognizer on integers equates n and m precisely when they share the same absolute value. Researchers building recognition geometries cite this to confirm the induced partition of ℤ into classes indexed by ℕ. The proof reduces to reflexivity once the recognizer map and indistinguishability predicate are unfolded.
Claim. $n$ and $m$ are indistinguishable under the magnitude recognizer if and only if $|n| = |m|$, where the recognizer sends each integer to its absolute value.
background
Recognition geometry pairs a configuration space with a recognizer that maps each configuration to an event. The magnitude recognizer is the map sending $n$ to $|n|$, with the associated indistinguishability relation holding exactly when two configurations produce the same event. This concrete example on ℤ shows infinitely many classes (one for each natural number), contrasting with the three-class sign recognizer in the same module.
proof idea
The proof is a one-line wrapper that applies reflexivity. Unfolding the definitions of Indistinguishable and magnitudeRecognizer makes both sides of the biconditional identical by construction of the absolute-value map.
why it matters
This result populates the examples_status summary that demonstrates composition of sign and magnitude recognizers. It supplies a concrete instance confirming that the magnitude map induces the expected equivalence classes before the composition principle is stated. The theorem sits inside the catalog of recognizers that illustrate how recognition geometry refines partitions on ℤ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.