D_quad2_at_3
plain-language theorem explainer
The quadratic correction term evaluates to exactly 3/2 when the spatial dimension is fixed at three. Researchers deriving lepton generation steps from first principles would cite this to confirm numerical coincidence with the linear D/2 term at D=3. The proof is a direct definition unfolding followed by arithmetic normalization.
Claim. The quadratic form of the dimension-dependent correction coefficient evaluates to three-halves at spatial dimension three: $c_2(3) = 3/2$.
background
The module proves exclusivity for the coefficient (W + D/2) in the tau generation step step_μ→τ = F - (W + D/2) · α. Alternatives such as quadratic forms in D are shown to match D/2 numerically at D=3 but differ algebraically elsewhere. Axis additivity requires any admissible correction f to satisfy f(0)=0 and f(a+b)=f(a)+f(b) for independent axes, with no constant offset permitted.
proof idea
The proof is a one-line wrapper that unfolds the definition of the quadratic correction and applies numerical normalization to obtain the equality at dimension three.
why it matters
This result exhibits the numerical coincidence of the quadratic alternative with the linear D/2 term at D=3, reinforcing the module's distinction between algebraically equivalent forms (such as F/4) and merely coincident ones. It supports the tau step exclusivity argument by preparing the ground for later algebraic separation via axis additivity. The declaration sits inside the Recognition Science forcing chain at the point where D=3 is fixed (T8) and the eight-tick octave structure is already in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.