fine_structure_leakage
plain-language theorem explainer
The definition sets the parity-split fine structure leakage equal to half the fine-structure constant alpha. Physicists deriving CKM matrix elements from cubic voxel topology cite it to obtain the geometric prediction for V_ub. It is realized as a direct one-line assignment of the imported alpha constant divided by two.
Claim. The fine-structure leakage is defined by $L = alpha / 2$, where $alpha$ is the fine-structure constant.
background
The module formalizes cubic voxel topology constraints that force CKM and PMNS mixing parameters. The fine-structure constant enters as the vacuum polarization mediator coupling non-adjacent generations. Upstream, Constants.Alpha.alpha supplies the symbolic value $1/alphaInv$ derived from phi-forcing, while SpectralEmergence.of establishes the three-generation structure from face-pair counts on the Q3 lattice and LedgerFactorization.of calibrates the J-cost on the positive reals.
proof idea
This is a one-line definition that directly divides the fine-structure constant alpha by two, inheriting its value from the Constants.Alpha module.
why it matters
It supplies the geometric prediction for V_ub in CKMGeometry.V_ub_pred and enters jarlskog_witness_pos to establish positivity of the Jarlskog invariant. The definition closes the link from T8 spatial dimensions and the alpha band to observable mixing parameters, as used in CKMElementScoreCardCert for matching within experimental error bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.