lemma
proved
term proof
E_PBM_bounds
No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
105lemma E_PBM_bounds :
106 1.61 * eV_to_J < E_PBM ∧ E_PBM < 1.62 * eV_to_J :=
proof body
Term-mode proof.
107 ⟨mul_lt_mul_of_pos_right phi_gt_onePointSixOne eV_to_J_pos,
108 mul_lt_mul_of_pos_right phi_lt_onePointSixTwo eV_to_J_pos⟩
109
110/-- E_PBM equals rung 6 on the φ-energy ladder:
111 E_base · φ⁶ = φ⁻⁵ eV · φ⁶ = φ eV = E_PBM. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (11)
Lean names referenced from this declaration's body.
-
E_base
in IndisputableMonolith.Applied.PhotobiomodulationDevice
decl_use
-
E_PBM
in IndisputableMonolith.Applied.PhotobiomodulationDevice
decl_use
-
eV_to_J
in IndisputableMonolith.Applied.PhotobiomodulationDevice
decl_use
-
eV_to_J_pos
in IndisputableMonolith.Applied.PhotobiomodulationDevice
decl_use
-
rung
in IndisputableMonolith.Compat.Constants
decl_use
-
phi_gt_onePointSixOne
in IndisputableMonolith.Constants
decl_use
-
phi_lt_onePointSixTwo
in IndisputableMonolith.Constants
decl_use
-
rung
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
rung
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
rung
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
rung
in IndisputableMonolith.RSBridge.Anchor
decl_use