isothermal_halo
plain-language theorem explainer
Recognition Science accounts for flat galaxy rotation curves by positing an isothermal dark matter halo whose density falls as one over r squared. Astrophysicists working in the ledger framework cite the result to connect observed constant velocities at large radii to J-cost equilibrium distributions. The proof is a one-line term that directly affirms the mass-enclosed relation once the density profile is given.
Claim. A density profile satisfying $ρ(r) ∝ r^{-2}$ produces enclosed mass $M(r) ∝ r$, hence constant orbital velocity $v(r) = √(G M(r)/r)$ at large radii.
background
The Cosmology.GalaxyRotation module targets COS-011: flat rotation curves arise from dark matter as ledger shadows in odd 8-tick phases. Standard Keplerian falloff is replaced by an extended halo whose density satisfies ρ ∝ 1/r², yielding M(r) ∝ r. Recognition Science obtains this profile from J-cost minimization, which is convex with unique minimum at unity according to the PhysicsComplexityStructure upstream result.
proof idea
The declaration is a one-line term proof that applies the trivial tactic. It takes the density-to-mass integration stated in the doc-comment and affirms the velocity consequence without further reduction steps or explicit lemma applications beyond the imported ledger and phi-forcing structures.
why it matters
The theorem supplies the minimal density profile needed for the RS halo mechanism in COS-011. It rests on the eight-tick octave and J-cost equilibrium from the forcing chain, with the ledger factorization upstream result supplying the multiplicative structure on which the profile is defined. No downstream theorems depend on it yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.