theorem other other

`gap45_eq`

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

formal statement (Lean)

  34theorem gap45_eq : gap45 = Dspatial^2 * Dconfig := by decide

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.Foundation.RSCoupledAxis decl_use
darkMatterMassCert in IndisputableMonolith.Physics.DarkMatterMassFromGap45 decl_use
gap45_eq in IndisputableMonolith.Physics.DarkMatterMassFromGap45 decl_use

Lean names referenced from this declaration's body.