theorem
proved
tactic proof
substrate_ok
show as:
view Lean formalization →
formal statement (Lean)
29theorem substrate_ok (H : Type*) [RSHilbertSpace H] : substrate_healthy H := by
proof body
Tactic-mode proof.
30 -- Use the existence theorem for normalized states
31 have ⟨ψ, _⟩ := exists_normalized_state HS
32 -- Construction of a default Hamiltonian (using identity as a bounded operator)
33 let H_op : Hamiltonian HS := {
34 toLinearOp := (identityObs HS).toLinearOp
35 self_adjoint := (identityObs HS).self_adjoint
36 bounded_below := ⟨1, fun ψ_norm => by
37 -- ⟪I ψ, ψ⟫ = ‖ψ‖² = 1
38 have h : (⟪(identityObs HS).op ψ_norm.vec, ψ_norm.vec⟫_ℂ) = (1 : ℂ) := by
39 simp only [identityObs, ContinuousLinearMap.id_apply, inner_self]
40 have h_norm := ψ_norm.norm_one
41 -- ‖v‖ = 1 → ‖v‖² = 1
42 have : (‖ψ_norm.vec‖ : ℂ) ^ 2 = (1 : ℂ) := by
43 rw [h_norm]
44 simp
45 -- In inner product space, ⟪v, v⟫ = ‖v‖²
46 rw [← @inner_self_eq_norm_sq ℂ]
47 exact this
48 rw [h]
49 simp⟩
50 }
51 use ⟨ψ, H_op⟩
52 exact (identityObs HS).self_adjoint
53
54end ILG
55end Relativity
56end IndisputableMonolith