theorem proved decidable or rfl

`phi_rung_jcost_energy`

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

formal statement (Lean)

 147theorem phi_rung_jcost_energy (n : ℤ) :
 148    jcost_energy (phi ^ n) (zpow_pos phi_pos n) =
 149    E_coh_storage * Jcost (phi ^ n) := by

Decided by rfl or decide.

 150  rfl
 151
 152/-- **THEOREM EN-004.11**: Ground state minimizes energy for any positive x. -/

Lean names referenced from this declaration's body.

E_coh_storage in IndisputableMonolith.Engineering.EnergyStorageDensityStructure decl_use
jcost_energy in IndisputableMonolith.Engineering.EnergyStorageDensityStructure decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use