pith. machine review for the scientific record. sign in
def definition def or abbrev high

solar_coefficient

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 107def solar_coefficient : ℕ := cube_edges_count 3 - 2

proof body

Definition body.

 108

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.