Cosmology Neutrino Mass3 From Phi Ladder

Neutrino mass from the phi ladder

Neutrinos are the lightest known massive particles, and their absolute masses remain a puzzle. Cosmology sets an upper bound on the sum of the three neutrino masses: the Planck satellite data give sum m_nu < 0.12 eV. In Recognition Science, the proposed neutrino mass3 from the phi ladder is an attempt to derive a specific neutrino mass from the golden ratio phi, the number (1 + sqrt(5))/2 ≈ 1.618. The idea is that particle masses sit on a ladder of powers of phi, and the lightest neutrino mass would be roughly phi^(-rung) eV, with a specific value around 1340 eV divided by phi^rung. This is a hypothesis, not a result: the module itself does not establish any physical mass.

What the module does establish, in a machine-checked library of formal theorems, is a small set of general facts about the cost function J(x) = (x + 1/x)/2 - 1. The module defines a domain cost as J(m/e), the cost of recognizing a mass m relative to a reference mass e. It proves three things: the cost is zero when m equals e, the cost is nonnegative for positive masses, and the constant phi - 3/2 is positive. These are true for any positive masses, because the cost function has those properties universally. The module also packages these facts into a certificate structure, showing the certificate is inhabited. All of this is correct but says nothing specific to neutrinos.

The gap is that the module defines domainCost as J(m/e) without ever defining what m and e are for a neutrino. The docstring itself admits this: the paragraph about neutrino masses is a research note recording where the idea was meant to go, not a result. To turn the module into a theorem about neutrinos, one would need a definition of m and e in terms of neutrino physics, for example tying the ladder to the electron mass or to the Planck bound. Without such a definition, the module proves only the scaffolding: the cost function behaves as expected, and the golden ratio threshold is positive. The physical prediction remains a hypothesis with a named falsifier: a measured neutrino mass sum that does not sit on the phi ladder would falsify it.

In plain language: the module is a clean but empty shell. It proves that a certain cost function has sensible properties, and that phi is bigger than 1.5. It does not prove that neutrinos have any particular mass. The interesting physics, the phi ladder itself, is a research note, not a theorem. A reader should treat the module as a foundation stone, not as a completed building. The next step would be to supply the missing physical definitions and then check whether the predicted masses survive comparison with experiment.

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)

theorem cert_inhabited : Nonempty NuMass3Cert := ⟨cert⟩

What this page does not claim

The module does not prove any neutrino mass value. The module does not establish the phi ladder as a physical law. The Planck bound 0.12 eV is an external measurement, not a framework theorem.

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/Cosmology/NeutrinoMass3_FromPhiLadder.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: