theorem proved term proof

`rs_energy_storage_hierarchy`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 201theorem rs_energy_storage_hierarchy :
 202    (∀ n : ℤ, 0 < phi_rung_energy n) ∧
 203    (∀ n m : ℤ, m < n → phi_rung_energy m < phi_rung_energy n) ∧
 204    E_chemical < E_nuclear := by

proof body

Term-mode proof.

 205  refine ⟨phi_rung_energy_pos, ?_, nuclear_exceeds_chemical⟩
 206  intros n m h
 207  exact phi_ladder_energy_strictly_increasing m n h
 208
 209/-- Certificate: EN-004 Energy Storage Density — DERIVED -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

en004_certificate in IndisputableMonolith.Engineering.EnergyStorageDensityStructure decl_use

depends on (7)

Lean names referenced from this declaration's body.

Energy in IndisputableMonolith.Constants.RSNativeUnits decl_use
E_chemical in IndisputableMonolith.Engineering.EnergyStorageDensityStructure decl_use
E_nuclear in IndisputableMonolith.Engineering.EnergyStorageDensityStructure decl_use
nuclear_exceeds_chemical in IndisputableMonolith.Engineering.EnergyStorageDensityStructure decl_use
phi_ladder_energy_strictly_increasing in IndisputableMonolith.Engineering.EnergyStorageDensityStructure decl_use
phi_rung_energy in IndisputableMonolith.Engineering.EnergyStorageDensityStructure decl_use
phi_rung_energy_pos in IndisputableMonolith.Engineering.EnergyStorageDensityStructure decl_use