BaselineCandidate
plain-language theorem explainer
A baseline candidate is an integer numerator encoding the lightest neutrino rung in quarter-rung units via r₁ = n/4. Anyone enumerating the finite neutrino absolute-baseline choice set under the structural gap profile cites this carrier. It is a pure data structure (Repr, DecidableEq), with no proof obligations.
Claim. A baseline candidate is specified by a single integer $n \in \mathbb{Z}$ such that the lightest neutrino rung is $r_1 = n/4$ (quarter-rung units).
background
The module closes a finite-search step for the neutrino absolute baseline. The lightest rung is parameterized by a quarter-rung numerator: $r_1 = r_{1,\mathrm{num}}/4$. Downstream fields then fix the structural gap profile in numerator form ($r_2 - r_1 = 2$, then a $+7/2$ step to $r_3$), a deep-atmospheric window on $r_3$, and the canonical $-1/4$ phase class.
Under those constraints the admissible set collapses to the singleton $r_1 = -239/4$. This structure is the minimal handle for that enumeration: one integer, equality-decidable, so the candidate pool can be listed and filtered in Lean.
proof idea
No proof. The declaration is a one-field structure on $\mathbb{Z}$ with derived Repr and DecidableEq. Sibling definitions (r2_num, r3_num, quarterRung, gap and window predicates) build the rest of the candidate data on top of this carrier.
why it matters
This is the seed type for the O5 neutrino baseline choice-set enumeration. Every later filter (structural gap profile, deep-atmospheric window, quarter-phase class) and the collapse to the singleton $r_1 = -239/4$ is stated over values of this structure. In the broader Recognition ladder, neutrino rungs sit on the same $\varphi$-ladder mass formula (yardstick $\cdot \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$); fixing the absolute baseline is the missing discrete choice once gaps are structural. The module imports the neutrino sector physics layer and turns that choice into a finite, machine-checkable set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.