solar_coefficient
plain-language theorem explainer
The definition sets the solar radiative correction coefficient to the edge count of a three dimensional cube minus two. Researchers deriving PMNS neutrino mixing angle corrections cite it to obtain the factor of ten in the solar sector term. It is obtained by direct specialization of the general cube edge formula to dimension three.
Claim. The solar coefficient equals $E(3)-2$, where $E(D)=D·2^{D-1}$ is the number of edges in a $D$-dimensional cube.
background
The PMNS Radiative Correction Derivation module obtains the integer coefficients 6, 10, and 3/2 for mixing angle corrections from the topology of a three dimensional cube. The solar coefficient counts passive edge contributions after subtracting the two active modes in the electron neutrino sector. The upstream cube_edges_count result supplies the general expression for edges in a D cube as D times two to the power of D minus one.
proof idea
One-line definition that invokes the cube edge count function at dimension three and subtracts two.
why it matters
This definition supplies the integer ten required for the solar radiative correction term 10α in the prediction sin²θ₁₂ = φ^{-2} - 10α. It is used inside the CorrectionDerivationCert structure to certify that the coefficients 6, 10, and 3/2 are forced by three cube topology. The placement aligns with the forcing of three spatial dimensions and the eight tick octave closure in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.