Foundation Dimensional Bridge Structural M E Rs Band

The electron mass band

The electron has a measured mass of about 0.511 MeV, a value known to high precision from experiments. In the Recognition Science framework, the electron mass appears in native units as the golden ratio cubed, written φ³. The declaration m_e_RS_band is a machine-checked theorem that proves this native value lies strictly between 4.22 and 4.24. It does not touch the SI measurement; it only fixes a narrow numerical window for the framework's own dimensionless quantity.

The golden ratio φ is roughly 1.618, so φ³ is about 4.236. The theorem's proof uses only the known bounds 1.61 < φ < 1.62 and the defining identity φ² = φ + 1, then applies arithmetic to show the cube falls in the stated interval. The declaration is a structural result: it establishes a fact about the framework's internal scaling ladder, not a prediction about laboratory data.

In Recognition Science, the framework models the electron as sitting on a phi-power ladder of masses. The rung for the electron is φ³ in coherence-mass units. This band is the formal certificate that the rung lands where the ladder says it should. The measured SI value enters only later, through a separate conversion bridge that maps native units to kilograms and electronvolts. That bridge is a calibration, not a derivation: it needs an external anchor to display the native mass in SI units.

The framework's library proves the band and the bridge structure, but it does not prove that the SI electron mass follows from first principles. The conversion factor E_coh = m_e_SI / φ³, about 0.121 MeV, is close to the golden quantum J(φ) ≈ 0.118 MeV, but this proximity is a named residual, an open frontier. The honest statement is that the framework pins its own native mass tightly, while the step from that native mass to the measured 0.511 MeV remains an open problem, not a theorem.

/-- Restatement of the electron rung result. -/
theorem m_e_RS_band : 4.22 < m_e_RS ∧ m_e_RS < 4.24 := by
  unfold m_e_RS
  constructor
  · nlinarith [phi_gt_onePointSixOne, phi_sq_eq, sq phi]
  · nlinarith [phi_lt_onePointSixTwo, phi_sq_eq, sq phi]

/-- Restatement of the electron rung result. -/
theorem m_e_RS_band : 4.22 < m_e_RS ∧ m_e_RS < 4.24 := by
  unfold m_e_RS
  constructor
  · nlinarith [phi_gt_onePointSixOne, phi_sq_eq, sq phi]
  · nlinarith [phi_lt_onePointSixTwo, phi_sq_eq, sq phi]

/-- Proximity to J(φ): |E_coh_MeV - J(φ) · 1 MeV| < 0.013 MeV.

The bound `0.013` is the loose value provable from the `phi ∈ (1.61, 1.62)`
band currently available in `Constants.lean`; the actual numerical proximity
is roughly `0.0026` (computed from `phi ≈ 1.61803`, `m_e_SI/phi^3 ≈ 0.12063`,
`phi - 3/2 ≈ 0.11803`). Tightening this bound requires sharper `phi` bounds. -/
theorem E_coh_near_JPhi :
    |E_coh_MeV - (phi - 3/2)| < 0.013 := by
  unfold E_coh_MeV m_e_SI_MeV m_e_RS
  have ⟨h_lo, h_hi⟩ := E_coh_band
  unfold E_coh_MeV m_e_SI_MeV m_e_RS at h_lo h_hi
  have h_jphi_lo : 0.110 < phi - 3/2 := by linarith [phi_gt_onePointSixOne]
  have h_jphi_hi : phi - 3/2 < 0.120 := by linarith [phi_lt_onePointSixTwo]
  rw [abs_lt]
  constructor <;> linarith

What this page does not claim

The theorem does not derive the SI electron mass of 0.511 MeV from first principles. The proximity to J(φ) is not a derivation of the electron mass; it is a named open residual. The band 4.22 to 4.24 is not a measurement of any physical quantity in SI units.

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/Foundation/DimensionalBridgeStructural.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: