Encyclopedia Masses Masses Mass Genesis Physical Stability Image Realized Of Physically Stable

ARTICLE 4 claims 3 theorems 1 model

Masses Mass Genesis Physical Stability Image Realized Of Physically Stable

A machine-checked proof shows that a purely structural definition of physical stability picks out exactly the nine known charged particles and no others.

Verify this page

The stability filter

In particle physics, the question of which particles exist is usually answered by experiment. The Recognition Science framework asks a different question: can a purely structural rule, one that never mentions the known particle list, single out exactly the particles that are observed? The declaration realized_of_physicallyStable is the machine-checked answer to that question. It proves that a predicate called physical stability, defined only from abstract invariants, is satisfied by precisely the nine realized charged topologies, which correspond to the electron, muon, tau, up, charm, top, down, strange, and bottom particles.

The definition of physical stability is built from constraints that a stable closed charged light pattern must satisfy. These include having exactly one active edge per tick, a specific passive-edge count, a sector pinned by the topology, and a charge skew, spin class, and loop rank fixed to that sector's values. The generation torsion must lie in a three-rung ladder that is itself forced by earlier results in the framework. None of these conditions mentions the realized row list. The theorem physicalStability_exact_image then proves the two-way implication: every realized topology is physically stable, and every physically stable topology is realized. This is the genuine no-extra-particles statement.

The proof is carried out in a machine-checked library of formal theorems, with zero admitted axioms beyond the standard logical ones. The result is a theorem in the strict sense: it derives, from the structural definition alone, that the stability filter cuts out exactly the nine known rows and nothing else. This is not a fitted model or an empirical match; it is a proved equivalence between a structural predicate and the observed particle set.

What the declaration does not claim is equally important. It does not claim that physical stability, as defined here, is the unique possible stability predicate, nor that it explains why these nine particles have their specific masses. The theorem concerns only the topology of the particles, not their mass values. It also does not claim that the structural predicate is physically motivated in an independent sense; the ladder of torsion values is described as closure-forced within the framework, but that forcing is a framework-internal result, not an experimental observation.

The consequence for the framework is that the particle spectrum is not an input but an output of a structural condition. The reader can now see that the nine known charged particles form a closed set under a precisely stated stability rule, and that any attempt to add a tenth particle would violate at least one of the structural invariants. This turns the empirical list of particles into a derived consequence of a definition, within the framework's own terms.

THEOREM realized_of_physicallyStable · 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
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⟩
MODEL PhysicallyStableCharged · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean
PhysicallyStableCharged · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean:65 
/-- **Physical stability of a charged closed light pattern**, as structural constraints
on its primitive topology. No reference to the realized row list. -/
def PhysicallyStableCharged (T : PatternTopology) : Prop :=
  sectorFromTopology T ≠ Anchor.Sector.Electroweak ∧
  T.q3ActiveEdges = 1 ∧
  T.q3PassiveEdges = Anchor.E_passive ∧
  T.q3LoopRank = stableLoop (sectorFromTopology T) ∧
  T.spinClass = stableSpin (sectorFromTopology T) ∧
  T.chargeSkew = stableCharge (sectorFromTopology T) ∧
  T.generationTorsion ∈ stableLadder (sectorFromTopology T) ∧
  T.sector = sectorFromTopology T ∧
  T.rung = T.spinClass + T.generationTorsion + 1 ∧
  T.Z = stableZ (sectorFromTopology T) T.chargeSkew
THEOREM no_stable_charged_at · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean
no_stable_charged_at · IndisputableMonolith/Masses/MassGenesis/PhysicalStabilityImage.lean:378 
/-- **No extra stable charged particle.** A physically stable charged topology cannot
sit at any sector/rung pair absent from the nine realized rows. -/
theorem no_stable_charged_at {s : Anchor.Sector} {r : ℤ}
    (hnone : NoRealizedSectorRung s r)
    {T : PatternTopology} (hP : PhysicallyStableCharged T)
    (hlabels : sectorFromTopology T = s ∧ rungFromTopology T = r) : False :=
  exact_image_excludes_nonrealized_sector_rung physicalStability_charged_image hnone hP hlabels

What this page does not claim

The declaration does not claim that physical stability is the unique possible stability predicate. The declaration does not claim to explain the measured masses of the nine particles. The declaration does not claim that the torsion ladder is derived from experiment rather than from framework-internal forcing.

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