Constants Proton Electron Mass Ratio Proton Electron Ratio Implies Phi Gap

The phi gap

The proton-to-electron mass ratio is one of the plainest numbers in physics: a proton weighs about 1,836.15 times as much as an electron. The ratio has no explanation in the standard model; it is an input, not an output. Recognition Science (RS) takes a different route. It builds particle masses on a ladder of powers of the golden ratio φ, about 1.618, and the declaration proton_electron_ratio_implies_phi_gap is a small but load-bearing step in that program.

In RS, the electron sits on rung 2 of the ladder, so its mass is written as a base unit times φ². The proton sits on some higher rung, call it r_p. The framework's machine-checked library proves a structural theorem: if both masses lie on the ladder, their ratio is exactly φ^(r_p − 2). The declaration in question is a restatement of that result. It takes as a premise that the ratio equals φ^(r_p − 2) and concludes the same equality. Formally, it is a tautology, a one-line proof. Its role is not to prove the ratio; it is to name the condition that the measured ratio must satisfy for the ladder picture to hold.

The measured value 1,836.15 is not itself derived in the library. The framework's own notes mark the full proton derivation as blocked, pending a separate account of quark confinement. What the declaration does establish is the shape of the claim: if the proton and electron both live on the φ-ladder, then the mass gap between them is a whole-number power of φ. That structural form is the testable prediction. It predicts that the ratio, when expressed as φ^k, has an integer exponent k. The measured ratio gives k ≈ 16.02, close to but not exactly an integer, a discrepancy the framework attributes to the unfinished proton derivation.

The declaration does not claim that the ratio is exactly a power of φ, nor that the proton's rung has been identified. It does not claim the measured ratio has been reproduced. It claims only the conditional: ladder membership forces the ratio's form. That conditional is what makes the eventual proton derivation meaningful. If a future derivation fixes r_p, the ratio follows with no free parameters. Until then, the phi gap remains a structural target, not a measured fact.

theorem mass_ratio_structural (r_p : ℤ) (m_p : ℝ)
    (hm_p : m_p = mass_on_rung r_p)
    (_hm_p_pos : 0 < m_p) :
    m_p / m_e = phi ^ (r_p - 2) := by
  rw [hm_p, m_e, mass_on_rung, mass_on_rung]
  field_simp [zpow_ne_zero _ phi_ne_zero]
  exact (zpow_sub₀ phi_ne_zero r_p 2).symm

/-- Proton/electron ladder structure implies the stated ratio formula. -/
theorem proton_electron_ratio_implies_phi_gap (r_p : ℤ) (m_p : ℝ)
    (h : m_p / m_e = phi ^ (r_p - 2)) :
    m_p / m_e = phi ^ (r_p - 2) :=
  h

What this page does not claim

The measured ratio 1836.15 is not derived in the library. The proton's rung r_p is not identified by this declaration. The ratio is not claimed to be exactly a power of φ in the measured world.

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/Constants/ProtonElectronMassRatio.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: