Pith. sign in
module module moderate

IndisputableMonolith.Physics.PMNSMixingAnglesFromRS

show as:
view Lean formalization →

Module supplies definitions for PMNS neutrino mixing parameters derived in the Recognition Science framework. It encodes maximal mixing at tan(π/4)=1 together with solar tangent bands and a certification type. Neutrino physicists would reference these objects for RS-native angle predictions. The module consists entirely of type and constant declarations built on the imported constants module.

claimMaximal mixing satisfies $\tan(\pi/4)=1$. PMNSParameter is the type of mixing parameters; solarTangent and solarTangent_band give the solar sector; PMNSCert certifies the full set.

background

The module imports IndisputableMonolith.Constants whose sole documented object is the RS time quantum satisfying $\tau_0=1$ tick. It introduces sibling definitions PMNSParameter, pmnsParameterCount, maximal_mixing, solarTangent, solarTangent_band, PMNSCert and pmnsCert. These objects locate the neutrino mixing sector inside the same RS-native unit system used for all other constants.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the maximal mixing relation tan(π/4)=1 that anchors PMNS derivations inside Recognition Science. It prepares the ground for PMNSCert and pmnsCert objects that certify the angles. No external downstream theorems are recorded yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)