D_half_at_3
plain-language theorem explainer
The declaration shows that the half-dimension correction evaluates exactly to 1.5 at spatial dimension three. Researchers deriving the tau generation step coefficient in Recognition Science cite it to anchor the numerical value of the D/2 term. The proof reduces directly to the definition via unfolding followed by numerical normalization.
Claim. For the half-dimension correction defined by $correction_D_half(d) = d/2$, the value at $d=3$ equals $3/2$.
background
The Tau Step Exclusivity module examines candidate correction terms for the coefficient in the tau generation step formula step_μ→τ = F - (W + D/2) · α. correction_D_half is introduced as the first candidate, defined by d/2, and is contrasted with algebraically equivalent forms such as F/4 and numerically coincident but distinct forms such as E/8, D(D-1)/4, and D²/6. The local setting requires that admissible corrections satisfy axis additivity (f(0)=0 and f(a+b)=f(a)+f(b)) together with no constant offset, which distinguishes the candidates once D is fixed at three.
proof idea
The proof is a one-line wrapper that unfolds the definition of correction_D_half and applies norm_num to evaluate the arithmetic at d=3.
why it matters
This result forms one verification step in the module's demonstration that all listed candidates evaluate to 1.5 when D=3, thereby supporting the selection of the D/2 form for the tau step coefficient. It aligns with the framework's T8 forcing of three spatial dimensions and the requirement that the correction remain additive along independent axes. No downstream theorems are recorded, leaving the full exclusivity argument to be completed by the remaining candidate evaluations in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.