From 045b15d75688057b1efcb3718eb03d7ca9ec841d Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Sat, 19 Sep 2026 03:20:04 -0400 Subject: [PATCH 1/2] C_47: record the lower bound 1.68550999 from a weighted lattice Adds a Known lower bounds row for the two-mass lattice construction, the [Lin2026] reference to its Lean formalization (registered on Palomar as PALOMAR-2026-09-19-000002), and updates the README cell and Recent progress. Co-Authored-By: Claude Opus 5 --- README.md | 3 ++- constants/47a.md | 7 +++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index c2c630f..5a9bb81 100644 --- a/README.md +++ b/README.md @@ -82,7 +82,7 @@ Bounds for which the level of available verification is currently at minimal lev | [44](https://teorth.github.io/optimizationproblems/constants/44a.html) | Maximal number of relevant variables in Boolean functions of degree $d$ | 1.5 | 4.394 | | [45](https://teorth.github.io/optimizationproblems/constants/45a.html) | Density of odd integers that are the sum of a prime and a power of two | 0.107648 | 0.490180063290061 | | [46](https://teorth.github.io/optimizationproblems/constants/46a.html) | Fourier restriction constant for the 2-sphere | 3 | $\frac{22}{7}\approx 3.142857$ | -| [47](https://teorth.github.io/optimizationproblems/constants/47a.html) | Centered Hardy-Littlewood maximal constant in dimension $2$ | $\frac{3}{4}-\frac{\sqrt{2}}{4}+\frac{\sqrt{6}}{2}\approx 1.6211915$ | 4 | +| [47](https://teorth.github.io/optimizationproblems/constants/47a.html) | Centered Hardy-Littlewood maximal constant in dimension $2$ | 1.68550999 | 4 | | [48](https://teorth.github.io/optimizationproblems/constants/48a.html) | One-dimensional convex sub-Gaussian comparison constant | $\approx 5.33386$ | $\approx 5.33386$ | | [49](https://teorth.github.io/optimizationproblems/constants/49a.html) | Erdős–Szemerédi $3$-sunflower-free capacity | >1.551 ($\geq 1.554*$) | $\frac{3}{2^{2/3}} \approx 1.88988$ | | [50](https://teorth.github.io/optimizationproblems/constants/50a.html) | Approximation ratio for quantum Max Cut | 0.614 | $<1$ (0.5 for product states) | @@ -158,6 +158,7 @@ Bounds for which the level of available verification is currently at minimal lev - [15a](https://teorth.github.io/optimizationproblems/constants/15a.html) **improved upper bound:** $C_{15a} \leq 2.371177$ by [E. Dupont, M. Eisenberger, B. Kozlovskii, A. Mehrabian, F. J. R. Ruiz, A. See, R. Zhou, J. Alman, V. Vassilevska Williams, M. Balog](https://arxiv.org/abs/2608.16884), 17 Aug 2026. - [43](https://teorth.github.io/optimizationproblems/constants/43a.html) **improved lower bound (unverified):** $C_{43} \geq 0.860*$ (exact $43/50$; certificate-layer result conditional on the lemma set of [KHSHGW2026](https://arxiv.org/abs/2601.22365)) by [J. Savva](https://doi.org/10.5281/zenodo.22223485), 1 Sep 2026. - [88a](https://teorth.github.io/optimizationproblems/constants/88a.html) **improved upper bound:** $C_{88a} \leq 186$ via $\mathrm{DHL}[40,2]$, by [OpenAI](https://cdn.openai.com/pdf/51126fac-1b68-4128-9666-c908bcc16033/short_gaps.pdf), 30 Aug 2026, with a Lean 4 formalization conditional on three declared axioms. +- [47](https://teorth.github.io/optimizationproblems/constants/47a.html) **improved lower bound:** $C_{47} \geq 1.68550999$ by [Y. Lin](https://github.com/CoolRmal/centered-maximal-constant), 19 Sep 2026, with a Lean 4 formalization registered on Palomar. ## Maintainers diff --git a/constants/47a.md b/constants/47a.md index abf49d8..343d68f 100644 --- a/constants/47a.md +++ b/constants/47a.md @@ -41,6 +41,7 @@ the optimal weak-type $(1,1)$ constant of the centered Hardy–Littlewood maxima | ----- | --------- | -------- | | $\dfrac{3}{4}-\dfrac{\sqrt{2}}{4}+\dfrac{\sqrt{6}}{2}\approx 1.6211915$ | [Ald2000] | Aldaz's Proposition 1.4 gives a lower bound in every dimension $n\ge 2$. Specializing the formula to $n=2$ gives the displayed value. [Ald2000-prop1.4] | | $\dfrac{11+\sqrt{61}}{12}\approx 1.5675208$ | [Mel2003], [Ald2011] | Melas proved $c_1=\dfrac{11+\sqrt{61}}{12}$. Since $c_{d+1}\ge c_d$, we get $c_2\ge c_1$. [Mel2003-c1-formula] [Ald2011-monotone] | +| $\Phi\approx 1.6855099933$ | [Lin2026] | Periodic measure with two masses: mass $1$ at the points $(ih,jV)$ with $i$ even and mass $w=(17+4\sqrt{22})/9$ at those with $i$ odd ($i,j\in\mathbb{Z}$), where $h=(5+\sqrt{22})/6$ and $V=(11+\sqrt{22})/6=h+1$. A period cell of area $2hV$ carries mass $1+w$, and six explicit witness squares show that the maximal function of this measure is at least $1$ on the cell outside four open slots of size $a\times b$, where $u=(2+\sqrt{22})/3$, $a=2h-\sqrt{2(2+w)}/2-u/2\approx 0.386845$ and $b=V-\sqrt{2}u/2-\sqrt{w}/2\approx 0.041439$. Hence $\Phi=(2hV-4ab)/(1+w)$, an algebraic number of degree $16$. Truncating the lattice and smearing each atom over a small square turns this into integrable test functions. The statements $\Phi\le c\_2$ and $1.685<\Phi<1.686$ are formalized in Lean 4 and registered on Palomar. [Lin2026-construction] | ## Additional comments and links @@ -83,6 +84,11 @@ the optimal weak-type $(1,1)$ constant of the centered Hardy–Littlewood maxima **loc:** arXiv PDF p.2, Introduction. **quote:** “No best constants are known for dimensions larger than one.” +- **[Lin2026]** Lin, Yongxi. *A lower bound 1.6855 for the planar centred Hardy-Littlewood maximal constant over squares.* Lean 4 formalization, [GitHub](https://github.com/CoolRmal/centered-maximal-constant) at commit `c6a8cb2`, registered on the Palomar registry as [PALOMAR-2026-09-19-000002](https://palomar-registry.org/entry?id=PALOMAR-2026-09-19-000002&version=1) (2026). + - **[Lin2026-construction]** + **loc:** `README.md` (section *The construction*) and `docs/PROOF.md`. + **note:** The Lean statement `CenteredMaximal.ofReal_phi_le_weakTypeConstant_two` uses closed cubes and the strict level set $\\{Mf>\alpha\\}$, which gives the same constant as the non-strict level set used above. The compared theorems depend only on the axioms `propext`, `Classical.choice` and `Quot.sound`. + - **[Mel2003]** Melas, Antonios D. *The best constant for the centered Hardy–Littlewood maximal inequality.* Annals of Mathematics (2) **157** (2003), no. 2, 647–688. DOI: [10.4007/annals.2003.157.647](https://doi.org/10.4007/annals.2003.157.647). [Google Scholar](https://scholar.google.com/scholar?q=The+best+constant+for+the+centered+Hardy-Littlewood+maximal+inequality+Melas). [arXiv PDF](https://arxiv.org/pdf/math/0311452.pdf) - **[Mel2003-c1-formula]** **loc:** arXiv PDF p.3, Introduction (equation (1.8) and the following sentence). @@ -105,3 +111,4 @@ the optimal weak-type $(1,1)$ constant of the centered Hardy–Littlewood maxima Prepared with assistance from ChatGPT 5.2 Pro. This update was prepared with assistance from GPT-5.5 Pro; citations and mathematical details were reviewed by the human contributor. +The [Lin2026] lower bound was added with assistance from Claude (claude-opus-5). From 8c38d316f0bc2605afef6ccf7ffa433512da4afc Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Sat, 19 Sep 2026 11:33:40 -0400 Subject: [PATCH 2/2] Shorten the C_47 row and drop the contribution note line Co-Authored-By: Claude Opus 5 --- constants/47a.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/constants/47a.md b/constants/47a.md index 343d68f..3ade45d 100644 --- a/constants/47a.md +++ b/constants/47a.md @@ -41,7 +41,7 @@ the optimal weak-type $(1,1)$ constant of the centered Hardy–Littlewood maxima | ----- | --------- | -------- | | $\dfrac{3}{4}-\dfrac{\sqrt{2}}{4}+\dfrac{\sqrt{6}}{2}\approx 1.6211915$ | [Ald2000] | Aldaz's Proposition 1.4 gives a lower bound in every dimension $n\ge 2$. Specializing the formula to $n=2$ gives the displayed value. [Ald2000-prop1.4] | | $\dfrac{11+\sqrt{61}}{12}\approx 1.5675208$ | [Mel2003], [Ald2011] | Melas proved $c_1=\dfrac{11+\sqrt{61}}{12}$. Since $c_{d+1}\ge c_d$, we get $c_2\ge c_1$. [Mel2003-c1-formula] [Ald2011-monotone] | -| $\Phi\approx 1.6855099933$ | [Lin2026] | Periodic measure with two masses: mass $1$ at the points $(ih,jV)$ with $i$ even and mass $w=(17+4\sqrt{22})/9$ at those with $i$ odd ($i,j\in\mathbb{Z}$), where $h=(5+\sqrt{22})/6$ and $V=(11+\sqrt{22})/6=h+1$. A period cell of area $2hV$ carries mass $1+w$, and six explicit witness squares show that the maximal function of this measure is at least $1$ on the cell outside four open slots of size $a\times b$, where $u=(2+\sqrt{22})/3$, $a=2h-\sqrt{2(2+w)}/2-u/2\approx 0.386845$ and $b=V-\sqrt{2}u/2-\sqrt{w}/2\approx 0.041439$. Hence $\Phi=(2hV-4ab)/(1+w)$, an algebraic number of degree $16$. Truncating the lattice and smearing each atom over a small square turns this into integrable test functions. The statements $\Phi\le c\_2$ and $1.685<\Phi<1.686$ are formalized in Lean 4 and registered on Palomar. [Lin2026-construction] | +| $\Phi\approx 1.6855099933$ | [Lin2026] | Periodic measure: masses $1$ and $w=(17+4\sqrt{22})/9$ on alternating columns $x=ih$, rows $y=jV$, with $h=(5+\sqrt{22})/6$ and $V=h+1$. Its maximal function is at least $1$ on a period cell except four open $a\times b$ slots, so $\Phi=(2hV-4ab)/(1+w)$, where $u=(2+\sqrt{22})/3$, $a=2h-\sqrt{2(2+w)}/2-u/2$ and $b=V-\sqrt{2}u/2-\sqrt{w}/2$. Formalized in Lean 4 and registered on Palomar. [Lin2026-construction] | ## Additional comments and links @@ -111,4 +111,3 @@ the optimal weak-type $(1,1)$ constant of the centered Hardy–Littlewood maxima Prepared with assistance from ChatGPT 5.2 Pro. This update was prepared with assistance from GPT-5.5 Pro; citations and mathematical details were reviewed by the human contributor. -The [Lin2026] lower bound was added with assistance from Claude (claude-opus-5).