magnitude_indist_3_neg3

formal source

 136theorem sign_distinguishes_3_neg3 : ¬Indistinguishable signRecognizer 3 (-3) := by
 137  simp [Indistinguishable, signRecognizer, signOf]
 138
 139theorem magnitude_indist_3_neg3 : Indistinguishable magnitudeRecognizer 3 (-3) := by
 140  simp [Indistinguishable, magnitudeRecognizer]
 141
 142theorem sign_indist_3_5 : Indistinguishable signRecognizer 3 5 := by
 143  simp [Indistinguishable, signRecognizer, signOf]
 144
 145theorem magnitude_distinguishes_3_5 : ¬Indistinguishable magnitudeRecognizer 3 5 := by
 146  simp [Indistinguishable, magnitudeRecognizer]
 147
 148/-- **Composition Principle**: Neither sign nor magnitude alone distinguishes
 149    all pairs, but together they do (for nonzero integers). -/
 150theorem composition_refines :
 151    (∀ n m : ℤ, n ≠ 0 → m ≠ 0 →
 152      (Indistinguishable signRecognizer n m ∧ Indistinguishable magnitudeRecognizer n m) →
 153      n = m ∨ n = -m) := by
 154  intro n m hn hm ⟨hsign, hmag⟩
 155  simp only [Indistinguishable, signRecognizer, magnitudeRecognizer] at hsign hmag
 156  -- Same sign and same magnitude implies n = m or n = -m
 157  have h1 : n.natAbs = m.natAbs := hmag
 158  -- If signs match and magnitudes match, must be equal or negatives
 159  rcases Int.natAbs_eq_natAbs_iff.mp h1 with h | h
 160  · left; exact h
 161  · right; exact h
 162
 163/-! ## Physical Interpretation -/
 164
 165/-! ### Physical Interpretation
 166
 167These examples show how recognizers model measurement in physics:
 168- **Discrete** = perfect measurement (eigenvalue detection)
 169- **Sign/magnitude** = coarse measurements (binary outcomes)