Masses Rung Table Structure

The rung table

The rung table is a list of twelve integers, one for each of the twelve fermions in the standard model: six quarks, three charged leptons, and three neutrinos. Each integer is called a rung, a discrete step on a ladder that the framework uses to build particle masses. The table's structure is the claim that almost every rung is not a free number but a sum of two ingredients: a base that counts how many kinds of gauge channel the particle couples to, and a generation torsion that depends on which of the three generations the particle belongs to.

Classically, the standard model's particle masses are 12 independent parameters, measured and tabulated but not derived from anything deeper. The rung table is an attempt to reduce that freedom. The base rule is simple: two rungs per class of gauge channel. A neutrino couples to no gauge channel, so its base is 0. A charged lepton couples only to the electromagnetic channel, so its base is 2. A quark couples to both electromagnetism and color, so its base is 4. The generation torsion then adds a small integer that depends on the generation, and the rung is the sum.

The machine-checked library of formal theorems proves that this rule reproduces eleven of the twelve rungs. The proof is not a curve fit: the base rule is overdetermined, meaning the constants are forced by fitting only the charged leptons and up quarks, and then the down quark's base follows without any further freedom. The neutrino base is also forced, but the theorem's own documentation warns that this is not evidence for the rule, because a particle coupling to nothing gets a zero base whatever the parameters are. The one exception is the third neutrino, whose rung departs from the prediction by exactly two, landing it on the charged-lepton rung of the same generation. The framework records this as a clue or a coincidence, deliberately not deciding which.

In plain language, the rung table is not twelve independent integers. Eleven of them are determined by a channel count, the constant two, and a generation torsion that was already derived elsewhere. The twelfth, the third neutrino, remains unexplained, and the framework says so explicitly. That honesty is part of the result: the table's structure is strong enough to make the single exception visible, and the exception is left as an open problem rather than smoothed over.

/-- **Eleven of the twelve rungs are sector base plus generation torsion.** This is the live
table used by the mass predictions, not the parallel per-sector definitions in
`Masses.Anchor`. -/
theorem rung_eq_predicted_of_ne_nu3 (f : Fermion) (h : f ≠ .nu3) :
    rung f = rungPredicted f := by
  cases f <;>
    simp_all [rung, rungPredicted, rungBase, activeChannelClasses, couplesToCharge,
      couplesToColor, tildeQ, sectorOf, genOf, Integers.tau, Anchor.E_passive, Anchor.W,
      passive_field_edges, cube_edges, active_edges_per_tick, D, wallpaper_groups]

/-- **The base rule is overdetermined, and the surplus prediction is correct.** Fitting
`base = a * charge + b * colour` on charged leptons and up quarks forces `a = b = 2`, which
then predicts the down-quark base without further freedom, and the table agrees. -/
theorem down_base_is_a_prediction (a b : ℤ) (hlep : a = 2) (hup : a + b = 4) :
    a + b = rungBase .d := by
  rw [hup]
  have := rungBase_values
  omega

/-- **The twelfth departs by exactly two.** The only entry the structure does not explain. -/
theorem nu3_departs_by_two : rung .nu3 = rungPredicted .nu3 + 2 := by
  simp [rung, rungPredicted, rungBase, activeChannelClasses, couplesToCharge, couplesToColor,
    tildeQ, sectorOf, genOf, Integers.tau, Anchor.E_passive, Anchor.W, passive_field_edges,
    cube_edges, active_edges_per_tick, D, wallpaper_groups]

/-- **The table is not twelve independent integers.** Every entry except the third neutrino is
determined by the channel predicate, the constant two, and the already-derived torsion. -/
theorem table_determined_except_nu3 :
    ∀ f : Fermion, f ≠ .nu3 →
      rung f = 2 * activeChannelClasses f + Integers.tau (genOf f).val := by
  intro f hf
  have := rung_eq_predicted_of_ne_nu3 f hf
  simpa [rungPredicted, rungBase] using this

What this page does not claim

The rung table does not predict any actual mass value in kilograms or electronvolts. The third neutrino's departure is not explained by the module; it is recorded as open. The neutrino base is not claimed as evidence for the base rule.

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