pith. machine review for the scientific record. sign in
theorem proved term proof

composition_refines

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.