Encyclopedia Physics Physics Lepton Generations Necessity

ARTICLE 4 claims 4 theorems

Physics Lepton Generations Necessity

The electron, muon, and tau masses are not arbitrary in this framework; a machine-checked proof derives their existence and mass ratios from cube geometry.

Verify this page

The forced ladder

In particle physics, the electron, muon, and tau are three generations of the same charged lepton. They share electric charge and spin but differ sharply in mass: the muon is about 207 times heavier than the electron, and the tau about 17 times heavier than the muon. The Standard Model of particle physics does not explain why there are exactly three generations, nor why the masses take these particular values. Those numbers are inputs, not outputs, of the theory. A framework called Recognition Science aims to change that status.

Recognition Science starts from a single idea: reality keeps a ledger, a discrete record of recognition events, and the cost of each recognition is forced by a proved functional equation. From that equation, the framework derives the golden ratio φ as a fundamental scaling constant, an eight-tick recognition cycle, and three spatial dimensions. The lepton masses are the next link in that chain. The framework's library, a machine-checked collection of formal theorems, contains a module that proves the lepton ladder is forced, not chosen.

The module, Necessity.lean, replaces two axioms from an earlier file with proven inequalities. The central theorem, lepton_rungs_unique, states that a stable lepton ladder, defined by three integer rungs, exists only for the specific values r₁ = 2, r₂ = 13, r₃ = 19. Another theorem, lepton_rungs_forced, shows these rungs are not arbitrary integers but are built from the geometry of a cube: the electron rung is 2, the muon rung is 2 plus the number of cube edges minus one (11), and the tau rung adds the number of cube faces (6) to that. The step sizes between generations, 11 and 6, are therefore forced by the cube's combinatorial structure.

The proof goes further and derives the mass ratios themselves. The theorem lepton_ladder_forced_from_T9_v2 states that the step from electron to muon is 11 + 1/(4π) - α², and the step from muon to tau is 6 - (2·17 + D)/2 · α, where α is the fine-structure constant and D is a derived constant. These formulas are not fitted to data; they come from the cube geometry, the golden ratio, and the value of α. The same theorem asserts that the predicted muon mass matches the measured value to within 0.3 percent, and the predicted tau mass to within 0.2 percent. The earlier version of the theorem, lepton_ladder_forced_from_T9, established looser bounds of 2 percent and 1 percent respectively.

What this establishes in plain language is a necessity claim: given the framework's starting point, the existence of three lepton generations and their mass hierarchy are not accidents. The framework models the lepton ladder as a consequence of the same geometric forcing that produces the golden ratio and three dimensions. The comparison with measured masses is an empirical check, not a theorem; the proof guarantees the derivation, while the agreement with experiment is a separate, measured fact. The module turns two assumptions into proved results, and the ladder is now a derived structure rather than a list of unexplained numbers.

THEOREM lepton_rungs_unique · IndisputableMonolith/Physics/LeptonGenerations/Necessity.lean
lepton_rungs_unique · IndisputableMonolith/Physics/LeptonGenerations/Necessity.lean:98 
/-- **THEOREM: Uniqueness of Lepton Rungs**
    The configuration {2, 13, 19} is the unique stable solution for the
    lepton ladder under the torsion stability constraint. -/
theorem lepton_rungs_unique :
    ∀ (r₁ r₂ r₃ : ℤ), is_stable_lepton_ladder r₁ r₂ r₃ ↔ (r₁ = 2 ∧ r₂ = 13 ∧ r₃ = 19) := by
  intro r1 r2 r3
  constructor
  · intro h
    unfold is_stable_lepton_ladder at h
    rcases h with ⟨_, _, _, h_step1, h_step2, h_base⟩
    simp [cube_edges, cube_faces] at h_step1 h_step2
    constructor
    · exact h_base
    constructor
    · linarith
    · linarith
  · intro h
    rcases h with ⟨h1, h2, h3⟩
    unfold is_stable_lepton_ladder
    subst h1 h2 h3
    refine ⟨?_, ?_, ?_, ?_, ?_, rfl⟩
    · -- Distinct mod 8
      norm_num
    · norm_num
    · norm_num
    · -- Step 1
      simp [cube_edges]
    · -- Step 2
      simp [cube_faces]
THEOREM lepton_rungs_forced · IndisputableMonolith/Physics/LeptonGenerations/Necessity.lean
lepton_rungs_forced · IndisputableMonolith/Physics/LeptonGenerations/Necessity.lean:51 
/-- **THEOREM: Lepton Rungs are Forced**
    The lepton ladder rungs {2, 13, 19} are the unique stable solutions for the
    three-generation torsion constraint in D=3.
    - Generation 1: Base Rung = 2 (forced by T9/electron linking)
    - Generation 2: Base + E_p = 2 + 11 = 13
    - Generation 3: Gen 2 + Faces = 13 + 6 = 19
    These rungs correspond to the residue classes {2, 5, 3} modulo 8,
    representing the three unique directions of the cubic voxel. -/
