IndisputableMonolith.Physics.PMNS.Types
This module defines the PMNS mixing weights via the Born rule on recognition ladder steps, setting W_ij equal to phi to the minus Delta tau_ij. Researchers deriving neutrino parameters from RS time quanta would cite it. The module supplies type definitions and predicates, importing constants and matrix properties to formalize the assignment.
claim$W_{ij} = φ^{-Δτ_{ij}}$ where the weights follow the Born rule over ladder steps between fermion species.
background
Recognition Science takes the time quantum τ₀ = 1 tick as fundamental. The RSBridge.Anchor module supplies the 12 fermions, the ZOf charge index Z_i = q̃² + q̃⁴ (+4 for quarks), the gap function F(Z) = ln(1 + Z/φ)/ln(φ), and massAtAnchor at the anchor scale μ⋆. MatrixProperties adds stable predicates for unitary and normal matrices across Mathlib versions. This module applies those elements to define PMNS weights under the Born rule.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
This module supplies the weight assignment that feeds the open conjecture in IndisputableMonolith.Physics.PMNS.Construction on the existence of a unitary PMNS matrix whose entry magnitudes match the framework weights. It is not used for the hard-falsifiable angle or mass-splitting claims in MixingDerivation.
scope and limits
- Does not derive numerical mixing angles or mass splittings.
- Does not prove unitarity or existence of any PMNS matrix.
- Does not reference the T0-T8 forcing chain or RCL.
- Does not supply mass formulas or alpha-band constraints.