theorem proved term proof

`phi_rung_energy_pos`

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

formal statement (Lean)

  66theorem phi_rung_energy_pos (n : ℤ) : 0 < phi_rung_energy n := by

proof body

Term-mode proof.

  67  unfold phi_rung_energy
  68  exact mul_pos E_coh_storage_pos (zpow_pos phi_pos _)
  69
  70/-- **THEOREM EN-004.3**: Consecutive φ-rung energies differ by exactly φ. -/

used by (1)

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

rs_energy_storage_hierarchy in IndisputableMonolith.Engineering.EnergyStorageDensityStructure decl_use

depends on (7)

Lean names referenced from this declaration's body.

rung in IndisputableMonolith.Compat.Constants decl_use
rung in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
E_coh_storage_pos in IndisputableMonolith.Engineering.EnergyStorageDensityStructure decl_use
phi_rung_energy in IndisputableMonolith.Engineering.EnergyStorageDensityStructure decl_use
rung in IndisputableMonolith.Masses.AnchorPolicy decl_use
rung in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
rung in IndisputableMonolith.RSBridge.Anchor decl_use