2026-10-09 · chapter Yang–Mills and the mass gapPart 10 Towards a proof of the mass gap — building the first step of the staircasecomputer-assisted, interval arithmetic, window · Kiichi, Shiori and Rin

What computer-assisted means — the conditions on the chain inside the window

Real numbers on a computer are floating-point numbers, and the result of most operations is the true value rounded to the nearest representable number. For example, $0.1+0.2$ becomes $0.30000000000000004$ in double precision. Each rounding is small, so in many computations it can be ignored. But when claiming an inequality "$q\lt1$" about a value close to 1, such as $q\approx0.9989$, one must show that accumulated rounding does not flip the direction of the inequality.

Interval arithmetic is computation in which every number is held as "an interval that is sure to contain the true value". Intervals are built from intervals: addition is $[a,b]+[c,d]=[a+c,b+d]$, multiplication takes the minimum and maximum of the four products of the ends, and so on. When the ends are computed, rounding is taken outwards (the lower end downwards, the upper end upwards). Then the final interval $[q^-,q^+]$ is sure to contain the true $q$, and if $q^+\lt1$, then $q\lt1$ follows as an inequality. In this part, inequalities obtained in this way carry the label Computer-assisted. Floating-point values written as they are carry Reading.

An example that can be checked by hand. The true range of $g(x)=x-x^2$ on $x\in[0,1]$ is $[0,\tfrac14]$. A naive evaluation in interval arithmetic gives, from $x\in[0,1]$ and $x^2\in[0,1]$, $x-x^2\in[0-1,\,1-0]=[-1,1]$. This contains the true value, but the width has grown eightfold. The cause is that the intervals forget the dependence that $x$ and $x^2$ come from the same $x$. There are two ways to fix this.

• Split finely. Splitting into $[0,\tfrac12]$ and $[\tfrac12,1]$ gives $[0-\tfrac14,\tfrac12-0]=[-\tfrac14,\tfrac12]$ and $[\tfrac12-1,1-\tfrac14]=[-\tfrac12,\tfrac34]$, together $[-\tfrac12,\tfrac34]$, and the width shrinks to 1.25.
• Expand about the centre. With $g(x)=g(c)+g'(\xi)(x-c)$, $c=\tfrac12$ and $g'(\xi)=1-2\xi\in[-1,1]$, we get $\tfrac14+[-1,1]\cdot[-\tfrac12,\tfrac12]=[-\tfrac14,\tfrac34]$, and the width is 1. This takes the first-order part of the dependence outside the interval.

What we meet in §04 when making $\hbar$ an interval is a large-scale version of these two fixes. We split the window of $\hbar$ into 25 subintervals (split finely), and within each subinterval expand the expectations in $\hbar$ to take the first- and second-order movement outside the interval (expand about the centre).

Seen from a site in the core, consider the chain $x_{i-1},x_{i-2},\dots$ extending to one side. The term of the action between neighbours is $(x_{i-1}-x_i)^2/(2\varepsilon)$, and the measure is $e^{-S/\hbar}$. Fixing $x_i=y$ and integrating out the far side, the conditional law of $x_{i-1}$ takes the form

($U$ is the effective potential with the far side integrated out, and does not depend on $y$). Let $m(y)$ be the mean of $\rho_y$, and let the $\mathrm{Stein}$ kernel be

