correction_F_quarter
plain-language theorem explainer
The declaration defines the F-quarter correction as hypercube faces divided by four. Researchers deriving the tau lepton step coefficient in Recognition Science cite it to establish that this form is algebraically identical to the D-half term. The definition is a direct one-line cast and division using the upstream cube_faces function.
Claim. The correction term $F/4$ for dimension $d$ is defined by $F/4 := (2d)/4$, which equals $d/2$, where $F=2d$ counts the faces of the $d$-hypercube.
background
The module examines why the tau generation step must use the coefficient $W + D/2$ rather than other dimension-dependent corrections. Upstream, cube_faces is defined as $2d$ in AlphaDerivation, PlanckScaleMatching, and PMNSCorrections, giving the number of faces of the D-hypercube. The local setting requires admissible corrections to obey axis additivity, $f(0)=0$ and $f(a+b)=f(a)+f(b)$, so that only terms linear in the independent axes survive.
proof idea
One-line definition that applies cube_faces to the input dimension, casts the result to reals, and divides by four.
why it matters
This definition feeds the downstream theorems F_quarter_eq_D_half and F_quarter_admissible, which transport admissibility from the D-half form and close the algebraic-equivalence case in the exclusivity argument. It directly supports the module's claim that $F/4$ is not a distinct alternative but the same as $D/2$, reinforcing uniqueness of the $W + D/2$ coefficient for $D=3$ in the Recognition Science lepton mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.