Masses Mass Genesis Admissible Mass Image Forbidden Near Rows Not In Candidate I

The forbidden near rows

The framework's mass model arranges charged particles in a discrete ledger, a record where each particle occupies a row labeled by sector (lepton, up quark, or down quark) and a rung number. The nine known charged particles, electron through bottom quark, occupy nine specific rows. The declaration forbiddenNearRows_not_in_candidate_image checks six additional rows that lie near those nine, one rung away in each sector, and establishes by direct computation that none of them appears in the realized candidate image.

The six forbidden rows are: lepton rung 3 (near the electron at rung 2), lepton rung 12 (near the muon at rung 13), up quark rung 15 (between charm at 17 and top at 28), up quark rung 21, down quark rung 11 (near strange at 10), and down quark rung 17 (near bottom at 18). The check is a finite one: the declaration evaluates the candidate list and confirms each forbidden sector-rung pair is absent. This is a theorem in the machine-checked library of formal theorems, with no unproved assumptions and no added axioms.

What the declaration does not claim is the stronger physical statement. It does not establish that no stable closed light pattern exists at those rows; that remains an open obligation named ExactChargedTopologyImage in the same file. The file separates three layers explicitly: topology-derived labels for the realized rows, the finite candidate image from the generation ladder, and the remaining theorem that stable admissible topology has exactly this image and no extra neighboring rows. The forbidden-rows check covers only the second layer, the candidate list itself.

The check matters because it sharpens the model's prediction. If a near row were present in the candidate image, the framework would predict an undiscovered charged particle close in mass to a known one. The declaration rules that out for these six specific rows, within the candidate image as constructed. The physical closure, that no other stable patterns exist anywhere, stays open, and the framework names it as such rather than treating it as settled.

theorem forbiddenNearRows_not_in_candidate_image :
    forbiddenNearRows.all
      (fun sr => !realizedSectorRung sr.1 sr.2) = true := by
  native_decide

/-- A few immediate neighbor rows that are not in the realized charged image.
Exact physical exclusion follows only after `ExactChargedTopologyImage` is
proved for the physical admissibility predicate. -/
def forbiddenNearRows : List (Anchor.Sector × ℤ) :=
  [ (Anchor.Sector.Lepton, 3)
  , (Anchor.Sector.Lepton, 12)
  , (Anchor.Sector.UpQuark, 15)
  , (Anchor.Sector.UpQuark, 21)
  , (Anchor.Sector.DownQuark, 11)
  , (Anchor.Sector.DownQuark, 17) ]

What this page does not claim

The declaration does not establish that no stable closed light pattern exists at the forbidden rows. The declaration does not establish that the candidate image is physically complete. The declaration does not derive the rung numbers themselves from first principles.

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/AdmissibleMassImage.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: