An upper bound for the weak type (1,1) constant of the centred maximal operator over squares

Let c2 be the best constant in the weak type (1,1) inequality for the centred Hardy–Littlewood maximal operator over axis-parallel squares in the plane. The covering argument gives c2 ≤ 4, and Lin proved c2 < 3.879, with a proof formalized in Lean. We prove c2 ≤ 3.59123. The proof uses a comparison principle of Lin, in coordinates (u, v) in which squares become diamonds: if an even, nonnegative, integrable kernel K is at least 1 on the diamond |u| + |v| ≤ 1 and AαK ≥ 0 away from the origin, where Aα = −|∂u|α − |∂v|α and 0 < α < 2, then c2 is at most half the integral of K. We prove this principle in detail, following Lin, and give closed forms for Aα applied to cubic B-splines and to (|u| + |v|)−α. With these, AαK is explicit for kernels made of a truncation of (|u| + |v|)−α and finitely many tensor products of cubic B-splines. We exhibit such a kernel for α = 47/40 with B-spline spacing 1/32, and two independent programs verify its properties in interval arithmetic. This improves the bound c2 < 3.615749 that Lin obtained with a kernel of this type. We also prove c2 ≥ 1.7027237335, improving Lin's lower bound c2 ≥ 1.6855. The proof changes the parameters of Lin's periodic lattice of point masses slightly and adds 48 small atoms to each period cell, on horizontal segments of six equal atoms; a program in exact rational arithmetic computes the area of a part of the superlevel set of the maximal function of this measure. We also formalized the proof of the lower bound in Lean. The certificates of both bounds, their verification programs, the Lean proof of the lower bound, the search programs and the logs are archived at doi:10.5281/zenodo.23533974. They are also available at github.com/tejasvi/square-maximal-weak-type-v2.