magnitudeRecognizer
plain-language theorem explainer
The magnitude recognizer on the integers maps each n to its absolute value |n|. Researchers working with concrete recognition geometries cite it to exhibit countably infinite equivalence classes on ℤ. The definition is a structure instance whose nontriviality field is discharged by a one-line tactic supplying explicit witnesses 0 and 1.
Claim. The magnitude recognizer is the map $R:ℤ→ℕ$ given by $R(n)=|n|$, which induces the equivalence $n∼m$ if and only if $|n|=|m|$.
background
The Recognition Geometry module develops concrete examples to illustrate the general framework. The magnitude recognizer on ℤ uses the absolute-value function to partition integers into classes indexed by natural numbers, yielding infinitely many classes. Indistinguishability is defined via equality of the R values. This instance contrasts with the sign recognizer, which produces exactly three classes. The definition instantiates the Recognizer structure imported from Core and Recognizer modules; the upstream nontrivial result from KinshipGraphCohomology supplies the parallel notion of a nontrivial collection in another domain.
proof idea
The definition directly sets the R field to the natAbs function. The nontrivial field is discharged by a one-line tactic that supplies 0 and 1 as witnesses and applies simp to confirm their images differ.
why it matters
This definition is invoked by downstream theorems in the same module, including composition_refines (which shows sign and magnitude together refine equivalence for nonzero integers) and magnitude_indistinguishable (which states the equivalence condition explicitly). It realizes the magnitude example described in the module documentation and supplies a discrete illustration of how recognition geometries can produce infinitely many classes. It supports the broader program of exhibiting concrete instances that can later be composed or compared with the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.