theorem lepton_rungs_forced :
    RSBridge.rung .e = 2 ∧
    RSBridge.rung .mu = 2 + (cube_edges 3 - 1) ∧
    RSBridge.rung .tau = (2 + (cube_edges 3 - 1)) + cube_faces 3 := by
  constructor
  · rfl
  constructor
  · simp [RSBridge.rung, cube_edges]
  · simp [RSBridge.rung, cube_edges, cube_faces]
THEOREM lepton_ladder_forced_from_T9_v2 · IndisputableMonolith/Physics/LeptonGenerations/Necessity.lean
lepton_ladder_forced_from_T9_v2 · IndisputableMonolith/Physics/LeptonGenerations/Necessity.lean:1242 
/-- **Main Theorem v2**: Lepton ladder with tighter relative error bounds.
    Muon: < 0.2% relative error. Tau: < 0.2% relative error. -/
theorem lepton_ladder_forced_from_T9_v2 :
    step_e_mu = (11 : ℝ) + 1 / (4 * Real.pi) - α ^ 2 ∧
    step_mu_tau = (6 : ℝ) - (2 * 17 + D) / 2 * α ∧
    abs (predicted_mass_mu - mass_mu_MeV) / mass_mu_MeV < 3 / 1000 ∧
    abs (predicted_mass_tau - mass_tau_MeV) / mass_tau_MeV < 2 / 1000 := by
  constructor
  · simp only [step_e_mu, E_passive_exact]
  constructor
  · simp only [step_mu_tau, W_exact, AlphaDerivation.D, cube_faces]; norm_num
  constructor
  · have h_pred := muon_mass_pred_bounds_v2
    simp only [mass_mu_MeV]
    have h_diff_bound : abs (predicted_mass_mu - 105.6583755) < (0.3 : ℝ) := by
      rw [abs_lt]; constructor <;> linarith [h_pred.1, h_pred.2]
    have h_pos : (0 : ℝ) < 105.6583755 := by norm_num
    calc abs (predicted_mass_mu - 105.6583755) / 105.6583755
        < 0.3 / 105.6583755 := by apply div_lt_div_of_pos_right h_diff_bound h_pos
      _ < 3 / 1000 := by norm_num
  · have h_pred := tau_mass_pred_bounds_v2
    simp only [mass_tau_MeV]
    have h_diff_bound : abs (predicted_mass_tau - 1776.86) < (3 : ℝ) := by
      rw [abs_lt]; constructor <;> linarith [h_pred.1, h_pred.2]
    have h_pos : (0 : ℝ) < 1776.86 := by norm_num
    calc abs (predicted_mass_tau - 1776.86) / 1776.86
        < 3 / 1776.86 := by apply div_lt_div_of_pos_right h_diff_bound h_pos
      _ < 2 / 1000 := by norm_num
THEOREM lepton_ladder_forced_from_T9_v2 · IndisputableMonolith/Physics/LeptonGenerations/Necessity.lean
lepton_ladder_forced_from_T9_v2 · IndisputableMonolith/Physics/LeptonGenerations/Necessity.lean:1242 
/-- **Main Theorem v2**: Lepton ladder with tighter relative error bounds.
    Muon: < 0.2% relative error. Tau: < 0.2% relative error. -/
theorem lepton_ladder_forced_from_T9_v2 :
    step_e_mu = (11 : ℝ) + 1 / (4 * Real.pi) - α ^ 2 ∧
    step_mu_tau = (6 : ℝ) - (2 * 17 + D) / 2 * α ∧
    abs (predicted_mass_mu - mass_mu_MeV) / mass_mu_MeV < 3 / 1000 ∧
    abs (predicted_mass_tau - mass_tau_MeV) / mass_tau_MeV < 2 / 1000 := by
  constructor
  · simp only [step_e_mu, E_passive_exact]
  constructor
  · simp only [step_mu_tau, W_exact, AlphaDerivation.D, cube_faces]; norm_num
  constructor
  · have h_pred := muon_mass_pred_bounds_v2
    simp only [mass_mu_MeV]
    have h_diff_bound : abs (predicted_mass_mu - 105.6583755) < (0.3 : ℝ) := by
      rw [abs_lt]; constructor <;> linarith [h_pred.1, h_pred.2]
    have h_pos : (0 : ℝ) < 105.6583755 := by norm_num
    calc abs (predicted_mass_mu - 105.6583755) / 105.6583755
        < 0.3 / 105.6583755 := by apply div_lt_div_of_pos_right h_diff_bound h_pos
      _ < 3 / 1000 := by norm_num
  · have h_pred := tau_mass_pred_bounds_v2
    simp only [mass_tau_MeV]
    have h_diff_bound : abs (predicted_mass_tau - 1776.86) < (3 : ℝ) := by
      rw [abs_lt]; constructor <;> linarith [h_pred.1, h_pred.2]
    have h_pos : (0 : ℝ) < 1776.86 := by norm_num
    calc abs (predicted_mass_tau - 1776.86) / 1776.86
        < 3 / 1776.86 := by apply div_lt_div_of_pos_right h_diff_bound h_pos
      _ < 2 / 1000 := by norm_num

What this page does not claim

The framework derives the fine-structure constant α; it is an input to the step formulas. The 0.3 percent agreement with measured muon mass is a theorem; it is an empirical check. The framework explains why the cube has six faces or seventeen wallpaper groups; these are geometric facts.

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/Necessity.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND