pmns_weight
plain-language theorem explainer
The pmns_weight definition supplies the exponential weight W(dτ) = exp(−dτ ⋅ J_bit) for rung differences in the PMNS mixing matrix. Neutrino physicists deriving mixing angles from the Recognition ladder would cite this when normalizing Born-rule probabilities. It is a direct definition that transcribes the J-cost decay into real numbers, with the algebraic identity to φ^{-dτ} proved separately.
Claim. The weight for a neutrino transition spanning rung difference $dτ$ is $W(dτ) = e^{-dτ · J_{bit}}$, equivalently $φ^{-dτ}$.
background
In Recognition Science the J-cost function measures the recognition defect between states on the phi-ladder, with J_bit the per-bit cost extracted from the PhiForcingDerived structure. The PMNS weights are the Born-rule probabilities over discrete rung steps in the neutrino sector, where dτ is the integer rung difference supplied by the RSBridge rung map. Upstream results fix the RS-native units with τ₀ = 1 tick and c = 1, while the ledger factorization supplies the J calibration and the integration gap A enforces the φ-power balance at D = 3.
proof idea
This is a one-line definition that applies the real exponential to the product of the rung difference cast to ℝ and the J-bit cost constant.
why it matters
This definition is used by pmns_prob to normalize probabilities and by pmns_weight_eq_phi_pow to establish the phi-power form. It supplies the weight tensor required by the PMNSUnitarity structure. It implements the T5 J-uniqueness and T6 phi fixed point in the neutrino mixing sector, with the eight-tick octave constraining the rung spacing. The existence of a unitary matrix realizing these weights remains a quarantined conjecture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.