Physics Pmnsscore Card

The PMNS scorecard

The PMNS scorecard is a module in the Recognition Science framework's machine-checked library of formal theorems. It records how well the framework's predictions for neutrino mixing match the measured values from particle physics. Neutrino mixing describes how the three known neutrino types blend into each other as they travel; the PMNS matrix is the standard mathematical object that encodes this blending.

The scorecard covers four quantities. Three are the squared mixing angles sin²θ₁₂, sin²θ₁₃, and sin²θ₂₃, which measure how strongly the neutrino types mix. The fourth is the Jarlskog invariant, a number that quantifies how much CP violation (the asymmetry between matter and antimatter behavior) the mixing allows. The module also checks that the predicted CP-violating phase δ_CP falls in the expected quadrant, between 180° and 360°.

For each quantity, the module states a proved inequality: the absolute difference between the framework's prediction and the measured center value is less than a stated bound. For example, the theorem for sin²θ₁₂ says |sin2_theta12_pred - 0.307| < 0.01. The measured values come from PDG and typical NuFIT center values: sin²θ₁₂ ≈ 0.307, sin²θ₁₃ ≈ 0.0220, sin²θ₂₃ ≈ 0.545–0.546, and δ_CP ≈ 197°. The Jarlskog invariant is compared against 3.08 × 10⁻⁵ with a tolerance of 0.6 × 10⁻⁵.

All these inequalities are collected into a single structure called PMNSScoreCardCert, and a theorem proves that this certificate is nonempty: every stated bound holds simultaneously. The Lean code contains zero sorry and zero new axioms, meaning the proofs are complete within the framework's formal system. The status is PARTIAL_THEOREM: the intervals around the centers are proved, but the scheme dependence of the parameters is a named display residual, meaning the exact conventions for defining the angles can shift the comparison slightly.

The scorecard's purpose is honest bookkeeping. It does not claim the framework derives the PMNS matrix from first principles; it claims that the framework's predictions land within stated tolerances of measured values, and that this agreement is machine-checked. A falsifier is named: if a NuFIT or PDG update moves any sin²θ center outside the stated error certificates with no compensating change in the framework's inputs, the packaged matches are falsified.

theorem row_pmns_theta12 :
    |sin2_theta12_pred - 0.307| < 0.01 := pmns_theta12_match

theorem row_pmns_theta13 :
    |sin2_theta13_pred - 0.022| < 0.002 := pmns_theta13_match

theorem row_jarlskog :
    |jarlskog_pred - 3.08e-5| < 0.6e-5 := jarlskog_match

theorem row_deltaCP_pmns_in_open_band :
    Real.pi < deltaCP_pmns_torsion_correction ∧
      deltaCP_pmns_torsion_correction < 2 * Real.pi := deltaCP_pmns_range

theorem pmnsScoreCardCert_holds : Nonempty PMNSScoreCardCert :=
  ⟨{ theta12 := row_pmns_theta12
     theta13 := row_pmns_theta13
     theta23 := row_pmns_theta23
     jarlskog := row_jarlskog
     j_pos := row_jarlskog_pos
     deltaCP_band := row_deltaCP_pmns_in_open_band }⟩

What this page does not claim

The module does not derive the PMNS matrix from first principles; it only proves that predictions land within stated tolerances. The module does not prove the exact measured center values; it proves intervals around those centers. The scheme dependence of the parameters is not resolved by this module.

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/PMNSScoreCard.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: