storage_density_ratio

formal source

 159/-! ## §IV. Storage Density Hierarchy -/
 160
 161/-- Energy density ratio between two rungs: φ^(n - m). -/
 162def storage_density_ratio (n m : ℤ) : ℝ := phi ^ (n - m)
 163
 164/-- **THEOREM EN-004.12**: Storage density ratios are positive. -/
 165theorem storage_density_ratio_pos (n m : ℤ) : 0 < storage_density_ratio n m := by
 166  unfold storage_density_ratio
 167  exact zpow_pos phi_pos _
 168
 169/-- **THEOREM EN-004.13**: Higher rung → higher storage density. -/
 170theorem higher_rung_denser (n m : ℤ) (h : m < n) :
 171    1 < storage_density_ratio n m := by
 172  unfold storage_density_ratio
 173  exact one_lt_zpow₀ one_lt_phi (by omega)
 174
 175/-- **THEOREM EN-004.14**: The three-level energy hierarchy.
 176    Mechanical < Chemical < Nuclear (in RS rungs). -/
 177theorem energy_storage_density_hierarchy :
 178    phi_rung_energy (-10) < phi_rung_energy 0 ∧
 179    phi_rung_energy 0 < phi_rung_energy 45 := by
 180  constructor
 181  · unfold phi_rung_energy
 182    apply mul_lt_mul_of_pos_left _ E_coh_storage_pos
 183    exact zpow_lt_zpow_right₀ one_lt_phi (by norm_num)
 184  · unfold phi_rung_energy
 185    apply mul_lt_mul_of_pos_left _ E_coh_storage_pos
 186    exact zpow_lt_zpow_right₀ one_lt_phi (by norm_num)
 187
 188/-! ## §V. Maximum Theoretical Density -/
 189
 190/-- The φ-ladder energy is strictly increasing: higher rungs always give more energy. -/
 191theorem phi_ladder_energy_strictly_increasing (n m : ℤ) (h : n < m) :
 192    phi_rung_energy n < phi_rung_energy m := by