pmns_prob
pmns_prob normalizes the exponential rung-transition weight to a probability for PMNS mixing. Neutrino physicists extracting sin²θ_ij from the phi-ladder would cite this step when converting weights to Born-rule probabilities. The definition is a direct division of pmns_weight by the supplied total_weight.
claimThe PMNS transition probability for rung difference $dτ$ is $P(dτ) = W(dτ) / total_weight$, where $W(dτ) = exp(-dτ · J_bit)$ is the un-normalized weight.
background
The declaration lives in the Phase 7.2 module that derives CKM and PMNS matrices from the cubic ledger structure and 8-tick window overlaps. Rung assigns integer levels to fermions (neutrinos at 0, 11, 19) via the Anchor and RSBridge definitions. pmns_weight implements the Born rule over ladder steps as exp(-Δτ · J_bit).
proof idea
One-line wrapper that applies pmns_weight dτ and divides the result by the supplied total_weight.
why it matters in Recognition Science
It supplies the normalization that feeds the angle predictions sin2_theta12_pred, sin2_theta23_pred and sin2_theta13_pred in the same module. The step converts geometric path weights into observable mixing probabilities inside the 8-tick octave and phi-ladder framework. The attached conjecture comment ties the definition to forcing PMNS angles from rung differences.
scope and limits
- Does not compute numerical values of the mixing angles.
- Does not prove unitarity of the PMNS matrix.
- Does not define how total_weight is obtained from the ladder.
- Does not incorporate radiative corrections.
formal statement (Lean)
119noncomputable def pmns_prob (dτ : ℤ) (total_weight : ℝ) : ℝ :=
proof body
Definition body.
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.
124 - θ₁₂: Solar angle, sin²θ₁₂ ≈ solar_weight - solar_radiative_correction.
125 - θ₂₃: Atmospheric angle, sin²θ₂₃ ≈ atmospheric_weight + atmospheric_radiative_correction.
126 - θ₁₃: Reactor angle, sin²θ₁₃ ≈ reactor_weight. -/