Masses Mass Genesis Physical Stability Image Physical Stability Exact Image

The exact image theorem

The declaration physicalStability_exact_image in the Recognition Science framework's machine-checked library of formal theorems proves a precise no-extra-particles statement. It defines a predicate called physical stability, a set of structural rules a stable charged pattern must obey, and then proves that this predicate is satisfied by exactly the nine realized charged particle topologies: the electron, muon, tau, up, charm, top, down, strange, and bottom. The theorem is an if-and-only-if: a pattern is physically stable if and only if it is one of these nine realized rows.

The stability rules themselves are the interesting part. They do not merely list the nine particles. Instead, they impose constraints drawn from the framework's 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 directly. The theorem proves that these abstract constraints cut out exactly the nine realized rows and nothing else. This is the genuine no-extra-particles statement: no other pattern, no matter how exotic, satisfies the stability rules.

The proof is carried out in the Lean 4 proof assistant, with zero admitted axioms and zero 'sorry' placeholders. It is a formal, machine-checked derivation, not a paper-and-pencil argument. The theorem is tagged THEOREM in the framework's epistemic system, meaning it is a proved result within the framework's axioms. The framework's own documentation describes it as discharging a reduction: an earlier admissible mass image condition is reduced to this exact image theorem.

What the theorem does not claim is equally important. It does not claim that these nine particles are the only possible particles in the physical universe. It claims only that within the Recognition Science framework, given its definitions of physical stability and realized charged topologies, the stability predicate selects exactly these nine. It does not derive the values of the particle masses; the ladder of torsion values is forced by the framework, but the comparison to measured PDG masses is an empirical check, not part of the theorem. And it does not claim that the framework's structural invariants are the true physical laws; it proves a relationship between two formal objects defined within the framework.

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

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

/-- **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 prove that only nine particles exist in the physical universe. The theorem does not derive the numerical values of the particle masses. The theorem does not claim that the framework's structural invariants are the true physical laws.

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: