theorem
proved
tactic proof
nonzero_below_curie
show as:
view Lean formalization →
formal statement (Lean)
185theorem nonzero_below_curie (T T_C : ℝ) (hT_nonneg : T ≥ 0) (hT : T < T_C) (hT_C : T_C > 0) :
186 magnetizationRatio T T_C > 0 := by
proof body
Tactic-mode proof.
187 simp only [magnetizationRatio]
188 have h1 : ¬(T ≥ T_C) := by linarith
189 have h2 : T_C ≠ 0 := by linarith
190 simp only [h1, h2, or_self, ite_false]
191 -- √(1 - (T/T_C)²) > 0 when 0 ≤ T < T_C
192 apply Real.sqrt_pos_of_pos
193 -- Need: 1 - (T/T_C)² > 0, i.e., (T/T_C)² < 1
194 have h_ratio_nonneg : T / T_C ≥ 0 := div_nonneg hT_nonneg (le_of_lt hT_C)
195 have h_ratio_lt_one : T / T_C < 1 := by rw [div_lt_one hT_C]; exact hT
196 have h_abs_lt : |T / T_C| < 1 := by rw [abs_of_nonneg h_ratio_nonneg]; exact h_ratio_lt_one
197 have h_sq_lt_one : (T / T_C) ^ 2 < 1 := (sq_lt_one_iff_abs_lt_one _).mpr h_abs_lt
198 linarith
199
200/-! ## 8-Tick and φ Connection -/
201
202/-- Fe, Co, Ni are all 3d transition metals with Z = 26, 27, 28.
203 The 8-tick manifests in their electron configuration: [Ar] 3d^n 4s^2. -/