Four dual tuples suffice: a smaller exact certificate for the randomized metric-distortion bound 11641/5000
Abstract
Shah's recent bound of 11641/5000=2.3282 on randomized metric distortion rests on an exact rational certificate: forty-nine parametric dual tuples for a semi-infinite linear program, certified feasible by 107 polynomial inequalities, and fifty candidate bounds whose disjunction is certified to cover the unit square by Bernstein-basis subdivision over 1096 accepted boxes. We show that the certificate is far smaller than it looks. Four of the fifty candidate bounds already cover the square — the tuples z₁,z₂,z₃ and the tangency tuple at τ=3/5, with z₂ used only where x ≥ 1/4 — and the (1-p)x ≤ T(q) bound is not needed at all. The feasibility burden drops from 107 polynomial inequalities to 17. The four-tuple set is minimal for the subdivision search: dropping any one of the four makes it fail, and restoring the discarded bound does not repair the loss. Both halves of the reduced certificate are machine-checked in Lean 4. Two further facts about the published certificate are recorded: every one of its 107 feasibility polynomials passes the Bernstein test at the root, with no subdivision at all, so subdivision is needed only for the cover; and its own accepted cover invokes only 8 of its 50 candidates. We are careful about what is and is not verified: the passage from these polynomial inequalities to the distortion bound itself runs through four measure-theoretic steps of the source that are not formalized, and we say exactly which.
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
df7d2af77651fad16c7280a1ce873c7f114348f2e585a072e4376502a9707b83
Claim ledger
Stated results
DB1known data2026-09-03
Dual family 1 of arXiv:2608.29308v1 (y₁ = 80529/100000): all six Hᶠeas polynomials of Appendix B.3 (referee 2026-09-03: off by one) are nonnegative on the unit box (the first at least 1), each together with the exact polynomial division that defines it
DB2known data2026-09-03
Dual family 2 (y₂ = 1): its six Hᶠeas polynomials are nonnegative on the dyadic slab x in [1/4,1], each with its exact-division identity
DB3known data2026-09-03
Dual family 3: its three Hᶠeas polynomials are nonnegative on their boxes, each with its exact-division identity
DB4known data2026-09-03
The tangency dual tuple at tau = 60/100 (the source's z₄9): both Hᶠeas polynomials are nonnegative on [0,1], the first at least 1, each with its exact-division identity
DB5candidate2026-09-03
Four candidate bounds suffice for the outer cover of lem:star-loss: at every (q,x) of the unit square at least one of Hᵒut₁, Hᵒut₂, Hᵒut₃, Hᵒut₄9 is nonnegative, with Hᵒut₂ needed only where x >= 1/4 – the source covers with fifty
DB6measurement2026-09-03
The census of the source's certificate: all 107 dual-feasibility polynomials certify at the Bernstein root with zero subdivision; the published cover fires only 8 of its 50 candidates; and the reduced four-tuple certificate is minimal – dropping any one of z₁, z₂, z₃, z₄9 breaks the cover, and adding the (C3) bound back does not repair it
DB7routine2026-09-03
Negative controls: the target constant is load-bearing (all four candidate bounds are strictly negative at (q,x) = (3/8, 9/16) for the target that would give distortion 2.3); Hᶠeas_(5,2) is strictly negative at (1/16, 15/16), so dual family 2's slab hypothesis is not vacuous; z₂ is indispensable in the cover; a perturbed quotient breaks its exact-division identity; the strict positivity margin is sharp
DB8routine2026-09-03
The binomial double sums (B.1)-(B.3) of arXiv:2608.29308v1 collapse to differences of Psi = int f: r x Gₓ(0,y) = p - Psi(r) + Psi(ry) - Psi(x+ry), x d_yGₓ(0,y) = f(ry) - f(x+ry), r x Gₓ(1,0) = p - Psi(x) - Psi(r), r x Fₓ(b) = Psi(r+xb) - Psi(xb) - Psi(r), r x Rₓ = r p - Psi(r) – so the whole certificate is generated by f, f' and Psi with no binomial coefficients
This ledger entry is reported in prose and is not bound to a Lean theorem.DB9prose2026-09-03
The bridge from the certified polynomial inequalities to dist(P*) <= 11641/5000 is not formalized: prop:set-certificate, lem:rsl-loss-envelope (an infinite-dimensional program over two Borel measures), generalized-moment weak duality with the sign chain from Hᶠeas to dual feasibility, and the existence of RSL(D*) all remain prose
This ledger entry is reported in prose and is not bound to a Lean theorem.DB10measurement2026-09-03
The reach of the source's 49-tuple certificate: numerically it supports kappa >= 0.66408958, i.e. distortion >= 2.3281792, so the published kappa = 6641/10000 carries only 1.04e-5 of slack; certifying past it is priced at roughly 25x the 1022 boxes (about 2.7 CPU-h and 8 GB in Lean) for a fifth-decimal gain, and is parked
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- The Bernstein certificate behind the randomized metric-distortion bound 11641/5000 = 2.3282.
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7