Masses Mass Genesis Admissible Mass Image Charged Rows Nodup

The nine charged rows

The standard model of particle physics recognizes nine charged fermions: the electron, muon, and tau leptons, plus the up, charm, and top quarks and the down, strange, and bottom quarks. In the Recognition Science framework, these nine appear as a list called chargedRows, a discrete record of the currently realized charged particle rows. The theorem chargedRows_nodup proves that this list has no repeated entries: each of the nine appears exactly once. That is a formal statement about the list's internal structure, verified by direct computation in the framework's machine-checked library of formal theorems.

The proof is a computation, not a physical derivation. The declaration checks that the nine names are pairwise distinct by evaluating the list directly. It says nothing about whether these nine are the only possible charged rows, or whether the list matches any particular experimental measurement. The theorem is a bookkeeping fact: within the list as defined, there are no duplicates. It is the kind of guarantee that a large formal construction needs before it can reason about the list safely, since a duplicate would make counting arguments and membership proofs unreliable.

The surrounding module separates three claims that are easy to mix. First, it assigns each of the nine rows a topology-derived label, such as sector and rung, and proves those labels agree with the row definitions. Second, it packages the nine rows as a finite candidate image. Third, it names a separate obligation, ExactChargedTopologyImage, which would assert that stable admissible topology has exactly this image and no extra neighboring rows. That third claim is deliberately left as an open target: proving that no other stable closed light patterns exist is a real physical theorem, not a table lookup. The chargedRows_nodup theorem belongs to the first group; it is a structural guarantee about the list, not a claim about the physical completeness of that list.

What the theorem changes is practical: it lets the framework treat the nine rows as a set with exactly nine distinct members, which is what later reasoning about sectors, rungs, and forbidden near rows relies on. It does not, by itself, tell a reader which particles exist in nature. That question belongs to the physical closure theorem, which remains open. The distinction matters because a list with duplicates would still be a list, but a list with duplicates would break the counting and exclusion arguments that the framework builds on top of it.

In plain terms, the declaration is a hygiene check on a definition. It confirms that the framework's list of nine charged rows is clean, with no accidental repetition. It is the kind of small, precise lemma that a large formal system needs to stay trustworthy, and it is proved by direct computation rather than by appeal to any physical principle.

theorem chargedRows_nodup : chargedRows.Nodup := by
  decide

theorem chargedRows_length : chargedRows.length = 9 := by
  rfl

/-- The ordered charged image list: charged leptons, up family, down family. -/
def chargedRows : List ChargedMassRow :=
  [electron, muon, tau, up, charm, top, down, strange, bottom]

theorem chargedRows_nodup : chargedRows.Nodup := by
  decide

/-- A physical admissibility predicate has the exact charged image if it contains
all candidate rows and contains no other charged topologies. This is the true
remaining M2 theorem, parameterized by the eventual primitive `P`. -/
structure ExactChargedTopologyImage
    (P : PatternTopology → Prop) : Prop where
  complete :
    ∀ row : ChargedMassRow, row ∈ chargedRows → P (rowTopology row)
  no_extra :
    ∀ T : PatternTopology, P T →
      ∃ row : ChargedMassRow, row ∈ chargedRows ∧ T = rowTopology row

What this page does not claim

The theorem does not claim the nine rows are the only physically possible charged rows. The theorem does not claim the list matches any particular experimental measurement. The theorem does not prove that stable admissible topology has exactly this image and no extra rows.

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: