Masses Rung Table Structure Down Base Is A Prediction

A checkable surplus

The declaration down_base_is_a_prediction is a formal theorem in the framework's machine-checked library of formal theorems. It concerns the rung table, a discrete list of integers that the framework assigns to each fundamental fermion as a step on a ladder of predicted masses. The theorem states that if the rule for assigning a base rung is fitted to two known cases, the charged lepton and the up quark, then the value for the down quark follows with no further freedom. In the framework's own words, the base rule is overdetermined, and the surplus prediction is correct.

The rule itself is simple. Each fermion is assigned a base rung equal to twice the number of gauge channel classes it couples to. A neutrino couples to none, so its base is zero. A charged lepton couples to the electromagnetic channel, so its base is two. An up quark couples to both electromagnetic and colour channels, so its base is four. Fitting a linear form, base equals a times charge plus b times colour, to the charged lepton and the up quark forces both a and b to equal two. The theorem then checks that the same formula, with those fitted values, returns four for the down quark, exactly matching its independently defined base rung. The proof is a short algebraic identity, verified by the kernel with no assumptions beyond the standard axioms of the ambient type theory.

The theorem deliberately does not claim that the neutrino base is evidence for the rule. A species that couples to nothing gets a base of zero whatever the parameters are, so the neutrino's zero proves nothing. The framework states this limitation explicitly so the strength of the fit is not overcounted. The theorem also does not claim that the entire rung table is explained. Eleven of the twelve rungs match the predicted pattern of base plus generation torsion; the third neutrino departs by exactly two, landing on the charged lepton rung of its own generation. The framework records that departure as either a clue or a coincidence, and declines to choose.

What the theorem changes is the epistemic status of the down quark's rung. It is not one more number fitted to make a table work; it is a consequence of the same rule that fits two other entries, checked by a machine. A reader who trusts the framework's library can see that the down rung was not free. That is the entire claim, and it is exactly as strong as the two fitted inputs and the rule itself.

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

theorem rungBase_values :
    rungBase .nu1 = 0 ∧ rungBase .e = 2 ∧ rungBase .u = 4 ∧ rungBase .d = 4 := by
  refine ⟨?_, ?_, ?_, ?_⟩ <;>
    simp [rungBase, activeChannelClasses, couplesToCharge, couplesToColor, tildeQ, sectorOf]

theorem rungBase_values :
    rungBase .nu1 = 0 ∧ rungBase .e = 2 ∧ rungBase .u = 4 ∧ rungBase .d = 4 := by
  refine ⟨?_, ?_, ?_, ?_⟩ <;>
    simp [rungBase, activeChannelClasses, couplesToCharge, couplesToColor, tildeQ, sectorOf]

theorem rungBase_values :
    rungBase .nu1 = 0 ∧ rungBase .e = 2 ∧ rungBase .u = 4 ∧ rungBase .d = 4 := by
  refine ⟨?_, ?_, ?_, ?_⟩ <;>
    simp [rungBase, activeChannelClasses, couplesToCharge, couplesToColor, tildeQ, sectorOf]

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

What this page does not claim

The down quark's mass itself is not derived here, only its integer rung on a ladder. The neutrino base is not presented as evidence for the rule, because it is zero for any species that couples to nothing. The third neutrino's rung is not explained by the rule; it departs by exactly two and the framework records the departure as a clue or a coincidence.

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: