r3
plain-language theorem explainer
The atmospheric (third-generation) neutrino rung of a baseline candidate, returned as a rational quarter-rung. Forcing and matching theorems in the neutrino baseline module cite it when pinning the deep-atmospheric window to the canonical residue. One-line definition: apply the quarter-rung map to the structural third-rung numerator.
Claim. Given a baseline candidate $c$ encoded by the lightest-neutrino quarter-rung numerator, the atmospheric rung is the rational $r_3(c)=n_3(c)/4$, where $n_3(c)$ is the integer numerator fixed from the lightest rung by the structural gap profile $(+2$, then $+7/2)$.
background
The module closes a finite-search step for the neutrino absolute baseline. Candidates are parameterized by a single integer numerator for the lightest rung: $r_1=r_{1,\mathrm{num}}/4$. The structural gap profile then fixes the second and third numerators in closed form ($+2$, then $+7/2$ in rung units), so each candidate determines a full triple of quarter-rungs.
quarterRung is the map sending an integer numerator $n$ to the rational $n/4$. The third-rung numerator is the one that lands in the deep-atmospheric window once the phase class is imposed. In Recognition Science mass language these rungs sit on the $\varphi$-ladder (yardstick times $\varphi$ to a rung offset), so the rational $r_3$ is the atmospheric coordinate that later matching theorems compare to the canonical residue res_nu3.
Local setting (module header): under the deep-atmospheric window and the canonical $-1/4$ phase class, the admissible baseline set collapses to the singleton $r_1=-239/4$.
proof idea
Pure definition, not a proof. Body is the one-line composition of the quarter-rung map with the structural third-rung numerator of the candidate. No tactics, no lemmas discharged at this site.
why it matters
This accessor is the atmospheric coordinate used throughout the O5 neutrino baseline enumeration. Downstream, deep_window_phase_forces_r3_value shows that under the deep-atmospheric window and quarter-phase class one has $r_3(c)=-217/4$; canonical_r3_matches_res_nu3 identifies the canonical candidate's $r_3$ with res_nu3; and the deep-ladder / edge-confinement theorems force the same pair $(r_1,r_3)$ without extra filters.
It also appears in the lepton-generation necessity layer (lepton_rungs_unique, torsion_minimality_forced), where integer rung triples are constrained by torsion stability on the cubic ledger. In the broader framework the value feeds the $\varphi$-ladder mass formula for the heaviest neutrino generation once the baseline singleton is fixed. The module's stated closure target is exactly that singleton $r_1=-239/4$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.