IndisputableMonolith.Physics.PMNS.Types

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.RSBridge.Anchor
   4import IndisputableMonolith.Support.MatrixProperties
   5
   6namespace IndisputableMonolith.Physics.PMNS
   7
   8open Constants
   9
  10/-- The PMNS mixing weights follow the Born rule over the ladder steps.
  11    Weight W_ij = exp(-Δτ_ij * J_bit) = φ^-Δτ_ij. -/
  12noncomputable def pmns_weight (dτ : ℤ) : ℝ :=
  13  Real.exp (- (dτ : ℝ) * J_bit)
  14
  15/-- **DEFINITION: PMNS Unitarity Forcing**
  16    A matrix `U` satisfies `PMNSUnitarity U` if it is unitary and its Born-rule
  17    probabilities `‖U i j‖^2` match the framework’s predicted weight tensor.
  18
  19    Note: existence of such a `U` is currently treated as a quarantined conjecture
  20    (`IndisputableMonolith/Physics/PMNS/Construction.lean`). The certified particle
  21    claims do **not** depend on that existence statement. -/
  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
  29