Physics Tau Neutrino Mass From Phi Ladder

The tau neutrino mass estimate

The tau neutrino is the heaviest of the three neutrino types, the nearly massless particles that carry energy away from nuclear reactions. Experiments have never weighed it directly; they only set an upper limit. The Particle Data Group's 2024 review places that limit at 18.2 MeV, about 36 times the electron's mass. Within Recognition Science, a proposed phi-ladder formula gives a specific number: 0.014 MeV, roughly 1,300 times smaller than the bound.

The estimate multiplies the electron mass by two factors drawn from the golden ratio phi, the number 1.618... that solves r² = r + 1. The formula reads m_nu_tau = J(phi) * m_electron * phi^(-D), where J(phi) equals 0.118, the electron mass is 0.511 MeV, and phi^(-D) with D = 3 gives 0.236. Multiplying those three numbers yields 0.014 MeV. The exponent D matches the framework's three spatial dimensions, and the whole expression is a structural guess: it has no free parameters fitted to neutrino data.

The machine-checked library of formal theorems proves three general facts about the cost function J, but none of them touch the tau neutrino specifically. The proofs show that J(m/e) vanishes when m equals e, that it stays nonnegative for positive inputs, and that phi minus 1.5 is positive. These are properties of the cost function itself, stated once and universally in a shared template module. The module reuses that template with m and e as abstract real numbers; it never defines what m or e mean for a neutrino.

In plain language, the module certifies arithmetic about a cost function, not physics about neutrinos. The 0.014 MeV figure lives in a research note attached to the file, not in any theorem. What would turn this into a real result is a definition of m and e in the neutrino's own terms, connecting the abstract cost to an actual mass. Until that definition exists, the estimate remains a hypothesis with a named falsifier: a future measurement above 0.014 MeV would rule it out, though the current experimental bound is far too loose to test it.

structure TauNuMassCert where
  cost_at_eq : ∀ r : ℝ, r ≠ 0 → domainCost r r = 0
  cost_nonneg : ∀ m e : ℝ, 0 < m → 0 < e → 0 ≤ domainCost m e
  threshold_pos : 0 < canonicalThreshold

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 0.014 MeV value is not a proved theorem; it is a structural estimate recorded in a research note. The formal proofs apply to any positive real numbers, not to neutrinos specifically. The experimental bound of 18.2 MeV does not test the estimate, being over a thousand times larger.

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/Physics/TauNeutrino_MassFromPhiLadder.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: