solar_correction
plain-language theorem explainer
Solar radiative correction is defined to be ten times the fine-structure constant. Neutrino mixing derivations cite this when applying the solar weight correction to sin²θ₁₂. The definition multiplies the edge-derived coefficient by alpha in one step.
Claim. The solar radiative correction equals $10α$, where $α$ is the fine-structure constant.
background
The PMNS Radiative Correction Derivation module extracts integer coefficients from 3-cube topology for mixing predictions. Solar mixing uses edge-face counting on the 3-cube, where twelve edges minus the two active modes in the 1-2 sector produce ten passive contributions. Upstream solar_coefficient is defined as cube_edges_count 3 minus 2, with the doc-comment stating: 'The solar correction coefficient is edges minus the active pair.' Alpha is the reciprocal of the inverse fine-structure constant.
proof idea
One-line definition that multiplies the solar coefficient by alpha after casting to reals. It applies the upstream solar_coefficient and alpha definitions directly.
why it matters
This definition supplies the 10α term in the solar mixing prediction sin²θ₁₂ = φ⁻² − 10α. It feeds the geometric certificate solar_correction_geometric and the equality solar_correction_eq. The factor traces to cube topology in three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.