A Reproducible Certificate for the Brass--Sharifi Lower Bound in Lebesgue's Universal Cover Problem
This work provides a reproducible certificate for a known lower bound in a geometric optimization problem, but it is incremental as it does not improve the bound or provide formal verification.
The paper reproduces the Brass-Sharifi lower bound of 0.832 for the convex form of Lebesgue's universal cover problem by providing a certificate-based computation. The certificate includes a finite adaptive ledger, terminal-route replay, and other components that, when accepted, imply the bound.
Brass and Sharifi proved the lower bound 0.832 for the convex form of Lebesgue's universal cover problem by combining geometric estimates with a computer search over placements of a disk, an equilateral triangle, and a regular pentagon. This paper gives a certificate-based reproduction of that computation. The certificate consists of a finite adaptive ledger, a terminal-route replay, three local lower-bound certificate families, compact integrity audits for large tables, and a finite proof-obligation layer connecting the replayed data to the lower-bound statement. Under the stated verification model, acceptance of this finite certificate implies the Brass--Sharifi convex lower bound αcvx $\ge$ 0.832. We claim neither a numerical improvement over the Brass--Sharifi bound nor a nonconvex lower bound; proof-assistant formalization and independent external verification remain outside the present scope.