Masses Mass Genesis Admissible Mass Image Charged Rows Length

The charged row count

The declaration chargedRows_length is a machine-checked proof that a specific list, called chargedRows, contains exactly nine entries. That list is a discrete record of the known charged matter particles: the electron, muon, and tau; the up, charm, and top quarks; and the down, strange, and bottom quarks. Each entry is a ChargedMassRow, a formal name for one of these nine particles. The proof itself is trivial in the formal sense: the list is defined with those nine names, and the theorem simply verifies that the length matches the definition. It is a statement about the list as written, not about the physical world beyond it.

The theorem appears inside a larger machine-checked library of formal theorems, which the framework calls its ledger of recognition events. In this context, the nine rows are not chosen arbitrarily; each row carries a topology, a pattern of connections derived from the framework's forcing chain, and that topology determines the particle's sector, rung, charge, and coupling dimension. The library proves that these topology-derived labels agree with the labels assigned directly to each row. So the count of nine is consistent with the framework's structural picture, but the theorem itself does not derive that count from first principles. It merely records what the list contains.

What the declaration does not claim is the harder statement: that these nine rows are the only stable charged rows that could exist. That stronger claim is named separately as the ExactChargedTopologyImage obligation. The library deliberately keeps it as an open target, because proving that no extra stable closed light patterns exist is a physical theorem, not a table lookup. The nine-row count is a definitional fact, verified by computation; the exclusion of all other rows is a physical claim that remains to be proved.

In plain terms, the declaration settles a bookkeeping question: the framework's list of charged matter rows has exactly nine entries. It does not settle the question of why there are nine, or whether nine is forced by the framework's deeper principles. Those questions remain open, and the library says so explicitly. The count is a fact about the list, not a law about the universe.

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]

/-- One combined label theorem for rows. -/
theorem row_labels_eq (r : ChargedMassRow) :
    sectorFromTopology (rowTopology r) = rowSector r ∧
    rungFromTopology (rowTopology r) = rowRung r ∧
    ZFromTopology (rowTopology r) = rowZ r ∧
    couplingDimOfTopology (rowTopology r) = rowCouplingDim r :=
  ⟨row_sector_eq r, row_rung_eq r, row_Z_eq r, row_couplingDim_eq r⟩

/-- 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 prove that exactly nine charged rows are physically possible. The theorem does not derive the nine-row count from the framework's forcing principles. The theorem does not establish that the list of nine particles is complete in any physical sense.

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: