module module

`IndisputableMonolith.Engineering.EnergyStorageDensityStructure`

show as: view Lean formalization →

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

generate prose now

used by (1)

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

IndisputableMonolith.Engineering.TeslaTurbineStructure module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (25)

def E_coh_storage L55
theorem E_coh_storage_pos L58
def phi_rung_energy L63
theorem phi_rung_energy_pos L66
theorem phi_rung_energy_ratio L71
def chemical_rung L81
def nuclear_rung L84
def E_chemical L87
def E_nuclear L90
theorem nuclear_exceeds_chemical L93
def nuclear_chemical_ratio L100
theorem nuclear_chemical_ratio_gt_one L103
def jcost_energy L110
theorem jcost_energy_nonneg L113
theorem jcost_energy_zero_iff_ground L119
theorem jcost_energy_min_at_ground L139
theorem phi_rung_jcost_energy L147
theorem phi_coherent_minimizes_jcost_per_energy L153
def storage_density_ratio L162
theorem storage_density_ratio_pos L165
theorem higher_rung_denser L170
theorem energy_storage_density_hierarchy L177
theorem phi_ladder_energy_strictly_increasing L191
theorem rs_energy_storage_hierarchy L201
def en004_certificate L210