PBH

formal source

 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). -/
 149def darkSector : List (Fin 8) := [1, 3, 5, 7]
 150
 151/-- Why do odd phases not couple to photons?
 152
 153    Photons are phase-0 excitations.
 154    Only even-phase matter can exchange phase-0 quanta.
 155    Odd-phase matter is "invisible" to photons. -/
 156theorem odd_phases_dark :