Rung
plain-language theorem explainer
Rung is the type of rational numbers used to represent possibly fractional positions on the phi-ladder. Modules handling quark masses, neutrino refinements, or atmospheric layering cite the convention for uniform reporting across integer and fractional cases. The declaration is a direct abbreviation of ℚ with no further structure or obligations.
Claim. A rung on the $φ$-ladder is an element of the rational numbers $ℚ$.
background
The phi-ladder assigns masses and energies via yardstick times $φ$ raised to a rung index, with integer rungs used in the core model for rigidity. Upstream definitions such as rung in RSBridge.Anchor map fermions to integers (e.g., electron at 2, top quark at 21), while rung in AnchorPolicy dispatches by sector to integer values. The module supplies a type-light seam so that selected physics modules can explore quarter-ladder or other fractional placements without altering the core integer representation.
proof idea
The declaration is a direct abbreviation of the rational numbers ℚ.
why it matters
It supplies the uniform type used by downstream results including phi_energy_rung_step (adjacent rungs scale by $φ$), atmospheric_layering_one_statement (layer boundaries at rungs 0, 3, 7), and animal_z_complexity_one_statement (Z-complexity as geometric sequence on the ladder). The module doc notes this is a representation convention rather than a claim that fractional rungs are canonical, leaving open the question of which denominators are physically realized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.