加权数据选择：上半区与五维精确法则

在最小范数学习器的有限加权最小二乘设定下，该研究证明了加权数据选择在 $\lceil3d/2\rceil\leq n\leq2d-1$ 区间内的精确风险法则为 $\Gamma_d(n)=3-n/d$。该数据集层面的完整上界与紧度构造已在 Lean 4 中完成形式化验证。此外，针对较小预算 $(d,n)=(5,6)$，研究进一步给出了精确法则 $\Gamma_5(6)=11/5$。