pmns_prob
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.