theorem other other

`mass_pos`

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

formal statement (Lean)

  37theorem mass_pos (k : ℕ) : 0 < mesonMass k := pow_pos phi_pos k

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

OptimalConfig in IndisputableMonolith.Astrophysics.ObservabilityLimits decl_use
fermionKineticCert in IndisputableMonolith.Foundation.QRFT.FermionKineticCert decl_use
FermionKineticCert in IndisputableMonolith.Foundation.QRFT.FermionKineticCert decl_use
RSBH in IndisputableMonolith.Gravity.UltramassiveBH decl_use
rs_entropy_pos in IndisputableMonolith.Gravity.UltramassiveBH decl_use
rs_hawkingTemp_pos in IndisputableMonolith.Gravity.UltramassiveBH decl_use
temp_decreases_with_mass in IndisputableMonolith.Gravity.UltramassiveBH decl_use
temp_halves_on_double in IndisputableMonolith.Gravity.UltramassiveBH decl_use
mesonSpectrumCert in IndisputableMonolith.Physics.MesonSpectrumFromPhiLadder decl_use
HiggsBoson in IndisputableMonolith.QFT.HiggsMechanism decl_use
BlackHole in IndisputableMonolith.Quantum.BekensteinHawking decl_use
temperature_from_surface_gravity in IndisputableMonolith.Quantum.BekensteinHawking decl_use
BlackHole in IndisputableMonolith.Quantum.BlackHoleInformation decl_use
hawking_temperature_pos in IndisputableMonolith.Quantum.BlackHoleInformation decl_use

Lean names referenced from this declaration's body.

mesonMass in IndisputableMonolith.Physics.MesonSpectrumFromPhiLadder decl_use