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

[CoolRmal]

Summary

Records a new lower bound for $C_{47}$, the weak-type $(1,1)$ constant of the centered Hardy–Littlewood maximal operator over axis-parallel squares in the plane:

$$ c_2 \ \ge\ \Phi = \frac{2hV-4ab}{1+w} = 1.6855099933\ldots, $$

improving Aldaz's $\tfrac34-\tfrac{\sqrt2}{4}+\tfrac{\sqrt6}{2}\approx 1.6211915$ (2000). $\Phi$ is an explicit algebraic number of degree 16 (closed form in Challenge.lean of the linked repository).

The proof is a complete Lean 4 / Mathlib formalization, registered on the Palomar registry as PALOMAR-2026-09-19-000002 at commit c6a8cb2: https://github.com/CoolRmal/centered-maximal-constant

The construction

The previous record comes from a unit rectangular lattice. The improvement uses unequal masses: mass $1$ at $(ih,jV)$ for even $i$ and mass $w=(17+4\sqrt{22})/9$ for odd $i$, with $h=(5+\sqrt{22})/6$ and $V=h+1$. On a period cell (area $2hV$, mass $1+w$), six explicit witness squares show the maximal function of the measure is at least $1$ outside four thin open slots of size $a\times b$ (the formulas for $a$, $b$ are in the Comments cell). That gives covered area per unit mass $\Phi=(2hV-4ab)/(1+w)$. Truncating the lattice and smearing each atom over a small square turns the measure into integrable test functions, and letting the truncation grow gives $c_2\ge\Phi$. The Comments cell carries enough data to recompute $\Phi$ without downloading anything.

Verification

• Lean statements, compared by Comparator against a Mathlib-only Challenge.lean: ofReal_phi_le_weakTypeConstant_two ($\Phi\le c_2$), lt_phi / phi_lt ($1.685<\Phi<1.686$), and weakTypeConstant_le_two_pow ($c_d\le 2^d$). They depend only on propext, Classical.choice and Quot.sound: no sorry, no native_decide, no custom axioms.
• The Lean definition uses closed cubes and the strict level set ${Mf>\alpha}$; this gives the same constant as the non-strict level set on the constant page, and the note under [Lin2026-construction] says so.
• Registered on Palomar (PALOMAR-2026-09-19-000002): its mechanical check reran the comparator in a sandbox and replayed the proof through Lean's kernel and the independent NanoDa kernel. The result has not been peer reviewed. I have not added an asterisk to the README cell; please add one if you prefer to reserve unmarked cells for published results.

Changes (Markdown only)

• constants/47a.md: new row in Known lower bounds, a [Lin2026] reference with a [Lin2026-construction] note, and a contribution note.
• README.md: the $C_{47}$ lower-bound cell becomes 1.68550999, plus a line in Recent progress.

AI use

The construction was found and certified with AI assistance, and formalized with AI assistance in Claude Code under my direction; formalization.yaml in the repository records the models. This pull request was prepared with assistance from Claude (claude-opus-5).

🤖 Generated with Claude Code