thermal_ratio_pos

formal source

  67  norm_num
  68
  69/-- **THEOREM EN-002.3**: Room temperature thermal ratio is positive. -/
  70theorem thermal_ratio_pos : 0 < thermal_ratio_room_temp := by
  71  unfold thermal_ratio_room_temp
  72  norm_num
  73
  74/-! ## §II. Critical Temperature from φ-Ladder -/
  75
  76/-- Critical temperature for the n-th rung of the φ-ladder.
  77    T_c(n) = E_coh · φ^n / k_B (in suitable units).
  78    The RS prediction: each material sits on a particular rung n. -/
  79def T_c_rung (n : ℤ) : ℝ := phi ^ n
  80
  81/-- **THEOREM EN-002.4**: Critical temperature is positive for all rungs. -/
  82theorem tc_rung_pos (n : ℤ) : 0 < T_c_rung n := by
  83  unfold T_c_rung
  84  apply zpow_pos phi_pos
  85
  86/-- **THEOREM EN-002.5**: Higher rungs give higher critical temperatures.
  87    T_c(n+1) = φ · T_c(n) > T_c(n) since φ > 1. -/
  88theorem phi_ladder_tc_monotone (n : ℤ) : T_c_rung n < T_c_rung (n + 1) := by
  89  unfold T_c_rung
  90  rw [zpow_add_one₀ phi_ne_zero]
  91  have hphi_gt1 : 1 < phi := one_lt_phi
  92  have hpos : 0 < phi ^ n := zpow_pos phi_pos n
  93  exact lt_mul_of_one_lt_right hpos hphi_gt1
  94
  95/-- **THEOREM EN-002.6**: The φ-ladder spans all temperature scales.
  96    For any temperature T > 0, there exists a rung n such that T_c(n) > T. -/
  97theorem phi_ladder_unbounded (T : ℝ) (hT : 0 < T) :
  98    ∃ n : ℤ, T < T_c_rung n := by
  99  unfold T_c_rung
 100  -- phi⁻¹ < 1 since phi > 1, so phi⁻¹^k → 0 as k → ∞