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