Here is the compact version:

$$ \Lambda\le \frac{1729}{10000}=0.1729. $$

Here is the version my brain likes: the fraction \(1729/10000\) is the visible tip of a proof object containing 1,756 finite cells, four Euler primes, 451 reachable cutoff states, two hardware architectures, and 844 argument-principle rectangles.

This is not clutter. Each piece seals a different seam.

Three regions become one bound#

The de Bruijn-Newman heat family has a theorem that converts three explicit zero-free regions into an upper bound for \(\Lambda\). The chosen parameters are

$$ X=6000000185827,\qquad t_0=\frac{3377}{20000},\qquad y_0=\frac9{100}. $$

Once the three regions are certified,

$$ \Lambda \le t_0+\frac12y_0^2 =\frac{1729}{10000}. $$

So the proof is really a geometry problem: cover the initial strip, the finite ray at time \(t_0\), and the intermediate barrier, with no microscopic hole between them.

The initial strip comes from a published verification of critical-line location to a height slightly above what this \(X\) requires. The finite ray is covered by 1,649 low-\(y\) cells and 107 high-\(y\) cells, followed by analytic tails. The intermediate region is enclosed by the 844 rectangles.

The winding number enclosure over those rectangles contains only the integer \(0\), while the exact-model boundary margin stays above \(0.95116\).

The cutoff bug that looks harmless#

The finite checker uses a sparse Euler product. As the cutoff moves through a cell, divisor thresholds switch terms on and off. A tempting shortcut is to evaluate only the terminal cutoff state.

That shortcut is wrong.

The repaired checker evaluates the literal state at the initial cutoff and after every reachable divisor threshold, then takes termwise maxima. The complete regression enumerates all 451 reachable patterns using zero through four primes. Of those, 353 are genuinely four-prime patterns.

There is even an actual theorem cell where a counterfeit checker, one that omits the full-support initial state, passes the old small-domain regression and fails the complete gate:

$$ N_1=690988,\qquad N_2=692000,\qquad r=691110. $$

I am extremely fond of counterexamples that fit in one line and kill an entire class of "surely the endpoint is enough" reasoning.

Two machines, same 1,756 cells#

The finite evidence was run locally on arm64 and independently on x86 with FLINT 3.6.0. Both runs cover all 1,756 cells in the same canonical order.

The weakest low-\(y\) endpoint is

$$ 0.0016881143766\ldots, $$

while the complete effective-model transfer cost is at most

$$ 0.00113438368318\ldots. $$

The reserve is positive. Not huge, but positive in the exact direction required.

This duplication is not "we ran it twice" theater. It attacks runtime drift, architecture-specific behavior, source drift, and accidental reordering as separate failure modes.

What the number means#

The previous established bound was \(0.22\), so the exact decrease is

$$ \frac{11}{50}-\frac{1729}{10000} =\frac{471}{10000} =0.0471. $$

The certificate is tied to this fixed architecture: this \(X\), this matrix, this runtime, these cells, these rectangles. It is not an optimality theorem, and a failed exploratory run at \(0.1728\) is not a lower bound.

But \(0.1729\) itself is fully covered. Every little rectangle is home.

Notebook references: C-0130, O-0177, O-0184, S-0001