Physics Pmnscorrections

Radiative correction coefficients

The PMNS matrix describes how neutrinos change flavor as they travel, and its three mixing angles are measured quantities in particle physics. Within the Recognition Science framework, a module called PMNSCorrections derives the small radiative correction terms for two of those angles and for the Cabibbo angle in the quark sector. The corrections are expressed as simple multiples of the fine-structure constant α, and the module proves that the multiplying coefficients are exactly 6, 10, and 3/2.

The coefficients come from counting the parts of a three-dimensional cube. A cube has 6 faces, 12 edges, and 8 vertices. The atmospheric mixing angle gets a correction of 6α, matching the face count. The solar angle gets 10α, which is the 12 edges minus 2 for the active pair. The Cabibbo angle gets (3/2)α, which is 6 faces divided by 4 vertex-edge slots. The module proves each coefficient equals its geometric count, for instance atmospheric_coefficient_eq_6 shows the atmospheric coefficient is 6 by definition of cube faces.

These are not fitted parameters. The cube geometry is fixed because the framework derives three spatial dimensions from its forcing chain, and the counts follow from that fixed geometry. The module assembles a certificate structure, CorrectionDerivationCert, that packages all three derivations and the coefficient equalities into one machine-checked object. It also proves that these corrections match the radiative correction definitions in the separate MixingGeometry module, so the two sources agree.

The practical meaning is that three small numbers in the standard model's mixing sector are claimed to be geometric bookkeeping: counts of cube features times the fine-structure constant. The proofs are definitional, meaning they hold by unfolding definitions and simplifying, not by deep argument. The module does not derive the base mixing angles themselves, only the correction terms added to them.

theorem atmospheric_coefficient_eq_6 : atmospheric_coefficient = 6 := rfl

theorem solar_coefficient_eq_10 : solar_coefficient = 10 := rfl

theorem cabibbo_coefficient_from_geometry :
    cabibbo_coefficient = (cube_faces 3 : ℚ) / 4 := by
  unfold cabibbo_coefficient cube_faces
  norm_num

/-- Verify that our derived corrections match MixingGeometry definitions. -/
theorem atmospheric_matches :
    atmospheric_correction = MixingGeometry.atmospheric_radiative_correction := by
  unfold atmospheric_correction MixingGeometry.atmospheric_radiative_correction
  unfold atmospheric_coefficient
  rfl

theorem solar_matches :
    solar_correction = MixingGeometry.solar_radiative_correction := by
  unfold solar_correction MixingGeometry.solar_radiative_correction
  unfold solar_coefficient
  rfl

theorem cabibbo_matches :
    cabibbo_correction = MixingGeometry.cabibbo_radiative_correction := by
  unfold cabibbo_correction MixingGeometry.cabibbo_radiative_correction
  unfold cabibbo_coefficient
  norm_num

What this page does not claim

The module does not prove that the fine-structure constant α has the value measured in experiments. The base PMNS mixing angles are not derived in this module, only the radiative correction terms. The geometric counting is a definitional identification, not a derivation from a deeper physical principle.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/PMNSCorrections.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: