Astrophysics Dark Matter Halo From Jcost

Halo concentration and the cost function

Dark matter halos are the vast, roughly spherical clouds of unseen matter that surround galaxies. A useful way to describe them is the NFW profile, a standard formula for how density falls off with distance from the center. Its key parameter is the concentration parameter, usually written as c. For galaxy clusters, c typically falls in a range from about 5 to 25, meaning the central density is that many times higher than the outer density.

In Recognition Science, the framework's central object is a cost function, a measure of how much it costs to recognize one thing as another. The framework's library of machine-checked theorems proves this cost function is forced to take one specific form. In the module for dark matter halos, the framework defines a cost for a halo by taking the ratio of two masses, m and e, and plugging that ratio into the cost function. The research note attached to the module suggests that the concentration parameter c might be related to powers of the golden ratio, roughly 6.85 or 11.09, which would cover the lower part of the observed cluster range.

The formal theorems in the module do not prove that connection. What the machine-checked proofs establish is three general facts about the cost function on a ratio: it is zero when the two masses are equal, it is never negative for positive masses, and a particular constant built from the golden ratio is positive. These facts hold for any ratio of positive numbers, not specifically for dark matter halos. The module defines a certificate structure that bundles these three properties together and proves that such a certificate exists.

The gap between the research note and the formal proof is deliberate. The cost function is defined as Jcost (m / e) without any reference to what m and e mean in astrophysics. To turn this into a theorem about halos, the module would need a definition of m and e in terms of halo properties, such as a virial mass and a scale radius. That definition is not present. The result is a template: a proof that certain formal properties hold, waiting for a physical identification that would make it a statement about dark matter.

What the module does establish, in plain language, is that the framework's cost function behaves sensibly when applied to a ratio of positive masses. It does not establish that the concentration parameter follows a golden ratio ladder, nor that the framework explains halo shapes. The empirical range of c from 5 to 25 remains a measurement, not a derived consequence.

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

The module does not prove that halo concentration follows a golden ratio ladder. The module does not establish any empirical match with measured concentration parameters. The module does not provide a physical definition of the masses m and e in terms of halo properties.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Astrophysics/DarkMatterHaloFromJCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: