module module moderate

`IndisputableMonolith.Physics.PMNSCorrections`

The PMNSCorrections module defines D-cube geometry quantities and PMNS correction coefficients such as atmospheric and solar terms. Researchers deriving neutrino mixing matrices from cubic topology would cite these. The module consists entirely of direct definitions and equation statements.

claimNumber of vertices in a $D$-cube: $V=2^D$. Defines atmospheric_coefficient and solar_coefficient for PMNS corrections.

background

The module sits inside the Recognition Science treatment of mixing matrices. It imports the RS time quantum $ au_0=1$ tick from Constants and the cubic voxel topology constraints from MixingGeometry, whose doc states that the module formalizes the cubic voxel topology constraints that force the CKM and PMNS mixing parameters. Sibling definitions supply vertex, edge, and face counts together with the named atmospheric and solar coefficients.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Supplies the geometric primitives and correction terms required by the downstream MixingDerivation module. That module formalizes the geometric derivation of the mixing matrix elements from the cubic ledger structure, replacing numerical matches with topological proofs, and opens with the statement that it covers Phase 7.2: CKM & PMNS Mixing Matrix Derivation with edge-dual coupling as the first listed element.

scope and limits

Does not derive full PMNS matrix elements.
Does not perform numerical evaluation of coefficients.
Does not address CKM corrections.
Does not incorporate dynamical time evolution.

used by (1)

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

IndisputableMonolith.Physics.MixingDerivation module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.Alpha module_import
IndisputableMonolith.Physics.MixingGeometry module_import

declarations in this module (24)

def cube_vertices L63
def cube_edges_count L66
def cube_faces L69
theorem cube3_vertices L77
theorem cube3_edges L78
theorem cube3_faces L79
def atmospheric_coefficient L89
theorem atmospheric_coefficient_eq_6 L91
def atmospheric_correction L94
theorem atmospheric_correction_eq L96
def solar_coefficient L107
theorem solar_coefficient_eq_10 L109
def solar_correction L112
theorem solar_correction_eq L114
def cabibbo_coefficient L126
theorem cabibbo_coefficient_eq_3_2 L128
theorem cabibbo_coefficient_from_geometry L130
def cabibbo_correction L136
theorem cabibbo_correction_eq L138
theorem atmospheric_matches L145
theorem solar_matches L151
theorem cabibbo_matches L157
structure CorrectionDerivationCert L169
theorem correction_derivation_verified L177