Physics Lepton Generations Defs

Lepton mass ladder

Leptons are the family of elementary particles that do not feel the strong force; the charged ones are the electron, the muon, and the tau. Their masses are strikingly different: the muon is about 207 times heavier than the electron, and the tau is about 17 times heavier than the muon. Standard physics measures these values with great precision but does not explain why they take those particular numbers. The module Defs.lean in the Recognition Science library defines a specific mechanism that aims to do so.

The framework's central idea is that reality keeps a ledger, a discrete record of recognition events, and that the cost of each recognition is fixed by a proved function. From that cost function, the framework derives the golden ratio phi and a set of geometric constants. The lepton module applies those constants to the electron's structural mass, which is already defined elsewhere, and multiplies it by powers of phi to reach the muon and tau. Each step is not a free fit but a combination of named geometric and symmetry terms.

The first step, from electron to muon, uses the number of passive edges (11) and the spherical geometry factor 1/(4π). The definition is: step_e_mu = E_passive + 1/(4π) − α², where α is the fine-structure constant. The second step, from muon to tau, uses the six faces of a cube and the 17 wallpaper symmetry groups: step_mu_tau = 6 − (2·17 + 6)/2 · α. These steps are definitions in the module, not theorems; they encode a chosen model of how the masses progress.

The module also defines predicted residues, which are exponents for phi. The predicted muon residue is (gap 1332 − refined_shift) + step_e_mu, and the predicted tau residue is the muon residue plus step_mu_tau. The predicted masses are then electron_structural_mass times phi raised to those residues. The module stores the measured CODATA 2022 values for the muon (105.6583755 MeV) and tau (1776.86 MeV) as verification targets, so the predictions can be checked against experiment.

In plain language, the module sets up a concrete ladder: start with the electron mass, apply a geometric step to get a muon mass, apply another step to get a tau mass. The steps are built from fixed numbers that appear elsewhere in the framework. Whether those steps reproduce the measured masses is an empirical check that the module enables but does not itself carry out; the definitions are the machinery, not the proof.

/-- Step 1: Electron to Muon.
    Driven by Passive Edges (11) and Spherical Geometry (1/4π). -/
noncomputable def step_e_mu : ℝ :=
  (E_passive : ℝ) + 1 / (4 * Real.pi) - α ^ 2

/-- Step 2: Muon to Tau.
    Driven by Faces (6) and Wallpaper Symmetry (17).
    Coefficient: W + D/2 = (2W + D)/2. -/
noncomputable def step_mu_tau : ℝ :=
  (cube_faces D : ℝ) - (2 * wallpaper_groups + D) / 2 * α

/-- Predicted Muon Mass. -/
noncomputable def predicted_mass_mu : ℝ :=
  electron_structural_mass * phi ^ predicted_residue_mu

What this page does not claim

The module does not prove that the predicted masses equal the measured masses. The fine-structure constant alpha is not derived in this module; it is an input from the constants file. The module does not explain why the electron mass itself takes its measured value.

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/LeptonGenerations/Defs.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: