diff_magnitude_dist
plain-language theorem explainer
The magnitude recognizer on integers separates 2 from 3 because their absolute values differ. Workers on concrete recognition geometries cite this to verify that the absolute-value map induces distinct classes for distinct positive integers. The proof is a one-line term-mode simplification that unfolds the indistinguishability predicate and the recognizer definition.
Claim. Let $R : ℤ → ℕ$ be the magnitude recognizer defined by $R(n) = |n|$. Then $R(2) ≠ R(3)$.
background
The module supplies concrete recognition geometries on discrete spaces. The magnitude recognizer is the map sending each integer to its absolute value, yielding infinitely many classes indexed by nonnegative integers. Indistinguishability under a recognizer holds precisely when two configurations produce the same recognition event, i.e., map to the identical element of the event space. This example is placed beside the sign recognizer, which partitions ℤ into three classes (negative, zero, positive). The upstream definition of Indistinguishable is the core equivalence relation of recognition geometry; the magnitude recognizer itself is introduced locally as the absolute-value map.
proof idea
The proof is a term-mode one-liner that applies simp to the definitions of Indistinguishable and magnitudeRecognizer, reducing the negated equality directly to the fact that the natural numbers 2 and 3 are distinct.
why it matters
This theorem supplies a basic verification that the magnitude recognizer distinguishes integers of different sizes, supporting the module's key observation that magnitude alone separates 2 from 3 while sign does not. It illustrates how recognizers induce different partitions on the same configuration space and prepares the ground for the refinement claim when sign and magnitude are composed. It contributes to the examples section that demonstrates the framework's concrete behavior before composition is invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.