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)
132theorem hbar_range : (0.088 : ℝ) < hbar ∧ hbar < (0.093 : ℝ) := hbar_bounds
proof body
Term-mode proof.
133
134/-! ## Mass generation ratios -/
135
136/-- The muon/electron mass ratio involves φ¹¹ ≈ 199.
137 Specifically m_μ/m_e ≈ φ^(r_μ - r_e) = φ^(13-2) = φ¹¹. -/
depends on (7)
Lean names referenced from this declaration's body.
-
hbar
in IndisputableMonolith.Constants
decl_use
-
hbar_bounds
in IndisputableMonolith.Constants
decl_use
-
hbar
in IndisputableMonolith.Constants.Codata
decl_use
-
m_e
in IndisputableMonolith.Constants.ProtonElectronMassRatio
decl_use
-
Mass
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
hbar
in IndisputableMonolith.Information.ComputationLimitsStructure
decl_use
-
hbar
in IndisputableMonolith.Quantum.EntanglementEntropy
decl_use