Astrophysics White Dwarf Mass From Phi Ladder

The white dwarf mass claim

A white dwarf is the compressed core left after a star like the Sun exhausts its fuel. Observed white dwarfs are not spread evenly in mass; they cluster around 0.6 times the Sun's mass, with the most common values falling between 0.59 and 0.62 solar masses. Astronomers have measured this peak for decades, and it reflects the physics of electron degeneracy pressure balancing gravity in the star's interior.

Recognition Science (RS) offers a different route to that number. The framework's core result forces a specific cost function, and from it a ladder of preferred scales emerges. The golden ratio phi, about 1.618, sits at the base of that ladder. The framework's claim is that the white dwarf mass peak sits at rung phi^(-1) of its stellar mass ladder, which evaluates to phi^(-1) solar masses, approximately 0.618 solar masses. That lands inside the observed 0.59 to 0.62 window.

The formal module behind this claim proves something narrower. Its definitions set domainCost, a cost measuring the gap between a candidate mass m and a reference mass e, as Jcost(m/e). The machine-checked library of formal theorems proves three general facts about this cost: it is zero when m equals e, it is never negative for positive inputs, and the quantity phi minus 3/2 is positive. Those are properties of the cost function itself, not of white dwarfs.

What the module does not do is connect that cost to any astrophysical definition of m or e. The docstring states this plainly: the file proves nothing specific to white dwarfs because domainCost is defined without reference to one. The white dwarf mass value is a research note, a statement of where the idea was meant to go, not a theorem about stars. To make it a theorem, the module would need a definition of m and e in terms of stellar physics, such as the Chandrasekhar limit or electron degeneracy pressure.

In plain language: the framework has a proved cost function and a phi-power ladder, and it has a hypothesis that white dwarfs sit on that ladder at a specific rung. The formal proof establishes the ladder's properties, not the astrophysical placement. The agreement with the measured mass window is a numerical coincidence or a promising lead, depending on one's view, but it is not a derived result.

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

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

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 white dwarf mass value is a proved theorem. The framework derives the white dwarf mass from stellar physics. The 0.618 solar mass value is a prediction with a named falsifier.

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