rungResidueClass
plain-language theorem explainer
The definition collects fermions whose rung values are congruent modulo 360, encoding the synchronization between the eight-tick octave and rung-45 structure. Modelers of fermion mass hierarchies under the Recognition Science anchor policy cite it to identify sets sharing a common residue class for equal-Z degeneracy at the anchor scale. It is realized directly as a set comprehension that applies modular equality to the rung map.
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 supplies the bridge from the recognition framework to the Standard Model by defining the Fermion inductive type (six quarks, three charged leptons, three neutrinos) together with the ZOf charge-index map and the gap display function $F(Z) = ln(1 + Z/φ)/ln(φ)$. The rung map assigns each fermion an integer position on the phi-ladder; the 360-unit modulus is the joint period of the eight-tick octave (T7) and the rung-45 offset. Upstream results on phi-forcing and ledger factorization supply the J-cost and defect structures that justify treating rung as the discrete coordinate for mass placement.
proof idea
One-line definition that builds the set via the comprehension {f | Int.ModEq 360 (rung f) a}.
why it matters
The definition supplies the rung-offset half of the admissible-family encoding required by the anchor policy, which asserts that the integrated RG residue at μ* equals gap(ZOf i) to tolerance 1e-6. It feeds the parent construction of equal-Z families and thereby supports the mass formula yardstick · φ^(rung-8+gap(Z)) on the phi-ladder. The 360 modulus directly implements the T7 eight-tick octave landmark while remaining compatible with the D=3 spatial dimension and the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.