atmospheric_coefficient
plain-language theorem explainer
The atmospheric coefficient is defined as the number of faces on a three-dimensional cube. Neutrino physicists deriving PMNS mixing corrections cite this to fix the atmospheric term at 6α. It is a direct specialization of the cube_faces function to dimension 3.
Claim. The atmospheric coefficient equals the number of faces of the three-dimensional cube, $F(3) = 6$.
background
The PMNS Radiative Correction Derivation module extracts integer coefficients for neutrino mixing angle corrections from the topology of the three-dimensional cubic ledger. The cube_faces definition, appearing upstream in AlphaDerivation as 2D and in PlanckScaleMatching as the number of faces of the D-hypercube, is specialized here to D = 3. The module states that atmospheric mixing is governed by cube topology, with each of the six faces contributing one unit of vacuum polarization to the μ-τ sector.
proof idea
This is a one-line wrapper that applies cube_faces to the argument 3.
why it matters
This definition supplies the integer 6 that appears in the atmospheric correction term sin²θ₂₃ = ½ + 6α. It feeds atmospheric_coefficient_eq_6, atmospheric_correction, and CorrectionDerivationCert, which certifies that the coefficients 6, 10, and 3/2 are forced by the topology of the 3D cubic ledger. In the Recognition framework it realizes the D = 3 spatial dimension from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.