PBH
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.