| $4$ | [Bil26] | Same nonlinear system as [Tao19], with a sharper *point-source Green function* estimate on the right inverse (norm $O(n)$ on scalar point sources, versus $O(n^2)$ in the worst case), proved by interpreting iterated Cuntz block coefficients as a killed walk and comparing them with binomial incidence matrices. This upgrades the fixed-point scale from $\delta \asymp n^{-5}$ to $\delta \asymp n^{-4}$ and improves the exponent from $5$ to $4$. Result and Lean 4 formalization produced autonomously by GPT-5.6 Sol High (13 min for the proof, ${<}3$ h for the formalization). |tracked since 2026-07-24 — no movement seen yet
Lower bound, last-listed row
| $1$ | [Pop82] | Popa's quantitative Wintner–Wielandt bound $m_H(\varepsilon) \ge \tfrac{1}{2}\log(1/\varepsilon)$; see [Tao19, Theorem 0.1] for a short reproduction. Conjectured to be sharp. |tracked since 2026-07-24 — no movement seen yet
Checked against material for its cited source
The row shown above: bound row $4$line 19 citing [Bil26] — the claim we checked: that the cited note proves the exponent 4 by the point-source Green function estimate the row's comment describes. What we read supports it. This verdict does not cover the proof's correctness, any Lean formalization, and the comment's account of how the result was produced (the model named and the times taken). source link (read in the cited note: the blog post at the entry's URL (as text, dated July 17, 2026), which gives no proof itself, and the paper it links as "Paper (local PDF)", whose title is the entry's title, printed pp. 1–13 read from page images. The site's history shows one commit of that PDF, on the entry's access date). Selected: drawn by its position in the list of cited rows, not because it looked wrong.
1 bound row(s) here have been checked against material for their cited source (1 drawn by position, 0 chosen because something already looked wrong). Across this whole ledger 70 row(s) have been drawn by position, against 691 rows that name a source, counted on 2026-09-27: 64 were checked against material for their cited sources and for 6 the cited source could not be read at all. 5 more were chosen for suspicion and checked; they are counted apart, because a set selected for suspicion carries no rate. A row not listed here has NOT been checked.
Cite this rowBounds Ledger — Exponent for commutators close to the identity (85a)
upper bound: $4$ (tracked since 2026-07-24 — no movement seen yet)
lower bound: $1$ (tracked since 2026-07-24 — no movement seen yet)
Mirrored from teorth/optimizationproblems@2c1968c. These are the last-listed rows of that constant's bounds table — a listing position, not a statement that this bound is the strongest or most recent. A snapshot at that sha, not a live read.
https://u00dxk2.github.io/bounds-ledger/c/85a.html