[carlostoledo1891]

The 84b upper-bound row records 1.999281 ("giving $c \ge 0.000719$"), citing Althoefer's note [Al26]. The note's theorem is $c \ge 0.0007$. The value 0.000719 appears only beside it: "The optimized value suggested by the same calculation is about $0.000719$, but $0.0007$ is the safer quoted constant." That suggested value is out of reach of the calculation the note prints. I rechecked the chain in interval arithmetic, with code that shares nothing with the note:

• The theorem holds. At the note's own choice ($Y = 1415$, $X = \lfloor e^{1423} \rfloor$) every step holds, and the chain gives $c \approx 0.000706$. So $C_{84b} \le 1.9993$, given [BSSZ2026, §5], the note's lattice-doubling lemma and its regulator bound, which I took as given.
• 0.000719 is not reached. For every choice of $s > 1$, $X$ and $Y$, the same chain gives $c \le 0.0007150508$ (the maximum sits near $Y = 1399$). The regulator factor is at least 101.9 for every $s$, and the additive factor forces $\log X > Y + \log M_1 - 2 \log Y$.

This PR records the theorem. It is Markdown only: 2 files, 4 insertions, 3 deletions.

• README: the cell $<2$ (1.999281*) becomes $<2$ (1.9993*), and the 28 May line in Recent progress is corrected in place: it now records $1.9993*$ and names the $1.999281$ it replaces, so the old value no longer reads as the record (edited in place on review; it was a separate correction line at first).
• 84b.md: the row's bound becomes $1.9993$*. It quotes the note's own sentence and adds a [T2026] reference.

I kept the asterisk, because what was checked is the note's arithmetic, not the inputs it cites. Prof. Althoefer is welcome to supersede this with the calculation that reaches 0.000719, if there is one. The branch is cut from 46dbf036 and merges cleanly with #232, #242, #243 and #249 (and with #235, #250 and #251).

Re-derive (standard library, about a minute): python3 tools/run-sumproduct-ledger.py --check in https://github.com/carlostoledo1891/cert-machine at 422b952 (archived as doi:10.5281/zenodo.23171167); the note's tex is pinned there by sha256 (2f6bbdcb…, unchanged today). Write-up: §4 of https://carlostoledo.co/reports/optimization-constants.html

AI-assisted: built with Claude (Anthropic) in a certified-arithmetic setting; the interval check, the record and this pull request were prepared with it, and every number and reference above was checked against the record, the note and the registry files.

🤖 Generated with Claude Code

[chessing234]

the table change to 1.9993* is the theorem's constant, and the asterisk stays. the 23 oct note is sitting between the 28 may and 3 jun lines. recent progress is newest first, so that note belongs at the top, and the older 1.999281 bullet should not stay next to it as if it were still the record.

[carlostoledo1891]

Thanks — agreed on the second point: the 28 May bullet now carries the corrected value itself (24cf417), so there is one 84b bullet and 1.999281 appears only as the value it replaced. I left it in place rather than at the top: the section isn't sorted newest-first (the 10c correction of #177, for example, went at the end), and the result is still Althoefer's of 28 May; the 23 Oct date sits on the correction inside the bullet. Happy to move it if a maintainer prefers. The description above is updated to match.

[JeetuSK0808]

A separate check agrees with this. Without using your code, this recomputes the [Al26] chain in interval arithmetic (mpmath), taking the note's lemmas and inputs as given. At the note's own choice Y = 1415, X = e^1423, the saving is c ≈ 0.000706. Optimizing Y and X with R_K ≤ 103^d gives at most about 0.000707. Even with the regulator constant pushed to its limit 101.9560758, the maximum is about 0.000714. So 0.000719 isn't reached, and 1.9993 is the right entry.

At the regulator limit this gives 0.00071385 where you get 0.0007150507. The difference is probably in how the limit enters the chain. Both are below 0.000719, so it doesn't affect the correction.

Code and table: https://github.com/JeetuSK0808/tao-constants-certificates/tree/f43c315/c84b-sum-product-check

(Written with Claude Code.)

[carlostoledo1891]

Thank you, and your maximum is the right number. We recomputed your chain with X optimised exactly (no grid): 0.0007139 at Y ≈ 1400.8 at the regulator limit, within 5·10⁻⁸ of your 0.00071385. Our 0.0007150507 is a ceiling rather than the maximum: it bounds −log(515/Y)/L using only the necessary condition log X > Y + log M₁ − 2 log Y, with the regulator taken at its proven lower bound 101.9, so it sits about 1.1·10⁻⁶ above the maximum. Both are below 0.000719.

[carlostoledo1891]

A correction to our own digits: the ceiling is 0.00071505073…, and we printed it truncated as 0.0007150507, which is below the value it bounds. Rounded up, it is 0.0007150508. #275 fixes the row, and the description above now says so too. Nothing else changes, and 0.000719 stays out of reach.