quarterRung
plain-language theorem explainer
Maps an integer quarter-rung numerator to the corresponding rational rung on the neutrino phi-ladder by dividing by four. Every baseline candidate in the O5 choice-set enumeration reads its rungs through this converter. The body is the literal cast-and-divide definition; no proof content.
Claim. For any integer $n$, the quarter-rung value is the rational $n/4$.
background
The neutrino baseline module enumerates admissible absolute rungs for the lightest neutrino by a quarter-rung integer numerator. Structural gaps are written in numerator form ($+2$, then $+7/2$), and a deep-atmospheric window plus the canonical $-1/4$ phase class are imposed so the admissible set collapses to the singleton $r_1=-239/4$.
Rungs themselves live on the Recognition Science phi-ladder (masses scale as yardstick times $\varphi$ to a rung power). Working in units of $1/4$ keeps all candidate arithmetic integral until the final rational values are needed. This definition is the single conversion step from those numerators to $\mathbb{Q}$.
proof idea
Pure definition: cast the integer numerator to $\mathbb{Q}$ and divide by $4$. No lemmas, no tactics.
why it matters
Local plumbing for the O5 neutrino baseline closure. The three rung extractors $r_1,r_2,r_3$ are thin wrappers around it, and the forcing theorems (deep-window plus phase class imply $r_1=-239/4$ and $r_3=-217/4$) and the matching theorems against the neutrino-sector residues all simp through this converter. Without a uniform quarter-rung map, the finite-search collapse to a singleton baseline would not type-check against the existing residue constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.