correction_D_quad2
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not claim that D²/6 is the realized physical correction.
- Does not derive the correction coefficient from the Recognition functional equation.
- Does not address behavior in dimensions other than the additivity test at D=3.
Lean usage
theorem D_quad2_at_3 : correction_D_quad2 3 = 3/2 := by unfold correction_D_quad2; norm_numformal statement (Lean)
77noncomputable def correction_D_quad2 (d : ℕ) : ℝ := ((d : ℝ) ^ 2) / 6
proof body
Definition body.
78
79/-! ## Part 3: All Candidates Equal 1.5 in D=3 -/
80