IndisputableMonolith.Physics.PMNSMixingAnglesFromRS
The module supplies type definitions and basic functions for PMNS neutrino mixing angles expressed in Recognition Science units. Neutrino phenomenologists and RS model builders would cite it when extracting angle predictions from the phi-ladder. The module consists entirely of definitions and record types that rest on the imported Constants module.
claimPMNSParameter is the record type holding the three mixing angles; maximal_mixing satisfies $tan(π/4)=1$; solarTangent and solarTangent_band give the solar mixing parameter and its allowed interval.
background
The module imports Mathlib and IndisputableMonolith.Constants. The upstream Constants module supplies the RS time quantum τ₀ = 1 tick. Sibling declarations introduce PMNSParameter as the structure for the three neutrino mixing angles, pmnsParameterCount as the dimension of the parameter space, maximal_mixing as the angle obeying tan(π/4)=1, solarTangent together with its band, and the certification objects PMNSCert and pmnsCert.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies the concrete PMNS angle definitions required by downstream Recognition Science derivations of neutrino masses and mixing. It directly implements the maximal-mixing case tan(π/4)=1 that follows from the J-uniqueness and eight-tick octave of the forcing chain.
scope and limits
- Does not derive numerical values for the angles from first principles.
- Does not prove consistency with experimental data.
- Does not contain the full PMNS matrix construction.