MajoranaPhases
plain-language theorem explainer
MajoranaPhases is a structure that records the two real parameters α₁ and α₂ for Majorana neutrinos. Neutrino physicists examining neutrinoless double beta decay would reference it when extending the PMNS matrix under Recognition Science. The definition is introduced directly as a record type with no computation or lemmas required.
Claim. The Majorana phases are two real numbers α₁, α₂ ∈ ℝ that appear when neutrinos are Majorana fermions. These phases leave oscillation probabilities unchanged yet enter the amplitude for neutrinoless double beta decay. Recognition Science supplies them through eight-tick phase constraints.
background
The PMNS matrix module derives neutrino flavor mixing from φ-quantized angles in Recognition Science. Large mixing angles appear: θ₁₂ ≈ 34°, θ₂₃ ≈ 45° (maximal), θ₁₃ ≈ 8.6°. The eight-tick phase supplies discrete values kπ/4 for k = 0..7, while tick denotes the fundamental time quantum τ₀ = 1. Upstream results include the phase definition from EightTick and the unimodular phase from the RiemannHypothesis wedge.
proof idea
The declaration is a direct structure definition that introduces the two real fields α₁ and α₂. No lemmas or tactics are invoked; the structure simply packages the phases for later use in RS predictions.
why it matters
This structure supplies the Majorana phases that complete the RS neutrino mixing summary, alongside the listed predictions for θ₂₃, θ₁₂, θ₁₃, δ_CP and normal ordering. It supports the target derivation of the PMNS matrix from φ-angles and the associated paper proposition on golden-ratio geometry. The phases connect to the eight-tick octave and the phase functions imported from EightTick and Wedge. No downstream uses are recorded, leaving explicit numerical prediction of α₁ and α₂ as an open step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.