correction_D_quad2
plain-language theorem explainer
The definition supplies the quadratic candidate f(d) = d²/6 as an alternative dimension-dependent correction for the alpha term in the muon-to-tau step. Researchers deriving lepton mass ratios from Recognition Science principles cite it when testing which forms survive the axis-additivity filter among those that numerically match at D=3. It is introduced via a direct one-line definition that immediately enables equality checks and additivity counterexamples in sibling results.
Claim. The quadratic correction candidate is given by the function $f(d) = d^2 / 6$ for natural-number dimension $d$.
background
The Tau Step Coefficient Exclusivity module examines candidate corrections to the coefficient of alpha in the step formula step_μ→τ = F - (W + D/2) · α. It isolates the forced linear term by requiring admissible corrections to obey axis additivity: if the term sums independent per-axis contributions then f(0)=0 and f(a+b)=f(a)+f(b). This definition supplies the D²/6 candidate, which is algebraically distinct from D/2 yet evaluates to the same numerical value 1.5 when D=3.
proof idea
The declaration is a direct definition that computes the square of the input dimension divided by six.
why it matters
It supplies the input for the downstream theorems D_quad2_at_3 (which records the value 3/2 at D=3) and D_quad2_not_axisAdditive (which exhibits the counterexample 1+1 to additivity). These results eliminate the quadratic branch and thereby reinforce the uniqueness of the linear D/2 term required by the Recognition framework's axis-additivity principle and the forcing of D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.