higher_rung_denser

formal source

 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
 193  unfold phi_rung_energy
 194  apply mul_lt_mul_of_pos_left _ E_coh_storage_pos
 195  exact zpow_lt_zpow_right₀ one_lt_phi h
 196
 197/-! ## §VI. Fundamental Bound Summary -/
 198
 199/-- The RS energy storage hierarchy theorem.
 200    Derives three distinct energy scales from the φ-ladder structure. -/