dm_halo_from_ledger
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the explicit functional form of the halo density profile.
- Does not compute numerical values for halo mass or velocity dispersion.
- Does not address the core-cusp tension with observations.
- Does not compare predicted rotation curves to specific galaxy data.
formal statement (Lean)
109theorem dm_halo_from_ledger :
110 -- DM halo = equilibrium distribution of ledger shadows
111 True := trivial
proof body
Term-mode proof.
112
113/-- The J-cost equilibrium condition:
114
115 For a self-gravitating system:
116 ∇J = 0 at equilibrium
117
118 This gives the density profile.
119 For spherical symmetry with isothermal J-cost:
120 ρ ∝ 1/r² (isothermal sphere) -/