Masses Mass Genesis Admissible Mass Image Row Coupling Dim Eq

The coupling dimension

The declaration row_couplingDim_eq is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that for each of the nine charged particles in the framework's list, the coupling dimension computed from the particle's topology equals the coupling dimension assigned to that particle in the row data. The list is exactly the electron, muon, tau, up, charm, top, down, strange, and bottom. The theorem is checked by the library's kernel with no unproved assumptions.

The coupling dimension itself is a small natural number attached to each particle type. In the framework's data, the leptons (electron, muon, tau) have coupling dimension 1, the up-type quarks (up, charm, top) have 0, and the down-type quarks (down, strange, bottom) have 2. The theorem says that this number, whatever physical meaning it carries, is consistent with the topology that the framework derives for each row. It is a consistency result between two layers of the framework's construction, not a derivation of the coupling dimension from first principles.

What the theorem does not claim is more important than what it does. It does not prove that the nine rows are the only possible stable charged topologies. That stronger statement is a separate obligation, named ExactChargedTopologyImage, which the framework explicitly leaves open. The library proves that the nine rows are realized and that certain nearby forbidden rows are absent, but it does not prove that no other stable topology exists. The framework's own documentation calls this remaining step a real physical theorem, not a table lookup.

The theorem also does not assign physical meaning to the coupling dimension values. It only shows that the values 0, 1, and 2 are consistent with the topology map. Whether those numbers correspond to gauge couplings, charges, or something else is not part of this declaration. The framework's mass ladder and the comparison to measured particle masses are separate claims, governed by their own theorems and empirical checks.

In plain terms, row_couplingDim_eq is a bookkeeping check. It confirms that two independent descriptions of the same nine particles agree. The deeper question, whether these nine are the complete stable set, remains a named open target in the framework.

/-- Coupling dimensions are extracted from topology for every realized charged row. -/
theorem row_couplingDim_eq (r : ChargedMassRow) :
    couplingDimOfTopology (rowTopology r) = rowCouplingDim r := by
  cases r <;> native_decide

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

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

What this page does not claim

The theorem does not prove that the nine rows are the only possible stable charged topologies. The theorem does not assign physical meaning to the coupling dimension values 0, 1, and 2. The theorem does not derive the coupling dimension from the framework's forcing chain.

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: