module module moderate

`IndisputableMonolith.Verification.NeutrinoBaselineChoiceSet`

Defines the discrete baseline choice set for neutrino rung assignments on the deep phi-ladder. It packages quarter-rung numerators, a canonical candidate, and a small candidate pool against the deep-atmospheric window and structural gap profile. Verification authors cite it when fixing which (r1,r2,r3) triples are admissible before mass-scale checks. The module is definitional scaffolding over NeutrinoSector, not a proved uniqueness theorem.

claimA baseline candidate is a triple of quarter-rung data $(r_1,r_2,r_3)$ with $r_1 = n_1/4$ (and analogous numerators for $r_2,r_3$), together with a canonical choice, a finite candidate pool, a deep-atmospheric acceptance window, a quarter-phase class, and a structural gap profile used to score neutrino deep-ladder placements.

background

Recognition Science places neutrino masses on the deep phi-ladder: integer (or quarter-integer) rungs far below the electron rung $R_e = 2$, typically even integers near $-50$. The upstream NeutrinoSector module states the T14 hypothesis that neutrinos occupy that deep ladder and derives the mass-scale framework from it.

This verification module does not re-derive masses. It fixes the discrete choice language used when comparing baselines: quarter-rung encoding $r_i = n_i/4$, named numerators, a canonical candidate, and a small pool of alternatives. Auxiliary structure includes a deep-atmospheric window (the observational band the baseline must hit), a quarter-phase class, and a structural gap profile that records how the three rungs sit relative to the ladder gaps.

The setting is therefore combinatorial selection inside an already-posed physical hypothesis, not a new dynamical law.

proof idea

This is a definition module, not a proof module. It introduces BaselineCandidate and concrete numeric/structural fields (quarter-rung numerators, $r_1,r_2,r_3$, canonical candidate, candidate pool, deep-atmospheric window, quarter-phase class, structural gap profile). No uniqueness or mass theorem is proved here; downstream verification lemmas are expected to quantify over the pool or pin the canonical choice.

why it matters in Recognition Science

Without a fixed baseline choice set, neutrino-sector verification cannot state which deep-ladder triples are under test. The module sits under the Verification domain and imports NeutrinoSector (T14), so it supplies the discrete input language for any later check that the deep-ladder hypothesis matches atmospheric or hierarchical mass patterns.

Used-by edges are empty in the current graph, so it is presently a leaf definition layer rather than a proved stepping-stone. Its value is bookkeeping integrity: canonical candidate versus pool, quarter-phase class, and structural gap profile make baseline swaps explicit instead of silent parameter changes. Framework landmarks touched only indirectly are the phi-ladder mass formula and the deep-rung placement below $R_e = 2$; T0–T8 forcing is upstream of NeutrinoSector, not of this choice set.

scope and limits

Does not prove neutrino masses or fix absolute rung integers.
Does not derive the deep-ladder hypothesis; that lives in NeutrinoSector.
Does not assert uniqueness of the canonical candidate among all reals.
Does not encode oscillation angles, CP phase, or PMNS matrix entries.
Does not close experimental fits; only defines the discrete choice set.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Physics.NeutrinoSector module_import

declarations in this module (43)

structure BaselineCandidate L25
def r2_num L30
def r3_num L33
def quarterRung L36
def r1 L38
def r2 L39
def r3 L40
def canonicalCandidate L43
def candidatePool L46
def deepAtmosphericWindow L50
def quarterPhaseClass L54
def structuralGapProfile L58
def admissible L62
def validCandidates L65
def deepestEdgeOnlyAtmospheric L70
theorem candidate_pool_count L73
theorem structural_gap_profile_holds L76
theorem deepest_edge_atmospheric_num_eq L82
theorem deep_window_forced_from_edge_confinement L88
theorem quarter_phase_forced_from_eight_tick_offset L97
theorem filter_pair_forced_from_edge_confinement L106
theorem deepest_edge_only_forces_atmospheric_num L113
theorem deep_window_phase_forces_r3_num L122
theorem deep_window_phase_forces_r3_value L133
theorem deep_window_phase_forces_r1_num L141
theorem deep_window_phase_forces_r1_value L150
theorem deep_window_phase_forces_res_nu3 L158
theorem deep_window_phase_forces_res_nu1 L167
theorem edge_confinement_forces_canonical_baseline L177
theorem absolute_baseline_num_forced_from_deep_ladder L187
theorem absolute_baseline_num_forced_eq_neg239 L195
theorem deep_ladder_constraint_iff_canonical_candidate L205
def deepLadderForcedCandidate L219
theorem deep_ladder_forced_candidate_eq_canonical L223
theorem deep_ladder_geometry_forces_canonical_baseline L229
theorem valid_candidate_count L236
theorem valid_candidates_singleton L239
theorem canonical_is_valid L243
theorem unique_valid_candidate L248
theorem canonical_r1_matches_res_nu1 L254
theorem canonical_r3_matches_res_nu3 L259
theorem baseline_choice_set_collapsed L268
theorem admissible_baselines_match_res_nu1 L272