Physics Muon Mass3 From Phi Ladder

What the module actually proves

The muon is a heavier cousin of the electron, with a measured mass of about 105.66 MeV/c². Physicists have long sought to derive that number from deeper principles. The module named MuonMass3_FromPhiLadder in the Recognition Science library appears, by its title, to attempt such a derivation using a ladder of powers of the golden ratio. The file even contains a research note sketching a hoped-for formula: m_mu = phi^11.5 * E_coh, with E_coh a coherence energy, which would give about 30.6 MeV, far from the measured value. The note itself admits the attempt is "Still off. Structural."

What the module actually proves, in machine-checked form, is much narrower. It defines a cost function Jcost(m/e), which measures the recognition cost of a ratio between two masses. It then proves three general facts about this cost: it equals zero when the two masses are equal, it is never negative for positive masses, and the number phi - 3/2 is positive. These are true for any two positive real numbers, not just for the muon and electron. The file's own docstring states this plainly: the Lean code proves nothing specific to the muon subject, because the cost function is defined without any reference to a particular particle.

In Recognition Science, the cost (a measure of how hard it is to recognize one quantity as another) is central: a proved theorem forces the cost function to have the form J(x) = (x + 1/x)/2 - 1. The module here reuses that general cost, but it does not connect it to any physical mass. A true theorem about the muon would need a definition of m and e in the muon's own terms, such as a formula tying the muon mass to a coherence energy. That definition is absent, so the module remains a template, not a result.

The practical lesson is about provenance. A file name and a research note can suggest a physical derivation, but the machine-checked content is what counts. Here, the content establishes only that the cost function behaves sensibly at equality and positivity. It does not predict the muon mass, does not fit the measured value, and does not advance the phi-ladder program. A reader who wants a muon mass derivation should look for a module that defines the muon mass in physical terms; this one does not.

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

This module does not derive or predict the muon mass. The research note's formula m_mu = phi^11.5 * E_coh is not a proved result. The cost function's general properties do not imply any physical connection to the muon.

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/MuonMass3_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: