lemma proved term proof

`E_base_pos`

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

formal statement (Lean)

  70lemma E_base_pos : 0 < E_base :=

proof body

Term-mode proof.

  71  mul_pos (Real.rpow_pos_of_pos phi_pos _) eV_to_J_pos
  72
  73/-- The φ-energy ladder: E(n) = E_base · φⁿ.
  74    Maps real-valued rung n to photon energy in joules. -/

used by (1)

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

phi_energy_rung_pos in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use

depends on (8)

Lean names referenced from this declaration's body.

E_base in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
eV_to_J_pos in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
rung in IndisputableMonolith.Compat.Constants decl_use
rung in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
E in IndisputableMonolith.Foundation.SpectralEmergence decl_use
rung in IndisputableMonolith.Masses.AnchorPolicy decl_use
rung in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
rung in IndisputableMonolith.RSBridge.Anchor decl_use