atmospheric_correction_geometric
plain-language theorem explainer
The theorem equates the atmospheric radiative correction derived geometrically from cube topology to the PMNS correction definition. Physicists deriving mixing matrices from ledger structures cite it to confirm cross-module consistency in the geometric approach. The proof is a one-line wrapper applying symmetry to the prior atmospheric_matches theorem.
Claim. The atmospheric radiative correction factor, defined geometrically as $6$ times the fine-structure constant, equals the atmospheric correction in the PMNS framework.
background
Module Phase 7.2 derives CKM and PMNS mixing elements from cubic ledger structure via edge-dual coupling and 8-tick windows. The geometric atmospheric_radiative_correction is defined as $6$ times alpha, representing the face-mediated radiative correction from maximal parity mix. The PMNSCorrections version defines atmospheric_correction as the product of an atmospheric_coefficient and alpha. Upstream, the atmospheric_matches theorem verifies equality between the MixingGeometry and PMNSCorrections versions by direct unfolding and reflexivity.
proof idea
One-line wrapper that applies the symmetry of the atmospheric_matches theorem from PMNSCorrections.
why it matters
The equality anchors the geometric derivation of the atmospheric angle to the PMNS corrections module, confirming that cube topology forces the factor of 6. It supports the broader claim that 8-tick closure enforces unitarity of the mixing matrix. The result fills a consistency step in the topological ratios for mixing angles and touches the open question of full numerical bounds on phi powers for reactor-angle matching.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.