PBH
Primordial black holes appear as a structure carrying a real-valued mass in solar units together with a formation-epoch string. Early-universe cosmologists enumerating dark-matter candidates inside the Recognition Science ledger-shadow picture would cite the definition when listing phase-mismatched objects that still gravitate. The declaration is a bare structure introduction that adds no computation or lemmas.
claimA primordial black hole is a structure whose data consist of a mass $m$ (in solar masses) and a formation epoch recorded as a string.
background
The module presents dark matter as ledger shadows arising from the 8-tick phase cycle: visible-sector phases couple to photons while dark-sector phases do not, yet both contribute J-cost to geometry. Upstream, tick supplies the fundamental RS time quantum (one tick equals the unit interval), phase(k) returns $kπ/4$ for $k$ in Fin 8, and the cost functions from MultiplicativeRecognizerL4 and ObserverForcing supply the non-negative recognition cost that remains universal across sectors. The local setting is the temporal projection of the σ=0, Z≠0 phantom sector at the scale of odd-phase orbits.
proof idea
The declaration is a bare structure definition that introduces the PBH type with its two fields; no lemmas or tactics are applied.
why it matters in Recognition Science
The structure supplies one concrete dark-sector candidate inside the COS-010 ledger-shadow account and sits beside the sibling WIMP and Axion declarations. It fills the paper proposition that dark matter consists of non-luminous ledger configurations whose gravitational activity follows from universal J-cost while electromagnetic coupling is suppressed by 8-tick phase mismatch. The entry therefore anchors the T7 eight-tick octave landmark to a concrete cosmological object.
scope and limits
- Does not compute a mass spectrum or abundance from the phi-ladder.
- Does not assert that PBHs saturate the observed Ω_dm.
- Does not embed the formation epoch inside the tick or phase algebra.
- Does not incorporate J-cost or recognition cost into the structure fields.
formal statement (Lean)
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. -/