magnitude_indist_3_neg3
plain-language theorem explainer
Under the magnitude recognizer on integers, which sends each n to its absolute value, the values 3 and -3 map to the same natural number and are therefore indistinguishable. Researchers constructing concrete partitions in recognition geometry cite this to exhibit how magnitude collapses signs into shared classes. The proof is a one-line simp wrapper that unfolds the two definitions and checks the equality directly.
Claim. Let $r:ℤ→ℕ$ be the magnitude recognizer $r(n)=|n|$. Then $3$ and $-3$ are indistinguishable under $r$, i.e., $r(3)=r(-3)$.
background
Recognition geometry equips a configuration space with a recognizer that maps each configuration to an event; indistinguishability is the induced equivalence relation of producing identical events. The magnitude recognizer on ℤ is the map sending every integer n to its absolute value |n|, so the equivalence classes are {0}, {±1}, {±2}, … . The module supplies concrete examples that contrast this infinite partition with the three-class sign partition and with their composition.
proof idea
The proof is a one-line wrapper that applies simp to the definitions of Indistinguishable and magnitudeRecognizer. Unfolding yields the equality |3| = |-3| in ℕ, which is immediate.
why it matters
The result is referenced in the examples_status definition, which records that sign and magnitude each leave some pairs indistinguishable while their joint use separates nonzero integers up to sign. It supplies a basic verified instance of the magnitude partition inside the Recognition Geometry examples, illustrating how recognizers induce concrete quotients without invoking the full forcing chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.