rungResidueClass
plain-language theorem explainer
The rung residue class collects fermions whose rung level is congruent to a given integer modulo 360. Mass modelers cite it when grouping species under the equal-Z degeneracy policy at the anchor scale. It encodes the synchronization of the eight-tick octave with rung-45 steps on the phi-ladder. The definition is realized as a direct set comprehension that applies modular equality to the rung function.
Claim. For an integer $a$, the rung residue class is the set of fermions $f$ such that rung$(f) ≡ a mod 360$.
background
The RSBridge.Anchor module bridges the recognition framework to particle physics by defining Fermion as the inductive type with twelve elements (six quarks, three charged leptons, three neutrinos). The rung function assigns each fermion an integer level on the phi-ladder used in the mass formula yardstick * phi^(rung - 8 + gap(Z)). ZOf computes the charge-indexed integer Z_i = q̃² + q̃⁴ (+4 for quarks), and gap(Z) = ln(1 + Z/φ)/ln(φ) is the closed-form display function claimed to match the integrated RG residue at anchor scale μ*. The 360 modulus is the joint sync scale of the eight-tick octave (period 2^3) and rung-45 steps.
proof idea
The definition is a direct set comprehension that applies the Int.ModEq predicate to the rung value of each fermion against the parameter a.
why it matters
It supplies the rung-offset half of the admissible-family encoding that combines with equal-Z degeneracy for pure phi-power mass ratios at μ*. This supports the single-anchor phenomenology claim that integrated RG flow equals gap(ZOf i) to ~1e-6 tolerance and feeds the downstream mass computations. It realizes part of the phi-ladder structure with D=3 and the T7 eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.