Verification Neutrino Baseline Choice Set

Neutrino baseline choice set

The neutrino baseline choice set is a finite list of candidate values for the lightest neutrino's mass rung, defined within the Recognition Science framework. The framework models neutrino masses as positions on a discrete ladder of quarter-rungs, where each candidate is encoded by an integer numerator r1_num. The module under discussion enumerates a pool of 121 such candidates, spanning a range of possible numerators, and then applies three constraints to filter this pool down to the admissible set.

The three constraints are a structural gap profile, a deep-atmospheric window, and a quarter-phase class. The structural gap profile fixes the spacing between the first three rungs: the second rung sits 8 quarter-rungs above the first, and the third sits 14 above the second, matching the pattern +2 and +7/2 in integer form. The deep-atmospheric window requires the third rung's numerator to lie strictly between -220 and -216. The quarter-phase class requires that (r3_num + 1) be divisible by 4, a condition tied to an eight-tick offset in the framework's cycle.

Applying these constraints collapses the 121-candidate pool to a singleton. The machine-checked library proves that the admissible set contains exactly one candidate: the canonical candidate with r1_num = -239, corresponding to r1 = -239/4 and r3 = -217/4. This result is established by a chain of theorems: the deep atmospheric window and quarter-phase class together force r3_num to -217, which then forces r1_num to -239 via the structural gap. The final theorem, baseline_choice_set_collapsed, states that the valid candidates list is exactly the singleton list containing this canonical candidate.

In plain language, the module demonstrates that within the framework's assumptions, the neutrino baseline is not a free parameter but a uniquely determined value. The search is finite and exhaustive: the pool of 121 candidates is explicitly enumerated, and the filter is a computable predicate. The proof that only one candidate survives is a direct computation, verified by the machine-checked library, not a heuristic or an approximation.

The practical consequence is that the framework's neutrino sector has no adjustable baseline freedom at this level of description. This is a structural result about the framework's internal consistency, not a measurement of a physical neutrino mass. The value -239/4 is a prediction of the framework, to be compared against experimental data, not a derived constant from first principles.

theorem valid_candidates_singleton :
    validCandidates = [canonicalCandidate] := by
  native_decide

/-- Enumerated-choice closure summary for O5 under the current filter set. -/
theorem baseline_choice_set_collapsed :
    validCandidates = [canonicalCandidate] := valid_candidates_singleton

theorem candidate_pool_count : candidatePool.length = 121 := by
  native_decide

/-- The deep-atmospheric window plus quarter-phase class force `r3_num = -217`. -/
theorem deep_window_phase_forces_r3_num (c : BaselineCandidate)
    (hwin : deepAtmosphericWindow c = true)
    (hphase : quarterPhaseClass c = true) :
    r3_num c = -217 := by
  have hwin' : (-220 : ℤ) < r3_num c ∧ r3_num c < (-216 : ℤ) := by
    exact decide_eq_true_eq.mp (by simpa [deepAtmosphericWindow] using hwin)
  have hphase' : ((r3_num c + 1) % 4) = (0 : ℤ) := by
    exact decide_eq_true_eq.mp (by simpa [quarterPhaseClass] using hphase)
  exact deepest_edge_only_forces_atmospheric_num (r3_num c) ⟨hwin', hphase'⟩

/-- With fixed spacing (`r3_num = r1_num + 22`), the same filters force `r1_num = -239`. -/
theorem deep_window_phase_forces_r1_num (c : BaselineCandidate)
    (hwin : deepAtmosphericWindow c = true)
    (hphase : quarterPhaseClass c = true) :
    c.r1_num = -239 := by
  have hr3 : r3_num c = -217 := deep_window_phase_forces_r3_num c hwin hphase
  have hr3' : c.r1_num + 22 = (-217 : ℤ) := by simpa [r3_num] using hr3
  omega

What this page does not claim

This module does not measure a physical neutrino mass. The value -239/4 is not derived from first principles; it is a prediction to be tested. The uniqueness result does not extend beyond the stated constraints without further proof.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/NeutrinoBaselineChoiceSet.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: