solar_matches
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the base phi^{-2} scaling for solar mixing.
- Does not compute numerical values of the mixing angles.
- Does not address atmospheric or reactor sectors.
- Does not include higher-order radiative effects.
formal statement (Lean)
151theorem solar_matches :
152 solar_correction = MixingGeometry.solar_radiative_correction := by
proof body
Term-mode proof.
153 unfold solar_correction MixingGeometry.solar_radiative_correction
154 unfold solar_coefficient
155 rfl
156