D_quad1_at_3
plain-language theorem explainer
The declaration shows that the quadratic candidate correction D(D-1)/4 evaluates to exactly 3/2 at spatial dimension three. Researchers deriving the tau lepton step coefficient in Recognition Science cite this to confirm numerical coincidence among alternative forms before applying additivity to rule them out. The proof is a direct unfolding of the definition followed by arithmetic normalization.
Claim. The quadratic candidate correction term satisfies $D(D-1)/4 = 3/2$ at $D=3$.
background
The module examines the tau generation step formula step_μ→τ = F - (W + D/2) · α and asks why the coefficient must be W + D/2 rather than alternatives such as W + D(D-1)/4. The definition correction_D_quad1 supplies one such alternative: the quadratic form D(D-1)/4. Module documentation states that several alternatives evaluate to 1.5 at D=3 yet differ algebraically, and are excluded once axis additivity (f(0)=0 and f(a+b)=f(a)+f(b)) plus absence of constant offset are imposed. The upstream definition is the sole dependency.
proof idea
The term proof unfolds the definition of the quadratic candidate and applies numerical normalization to obtain the equality at argument 3.
why it matters
This evaluation establishes that the quadratic alternative coincides with the target coefficient 3/2 at D=3, forming part of the case that only the linear D/2 form survives axis additivity in all dimensions. It supports the exclusivity argument for the tau step coefficient and connects to the framework's T8 forcing of D=3. The result is used to separate algebraically equivalent rewritings (such as F/4) from numerically coincident but distinct quadratics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.