The sharp constant in the degrees-of-freedom bound for binary isotonic regression: an exact certificate, and an erratum to a numerical check

Abstract

Rossellini, Barber, Ren and Soloff [RBRS] bound the number of distinct fitted values of isotonic regression on a binary sample of size n by an explicit quantity f(n) built from the Euler totient, and write f(n)=c n^(2/3)+δₙ with c=3/(4π²)^(1/3). A proposition of that paper asserts δₙ ≤ 0.63 n^(1/6) for all n ≤ 2 · 10²³, and reduces it by two concavity interpolations to the Farey-type inequality R_K:=B_K-c n_K^(2/3) ≤ 0.63 n_K^(1/6) for all K ≤ 10⁸, where n_K=1+Σ_(j ≤ K)jφ(j) and B_K=1+Σ_(j ≤ K)φ(j) are the sum of the denominators and the number of terms of the Farey series of order K; that inequality is verified there by a printed floating-point script. We determine the optimal constant. It is αᵃˢᵗ=5 · 10^(-1/6)-3√(10) (4π²)^(-1/3)=0.6203305642542976…, a transcendental number. We prove R_K ≤ αᵃˢᵗ n_K^(1/6) for every K ≤ 10⁶+1, with equality at K=3; hence δₙ ≤ αᵃˢᵗ n^(1/6) for every n ≤ n_(10⁶)=202 642 368 741 515 820, which is 17 of the 23 decades the source asserts, and no smaller constant works on any range containing n=10, where f(10)=5 and δ₁₀=αᵃˢᵗ · 10^(1/6) exactly. The finite verification is an exact integer certificate: the inequality is cubed to remove the cube root in c, sixth roots enter as checked rationals m/2²⁰, and π enters only through a twenty-digit rational bound, so no floating-point arithmetic occurs anywhere in it. We also record an erratum to the source's printed script, whose cumulative sums are accumulated in binary64 through an unintended integer-type promotion: at K=10⁶ the exact n_K is 202 642 368 741 515 820 against the script's 202 642 368 741 518 368, and near K=9.3 · 10⁷ the script's value of the quantity it maximises has the wrong sign. The proposition's conclusion is unaffected, the maximum sitting at K=3 in small exact integers; this corrects the certificate, not the theorem. Everything above is machine-checked in Lean 4 except three things, each flagged in the text: the transcendence, a one-line consequence of Lindemann's theorem proved by hand; the decimal digits of αᵃˢᵗ beyond the ten of the certified enclosure; and the measurements of the printed script over its full range, of which only the exact value at K=10⁶ is formal.

Open review

This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.

Archived files

1. Version 1 · current (opens in a new tab)

   Source snapshot 2026-09-07 03:53 UTC

   File fingerprint

   71b7b4299718d726a44dbe3fc376e2ba0f81f3a1787d359ab928931465523a8e