diff_magnitude_dist
The theorem establishes that integers 2 and 3 produce distinct events under the magnitude recognizer, which maps each integer to its absolute value. Recognition geometers cite it when confirming that the magnitude map separates positive integers of unequal size. The proof reduces the negated equality to an immediate numerical falsehood by unfolding the two definitions.
claimLet $R:ℤ→ℕ$ be the magnitude recognizer $R(n)=|n|$. Then $R(2)≠R(3)$.
background
The module supplies concrete recognition geometries on the integers. The magnitude recognizer is the map $n↦|n|$, which partitions ℤ into infinitely many classes indexed by the nonnegative integers. Two configurations are indistinguishable under a recognizer precisely when they yield the same recognition event, i.e., when the recognizer function returns equal values. The upstream Composition axiom supplies the multiplicative consistency condition that later forces the functional form of recognition cost, but is not invoked in this elementary example.
proof idea
The proof is a one-line wrapper that applies simp to the definitions of Indistinguishable and magnitudeRecognizer, reducing the claim to the false statement 2=3.
why it matters in Recognition Science
The result illustrates that magnitude alone distinguishes 3 from 5 while sign alone distinguishes 3 from -3, thereby motivating the composition construction that refines both. It occupies an example slot in the Recognition Geometry module and aligns with the module's stated key insight that composition of recognizers increases distinguishing power. No open question is touched.
scope and limits
- Does not address the sign recognizer or its equivalence classes.
- Does not extend the claim to real numbers or continuous configuration spaces.
- Does not invoke or depend on the Recognition Composition Law.
- Does not treat quotient spaces or indistinguishability after identification.
formal statement (Lean)
121theorem diff_magnitude_dist : ¬Indistinguishable magnitudeRecognizer 2 3 := by
proof body
Term-mode proof.
122 simp [Indistinguishable, magnitudeRecognizer]
123
124/-! ## Example 4: Composition Refines Both -/
125
126/-- **Key Observation**: Combining sign and magnitude gives a finer recognizer.
127
128 - Sign alone: 3 ~ -3 (both positive/negative)... wait, that's wrong
129 - Actually sign: 3 ≁ -3 (positive vs negative)
130 - Magnitude alone: 3 ~ -3 (both have magnitude 3)
131
132 So sign distinguishes 3 from -3, but magnitude doesn't.
133 Conversely, magnitude distinguishes 3 from 5, both positive.
134
135 The composition (sign, magnitude) distinguishes both. -/