solar_correction_geometric
plain-language theorem explainer
The solar_correction_geometric theorem equates the geometric solar radiative correction (ten times alpha, forced by cube topology) to the PMNS solar correction. Neutrino mixing researchers deriving angles from the cubic ledger would cite it to confirm the radiative factor. The proof is a one-line term-mode reduction via simpa on the symmetric form of the solar_matches lemma.
Claim. The geometric solar radiative correction equals the PMNS solar correction: $10 alpha = solar_coefficient * alpha$, where the coefficient ten is fixed by the cubic ledger topology.
background
In the Phase 7.2 module, mixing matrix elements are derived geometrically from the cubic ledger structure and 8-tick window overlaps rather than fitted numerically. The upstream MixingGeometry.solar_radiative_correction is the definition $10 * Constants.alpha$, described as arising from phi^{-2} scaling plus a 10-alpha radiative correction. PMNSCorrections.solar_correction is the parallel definition $(solar_coefficient : R) * alpha$. The solar_matches theorem from PMNSCorrections unfolds both definitions to establish equality.
proof idea
This is a term-mode one-line wrapper. It invokes simpa on the symmetric form of the solar_matches theorem, which directly equates the two expressions by definition unfolding.
why it matters
The result anchors the solar angle correction inside the geometric mixing derivation, confirming that the cube-topology factor of ten matches the PMNS expression. It supports the module's claims on edge-dual coupling, topological ratios such as |V_cb| = 1/24, and 8-tick unitarity. The declaration closes the equivalence step between MixingGeometry and PMNSCorrections without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.