structure definition def or abbrev

`Axion`

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

formal statement (Lean)

 118structure Axion where
 119  mass : ℝ  -- eV
 120  decay_constant : ℝ  -- GeV
 121
 122/-- Primordial black holes: BHs from early universe
 123    - Mass range: 10⁻¹⁸-10⁵ M_sun (windows remain)
 124    - Form from density perturbations
 125    - Status: Some windows still open -/

used by (10)

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

axion_coupling in IndisputableMonolith.Experimental.Xenon1TExcess decl_use
axion_coupling_small in IndisputableMonolith.Experimental.Xenon1TExcess decl_use
tritium_most_likely in IndisputableMonolith.Experimental.Xenon1TExcess decl_use
chiralAnomalyConsequences in IndisputableMonolith.QFT.Anomalies decl_use
comparison in IndisputableMonolith.StandardModel.StrongCP decl_use
experimentalTests in IndisputableMonolith.StandardModel.StrongCP decl_use
rs_axion_compatible in IndisputableMonolith.StandardModel.StrongCP decl_use
strongCPNumericalCert in IndisputableMonolith.StandardModel.StrongCP decl_use
thetaContributions in IndisputableMonolith.StandardModel.StrongCP decl_use
theta_zero_selected in IndisputableMonolith.StandardModel.StrongCP decl_use

depends on (4)

Lean names referenced from this declaration's body.

Mass in IndisputableMonolith.Constants.RSNativeUnits decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
Status in IndisputableMonolith.Measurement.RSNative.Core decl_use
density in IndisputableMonolith.Physics.NeutronStarCrustalRegimesFromRS decl_use