atmospheric_weight
atmospheric_weight assigns the real value 1/2 as the base atmospheric mixing weight, encoding maximal parity mix for neutrino oscillations. Neutrino physicists deriving PMNS angles from cubic voxel constraints cite it when computing sin²θ23. The definition is a direct constant assignment with no further reduction.
claimThe atmospheric mixing weight is defined as $1/2$, the contribution from maximal parity mixing in the atmospheric sector.
background
The module formalizes cubic voxel topology constraints that force CKM and PMNS mixing parameters. atmospheric_weight supplies the leading term for the atmospheric sector before any radiative adjustment. It sits alongside sibling definitions such as solar_weight and reactor_weight that partition the mixing contributions by sector.
proof idea
Direct constant definition assigning the real number 1/2.
why it matters in Recognition Science
It supplies the base term in sin2_theta23_pred and is invoked by pmns_theta23_match to obtain agreement with the observed value 0.546 within 1 percent. The parent theorem atmospheric_angle_forced adds the radiative correction 6*alpha to recover the full prediction. This step implements the rung-ratio forcing of mixing angles within the Recognition framework.
scope and limits
- Does not derive the numerical value from voxel topology.
- Does not incorporate the radiative correction term.
- Does not address solar or reactor mixing sectors.
- Does not supply error bounds or precision estimates.
Lean usage
example : atmospheric_weight = 1 / 2 := rflformal statement (Lean)
57noncomputable def atmospheric_weight : ℝ := 1 / 2
proof body
Definition body.
58
59/-- The atmospheric radiative correction factor.
60 Estimated as Faces * alpha. -/