pmns_weight_eq_phi_pow
plain-language theorem explainer
The declaration establishes that the PMNS weight for integer rung separation dτ equals the golden ratio raised to negative dτ. Researchers computing neutrino mixing probabilities from the phi-ladder in Recognition Science would cite this identity to normalize path weights. The proof reduces the claim via unfolding and real exponentiation rules to an algebraic identity.
Claim. For any integer rung difference $dτ$, the PMNS transition weight satisfies $w(dτ) = φ^{-dτ}$, where $w$ is the normalized path weight and $φ$ is the Recognition Science self-similar fixed point.
background
The module derives CKM and PMNS mixing matrices geometrically from the cubic ledger structure. Edge-dual coupling sets generation overlaps through 8-tick windows, with topological ratios fixing elements such as |V_cb| = 1/24. The weight function encodes normalized path weights for rung transitions on the phi-ladder, drawing on J-cost minima at the identity event and Born-rule probabilities as squared norms from the quantum ledger.
proof idea
The tactic proof unfolds the pmns_weight definition then applies simp with J_bit. It rewrites via Real.exp_neg, reduces the exponential via a calc block using Real.rpow_def_of_pos on positive phi, converts the real power to integer power with Real.rpow_intCast, and closes with simpa.
why it matters
This identity supplies the explicit weight scaling needed for PMNS probability derivations in the mixing geometry module. It anchors the eight-tick octave closure and phi fixed-point structure from the forcing chain, supporting unitarity of the mixing matrix in Phase 7.2. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.