The constant of doubly uniform regret in one-dimensional online linear regression is three

This is AI-generated research: the results, proofs and code were found and written by AI. Credit goes to all the humans whose work it builds on. We consider online linear regression in dimension one when the features are revealed one at a time, with no bound known in advance, and the regret is measured against every linear predictor, with no bound on its parameter. For outcomes bounded by B and a horizon T≥355713, both known to the learner, the minimax regret lies between B²(3log T-2loglog T-15.2) and B²(3log T+0.37): an explicit learner attains the upper bound, and an explicit randomized adversary, with features in $[0,1]$, forces the lower bound. A learner that knows neither B nor T has regret at most M²(3log T+4loglog(T+2)+12+2/√ T+4/T) on every play, with M the largest absolute outcome. Lean 4 proves these bounds. Chen, Qian, Rakhlin and Zhivotovskiy (COLT 2026) showed that this regret is of order log T, answering a question of Gaillard et al. (ALT 2019); we find its constant, $3$, which is $1$ with the features known in advance. The order log T is Theorem 5 and Proposition 6 of Chen, Qian, Rakhlin and Zhivotovskiy, Self-Normalized Martingales and Uniform Regret Bounds for Linear Regression (COLT 2026, PMLR 336; arXiv:2605.01628). The question is in Section 4.1 of Gaillard et al., Uniform regret bounds over Rᵈ for the sequential linear regression problem with the square loss (ALT 2019, PMLR 98; arXiv:1805.11386). Lean 4 with Mathlib proves the main theorem with its constants, the bounds of the explicit learner and of the explicit adversary with every numerical step and the drift certificate, the extensions to bounded features and randomized learners, and the bound of the learner that knows neither B nor T with its corollaries, with no hypothesis and only the standard axioms. Code, Lean proofs and certificates: github.com/mt0-svg/regret-kappa