An asserted inequality, proved and sharpened: the exact minimum of the threshold-rounding ratio of Elbassioni and Ray
Abstract
In their analysis of a threshold-rounding algorithm for stabbing axis-parallel segments, Elbassioni and Ray exhibit a family of fractional solutions of the standard LP relaxation whose rounding cost ratio tends to an explicit two-variable function γ(τₓ,τ_y) of the two rounding thresholds, and assert that γ ≥ 1.89 everywhere, with the sentence: "We skip the technical proof since it does not yield much insight and since this can be easily checked numerically." The assertion stands unproved in the 2021 preprint, and Appendix B of the 2024 journal version repeats it word for word, with the thresholds renamed. We prove it, and we determine the constant it approximates. The minimum of γ over [0,1)² is attained at (t^(*),1/2) and at (1/2,t^(*)), where t^(*) is the unique root in [(7)/(20),2/5] of the integer quartic q(t)=6000t⁴-16040t³+14600t²-5080t+577; and that minimum lies between 1.891152196075811250 and 1.891152196075811251. So the published 1.89 is true, and short of the truth by 1.152… × 10⁻³. The proof of the inequality is a twenty-five-box Bernstein certificate in exact integer arithmetic, with the certified coefficient arrays computed from the source's own density rather than stored. The exact minimum needs neither a derivative nor any arithmetic in the quartic field: two divided differences turn it into polynomial identities and a handful of further rational positivity certificates, and one of those identities makes the resulting bracket for the minimum quadratically accurate, which is where the eighteen decimal places come from. Every statement below is machine-checked in Lean 4.
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
- Version 1 · current (opens in a new tab)
Source snapshot 2026-09-07 03:53 UTC
File fingerprint
720b1d9e22b35eae19c22fa05f2d956304bafefed1fbe1f90a3402e590b3bd08
Claim ledger
Stated results
SG1candidate2026-09-02
the inequality arXiv:2106.12385v1 asserts and declines to prove: gamma(tauₓ, tau_y) >= 189/100 for every pair of thresholds in [0,1)², by a 25-box Bernstein certificate at multidegree (8,8) computed inside the proof from the source's own density
SG2candidate2026-09-02
the exact minimum, which neither version of the source states: min gamma over [0,1)² equals gamma(t*, 1/2) = gamma(1/2, t*), where t* is the unique root in [7/20, 2/5] of the integer quartic 6000 t⁴ - 16040 t³ + 14600 t² - 5080 t + 577
SG3routine2026-09-02
the minimiser is a well-defined algebraic number: the quartic 6000 t⁴ - 16040 t³ + 14600 t² - 5080 t + 577 has exactly one root in [7/20, 2/5], by a Bernstein certificate for its first divided difference (V >= 125 there, hence strict monotonicity) plus the intermediate value theorem
SG4candidate2026-09-02
the value of the minimum to eighteen decimal places: 1.891152196075811250 <= min gamma <= 1.891152196075811251, so the source's 1.89 is true and short of tight by 1.152...e-3, and no analysis of this shape can be pushed past 1.8911521960758112...
SG5routine2026-09-02
negative controls: gamma >= 19/10 is false and even gamma >= 757/400 is false (both refuted at gamma(3/8,1/2) = 11499/6080); gamma(x,x) = 1/(1-x) above 1/2 so gamma takes every integer value >= 2 and the hypothesis tau < 1 cannot be dropped; gamma(0,0) = 160/57, gamma(1/2,1/2) = 2, gamma(99/100,99/100) = 100; and six Boolean controls on the certificate machinery all reject
SG6measurement2026-09-02
the compute-first-values gate, in exact rational arithmetic outside Lean: int₀¹ f = 1 and int₀¹ t f = 57/160 (so f is a genuine density and the source's normaliser is 57/80); F and G as piecewise polynomials, continuous at 1/5, 2/5 and 1/2; gamma(0,0) = 160/57; the quartic rederived from f by differentiating along tau_y = 1/2; its two roots in (1/5,2/5) at 0.234328098064746616... (a local maximum, gamma = 1.92202871178...) and t* = 0.380515916462463880198512617...; min gamma = 1.8911521960758112504454342...; and the Bernstein feasibility survey that sized the certificates
This ledger entry is reported in prose and is not bound to a Lean theorem.SG7routine2026-09-02
F and G really are the integrals of the source's density: int₀ᵗau t f(t) dt = Gmom tau and intₜau¹ f = Ftail tau for every tau in [0,1], hence int₀¹ f = 1 (f is a genuine probability density, as the source intends) and int₀¹ t f = 57/160 (the source's normaliser 2 int t f is 57/80)
Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- Khaled Elbassioni and Saurabh Ray, *Threshold Rounding for the Standard LP Relaxation of some Geometric Stabbing Problems* (arXiv:2106.12385v1, cs.CG, 23 June 2021; journal version *Geometric Stabbing via Threshold Rounding and Factor Revealing LPs*, Discrete Comput. Geom. 71 (2024) 787–822; online 2023-11-27), analyse an LP-rounding algorithm for stabbing axis-parallel segments and prove that the integrality gap of their LP is at most 1.935. Then, to show that their *analysis* cannot be pushed much further, they exhibit a family of fractional solutions and reduce its cost ratio to a two-v
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7