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

solar_weight

show as:
view Lean formalization →

solar_weight supplies the leading geometric term phi to the power of negative two for the solar neutrino mixing angle in the Recognition Science mixing geometry. Neutrino phenomenologists deriving PMNS parameters from rung ratios would cite this definition when constructing sin squared theta twelve predictions. It is introduced as a direct power assignment with no further reduction.

claimThe solar mixing weight is given by $w_2 = phi^{-2}$.

background

The module formalizes cubic voxel topology constraints that force the CKM and PMNS mixing parameters from the simplicial ledger. Phi is the self-similar fixed point forced by the Recognition Composition Law in the upstream foundation. Upstream results supply the fine-structure constant alpha as 1 over alphaInv, the passive edge count E_passive equal to 11 in three dimensions, and the phi-ladder finite-N correction factor 1 over (phi times N). The 'as' structure identifies discrete Laplacian actions with continuum limits via weighted edge sums.

proof idea

The definition is a one-line assignment of the real number obtained by raising phi to the integer power negative two.

why it matters in Recognition Science

This definition provides the base weight for sin2_theta12_pred in the PMNS derivation module, which is then corrected by solar_radiative_correction to match the observed solar angle. It fills the T6 phi fixed-point step into the mixing geometry and feeds the downstream solar_angle_forced theorem that equates the corrected expression to phi^{-2} minus ten alpha. The parent conjecture states that neutrino mixing angles are forced by rung differences on the phi-ladder.

scope and limits

formal statement (Lean)

  42noncomputable def solar_weight : ℝ := phi ^ (-2 : ℤ)

proof body

Definition body.

  43
  44/-- The solar radiative correction factor.
  45    Estimated as (E_passive - 1) * alpha. -/

used by (5)

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

depends on (5)

Lean names referenced from this declaration's body.