correction_D_quad1
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not assert equality to the linear term D/2 outside dimension three.
- Does not embed physical constants or mass ladder formulas.
- Does not establish uniqueness of any correction form.
formal statement (Lean)
74noncomputable def correction_D_quad1 (d : ℕ) : ℝ := (d : ℝ) * ((d : ℝ) - 1) / 4
proof body
Definition body.
75
76/-- Candidate 5: D²/6 (another quadratic) -/