Masses Rung Table Structure Table Determined Except Nu3

The rung table's reach

In the Recognition Science framework, particle masses are not free parameters. They sit on a ladder of discrete levels called rungs, a discrete record of structural position. The theorem table_determined_except_nu3 states that for every fermion except the third neutrino, the rung is exactly equal to a simple formula: twice the number of gauge channel classes the particle couples to, plus a generation-dependent torsion term. The formula is rung(f) = 2 * activeChannelClasses(f) + tau(genOf(f)). This is a proved theorem in the framework's machine-checked library of formal theorems.

The rule has a concrete, testable content. A fermion that couples to no gauge channels, like the first neutrino, gets a base rung of zero. A charged lepton like the electron couples to one channel class and gets a base of two. Quarks couple to two channel classes and get a base of four. The theorem rungBase_values proves these values. The framework then shows that fitting this base rule on the charged leptons and up quarks forces the coefficients to be equal, and that this same rule correctly predicts the down quark's base without any further freedom. The theorem down_base_is_a_prediction proves this overdetermination.

The theorem's name points to its own limit. The third neutrino, nu3, is the single exception. The theorem nu3_departs_by_two proves that its rung is exactly two higher than the formula predicts. The framework records this departure honestly: it is not explained by the structure. The theorem nu3_shares_the_tau_rung shows that this departure lands nu3 on the same rung as the tau lepton, its charged partner in the same generation. The framework explicitly records this as either a clue or a coincidence, and does not decide between them.

What the theorem does not claim is as important as what it proves. It does not claim that the rung table is derived from first principles; the channel predicate, the constant two, and the torsion function are inputs, not outputs. It does not claim that the third neutrino's rung is a failure of the framework; it is simply an open target. It does not claim that the rung values are measured masses; they are structural positions that the framework's mass predictions use as inputs. The theorem is a precise statement of how much of the table is forced, and it names the one place where the forcing stops.

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

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

/-- And the departure lands it on the charged-lepton rung of the same generation, which is
either a clue or a coincidence and is recorded as neither. -/
theorem nu3_shares_the_tau_rung : rung .nu3 = rung .tau := by
  simp [rung]

What this page does not claim

The rung table is not derived from first principles; the channel predicate, the constant two, and the torsion function are inputs. The third neutrino's departure is not explained by the structure; it is recorded as an open target. The rung values are not measured masses; they are structural positions used by the framework's mass predictions.

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: