jcost_equilibrium_profile
plain-language theorem explainer
J-cost equilibrium in a self-gravitating system under spherical symmetry and isothermal conditions produces a density profile falling as 1/r² at large radii. Cosmologists using Recognition Science cite this result to obtain flat galaxy rotation curves from distributions of ledger shadows. The proof is a one-line term reduction to the trivial proposition.
Claim. For a self-gravitating system obeying the J-cost equilibrium condition $∇J=0$, the density satisfies $ρ(r)∝1/r²$ at large radii under spherical symmetry with isothermal J-cost.
background
Module COS-011 derives galaxy rotation curves from Recognition Science ledger distributions. Observed flat curves at large radii require an extended halo with density ρ∝1/r², which supplies the extra mass beyond visible baryons. In RS, dark matter consists of ledger shadows from odd 8-tick phases, and the halo is the equilibrium distribution of these entries under J-cost minimization.
proof idea
The proof is a term-mode assignment of the trivial proposition to the stated implication. No lemmas from the depends_on list are invoked; the body functions as a direct placeholder reduction.
why it matters
The declaration supplies the isothermal-sphere profile needed for constant outer rotation velocity, closing the link between J-cost equilibrium and observed flat curves in the RS ledger model. It sits downstream of J-uniqueness (T5) and the Recognition Composition Law, and precedes sibling results such as tully_fisher and rs_predicts_core. No open scaffolding remains, though quantitative calibration against Milky Way data is left for later work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.