composition_refines

formal source

 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)
 170- **Composition** = combined measurements with finer resolution
 171
 172In quantum mechanics, observables ARE recognizers mapping states to eigenvalues. -/
 173
 174/-! ## Module Status -/
 175
 176def examples_status : String :=
 177  "✓ Discrete Recognition on Fin n\n" ++
 178  "  • discrete_indist_iff_eq: indistinguishable ↔ equal\n" ++
 179  "  • discrete_singleton_cells: each config is its own cell\n" ++
 180  "\n" ++