module module moderate

`IndisputableMonolith.Physics.PMNSCorrections`

The PMNSCorrections module defines D-cube vertex counts and atmospheric plus solar correction coefficients that enter PMNS mixing calculations in the Recognition Science framework. Neutrino physicists working on geometric derivations of mixing angles would cite these objects. The module contains only definitions and supporting equations with no theorems or proofs.

claimThe module introduces the vertex count $V=2^D$ for a D-cube together with edge and face counts, the atmospheric coefficient satisfying equation 6, and the solar coefficient satisfying equation 10.

background

The module sits inside the geometric foundation for mixing matrices supplied by the MixingGeometry import, which formalizes cubic voxel topology constraints that force the CKM and PMNS mixing parameters. It also imports the RS time quantum τ₀ = 1 tick from Constants and the fine-structure definitions from Constants.Alpha. The supplied DOC_COMMENT records the central geometric identity: number of vertices in a D-cube equals 2^D.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

These definitions are imported by the MixingDerivation module, whose doc-comment states it formalizes the geometric derivation of the mixing matrix elements from the cubic ledger structure, replacing numerical matches with topological proofs, and carries the Phase 7.2 label for CKM & PMNS mixing matrix derivation.

scope and limits

Does not contain theorems or proofs of any coefficient relations.
Does not derive numerical values for mixing angles.
Does not address CKM matrix elements.
Does not import or reference the full PMNS matrix construction.

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