correction_D_quad1
plain-language theorem explainer
This definition supplies the quadratic candidate D(D-1)/4 as an alternative dimension-dependent correction for the tau generation step coefficient. Researchers examining lepton mass hierarchies and alternative forms for the alpha correction would cite it when checking numerical agreement at three dimensions. The entry is a direct algebraic definition with no lemmas or reductions.
Claim. The quadratic correction maps each natural number $d$ to $d(d-1)/4$.
background
In the tau step coefficient exclusivity module the generation formula is written step from mu to tau equals F minus (W plus D/2) times alpha. Several alternative corrections are examined to establish uniqueness once axis additivity and absence of constant offset are imposed. The quadratic D(D-1)/4 belongs to the class of numerically coincident but algebraically distinct candidates that equal 1.5 when D equals 3 yet differ from the linear term in other dimensions.
proof idea
The entry is a direct definition of the quadratic expression in the reals.
why it matters
The definition feeds the theorem that evaluates the quadratic at dimension three and the theorem that demonstrates failure of axis additivity via the witness 1 plus 1. It therefore participates in ruling out non-additive alternatives for the tau coefficient, consistent with the requirement that corrections remain additive across independent axes in the three-dimensional setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.