Encyclopedia Masses Masses Mass Genesis Physical Stability Image Physical Stability Charged Image

ARTICLE 4 claims 4 theorems

Masses Mass Genesis Physical Stability Image Physical Stability Charged Image

A single structural rule, stated without naming any particle, is proven to produce exactly the nine known charged fermions and no others.

Verify this page

The exact particle list

The standard model of particle physics lists nine charged fermions: the electron, muon, and tau leptons, and the up, charm, top, down, strange, and bottom quarks. A long-standing question is whether this list is arbitrary or forced by some deeper principle. The Recognition Science framework addresses this by asking what structural features a stable, closed pattern of charge must have, and then proving that those features alone pick out precisely the nine known particles.

The framework models a particle's internal state as a discrete record of events called a ledger, with a cost function that the framework proves must take a specific form. From this, it derives a recognition cycle of eight steps. The declaration physicalStability_charged_image is a theorem in the framework's machine-checked library of formal theorems. It proves that a predicate called PhysicallyStableCharged, which checks only structural invariants and never mentions any particle by name, is satisfied by exactly the nine realized charged topologies.

Those invariants are precise. A stable charged pattern must have exactly one active edge per tick, a specific number of passive edges, and a loop rank, spin class, and charge skew fixed by its sector (lepton, up quark, or down quark). Its generation torsion must lie on a forced three-rung ladder, such as [0, 11, 17] for leptons or [0, 13, 24] for up quarks. The predicate also enforces internal consistency between the sector, rung, and a computed Z value. The theorem proves that any pattern meeting these conditions is one of the nine realized rows, and conversely that every one of the nine rows meets the conditions.

This is a genuine no-extra-particles statement. The framework's library proves that no stable pattern exists at, for example, lepton rung 3 or up-quark rung 15. The predicate is non-circular: it does not reference the realized row list, so the match is a derived result, not an assumption. The proof is checked with zero gaps and zero new axioms, meaning it relies only on the standard logical foundations of the machine-checked library.

What the theorem does not claim is equally important. It does not derive the numerical masses of these particles; it establishes which particles exist. It does not prove that the structural invariants themselves are physically necessary; the ladder of torsion values is a physical input to the framework, forced elsewhere but not derived in this declaration. And it does not claim that the framework's model of particle structure is the only possible one. It shows that within this framework, the particle list is not arbitrary: it is the exact image of a stability condition.

THEOREM physicalStability_charged_image · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean
physicalStability_charged_image · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean:361 
/-- **M2 closure.** The physical-stability predicate has the exact charged topology
image: complete on the realized rows and admitting no extra topologies. -/
theorem physicalStability_charged_image :
    ExactChargedTopologyImage PhysicallyStableCharged :=
  exactImage_of_physicalStability physicalStability_exact_image
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 realized_of_physicallyStable · physicallyStable_of_realized · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean
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
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
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

The theorem does not derive the numerical masses of the nine particles. The theorem does not prove the physical necessity of the structural invariants themselves. The theorem does not claim that the framework's model of particle structure is the only possible one.

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