atmospheric_angle_forced
plain-language theorem explainer
The theorem forces the atmospheric neutrino mixing angle by showing that its geometric weight plus the face-mediated radiative correction sums exactly to one half plus six times the fine structure constant. Neutrino physicists deriving PMNS parameters from cubic voxel topology would cite this identity when closing the atmospheric sector. The proof is a one-line algebraic verification that unfolds the two weight definitions and applies the ring tactic.
Claim. $w_a + c_a = 1/2 + 6α$, where $w_a$ is the atmospheric mixing weight from maximal parity mix and $c_a$ is the face-mediated radiative correction, with $α$ the fine-structure constant.
background
The module formalizes cubic voxel topology constraints that force CKM and PMNS mixing parameters. Atmospheric weight is defined from the maximal parity mix; the radiative correction supplies the face-mediated adjustment. Upstream results supply the octave (period 8 ticks or ratio 2) and the definition of $α$ as the reciprocal of the derived fine-structure inverse, both used to anchor the constants in the mixing expressions.
proof idea
The proof unfolds atmospheric_weight and atmospheric_radiative_correction, then applies the ring tactic to reduce the left-hand side to the right-hand side.
why it matters
This identity closes the atmospheric sector of the mixing-angle derivation inside the Recognition Science framework, linking maximal parity mix to the fine-structure constant through the radiative term. It supports the geometric forcing of PMNS parameters under cubic voxel constraints and sits downstream of the octave and alpha definitions. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.