Masses Mass Genesis Physical Stability Image Physically Stable Of Realized

The stability test

The standard model of particle physics recognizes six quarks and three charged leptons: up, down, charm, strange, top, bottom, electron, muon, and tau. A central question for any theory of mass is why this list, and not a longer one, is realized in nature. The Recognition Science framework approaches this by defining a ledger, a discrete record of events, and asking which patterns of events are stable.

The declaration physicallyStable_of_realized is one half of an exact match. It states that if a topology is one of the nine realized charged topologies, then it satisfies a predicate called PhysicallyStableCharged. This predicate is built from structural invariants: one active edge per tick, a specific passive edge count, a sector pinned by the topology, and a generation torsion lying on a forced three-rung ladder. The predicate never mentions the realized row list by name.

The other half, realized_of_physicallyStable, runs in the opposite direction: any topology satisfying the stability predicate is one of the nine realized rows. Together, the theorem physicalStability_exact_image proves the two sets coincide. The framework's machine-checked library of formal theorems confirms this with zero unproven assumptions. The result is a genuine no-extra-particles statement: the structural rules cut out exactly the nine known charged particles and nothing else.

This is not a claim that the framework has derived the particle masses themselves. The stability predicate uses the three-rung ladder as a physical input; the ladder is forced by the framework's earlier results, not fitted to data. The theorem establishes a classification, not a numerical prediction. It does not say why the ladder has the values it has, nor does it address neutral particles, which lie outside this predicate's scope.

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

/-- **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⟩

What this page does not claim

The theorem does not derive the numerical values of particle masses. The theorem does not explain why the generation torsion ladder has its specific values. The theorem does not cover neutral particles.

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: