dm_halo_from_ledger
plain-language theorem explainer
The declaration states that dark matter halos correspond to the J-cost equilibrium distribution of odd 8-tick ledger shadows. Galaxy modelers working inside the Recognition Science program cite it when deriving flat rotation curves from ledger entries alone. The proof reduces to a single application of the trivial tactic.
Claim. The dark matter halo density profile equals the equilibrium distribution of odd eight-tick phase ledger entries that minimizes the J-cost.
background
The module sets out to explain flat galaxy rotation curves by treating dark matter as a distribution of ledger shadows. In Recognition Science, dark matter consists of odd 8-tick phase ledger entries whose spatial arrangement follows J-cost equilibrium. The J-cost is the cost of a recognition event, defined as the derived cost of the comparator in a multiplicative recognizer. Upstream results supply the necessary structures: LedgerFactorization.of calibrates J on positive ratios, ObserverForcing.cost identifies the cost of any recognition event with Jcost, and PhiForcingDerived.of encodes the underlying J-cost structure.
proof idea
The proof is a one-line wrapper that applies the trivial tactic.
why it matters
This declaration fills the COS-011 target by connecting the eight-tick octave to cosmological halo structure. It supplies the ledger-shadow mechanism that produces the isothermal density falloff required for constant rotation velocity at large radii. No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.