theorem proved term proof

`gap45_eq`

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

formal statement (Lean)

  23theorem gap45_eq : gap45 = 45 := rfl

Term-mode proof.

  24
  25/-- Dark matter mass ratio: m_DM/m_W = 1/gap45. -/

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

styleSuccessionCert in IndisputableMonolith.ArtHistory.StyleSuccessionFromJCost decl_use
StyleSuccessionCert in IndisputableMonolith.ArtHistory.StyleSuccessionFromJCost decl_use
cardinalitySpectrumCert in IndisputableMonolith.CrossDomain.CardinalitySpectrum decl_use
gap45_eq in IndisputableMonolith.CrossDomain.CardinalitySpectrum decl_use
gap45_eq in IndisputableMonolith.Foundation.RSCoupledAxis decl_use
darkMatterMassCert in IndisputableMonolith.Physics.DarkMatterMassFromGap45 decl_use

Lean names referenced from this declaration's body.