solar_correction_geometric
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the solar coefficient value from first principles.
- Does not compute or bound the full PMNS matrix elements.
- Does not incorporate loop corrections beyond the geometric 10-alpha term.
- Holds only inside Recognition Science units with c = 1.
formal statement (Lean)
223theorem solar_correction_geometric :
224 solar_radiative_correction = PMNSCorrections.solar_correction := by
proof body
Term-mode proof.
225 simpa using (PMNSCorrections.solar_matches).symm
226
227/-- **CERTIFICATE: Mixing Matrix Geometry**
228 Packages the proofs for CKM and PMNS mixing parameters. -/