atmospheric_correction
plain-language theorem explainer
Atmospheric radiative correction equals six times the fine-structure constant. Neutrino physicists cite it when writing the atmospheric PMNS prediction sin²θ₂₃ = ½ + 6α. The definition is obtained in one step by casting the 3-cube face count to reals and multiplying by alpha.
Claim. The atmospheric radiative correction is $6α$, where $α$ is the fine-structure constant.
background
The PMNS Radiative Correction Derivation module extracts integer coefficients from 3-cube topology for the three mixing sectors. Atmospheric mixing receives the face count because each of the six faces of the cubic ledger contributes one unit of vacuum polarization to the μ-τ sector. Upstream, alpha is the fine-structure constant defined by alpha := 1 / alphaInv. The sibling atmospheric_coefficient is defined as cube_faces 3 and carries the explicit interpretation that each face supplies one unit of vacuum polarization.
proof idea
One-line definition that casts atmospheric_coefficient to ℝ and multiplies by alpha.
why it matters
This definition supplies the coefficient 6 that appears in the atmospheric weight sin²θ₂₃ = ½ + 6α. It is invoked by the downstream theorems atmospheric_correction_eq (which unfolds to 6 * alpha) and atmospheric_matches (which equates it to the MixingGeometry version). The construction realizes the cube-topology step of the eight-tick octave closure for D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.