Astrophysics Neutron Star Max Mass Rs

Neutron star mass limits

A neutron star is the collapsed core of a massive star that exploded as a supernova. It packs roughly 1.4 to 2.3 times the Sun's mass into a sphere about 20 kilometers across, making it one of the densest objects in the universe. The maximum mass a neutron star can hold before collapsing into a black hole is a key prediction of nuclear physics and general relativity. The standard theoretical limit comes from the Tolman-Oppenheimer-Volkoff (TOV) equation, which balances gravitational pressure against the pressure from degenerate neutron matter. Observations of the pulsar PSR J0740+6620, published in 2021, measured a mass of about 2.35 solar masses, providing a firm empirical anchor for these limits.

In Recognition Science, the framework models this astrophysical limit using its core cost function, a measure of recognition effort that the framework proves must take a specific mathematical form. The module defines a domain cost as J(m/e), where m is a mass and e is a reference mass, and J(x) = (x + 1/x)/2 - 1. The framework's research note suggests that the maximum neutron star mass might be related to the golden ratio squared, φ² ≈ 2.618, times the solar mass. This gives a predicted limit of about 2.62 solar masses, which sits about 10 percent above the measured 2.35 solar masses for PSR J0740+6620.

The machine-checked library of formal theorems establishes three general facts about this cost function. First, the cost vanishes when the mass equals the reference mass, meaning recognition is free when there is no difference. Second, the cost is always nonnegative for positive masses, meaning recognition always costs something when the masses differ. Third, the quantity φ - 3/2 is positive, a threshold condition that the framework uses to mark a boundary. These three facts are assembled into a certificate structure called NSMaxMassCert, which the library proves is inhabited.

What the module does not do is prove that any specific neutron star mass equals φ² times the solar mass. The definition of domainCost uses the abstract ratio m/e without connecting it to actual neutron star physics. The docstring states this plainly: the paragraph about the 2.62 solar mass limit is a research note recording where the idea was meant to go, not a result. The three theorems hold for any positive real numbers, not for neutron stars specifically. To make this a theorem about neutron stars, one would need a definition of m and e in terms of the star's actual properties, such as its mass and radius.

The framework's contribution here is a candidate scaling relation, not a confirmed prediction. The golden ratio appears throughout the framework's forcing chain, so testing it against neutron star masses is a natural empirical check. The 10 percent gap between φ² and the measured maximum could close with better observations or a more refined model, or it could indicate that the simple scaling does not hold for neutron stars. The module provides the formal scaffolding to test this idea, but the astrophysical verdict remains open.

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]

theorem cert_inhabited : Nonempty NSMaxMassCert := ⟨cert⟩

What this page does not claim

The module does not prove that any specific neutron star mass equals φ² times the solar mass. The 2.62 solar mass limit is not a derived theorem; it is a research note recorded in the docstring. The three formal theorems hold for any positive real numbers, not for neutron stars specifically.

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/Neutron_Star_Max_Mass_RS.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: