pmns_weight

formal source

  90
  91/-- The PMNS mixing weights follow the Born rule over the ladder steps.
  92    Weight W_ij = exp(-Δτ_ij * J_bit) = φ^-Δτ_ij. -/
  93noncomputable def pmns_weight (dτ : ℤ) : ℝ :=
  94  Real.exp (- (dτ : ℝ) * J_bit)
  95
  96theorem pmns_weight_eq_phi_pow (dτ : ℤ) :
  97    pmns_weight dτ = phi ^ (-dτ : ℤ) := by
  98  -- Algebraic identity: exp(-dτ * ln(φ)) = φ^(-dτ)
  99  unfold pmns_weight
 100  -- simp turns RHS into inverse form via `zpow_neg`
 101  simp [J_bit]
 102  have hphi_pos : 0 < phi := phi_pos
 103  -- exp(-x) = (exp x)⁻¹
 104  rw [Real.exp_neg]
 105  have hexp : Real.exp (↑dτ * Real.log phi) = phi ^ (dτ : ℝ) := by
 106    calc
 107      Real.exp (↑dτ * Real.log phi)
 108          = Real.exp (Real.log phi * (dτ : ℝ)) := by simpa [mul_comm]
 109      _ = phi ^ (dτ : ℝ) := by
 110            simpa using (Real.rpow_def_of_pos hphi_pos (dτ : ℝ)).symm
 111  rw [hexp]
 112  have hz : phi ^ (dτ : ℝ) = phi ^ (dτ : ℤ) := by
 113    simpa using (Real.rpow_intCast phi dτ)
 114  simpa [hz]
 115
 116/-- **THEOREM: PMNS Probabilities from Born Rule**
 117    The mixing probability P_ij is the normalized path weight for a transition
 118    between rungs. -/
 119noncomputable def pmns_prob (dτ : ℤ) (total_weight : ℝ) : ℝ :=
 120  pmns_weight dτ / total_weight
 121
 122/-- **CONJECTURE: PMNS angles from Rung Ratios**
 123    The neutrino mixing angles are forced by the rung differences.