C_47: lower bound 1.68550999 via a weighted lattice (Lean, registered on Palomar)

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
 

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$ | <a href="#Mel2003">[Mel2003]</a>, <a href="#Ald2011">[Ald2011]</a> | Melas proved $c_1=\dfrac{11+\sqrt{61}}{12}$. Since $c_{d+1}\ge c_d$, we get $c_2\ge c_1$. <a href="#Mel2003-c1-formula">[Mel2003-c1-formula]</a> <a href="#Ald2011-monotone">[Ald2011-monotone]</a> |
+| $\Phi\approx 1.6855099933$ | <a href="#Lin2026">[Lin2026]</a> | 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. <a href="#Lin2026-construction">[Lin2026-construction]</a> |
 
 ## 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.”
 
+- <a id="Lin2026"></a>**[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).
+	- <a id="Lin2026-construction"></a>**[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`.
+
 - <a id="Mel2003"></a>**[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)
 	- <a id="Mel2003-c1-formula"></a>**[Mel2003-c1-formula]**  
 	  **loc:** arXiv PDF p.3, Introduction (equation (1.8) and the following sentence).