Weighted Data Selection: Sharp Upper-Half and Five-Dimensional Laws

Abstract:How much risk does a small reweighted training support retain? For finite weighted least squares with the minimum-norm learner, we prove the exact law $\Gamma_d(n)=3-n/d$ throughout $\lceil3d/2\rceil\leq n\leq2d-1$. The guarantee covers every observed feature rank and uses selections that preserve the full feature span. Balanced simplex anchors reduce dimension; positive-weight lifting and independent-line compression close the risk bound. Shifted coordinate pairs attain the matching lower bound. The complete dataset-level upper bound and sharpness construction are verified in Lean 4. At the smaller budget $(d,n)=(5,6)$, we also prove $\Gamma_5(6)=11/5$, matching the simplex-block prediction from $5=3+2$ over arbitrary interacting configurations. Circuit covers, comparison second moments, and circuit-plane probabilities give the sharp excess $6/5$, while polar-face geometry resolves shared rank-three circuits. The general simplex-block frontier connects these laws within the intermediate-budget selection problem.

Machine Learning (stat.ML); Machine Learning (cs.LG)

arXiv:2610.00101 [stat.ML]

(or arXiv:2610.00101v1 [stat.ML] for this version)

https://doi.org/10.48550/arXiv.2610.00101 Focus to learn more arXiv-issued DOI via DataCite (pending registration)

evidence/lean/axiom-audit.exit

evidence/lean/axiom-audit.log

evidence/lean/build-final.exit

evidence/lean/build-final.log

evidence/lean/fresh-full-theorem-check.exit

evidence/lean/fresh-full-theorem-check.log

evidence/lean/fresh-source-build.exit

evidence/lean/fresh-source-build.log

evidence/lean/full-theorem-check.exit

evidence/lean/full-theorem-check.log

evidence/lean/theorem_inventory.json

evidence/lean/verification_result.json

formalization/upper_half/Audit.lean

formalization/upper_half/FullTheoremCheck.lean

formalization/upper_half/README.md

formalization/upper_half/UpperHalf.lean

formalization/upper_half/UpperHalf/AnchorGeometry.lean

formalization/upper_half/UpperHalf/AnchorLift.lean

formalization/upper_half/UpperHalf/AnchorSystem.lean

formalization/upper_half/UpperHalf/AnchoredSpanning.lean

formalization/upper_half/UpperHalf/Budget.lean

formalization/upper_half/UpperHalf/CertificateCounts.lean

formalization/upper_half/UpperHalf/CertificateSupport.lean

formalization/upper_half/UpperHalf/Certified.lean

formalization/upper_half/UpperHalf/CheapSubset.lean

formalization/upper_half/UpperHalf/CoordinateAnchor.lean

formalization/upper_half/UpperHalf/CoordinateDataset.lean

formalization/upper_half/UpperHalf/ExactCertificate.lean

formalization/upper_half/UpperHalf/GlobalCertificate.lean

formalization/upper_half/UpperHalf/GramProjection.lean

formalization/upper_half/UpperHalf/GramSystem.lean

formalization/upper_half/UpperHalf/IndexedGeometry.lean

formalization/upper_half/UpperHalf/Induction.lean

formalization/upper_half/UpperHalf/IntrinsicFit.lean

formalization/upper_half/UpperHalf/IntrinsicReduction.lean

formalization/upper_half/UpperHalf/LineAlgebra.lean

formalization/upper_half/UpperHalf/LineCompression.lean

formalization/upper_half/UpperHalf/LineCoordinates.lean

formalization/upper_half/UpperHalf/LineSelection.lean

formalization/upper_half/UpperHalf/LowerBound.lean

formalization/upper_half/UpperHalf/MatrixLimit.lean

formalization/upper_half/UpperHalf/MaximalGeometry.lean

formalization/upper_half/UpperHalf/MaximalRegression.lean

formalization/upper_half/UpperHalf/MixedSelection.lean

formalization/upper_half/UpperHalf/NontrivialAnchor.lean

formalization/upper_half/UpperHalf/OrthogonalAlgebra.lean

formalization/upper_half/UpperHalf/PairDataset.lean

formalization/upper_half/UpperHalf/PositiveBasis.lean

formalization/upper_half/UpperHalf/PositiveSpan.lean

formalization/upper_half/UpperHalf/RankZero.lean

formalization/upper_half/UpperHalf/Regression.lean

formalization/upper_half/UpperHalf/RegressionAnchor.lean

formalization/upper_half/UpperHalf/ScalarBlock.lean

formalization/upper_half/UpperHalf/Sharpness.lean

formalization/upper_half/UpperHalf/ShiftedPairs.lean

formalization/upper_half/UpperHalf/SimplexAnchor.lean

formalization/upper_half/UpperHalf/StructuralAlternative.lean

formalization/upper_half/lake-manifest.json

formalization/upper_half/lakefile.lean

formalization/upper_half/setup.ps1

verification/exact_check_results.json

verification/requirements.txt

verification/verify_exact.py

(61 additional files not shown) You must enabled JavaScript to view entire file list.

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.