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

atmospheric_radiative_correction

show as:
view Lean formalization →

The atmospheric radiative correction factor equals six times the fine-structure constant. Neutrino mixing derivations cite it to adjust the atmospheric angle prediction from cube-face parity. The definition is introduced as a direct scaling by the six faces of the cubic voxel topology.

claimThe atmospheric radiative correction factor is given by $6α$, where $α$ is the fine-structure constant.

background

This definition sits inside the module on geometric foundations for mixing matrices, which formalizes cubic voxel topology constraints that force CKM and PMNS parameters. The fine-structure constant $α$ is imported from Constants.Alpha as the reciprocal of its derived inverse. Upstream results include the abstract Constants bundle from the Law of Existence, which supplies the non-negative Knet and related scalars, together with the PrimitiveDistinction theorem that reduces seven axioms to four structural conditions plus three definitional facts.

proof idea

The definition is a direct one-line assignment of the value 6 * Constants.alpha. No lemmas or tactics are applied beyond the constant import.

why it matters in Recognition Science

This supplies the face-mediated correction term used in the theorem atmospheric_angle_forced, which states atmospheric_weight + atmospheric_radiative_correction = 1/2 + 6 * Constants.alpha. It feeds directly into pmns_theta23_born_forced and pmns_theta23_match in MixingDerivation, closing the geometric account of the atmospheric angle from maximal parity mix and the eight-tick octave. The placement aligns with the Recognition Science forcing chain at T7 and T8, where D = 3 dimensions and the cubic topology determine the radiative leakage.

scope and limits

formal statement (Lean)

  61noncomputable def atmospheric_radiative_correction : ℝ := 6 * Constants.alpha

proof body

Definition body.

  62
  63/-- **THEOREM: Atmospheric Angle Forced**
  64    The atmospheric mixing angle is derived from the maximal parity mix
  65    with a face-mediated radiative correction. -/

used by (7)

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

depends on (9)

Lean names referenced from this declaration's body.