theorem
proved
tactic proof
minimal_area_eigenvalue
show as:
view Lean formalization →
formal statement (Lean)
80theorem minimal_area_eigenvalue (h : H_AreaQuantization H A ψ) (H : Type*) [RSHilbertSpace H] (A : AreaOperator H) :
81 ∃ (a_min : ℝ), a_min = ell0^2 ∧
82 (∀ ψ : H, is_ledger_eigenstate H ψ →
83 let eigenvalue := (⟪ψ, A.op ψ⟫_ℂ).re;
proof body
Tactic-mode proof.
84 eigenvalue ≠ 0 → eigenvalue ≥ a_min) := by
85 use ell0^2
86 constructor
87 · rfl
88 · intro ψ h_eigen eigenvalue h_nz
89 -- Use the quantization theorem to show ⟨ψ, Aψ⟩ = n * ell0^2
90 obtain ⟨n, h_quant⟩ := area_quantization h H A ψ h_eigen
91 have h_val : eigenvalue = n * ell0^2 := by
92 unfold eigenvalue
93 rw [h_quant]
94 simp only [Complex.mul_re, Complex.natCast_re, Complex.natCast_im,
95 zero_mul, sub_zero, Complex.ofReal_re]
96 -- Since eigenvalue ≠ 0 and n is Nat, n must be ≥ 1
97 have h_n_nz : n ≠ 0 := by
98 intro h_zero
99 subst h_zero
100 simp [h_val] at h_nz
101 have h_n_pos : 1 ≤ n := Nat.pos_of_ne_zero h_n_nz
102 -- n * ell0^2 ≥ 1 * ell0^2
103 have h_ell0_sq_pos : 0 < ell0^2 := pow_pos lambda_rec_pos 2
104 have h_cast : (1 : ℝ) ≤ (n : ℝ) := by norm_cast
105 have h_le := mul_le_mul_of_nonneg_right h_cast (le_of_lt h_ell0_sq_pos)
106 rw [one_mul] at h_le
107 rw [h_val]
108 exact h_le
109
110end AreaQuantization
111end Quantum
112end IndisputableMonolith