Masses Mass Genesis Admissible Mass Image

The admissible mass image

The admissible mass image is the finite list of charged particle types that Recognition Science's generation ladder can actually produce. The list has nine entries: the electron, muon, and tau; the up, charm, and top quarks; and the down, strange, and bottom quarks. These are the charged rows of the mass framework, the only rows that carry electric charge. The central result is a machine-checked proof that this list is exactly what the topology of the framework labels as realized, no more and no fewer.

The framework's ledger, a discrete record of recognition events, assigns each particle type a topology: a pattern of how the row sits in the generation structure. From that topology, the framework derives labels such as sector (lepton, up quark, or down quark), rung (a position on the mass ladder), and a coupling dimension. The proof shows, by exhaustive case analysis, that for each of the nine charged rows, these topology-derived labels match the row's own definitions exactly. It also shows the nine rows are distinct and that the list has length nine, so no two names collapse into one row.

The module packages a candidate image: the set of topologies that the generation ladder forces. It proves that every one of the nine rows realizes this image, and that no other topology outside the list can realize it. This is the completeness and no-extra part of the theorem. The proof is computational, checking all cases by decision procedure, and it carries no axioms beyond the standard three of the underlying logic.

What the module deliberately does not prove is the physical closure claim. The theorem states: if a stability predicate on topologies holds exactly for the realized rows, then the image is exact. But proving that such a stability predicate actually holds in the physical world, that no stable closed light pattern exists beyond these nine, is left as a named obligation, ExactChargedTopologyImage. The module proves the conditional and packages the candidate; it does not claim the physical premise.

In plain language: the framework has a machine-checked certificate that its generation ladder, if it produces any charged row, produces exactly these nine, and that no nearby row (six specific sector-rung pairs are named and excluded) can sneak in. The remaining step, showing that the physical stability condition itself holds, is the open target. This separation matters because it keeps a table lookup distinct from a physical theorem.

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

theorem chargedRows_nodup : chargedRows.Nodup := by
  decide

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

/-- **Instantiation.** The exact-image structure is inhabited by the canonical
realized-image predicate. This shows `ExactChargedTopologyImage` is satisfiable, not
vacuous: the open content is not the structure itself but matching a physical
stability predicate to this image. -/
theorem exactImage_realized :
    ExactChargedTopologyImage IsRealizedChargedTopology where
  complete := fun row hrow => ⟨row, hrow, rfl⟩
  no_extra := fun _T hP => hP

/-- **Reduction.** If a physical-stability predicate coincides with the canonical
realized image, then it has the exact charged image. This reduces the M2 closure to
proving the coincidence; the structural `complete` / `no_extra` content is already
discharged by `exactImage_realized`. -/
theorem exactImage_of_physicalStability
    {P : PatternTopology → Prop}
    (h : ExactImageFromPhysicalStability P) :
    ExactChargedTopologyImage P where
  complete := fun row hrow => (h (rowTopology row)).mpr ⟨row, hrow, rfl⟩
  no_extra := fun T hP => (h T).mp hP

What this page does not claim

The physical stability predicate that would close the exact image theorem is not proved here. The rung numbers themselves are not derived in this module, only matched to topology labels. No claim is made that these nine are the only possible particle types in the full framework, only the only charged rows in this image.

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: