Encyclopedia Masses Masses Mass Genesis Physical Stability Image

ARTICLE 4 claims 4 theorems

Masses Mass Genesis Physical Stability Image

A machine-checked proof shows that a simple set of structural rules for stable charged patterns yields exactly the nine known particle types, with no extras.

Verify this page

The stability image

In particle physics, the standard model lists nine charged fermions: the electron, muon, and tau leptons, and the up, charm, top, down, strange, and bottom quarks. A central question is whether this list is arbitrary or forced by deeper structure. The Recognition Science framework, which studies how reality keeps a discrete record of recognition events, addresses this by asking whether a purely structural definition of physical stability picks out exactly these nine particles and nothing else.

The module MassGenesis defines a predicate PhysicallyStableCharged on a pattern topology, which is a combinatorial description of a charged particle's internal structure. The predicate encodes nine plain conditions: exactly one active edge per tick, a fixed passive-edge count, a sector pinned by the topology, fixed charge skew, spin class, and loop rank within that sector, generation torsion lying on a forced three-rung ladder, and internal consistency of labels and rungs. The predicate never mentions the realized particle list; it is a purely structural definition.

The main theorem, physicalStability_exact_image, proves that this predicate cuts out exactly the nine realized charged topologies and nothing else. The proof runs in two directions: every realized topology satisfies the stability predicate, and every topology satisfying the predicate is realized. The library also proves concrete exclusions, such as no stable up quark at rung 15 and no stable lepton at rung 3 or 12, which demonstrate the absence of extra particles at specific locations. The entire development is machine-checked with zero axioms beyond the standard three.

The result is a genuine no-extra-particles statement: the nine charged fermions are not an arbitrary list but the unique solution to a structural stability condition. This does not derive particle masses, which remain an empirical check against measured values. It establishes that the existence and count of the charged fermions is forced by the framework's structural constraints, a step toward understanding why the standard model contains the particles it does.

THEOREM physicalStability_exact_image · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean
physicalStability_exact_image · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean:352 
/-- **No extra particles.** The structural physical-stability predicate coincides
pointwise with the realized charged image. This discharges the
`ExactImageFromPhysicalStability` obligation for a concrete, non-circular stability
criterion. -/
theorem physicalStability_exact_image :
    ExactImageFromPhysicalStability PhysicallyStableCharged := by
  intro T
  exact ⟨realized_of_physicallyStable, physicallyStable_of_realized⟩
THEOREM physicallyStable_of_realized · realized_of_physicallyStable · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean
physicallyStable_of_realized · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean:261 
theorem physicallyStable_of_realized {T : PatternTopology}
    (h : IsRealizedChargedTopology T) : PhysicallyStableCharged T := by
  obtain ⟨row, _, rfl⟩ := h
  cases row
  · exact stable_electron
  · exact stable_muon
  · exact stable_tau
  · exact stable_up
  · exact stable_charm
  · exact stable_top
  · exact stable_down
  · exact stable_strange
  · exact stable_bottom
realized_of_physicallyStable · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean:277 
theorem realized_of_physicallyStable {T : PatternTopology}
    (hP : PhysicallyStableCharged T) : IsRealizedChargedTopology T := by
  obtain ⟨hEW, hAct, hPass, hLoop, hSpin, hCharge, hTor, hSec, hRung, hZ⟩ := hP
  cases hsec : sectorFromTopology T with
  | Lepton =>
    rw [hsec] at hLoop hSpin hCharge hTor hSec hZ
    simp only [stableLoop, stableSpin, stableCharge, stableLadder, stableZ] at hLoop hSpin hCharge hTor hZ
    simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hTor
    rcases hTor with h | h | h
    · refine ⟨ChargedMassRow.electron, by decide, ?_⟩
      obtain ⟨a, p, l, sp, tg, cs, sec, rg, z⟩ := T
      subst hAct; subst hPass; subst hLoop; subst hSpin; subst h; subst hCharge; subst hSec
      dsimp only at hRung hZ
      subst hRung; subst hZ; rfl
    · refine ⟨ChargedMassRow.muon, by decide, ?_⟩
      rw [row_muon_lit]
      obtain ⟨a, p, l, sp, tg, cs, sec, rg, z⟩ := T
      subst hAct; subst hPass; subst hLoop; subst hSpin; subst h; subst hCharge; subst hSec
      dsimp only at hRung hZ
      subst hRung; subst hZ; rfl
    · refine ⟨ChargedMassRow.tau, by decide, ?_⟩
      rw [row_tau_lit]
      obtain ⟨a, p, l, sp, tg, cs, sec, rg, z⟩ := T
      subst hAct; subst hPass; subst hLoop; subst hSpin; subst h; subst hCharge; subst hSec
      dsimp only at hRung hZ
      subst hRung; subst hZ; rfl
  | UpQuark =>
    rw [hsec] at hLoop hSpin hCharge hTor hSec hZ
    simp only [stableLoop, stableSpin, stableCharge, stableLadder, stableZ] at hLoop hSpin hCharge hTor hZ
    simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hTor
    rcases hTor with h | h | h
    · refine ⟨ChargedMassRow.up, by decide, ?_⟩
      obtain ⟨a, p, l, sp, tg, cs, sec, rg, z⟩ := T
      subst hAct; subst hPass; subst hLoop; subst hSpin; subst h; subst hCharge; subst hSec
      dsimp only at hRung hZ
      subst hRung; subst hZ; rfl
    · refine ⟨ChargedMassRow.charm, by decide, ?_⟩
      rw [row_charm_lit]
      obtain ⟨a, p, l, sp, tg, cs, sec, rg, z⟩ := T
      subst hAct; subst hPass; subst hLoop; subst hSpin; subst h; subst hCharge; subst hSec
      dsimp only at hRung hZ
      subst hRung; subst hZ; rfl
    · refine ⟨ChargedMassRow.top, by decide, ?_⟩
      rw [row_top_lit]
      obtain ⟨a, p, l, sp, tg, cs, sec, rg, z⟩ := T
      subst hAct; subst hPass; subst hLoop; subst hSpin; subst h; subst hCharge; subst hSec
      dsimp only at hRung hZ
      subst hRung; subst hZ; rfl
  | DownQuark =>
    rw [hsec] at hLoop hSpin hCharge hTor hSec hZ
    simp only [stableLoop, stableSpin, stableCharge, stableLadder, stableZ] at hLoop hSpin hCharge hTor hZ
    simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hTor
    rcases hTor with h | h | h
    · refine ⟨ChargedMassRow.down, by decide, ?_⟩
      obtain ⟨a, p, l, sp, tg, cs, sec, rg, z⟩ := T
      subst hAct; subst hPass; subst hLoop; subst hSpin; subst h; subst hCharge; subst hSec
      dsimp only at hRung hZ
      subst hRung; subst hZ; rfl
    · refine ⟨ChargedMassRow.strange, by decide, ?_⟩
      rw [row_strange_lit]
      obtain ⟨a, p, l, sp, tg, cs, sec, rg, z⟩ := T
      subst hAct; subst hPass; subst hLoop; subst hSpin; subst h; subst hCharge; subst hSec
      dsimp only at hRung hZ
      subst hRung; subst hZ; rfl
    · refine ⟨ChargedMassRow.bottom, by decide, ?_⟩
      rw [row_bottom_lit]
      obtain ⟨a, p, l, sp, tg, cs, sec, rg, z⟩ := T
      subst hAct; subst hPass; subst hLoop; subst hSpin; subst h; subst hCharge; subst hSec
      dsimp only at hRung hZ
      subst hRung; subst hZ; rfl
  | Electroweak =>
    exact absurd hsec hEW
THEOREM no_stable_up_rung15 · no_stable_lepton_rung3 · no_stable_lepton_rung12 · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean
no_stable_up_rung15 · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean:401 
/-- **No extra up-type quark** at the forbidden up rung 15. -/
theorem no_stable_up_rung15
    {T : PatternTopology} (hP : PhysicallyStableCharged T)
    (hlabels : sectorFromTopology T = Anchor.Sector.UpQuark ∧ rungFromTopology T = 15) :
    False :=
  no_stable_charged_at (by intro row _; cases row <;> decide) hP hlabels
no_stable_lepton_rung3 · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean:386 
/-- **No fourth charged lepton** at the next lepton rung (3): the immediate
neighbor of the electron rung is physically empty. -/
theorem no_stable_lepton_rung3
    {T : PatternTopology} (hP : PhysicallyStableCharged T)
    (hlabels : sectorFromTopology T = Anchor.Sector.Lepton ∧ rungFromTopology T = 3) :
    False :=
  no_stable_charged_at (by intro row _; cases row <;> decide) hP hlabels
no_stable_lepton_rung12 · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean:394 
/-- **No fourth charged lepton** at the lepton rung 12 (between muon and tau frames). -/
theorem no_stable_lepton_rung12
    {T : PatternTopology} (hP : PhysicallyStableCharged T)
    (hlabels : sectorFromTopology T = Anchor.Sector.Lepton ∧ rungFromTopology T = 12) :
    False :=
  no_stable_charged_at (by intro row _; cases row <;> decide) hP hlabels
THEOREM physicalStabilityImageCert · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean
physicalStabilityImageCert · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean:446 
/-- The physical-stability image certificate holds. -/
def physicalStabilityImageCert : PhysicalStabilityImageCert where
  exact_image := physicalStability_exact_image
  charged_image := physicalStability_charged_image
  predicate_noncircular := fun _ => rfl
  spectrum_label_realized := stable_label_realized
  no_extra_stable_charged := by
    intro s r hnone T hP hlabels
    exact no_stable_charged_at hnone hP hlabels

What this page does not claim

This module does not derive the numerical values of particle masses. The stability predicate is not claimed to be the unique possible structural definition. The framework does not claim to explain why these nine particles exist in the standard model beyond the structural constraints.

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/Masses/MassGenesis/PhysicalStabilityImage.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