deep_window_phase_forces_res_nu1
plain-language theorem explainer
Under the deep-atmospheric window and canonical quarter-phase filters, any neutrino baseline candidate has lightest-neutrino rung equal to the canonical residual rung (−239/4). Downstream edge-confinement forcing cites this to pin the absolute baseline. Proof is a two-line calc: force the rational value, then match the residual definition.
Claim. Let $c$ be a baseline candidate (encoded by the quarter-rung numerator of the lightest neutrino rung $r_1$). If $c$ satisfies the deep atmospheric window on $r_3$ and lies in the canonical $-1/4$ quarter-phase class, then $r_1(c)=\mathrm{res}_{\nu_1}$.
background
This module closes a finite-search step for the neutrino absolute baseline. Candidates are parameterized by an integer quarter-rung numerator so that the lightest rung is $r_1=r_{1,\mathrm{num}}/4$. Structural gaps are fixed in numerator form ($+2$, then $+7/2$), which determines $r_2$ and $r_3$ from $r_1$.
Two Boolean filters cut the pool: a deep atmospheric window on the heaviest rung $r_3$, and membership in the canonical quarter-phase class (the built-in $-1/4$ spacing). The module claim is that these constraints collapse the admissible set to the singleton $r_1=-239/4$.
The residual symbol $\mathrm{res}_{\nu_1}$ is that same rational written as the framework's canonical lightest-neutrino rung. The present theorem is the alignment step: window plus phase already force $r_1$ onto that residual.
proof idea
Tactic proof by a two-step calc. First apply the sibling lemma that deep-window plus quarter-phase force the concrete value $r_1(c)=(-239:\mathbb{Q})/4$. Then rewrite that rational to $\mathrm{res}_{\nu_1}$ via the simplification identity res_nu1_simp (used symmetrically). No case split or search remains at this layer.
why it matters
Parent theorem edge_confinement_forces_canonical_baseline uses this after forcing the filter pair from edge-confinement of the atmospheric level: once the window and phase hold, $r_3$ and $r_1$ collapse to the canonical residuals $\mathrm{res}{\nu_3}$ and $\mathrm{res}{\nu_1}$. That is the full baseline-forcing statement for the O5 neutrino choice-set enumeration.
In Recognition Science the absolute neutrino baseline sits on the $\varphi$-ladder mass formula (yardstick times $\varphi$ to a rung offset). Pinning $r_1$ removes a discrete free parameter in the three-flavor rung triple and feeds verification that the structural gap profile plus atmospheric edge data select a unique lightest rung. The doc-comment records the built-in-spacing reading: the same forcing aligns with the canonical residual rather than a nearby quarter-rung neighbor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.