pith. machine review for the scientific record. sign in
def definition def or abbrev high

rung

show as:
view Lean formalization →

The rung definition assigns a fixed integer level on the phi-ladder to each of the twelve Standard Model fermions. Modelers computing particle masses via the Recognition Science mass formula cite these values when evaluating yardstick times phi to the power of rung minus eight plus gap of Z. The definition is realized by exhaustive case distinction on the Fermion constructors with no further reduction steps.

claimLet F denote the set of twelve Standard Model fermions (six quarks, three charged leptons, three neutrinos). The rung map r: F → ℤ is given by r(electron)=2, r(muon)=13, r(tau lepton)=19, r(up quark)=4, r(charm)=15, r(top)=21, r(down quark)=4, r(strange)=15, r(bottom)=21, r(ν₁)=0, r(ν₂)=11, r(ν₃)=19.

background

The RSBridge.Anchor module enumerates the Fermion type as the twelve Standard Model species and introduces the companion maps ZOf (charge-indexed integer) and gap (display function F(Z) = ln(1 + Z/φ)/ln(φ)). The rung assignment supplies the discrete index required by the mass formula yardstick ⋅ φ^(rung − 8 + gap(Z)) at the anchor scale μ⋆. Upstream results supply analogous rung maps in AnchorPolicy for lepton and quark sectors and a base rung constant in Constants. The module states the single-anchor phenomenology claim that the integrated RG residue equals gap(ZOf i) at the anchor.

proof idea

The definition is a direct pattern match on the Fermion inductive type, returning the listed integer for each constructor. No lemmas are invoked; the body is the base assignment itself.

why it matters in Recognition Science

This supplies the rung inputs required by forty downstream declarations, including energy bounds for photobiomodulation devices and settlement counts on the phi-ladder. It realizes the discrete levels of the Recognition mass formula and connects to the T5–T8 forcing chain through the phi fixed point and eight-tick octave. The assignment supports the anchor-scale claim without adding hypotheses.

scope and limits

formal statement (Lean)

  94noncomputable def rung : Fermion → ℤ
  95| .e   => 2   | .mu  => 13  | .tau => 19
  96| .u   => 4   | .c   => 15  | .t   => 21
  97| .d   => 4   | .s   => 15  | .b   => 21
  98| .nu1 => 0   | .nu2 => 11  | .nu3 => 19
  99

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (9)

Lean names referenced from this declaration's body.