pmns_weight
The definition supplies the PMNS mixing weight for rung difference dτ as exp(-dτ * J_bit). Neutrino mixing calculations cite this form to obtain probabilities via the Born rule over ladder steps. The body is a direct transcription of the exponential decay law from the recognition framework.
claimThe PMNS mixing weight for integer rung difference $dτ$ is $W(dτ) = e^{-dτ · J_{bit}}$, which equals $φ^{-dτ}$ under the framework identification of $J_{bit}$.
background
In the Recognition Science framework the PMNS matrix elements arise from geometric overlaps of 8-tick windows on the phi-ladder. The module derives mixing from cubic ledger structure and edge-dual coupling, with unitarity forced by 8-tick closure. J_bit is the recognition cost per bit step, drawn from the J-function in the forcing chain (T5).
proof idea
The definition is a direct one-line assignment of the exponential form. It encodes the Born-rule probability weight exp(-Δτ J_bit) for transitions between neutrino rungs.
why it matters in Recognition Science
This definition supplies the weight tensor used by PMNSUnitarity and pmns_prob to construct the mixing matrix. It fills the Phase 7.2 derivation of CKM and PMNS elements from topological ratios and 8-tick closure. The parent result pmns_weight_eq_phi_pow converts the expression to explicit phi powers, linking to the self-similar fixed point T6.
scope and limits
- Does not compute numerical values for specific mixing angles.
- Does not prove unitarity of the resulting matrix.
- Does not derive the rung assignments for the three neutrino generations.
- Does not address radiative corrections beyond the base weight.
Lean usage
pmns_prob dτ (pmns_weight 0 + pmns_weight 1 + pmns_weight 2)formal statement (Lean)
93noncomputable def pmns_weight (dτ : ℤ) : ℝ :=
proof body
Definition body.
94 Real.exp (- (dτ : ℝ) * J_bit)
95