Axion

formal source

 115    - From PQ solution to strong CP
 116    - Misalignment production
 117    - Status: Actively searched -/
 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 -/
 126structure PBH where
 127  mass : ℝ  -- Solar masses
 128  formation_epoch : String
 129
 130/-! ## RS: Ledger Shadows -/
 131
 132/-- In RS, dark matter = "ledger shadows":
 133
 134    The ledger has different "sectors" based on 8-tick phase:
 135    - **Visible sector**: Phases that couple to photons
 136    - **Dark sector**: Phases that don't couple to photons
 137
 138    Both gravitate (J-cost couples universally to geometry).
 139    But only visible sector emits/absorbs light. -/
 140structure LedgerSector where
 141  phase : Fin 8
 142  couples_to_photon : Bool
 143  gravitates : Bool := true  -- All sectors gravitate
 144
 145/-- The visible sector: phases 0, 2, 4, 6 (even phases). -/
 146def visibleSector : List (Fin 8) := [0, 2, 4, 6]
 147
 148/-- The dark sector: phases 1, 3, 5, 7 (odd phases). -/