Astrophysics Neutron Star Mass From Phi Ladder Neutron Star Mass Cert

The certificate's scope

Neutron stars are the crushed cores left behind when massive stars explode. Their masses cluster near 1.4 times the Sun's mass, and the Chandrasekhar limit of about 1.44 solar masses sets the maximum for a white dwarf, the stage before collapse. A research note in the Recognition Science framework proposed that neutron star masses peak at 1.33 solar masses, which is roughly 0.924 times the Chandrasekhar limit, a ratio expressible through the framework's cost function J.

The declaration NeutronStarMassCert (a certificate, a packaged bundle of proved statements) does not establish that specific astrophysical claim. What the machine-checked library of formal theorems proves are three general facts about the cost function when it compares a measured value to an expected one. First, the cost is zero when the measured value equals the expected value. Second, the cost is never negative for positive inputs. Third, the golden ratio minus 1.5 is positive. These three facts are assembled into a certificate structure, and the certificate is shown to exist.

The key limitation is in how the cost function is defined. The framework defines domainCost as J(measured / expected), a ratio of two real numbers, without any reference to neutron stars, Chandrasekhar limits, or solar masses. The certificate proves facts about this abstract ratio, not about the astrophysical quantities. To make the certificate a theorem about neutron stars, one would need to define what "measured" and "expected" mean in the specific context of stellar collapse. That definition is absent.

In Recognition Science, the cost function J(x) = (x + 1/x)/2 - 1 measures the forced cost of recognition, the price reality pays for comparing two quantities. The framework's library proves J vanishes at unity, is nonnegative for positive inputs, and that phi - 3/2 is positive. These are the three facts the certificate packages. The certificate is real, machine-checked, and axiom-clean, but it is a statement about the cost function's general properties, not about the mass distribution of neutron stars.

What a reader can take away: the certificate establishes a small, solid piece of mathematics about cost functions, and it honestly records that the astrophysical application remains a research note, not a result. The gap between the general theorem and the specific claim is explicit in the code, which is precisely what makes the certificate trustworthy. It proves what it proves and no more.

theorem domainCost_at_equilibrium (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 (measured expected : ℝ) : ℝ := Jcost (measured / expected)

What this page does not claim

The certificate does not claim that neutron star masses actually cluster at 1.33 solar masses. The certificate does not claim any specific astrophysical definition of measured or expected mass. The certificate does not derive the Chandrasekhar limit from the framework's axioms.

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