magnitudeRecognizer
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not extend the recognizer to real numbers or other base types.
- Does not derive physical constants or forcing-chain steps T0–T8.
- Does not prove any refinement or composition property by itself.
- Does not claim uniqueness among possible recognizers on ℤ.
Lean usage
theorem magnitude_indist_3_neg3 : Indistinguishable magnitudeRecognizer 3 (-3) := by simp [Indistinguishable, magnitudeRecognizer]formal statement (Lean)
105def magnitudeRecognizer : Recognizer ℤ ℕ where
106 R := fun n => n.natAbs
proof body
Definition body.
107 nontrivial := by
108 use 0, 1
109 simp
110
111/-- **Theorem**: n ~ m iff |n| = |m| -/