solar_matches
plain-language theorem explainer
The equality between the solar correction defined via cube edge counting and the geometric radiative correction holds by direct definition. Researchers deriving PMNS mixing angles from Recognition Science geometry would cite this to confirm the 10α term in the solar sector. The proof is a term-mode reduction that unfolds the relevant definitions and applies reflexivity.
Claim. The solar radiative correction factor equals the geometric version: $10α = 10α$, where the coefficient 10 is the number of passive edges in the 3-cube.
background
The PMNSCorrections module derives integer coefficients for PMNS mixing angles from 3-cube topology. The solar coefficient is defined as cube_edges_count 3 minus 2, so solar_correction is 10 times alpha. The upstream solar_radiative_correction in MixingGeometry is defined as 10 * Constants.alpha, with its doc noting the factor for the solar mixing angle from phi^{-2} scaling with a 10-alpha correction. The module setting states sin²θ₁₂ = φ^{-2} − 10α with the correction from edge-face counting.
proof idea
The proof unfolds solar_correction, MixingGeometry.solar_radiative_correction, and solar_coefficient, then applies rfl to confirm equality by direct computation.
why it matters
This theorem connects the PMNSCorrections definitions to MixingGeometry and feeds solar_correction_geometric in MixingDerivation, which packages the proofs for CKM and PMNS parameters. It confirms the coefficient 10 forced by 3-cube topology, consistent with D = 3 spatial dimensions in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.