PMNSUnitarity
PMNSUnitarity defines the property that a 3x3 complex matrix U is unitary and its squared moduli match the Recognition Science weight tensor derived from rung differences on the neutrino phi-ladder. Neutrino phenomenologists checking consistency between observed mixing and the exponential Born-rule weights would cite this interface. The declaration is a structure that directly conjoins the IsUnitary predicate with the forall matches_weights condition using pmns_weight on rung differences.
claimA matrix $U$ in $M_3(ℂ)$ satisfies PMNSUnitarity if it is unitary ($U^†U = I$) and for all indices $i,j$ the squared modulus satisfies $|U_{ij}|^2 = pmns_weight(r_i - r_j)/3$, where $r_k$ denotes the rung value of the neutrino state indexed by $k$ (nu1 at rung 0, nu2 at rung 11, nu3 at rung 19) and $pmns_weight(dτ) = exp(-dτ · J_bit)$.
background
The module states that PMNS mixing weights follow the Born rule over ladder steps, with weight $W_{ij} = exp(-Δτ_{ij} · J_bit) = φ^{-Δτ_{ij}}$. The pmns_weight definition implements this as Real.exp(-(dτ : ℝ) * J_bit). Rung assignments for neutrinos come from the RSBridge.Anchor definition: nu1 maps to 0, nu2 to 11, nu3 to 19. These integers label steps on the phi-ladder used throughout the mass and mixing derivations.
proof idea
This is a structure definition with an empty proof body. It packages two fields: the unitary axiom Matrix.IsUnitary U and the predicate matches_weights that applies pmns_weight to each rung difference (rung_i - rung_j) and normalizes by 3.
why it matters in Recognition Science
PMNSUnitarity supplies the predicate used by the open conjecture pmns_unitarity_exists, which asserts existence of a unitary matrix whose entry magnitudes reproduce the weight tensor. The parent result is pmns_weight from MixingDerivation, which encodes the exponential form tied to the J-cost functional. This interface links abstract unitarity to the concrete phi-ladder predictions for neutrino mixing without entering the hard falsifiable claims of the mixing derivation.
scope and limits
- Does not assert existence of any matrix satisfying the conditions.
- Does not compute explicit numerical mixing angles or phases.
- Does not fix the numerical value of J_bit.
- Does not extend to quark-sector mixing or other particle families.
- Does not incorporate CP-violating phases beyond the unitarity requirement.
formal statement (Lean)
22structure PMNSUnitarity (U : Matrix (Fin 3) (Fin 3) ℂ) : Prop where
23 unitary : Matrix.IsUnitary U
24 matches_weights : ∀ i j, ‖U i j‖ ^ 2 =
25 pmns_weight (IndisputableMonolith.RSBridge.rung (match i with | 0 => .nu1 | 1 => .nu2 | 2 => .nu3) -
26 IndisputableMonolith.RSBridge.rung (match j with | 0 => .nu1 | 1 => .nu2 | 2 => .nu3)) / 3
27
28end IndisputableMonolith.Physics.PMNS