magnitude_distinguishes_3_5
plain-language theorem explainer
The theorem establishes that the magnitude recognizer on integers places 3 and 5 in distinct equivalence classes. Researchers examining concrete partitions in recognition geometries would cite it to show magnitude yields infinitely many classes. The proof is a one-line term-mode simplification that unfolds the definitions of indistinguishability and the magnitude recognizer to reach an immediate contradiction.
Claim. The magnitude recognizer on the integers places 3 and 5 in distinct equivalence classes, since their absolute values differ: they are not identified under the recognizer.
background
The RecogGeom.Examples module supplies concrete recognition geometries on finite sets and on ℤ to illustrate the framework. The magnitude recognizer maps each integer to its absolute value, producing infinitely many classes indexed by nonnegative integers (0, 1, 2, ...). The module contrasts this with the sign recognizer, which yields exactly three classes, and notes that their composition refines distinctions for nonzero integers.
proof idea
The proof is a term-mode one-liner that applies simp to unfold Indistinguishable and magnitudeRecognizer. This reduces the negated equality to the fact that the absolute values of 3 and 5 differ, which holds directly.
why it matters
It contributes to the examples_status definition in the same module, which summarizes verification results for discrete, sign, and magnitude recognizers. The result supports the Composition Principle in the module documentation: neither sign nor magnitude alone distinguishes all pairs, but together they do for nonzero integers. It aligns with the Recognition Composition Law by demonstrating how magnitude supplies additional distinguishing power.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.