atmospheric_matches
plain-language theorem explainer
The equality confirms that the derived atmospheric correction 6α matches the geometric radiative correction from the 3-cube face count. Neutrino physicists working on PMNS mixing angles cite it to verify the coefficient originates in cube topology. The proof is a direct unfolding of the three definitions followed by reflexivity.
Claim. The atmospheric radiative correction, defined as the product of the 3-cube face count and the fine-structure constant, equals the geometric factor $6α$ from MixingGeometry.
background
The PMNS Radiative Correction Derivation module extracts integer coefficients from the 3D voxel ledger. atmospheric_coefficient is the face count of a 3-cube (cube_faces 3), so atmospheric_correction expands to 6α. Upstream, MixingGeometry.atmospheric_radiative_correction is defined as 6 * Constants.alpha with the accompanying statement that the atmospheric mixing angle follows from maximal parity mix with face-mediated radiative correction.
proof idea
The term proof unfolds atmospheric_correction, MixingGeometry.atmospheric_radiative_correction, and atmospheric_coefficient, then closes by reflexivity.
why it matters
It supplies the equality used by the downstream theorem atmospheric_correction_geometric, which states that the coefficient 6 is forced by cube topology. The result completes the derivation of the atmospheric weight in sin²θ₂₃ = ½ + 6α, consistent with the eight-tick octave and D = 3 in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.