. Integration by parts gives $\operatorname{Cov}_y(\varphi(X),X)=\mathbb E_y[\varphi'(X)\tau_y(X)]$ (the boundary term vanishes since $\int_L^R(m-t)\rho_y\,dt=0$). On the other hand, the logarithmic derivative of (1) in $y$ is $(x-m(y))/(\varepsilon\hbar)$, so

Proved here (differentiation under the integral sign and integration by parts; the box is bounded and the density is smooth). (3) reads: "each step back, the slope of a function (its Lipschitz constant) becomes at most $q$ times as large". Going back $d$ steps gives at most $q^d$ times. If $q\lt1$, the influence of fluctuations at distant sites on nearby sites decreases as a geometric series. This is the content of "the chain condition", and we call $q$ the Stein-kernel ratio.

A check. If $\rho_y$ is a normal distribution with variance $\sigma^2$, computing (2) gives $\tau_y\equiv\sigma^2$, and $q=\sigma^2/(\varepsilon\hbar)$. For the harmonic chain ($U$ a quadratic), one can check by hand that this ratio converges stage by stage to a fixed value.

What it is used for. In the construction of the logarithmic Sobolev constant of the site window (the product form of 10-07 §04), the quantity $S_W$ that adds up the influence of all stages outside the window enters as a factor. Adding the contribution of the stages inside the window and the contribution of the stages outside the window $\sum_{d\ge0}q^d=1/(1-q)$ on the two sides, left and right, gives

(the form with the ratio of the stages inside the window set to 1. The paper construction is not placed in the book, so the step that uses (4) sits on an Assumption row). If $q\lt1$, then $S_W$ is finite, and if $q\le0.998854904$, then $1/(1-q)\le873.3$ and $S_W\le1779.6$ Proved here (arithmetic).

Why $q$ is close to 1. The right wall of the box of the outer chain of the core is the top $0$, and there $V'(0)=0$. At the corner of this wall the classical ratio is exactly 1 (the corner at the wall in 10-07 §03), and the departure from 1 is set by the width $\eta\approx0.5\hbar$ of the thin layer near the wall, of size $1-q\approx\eta\ln(1/\eta)$ Reading (an expansion of the classical map, cross-checked with transfer-matrix values). The smaller $\hbar$ is, the closer $q$ comes to 1. This also shows that checking $q\lt1$ inside a fixed window of $\hbar$ leaves the behaviour as $\hbar\to0$ as a separate question.

The computer assistance of this part is interval arithmetic built on Python's double-precision floating point (float64). We collect the premises in one place.

• Rounding conventions. We assume that each arithmetic operation returns, as the IEEE 754 standard specifies, the floating-point number nearest the true value (correct rounding). The result of each operation is made into an interval by moving it outwards by one to the neighbouring floating-point number (the lower end one down, the upper end one up). The error of correct rounding is at most half a unit, so moving one unit outwards contains the true value. It is not a scheme that switches the rounding direction for each operation. Fused multiply–add (FMA) is not used.
• Summation error. Long sums are widened outwards by a known upper bound on summation error.
• The exponential function. The error of the standard mathematical functions is not guaranteed, so we use our own implementation of the exponential function and add an upper bound on its error to the interval. The arithmetic of the constants of the upper bound is checked in Lean.
• Integrals. For each grid cell we build upper and lower envelopes of the integrand (with a concavity correction) and squeeze the integral outwards. Truncation of the integral (cells with weight below $e^{-40}$ of the maximum) enters the interval as an upper bound on the truncated mass.

In this part this premise row is Assumption (row IA of 10-07 §05). That the computer and the language implementation keep correct IEEE 754 rounding is placed as a premise, not something we checked. When citing a computer-assisted result, we write this premise in the same row.

To get $q^+\lt1$ at a point value of $\hbar$ (for example $\hbar=3\cdot10^{-3}$), the interval arithmetic of §03 is enough. To say it for every $\hbar$ in the window $[3\cdot10^{-4},3\cdot10^{-3}]$, $\hbar$ itself must be put into an interval. Even if a downward trend is seen at three points, that the upper bound is monotone in $\hbar$ cannot be derived on paper (the formula for the upper bound contains two terms that are largest at opposite ends of $\hbar$).

We fix notation. $\beta=1/(\varepsilon\hbar)=2/\hbar$; for a subinterval $\hbar\in[\hbar_1,\hbar_2]$, $\beta\in[\beta_2,\beta_1]$; midpoint $\beta_0=(\beta_1+\beta_2)/2$, half-width $\Delta=(\beta_1-\beta_2)/2$, and $\tau=\beta-\beta_0\in[-\Delta,\Delta]$. $\hbar$ enters only through $\beta$.

Naive intervals break. Multiplying the exponent of the density $\beta(sx-A(x))$ by the interval of $\beta$ as it is allows the weight of each grid cell to move independently by factors $e^{\pm\Delta|sx-A|}$, and the width of the exponent is of order $10^2$. It is the same loss of dependence as $x-x^2$ in §01. Indeed, for the chain of the double well, at the second stage the interval of the mean spread over the whole box (width $0.89$), and the map of the stages lost its meaning.

Lemma TAU (making the expectation a linear-fractional function of $\tau$). Putting $h=g-g^*$ ($g^*$ a constant) and $\varphi_0=\beta_0h$, with $\beta=\beta_0+\tau$,

($S_0=\int fe^{\varphi_0}$, $S_1=\int fhe^{\varphi_0}$, $Z_0=\int e^{\varphi_0}$, $Z_1=\int he^{\varphi_0}$; $R$ are the integrals of the remainders). With the values of the remainders fixed, $t\mapsto(S_0+R_S+tS_1)/(Z_0+R_Z+tZ_1)$ is linear-fractional, and if the denominator is positive at $t=\pm\Delta$ it is monotone on $[-\Delta,\Delta]$. Hence for all $|\tau|\le\Delta$ the expectation lies between its two values at the ends $t=\pm\Delta$, and evaluating those two in intervals encloses it Proved here Leanmobius_between (assumptions: the denominator is positive at $t=\pm\Delta$, $-\Delta\le t\le\Delta$). The first-order term $\tau S_1/Z_0$ represents the real change with $\hbar$, and only $\Delta$ times the quadrature error and the remainder (of order $\Delta^2$) are left in the width of the interval.

Lemmas SH and SH2 (holding the enclosure tilted in $\tau$). The fixed points of the map of the stages (the conditional means $m_k$ of each stage of the chain) really move with $\hbar$. When the width of a subinterval is $3\%$, that movement alone is $1.5\times10^{-4}$, and putting it into the width of the enclosure ruins the downstream estimates. So we hold the enclosure in the form "$m_k-\tau\mu_k-\tau^2\nu_k$ lies in an interval" ($\mu_k$ and $\nu_k$ are floating-point sequences). On the output side the identity

extracts the first-order movement Proved here Leanshear_identity (assumptions: $C\ne0$, $C+tD\ne0$). Tilting to second order, the remaining width is of order $\Delta^3$. This is the form "expand about the centre" of §01.

Lemma DVτ (moving the centre with $\tau$). The upper bound on the variance has the form of a sum of two one-sided parts $\beta\,\mathbb E[(X-c)_+^2]+\beta\,\mathbb E[(c-X)_+^2]$, and when the mean moves by $\tau\mu$ one increases and the other decreases. Maximising the two separately at the ends of $\tau$ adds movements that in truth cancel. Moving the centre as $c_\tau=c+\tau\kappa$ and bounding by $(y-t)_+^2\le y_+^2-2ty_++t^2$ brought this loss down from $3.6\times10^{-3}$ to $2.2\times10^{-4}$ Proved here Leandvtau_pos (no assumptions).

Invariant sets. The chain is infinitely long, so we cannot run the map of the stages a finite number of times and stop. The map $\Phi_{[\hbar_1,\hbar_2]}$ on a subinterval is built to contain the results of the maps $\Phi_\hbar$ for all $\hbar\in[\hbar_1,\hbar_2]$, so if interval arithmetic confirms $\Phi_{[\hbar_1,\hbar_2]}(E^*)\subset E^*$ for some enclosure $E^*$, then $\Phi_\hbar(E^*)\subset E^*$ for every $\hbar$ Proved here (transitivity of inclusion). All later stages lie inside $E^*$, and it is enough to evaluate the upper bound on $q$ once on $E^*$.

Second-order tilting made subintervals of width 10% usable, and the window $[3\cdot10^{-4},3\cdot10^{-3}]$ was covered by 25 subintervals with ends $\hbar=3/N$ ($N=1000,1100,1210,\dots,9100,10000$, ratio between neighbours $\le1.1$). The grid width is $2^{-11}$, and the number of stages is 20 on the upper half and 25 on the lower half.

Write $q_{\rm free}$ for the ratio of the unmarked chain extending outside the site window of the core of the bridge (box $(-x_c,0)$, $x_c=0.89$) (route 1 of 10-07 §02). On each of the 25 subintervals we built the enclosures of the map of the stages and an invariant set in interval arithmetic, and obtained an upper bound $q^+_i$ on $q$ for all chain lengths $n\ge2$ and all pins of the box (the values at the end of the chain). The results are the left column of Table 2.

The values in the table (rounded up at 9 digits) increase as $\hbar$ decreases, with a bulge only at the two at the upper end. The limiting place is the cell where the value at the end of the chain lies just below the wall $0$. It is exactly the place in §02 where "the corner at the wall is exactly 1".

The outer chain of the seam of the ring (10-07 §03) is a chain moving in a region of fixed sign, and mapped to $(-\infty,0]$ by reflection it becomes the same type as Example 1. But there is no lower wall $-x_c$ as in the box of the bridge, so the certificate of Example 1 cannot be used as it is. We swapped the grid of the same machinery and closed it in two stages.

1. The chain conditioned on a box. For a chain conditioned on a finite box for each subinterval ($[-7/5,0]$ on the upper half, $[-6/5,0]$ on the lower half), the upper bound on the whole window is $0.998888525$ Computer-assisted. As it stands, four assumption rows are needed to pay separately for configurations that leave the box.
2. The unconditioned chain. Widen the box to $[-3,0]$, and put the contribution of the tail $(-\infty,-3]$ into the remainder of the interval arithmetic by a tangent upper bound from the convexity of the tail. The upper bound on the tail variance, in a form that pushes the law onto a single row at the end of the tail, is $\le0.357608022$ at every $\hbar$ (within $\lt5.25$ needed for convexity and $\le1$ needed for the correlation inequality). Pins deeper than $-3$ are covered by a closed-form upper bound, $\le0.592898559$. The results are the right column of Table 2, with maximum $0.998888530$ Computer-assisted (all pins $p\le0$, evaluation points $s\le0$, end value $z_0=-1$; (lim), (END_rand) and regularity are Assumption).

Comparing the two columns, the upper bound for the bridge bulges at the two at the upper end, while that for the ring is smallest on the third subinterval and then increases monotonically. At the lower end the ring is slightly closer to 1 (difference $3.4\times10^{-5}$), and the order of the floating-point point values (the ring closer to 1) appears in the upper bounds as well. Each row of the unconditioned chain is higher than the corresponding row of the conditioned chain by only $2.4\times10^{-9}$–$6.7\times10^{-7}$, with the same limiting place and shape.

The boundary stage is not covered. The claim of the right column is a claim for pins $p\le0$. In configurations where the lump touches the end of the window, the pin of the first outer stage falls in $(0,\tfrac12)$, and there the floating-point reading is $q\approx1.004〜1.045$ Reading. It is a single finite stage, so it does not break the finiteness of the construction, but when citing the right column of Table 2 the condition "pin $\le0$" cannot be dropped.

The correctness of the interval-arithmetic scripts themselves has not been formally verified. Instead they pass the following checks. All are checks to see "whether what we think we checked has drifted from what we wanted to check".

• Cross-check with another implementation. On every subinterval of Example 1, we ran the map of the stages by a floating-point recursion separate from the interval arithmetic, at three values of $\hbar$ (the two ends and the midpoint of the subinterval), and counted whether its values fell inside the interval enclosures at every stage and every grid point (75 runs, 0 misses). For the unconditioned chain of the ring, the same check at one $\hbar$ per subinterval (25 runs, 0 misses).
• Cross-check with point values. The floating-point point values obtained from the transfer matrix (26 ends) all lay below the upper bound of the subinterval containing that end (the smallest difference, at the lower end of the window, was $2.85\times10^{-4}$).
• Positive control. Whether the machinery reproduces the answer where it is known in closed form. For the pure Gaussian chain (variance per stage $v_k=(k-1)/k$, mean $m_k(s)=(k-1)s/k$, neither depending on $\hbar$), every point fell inside the enclosures with $\hbar$ kept as an interval. With the width of the interval of $\hbar$ set to 0, it gave the same values as the machinery at a point $\hbar$ to order $10^{-12}$. The unconditioned machinery for the ring reproduced the limiting place and shape of the version conditioned on a box on the same subintervals, with values within an upward difference of order $10^{-8}$ (they are not the same chain, so this is a check of reproduction, not agreement).
• Negative control. Whether the machinery rejects claims that should not hold. We confirmed that lowering the target upper bound at the limiting cell by $10^{-7}$ makes the Lean check fail to close, that replacing one entry of the table by 1 makes $\lt1$ on the whole window fail to close, and that setting the tail variance above the convexity line stops the tail stage.
• Pre-registration. Before running the computations, we wrote down the expected range of values, the limiting place, and the pass lines of the positive and negative controls, and recorded after the results whether they were right. In Example 1 we expected 60–120 subintervals and 25 sufficed (wrong), and the limiting place coming at the lower end of the window was right. That a prediction was wrong does not weaken the result, but it is a record that the pass lines were not moved after seeing the results.

The Lean column attached to computer-assisted results splits into the following three layers.

1. The algebraic core. The monotonicity of the linear-fractional function of Lemma TAU (mobius_between), the tilting identity (shear_identity), the inequality of Lemma DVτ (dvtau_pos), and the algebra of passing from the cover to the whole window (cover_le, assumption: $f\le c$ on each subinterval).
2. Recomputation of cells. From the input values output by the interval arithmetic (exact values of the floating-point numbers) and the rational ends of the subintervals, for the limiting cells and randomly chosen cells (46 in Example 1, 23 in the conditioned version for the ring), the formula for the upper bound at the last stage was recomputed inside Lean, closing "at most the interval-arithmetic value + $2\times10^{-9}$". This is not verification of every cell (a few dozen out of more than several million cells in one subinterval).
3. Assembly of the table. win_qfree_window_le_of_interval_table (Example 1), unc_window_lt_one_of_table (Example 2) and vt_window_of_table (tail variance) place as an assumption "$q(\hbar)\le q^+_i$ for every $\hbar$ in each subinterval" (the table of outputs of interval arithmetic; $q$ is an abstract function), and give as conclusion "$q\le\max_iq^+_i\lt1$ for every $\hbar$ in the window".

Outside Lean lie the map of the stages (the interval evaluation of Lemmas TAU, SH2 and DVτ), quadrature, the invariant sets, the layers of the formula for the upper bound on $q$, and the choice of evaluation points. So the machine-checking column guarantees "if the outputs of the interval arithmetic are correct, the conclusion on the whole window is correct as algebra", and "the outputs of the interval arithmetic are correct" rests on the premises of §03 and the checks of §07.

When the upper bound from interval arithmetic exceeds 1, all one can say is "this construction produces no certificate", not "the true value exceeds 1". We distinguish two cases.

(a) An example where it fails on the side of the tool. On the subinterval of width 10% in Table 1, the version with first-order tilting only gave the upper bound $1.00114$. On the same subinterval the version with second-order tilting shows the true value is $\le0.997808483$, so this "no" comes from the width of the tool (having put the curvature of the true $m$ in $\hbar$ into the interval). It is the kind of "no" that disappears with finer subintervals or a higher order of expansion.

(b) An example where it fails on the side of the object — the inner chain of the ring. For the stages inside the site window of the ring (the inner chain), measuring $q_{\rm in}$ by floating-point transfer gave $1.2707／1.2765／1.2421$ at $\hbar=3\cdot10^{-3}／10^{-3}／3\cdot10^{-4}$ Reading, moving upwards as the grid was refined. The limit is set by the stage with the pin at the edge of the far wall of the lump box, the corner where the wall force points out of the box (classical value $1.2857$) (10-07 §03). Here, even building interval machinery is not expected to give $q^+\lt1$. What it would give is only a finite upper bound $\bar q=\max(q_{\rm in},1)\approx1.3$. This "no" is of a kind that does not disappear however fine the tool is made, and it can only be absorbed on the side of the construction (making a form that does not need $q_{\rm in}\lt1$, or paying the coefficient $\bar q^{16}$).

When reading a computer-assisted result and seeing a report that the upper bound exceeded 1, check whether (a) or (b) is what is written.

What it does not say. (i) $\hbar$ outside the window $[3\cdot10^{-4},3\cdot10^{-3}]$. As seen in §02, $q$ approaches 1 as $\hbar\to0$, so the further the window is extended downwards, the finer the subintervals and grid must be, and no finite computation can cover the whole of $\hbar\to0$. The power form of H is a statement as $\hbar\to0$, so that is work for paper asymptotics. (ii) Anything outside the model on the lattice $\varepsilon=\tfrac12$ (the difference from the continuum path measure). (iii) Regularity (smoothness of eigenfunctions and conditional expectations) and the inputs of the sector framework. (iv) The boundary stage of Example 2 (pin $\in(0,\tfrac12)$). (v) Condition (H2) itself (10-07 §06).

This part is a study with Assumption H at its axis, and within it computer assistance is used as a tool that raises individual inequalities inside the window from floating-point readings to inequalities. Other views are treated in Part 11.

What this chapter can say

Sources and reproduction

Words used in this chapter — computer-assisted, interval arithmetic, outward rounding, loss of dependence, expanding about the centre, Stein-kernel ratio, chain condition, subinterval, tilting, invariant set, cross-check, positive and negative controls, pre-registration, boundary stage. Their meanings are in A-02 Glossary.

Next chapter to read: 10-09 The sector framework and the three strands of route 5 — states the five steps of the sum over sectors and the closing condition, the derivation of the needed value, how far the three strands that attacked the one remaining proposition got, and the common wall, the shortfall of the curvature at one site at the top.

← 10-07 The map of (H2) — seven routes and the seam of the ringContents10-09 The sector framework and the three strands of route 5 →