2026-10-09 · chapter Yang–Mills and the mass gapPart 10 Towards a proof of the mass gap — building the first step of the staircasethe integrated table, the dependency graph, bands of the range of ħ · Kiichi, Shiori and Rin

The whole book　Contents and reading orders

The integrated table and the dependency graph

What this chapter shows — For the four conditions (H1)–(H4) of the first step, we put every row of the tables of the five grades of 10-05, 10-06, 10-07, 10-09 and 10-11 into one table, and renumber the five dependency graphs and join them into one. We put it in a form in which readers can check by the rule of numbering (the number of a premise is smaller than the number of a conclusion) that there is no circle, and we see in figures where the computer-assisted rows lie on the road to the conclusion, and that there is still no $\hbar$ at which all rows are in place together.

Prerequisite chapters — 10-05 §07 (the format of the dependency graph), 10-06 §05, 10-07 §05, 10-09 §07, 10-11 §08 (the table of each condition), 10-00 §01 (the labels of the five grades).

Said first — The level is [Y3]. The integrated table is a map of "how far things are shown, and where assumption begins"; it is not a ruler for measuring progress. This part places Assumption H at the axis of the study, and this chapter lays out on one sheet the whole construction of its first step.

The order of this chapter

How the integrated table is made — the rules for putting five tables on one sheet, how identical rows are merged, the meaning of the columns
The integrated table — every row of the first step (Table 1), and the number of rows per grade (Table 2)
The dependency graph — the trunk (Figure 1) and the whole, how to check that there is no circle, and that the assumption rows do not contain the quantity of the conclusion
The family of bridges — Proposition L (one-dimensional version) and Proposition B (multi-dimensional version)
The position of the computer-assisted rows — what is on the road to the conclusion and what is not
There is no $\hbar$ at which all rows are in place — bands of the range (Figure 2, Table 4), and what is needed to bring them into line
The rows needed to reach the power form of H — two ways of supporting the row of the core (Table 5)
A note on how to read it — a map, not a fraction

How the integrated table is made — putting five tables on one sheet

The claim of the first step is Proposition 4.5 (10-05 §04): on conditions (H1)–(H4) and the premise rows, $C_P\le K\xi^2S_0/\hbar$ , and hence the power form of H, $\ln C_P/\ln\xi\to2$ . Each of the four conditions is written in its own chapter as a table of rows in the five grades (Proved here, Cited, Computer-assisted, Reading, Assumption) and as a dependency graph of numbered nodes. In this chapter we put them on one sheet by the following rules.

Count by rows. The unit is each row of the tables, not the name of a condition (whether (H1) is "closed"). This is because it is usual for rows with proofs and assumption rows to be mixed within one condition.
Make identical rows one. When the same statement appears in two chapters, we make it one row and write the nodes of both chapters in the source column. For example, [14] of 10-05 and [19] of 10-11 are both Proposition H3, and row LSW of 10-07 and [06] of 10-09 are both the remaining single proposition (LS_W♭). Row (T0′_P) of 10-05 ([04]) is supported in 10-11 by the pair of Proposition CORE3 and the local term, and in 10-07 and 10-09 by the lower bound of the core on the sector side, so we made it one node with an "or" of the two ways of support.
Rows left out. The rows of the list of detour plans (10-10) are not included, because none of them is a premise of any conclusion of the present construction. Of the rows of 10-04, the uniqueness of the measure is included in the common premise row P0, and the remaining spectrum of the fluctuation operator (of Pöschl–Teller type) is included as a single explanatory row.
Line up the family of bridges. Proposition L (10-04 §04) and Proposition B (10-01 §06) are the one-dimensional and multi-dimensional versions of the same bridge, "the relaxation time of the path measure is at least the square of the correlation length", so we included them as a family of adjacent nodes (§04). The other rows of Table 8 of 10-01 (H↑, H↓ and the rereading of mass, the chain, the version with discrete time, the step of infinite volume) do not enter the road to the conclusion of the first step, so they stay in the graph of 10-01.

The columns of Table 1 are as follows. No. is the number of the node in the dependency graph of §03; Symbol is the short name of the row; Grade is the label of the five grades; Range of $\hbar$ is what the row speaks about (nodes, window, three points, independent of $\hbar$ , $\hbar\to0$ , or "—" for not shown at any $\hbar$ ); Condition is which condition the row belongs to; Premise of which conclusion gives the numbers of the nodes that take the row as a direct premise, and whether following the edges of implication reaches the final conclusion (the power form of H); Source gives the tables and graph nodes of each chapter. Machine checking (Lean theorem names and assumptions) is placed under each row of the graph in §03.

The integrated table — every row of the first step

Table 1 is divided into five blocks by grade (within a block, in the order of the graph numbers). The smaller the number, the more it is a leaf (Assumption, Cited, Computer-assisted, Reading); the larger, the more it is a step of the construction; the last, [111], is the power form of H.

Table 1 The integrated table (every row of the first step. Numbers are the node numbers of the dependency graph in §03, and the order of the table is the same as the graph. "To the power form of H" is whether following the edges of implication from the row reaches the conclusion [111])
No.	Symbol	Content (one line)	Grade	Range of ħ	Condition	Premise of which conclusion	Source (chapter nodes)
Assumption Assumption rows (put without proof) (30 rows)
[001]	P0	Uniqueness of the measure at T=∞, Markov property, extension from local functions, the limit step, regularity	Assumption	—	Common	[071][073][077][081][106]. To the power form of H: reaches	10-05 [01], 10-11 [01], 10-04 §01
[002]	TUBE	(H2tube) Poincaré for the tube, uniform in tube length ≤ Cξ	Assumption	—	(H2)	[075]. To the power form of H: reaches	10-05 [03], 10-11 [04]
[003]	KG	(KG) The box gap of the reduced kink gas is of the Glauber type	Assumption	—	(H4)	[075]. To the power form of H: reaches	10-05 [05], 10-11 [05]
[004]	GLA	Closed formula for the gap of the Glauber box with fixed ends (original source bibliographic only)	Assumption	—	(H4)	Premise of no node. Part of the content of (KG) (a reading not made an independent node in the graph)	10-11 Table 6 GLA
[005]	X	(X) Cross term ℰ_Y(E[f\|Y]) ≤ (1+χ)ℰ(f), χ uniform	Assumption	—	(H4)	[075]. To the power form of H: reaches	10-05 [06], 10-11 [06]
[006]	MXA	(MIX_alt) The alternating maximal correlation between boxes c_alt < 1 is uniform	Assumption	—	(H3)	[072]. To the power form of H: reaches	10-05 [07], 10-11 [02]
[007]	MXC	(MIX_core) Upper bound for the alternating maximal correlation in the core c̄ < 1 (k ≥ 15)	Assumption	—	(H2)	[082]. To the power form of H: reaches	10-11 [07]
[008]	DSC	(ΔS_core) C_P ≤ c ħ^(−p) e^(ΔS/ħ) for core and window	Assumption	—	(H2)	[084]. To the power form of H: reaches	10-11 [08]
[009]	A5	Continuous version of Holley's comparison (the tail lemma)	Assumption	Six nodes	(H1)	[061]. To the power form of H: reaches	10-06 [05]
[010]	A10	The Poincaré–Miranda theorem (covering by boxes)	Assumption	(0,0.2]	(H1)	[063]. To the power form of H: reaches	10-06 [08]
[011]	A15	(T5) Regularity and density of the functions used	Assumption	—	(H1)	[060]. To the power form of H: reaches	10-06 [10]
[012]	B1	(T1b) Neighbour and end values > 2.5	Assumption	—	(H1)	[068]. To the power form of H: reaches	10-06 Table 2 B1
[013]	B2	(T1c) ħ between the nodes (in uniform form)	Assumption	Outside the nodes	(H1)	[068]. To the power form of H: reaches	10-06 Table 2 B2
[014]	B3	(T1c) ħ < 0.005 (in uniform form)	Assumption	—	(H1)	[068]. To the power form of H: reaches	10-06 Table 2 B3
[015]	B4	(T3d) End values of the two sites > 4	Assumption	—	(H1)	[068]. To the power form of H: reaches	10-06 Table 2 B4
[016]	B5	Transfer from the ring to scraps (with end values)	Assumption	—	(H1)	[068]. To the power form of H: reaches	10-06 Table 2 B5
[017]	IA	Premises of interval arithmetic (IEEE correct rounding, errors of sums, our own exp)	Assumption	—	(H2)	[042][043]. To the power form of H: does not reach	10-07 [01], 10-08 §03
[018]	LIM	(lim), (END_rand), regularity at the seam of the ring	Assumption	—	(H2)	[043][099][103]. To the power form of H: reaches	10-07 [02]
[019]	SM	The small assumptions of route 4 (inputs to the sectors)	Assumption	—	(H2)	[099]. To the power form of H: reaches	10-07 [04]
[020]	PROD	Proposition LSσ_W (construction of the upper bound for A_W of the product form)	Assumption	—	(H2)	[102]. To the power form of H: does not reach	10-07 [05]
[021]	LSWin	Input (LS_W) (the form of LSI for the marginals of site windows)	Assumption	—	(H2)	[087]. To the power form of H: reaches	10-09 [01]
[022]	PF	(PF_seg) (locality of volume on the bridge)	Assumption	—	(H2)	[089]. To the power form of H: reaches	10-09 [02]
[023]	BAR	Barta's row κ = 3/1000, b = 493/1000	Assumption	Independent of ħ	(H2)	[092]. To the power form of H: reaches	10-09 [03]
[024]	REG	The boundary term of Bochner and regularity of eigenfunctions	Assumption	—	(H2)	[090][092]. To the power form of H: reaches	10-09 [04]
[025]	PROX	The provisional rows of Proposition P5 (lifting assumption, Spec and others)	Assumption	—	(H2)	[096]. To the power form of H: does not reach	10-09 [05]
[026]	LSWb	(LS_W♭) A_W < A_max(ħ): the remaining single proposition of route 5	Assumption	—	(H2)	[099]. To the power form of H: reaches	10-09 [06], 10-07 [03]
[027]	K3	The next eigenvalue 3/4 of the fluctuation operator (of Pöschl–Teller type)	Assumption	Independent of ħ	Explanation	Premise of no node. An explanatory row that does not enter the premises of the conclusion of the first step	10-04 Table 3 K3
[028]	SPEC1	(A1) Discreteness of the spectrum, simplicity and positivity of the ground state (finite spatial lattice)	Assumption	—	Bridge	[107][108]. To the power form of H: does not reach	10-01 [06]
[029]	KU	(A3) κ uniform in β (the graduation of the multi-dimensional version)	Assumption	—	Bridge	[109]. To the power form of H: does not reach	10-01 [08]
[096]	P5	Proposition P5 (the lower end of the window, with a table of assumptions)	Assumption	8 nodes	(H2)	Premise of no node. A candidate to support the remaining single proposition (LS_W♭), with no edge of implication	10-09 [21]
Cited Rows citing an original source (10 rows)
[030]	MOB	Mobility of a single kink D = ħ/S₀ (at the level of the process)	Cited	ħ→0	(H4)	[075][105]. To the power form of H: reaches	10-05 [08], 10-11 [09]
[031]	BE	Bakry–Émery on convex domains (Kolesnikov–Milman)	Cited	Independent of ħ	(H2)	[076]. To the power form of H: reaches	10-11 [10]
[032]	A3	Muckenhoupt's bracket B ≤ C_P ≤ 4B	Cited	Independent of ħ	(H1)	[061]. To the power form of H: reaches	10-06 [03]
[033]	A4	Correlation inequality for MTP₂ (monotonicity of e, ħκ ≥ 0)	Cited	Independent of ħ	(H1)	[061]. To the power form of H: reaches	10-06 [04]
[034]	A6	Poincaré version of Helffer's criterion (Ledoux Proposition 3.1)	Cited	Independent of ħ	(H1)	[062]. To the power form of H: reaches	10-06 [06]
[035]	A12	Brascamp–Lieb (the cross κ_f, (T4))	Cited	Independent of ħ	(H1)	[063][064]. To the power form of H: reaches	10-06 [09]
[036]	BOC	Integral form of Bochner's formula (Ledoux Proposition 1.3)	Cited	Independent of ħ	(H2)	[090][092]. To the power form of H: reaches	10-09 [07]
[037]	SV	Singular-value representation of maximal correlation (Witsenhausen)	Cited	—	(H2)	Premise of no node. A representation used for how the reading values of Stage 2 are obtained	10-11 Table 6 SV
[038]	KR	For Gaussians, maximal correlation = linear canonical correlation (Kolmogorov–Rozanov)	Cited	—	(H2)	Premise of no node. Used for reading Proposition G	10-11 Table 6 KR
[039]	CORR	(A2) Formula for correlations of the stationary path measure	Cited	T=∞	Bridge	[108]. To the power form of H: does not reach	10-01 [07]
Computer-assisted Computer-assisted rows (4 rows)
[040]	A1	(T1a) Margin ħρ − 2ħκ ≥ 0.067 (neighbour and end in [0,2.5]²)	Computer-assisted	Six nodes	(H1)	[061]. To the power form of H: reaches (only by the road on which it joins the Assumptions B1–B5 at [068])	10-06 [01]
[041]	A9	(T3) λ_c ≥ 1.3×10⁻⁴ (ends in [0,4]²)	Computer-assisted	(0,0.2]	(H1)	[063][064]. To the power form of H: reaches (only by the road on which it joins the Assumptions B1–B5 at [068])	10-06 [07]
[042]	QF	q_free ≤ 0.998854904 (the chain outside the window)	Computer-assisted	Window	(H2)	[100]. To the power form of H: does not reach	10-07 [09]
[043]	QO	q_out ≤ 0.998888530 (the outer chain of the ring, pin ≤ 0)	Computer-assisted	Window	(H2)	[101]. To the power form of H: does not reach	10-07 [10]
Reading Reading rows (19 rows)
[044]	XI	ln ξ ≥ s/ħ (ξ ∝ ħ^½ e^(S₀/ħ)), the size of D/(Cξ)²	Reading	Three points, leading term	Conclusion	[084][111]. To the power form of H: reaches	10-05 [09], 10-11 [11]
[045]	CAL	c_alt = 0.731 / 0.410 / 0.138 (C = 2 / 4 / 8)	Reading	Model	(H3)	Premise of no node	10-11 [12]
[046]	MC2	Two-point maximal correlation of Stage 2 and B₂ (22.1 / 30.5 / 66.4)	Reading	Three points	(H2)	[082]. To the power form of H: reaches	10-11 [13]
[047]	CB	c̄_(≥15) ≤ 0.535 (measurement of a lower bound)	Reading	Three points	(H2)	[082]. To the power form of H: reaches	10-11 [14]
[048]	BIS	Bistability of the core on the box side, the fibres of the binary of the bump	Reading	Three points	(H2)	Premise of no node	10-11 [15]
[049]	CTL	Positive controls for Proposition H3 (pure Gaussian, Ising)	Reading	—	(H3)	Premise of no node	10-11 Table 6 CTL
[050]	KV	K ≈ 2.76 / 1.43 (C = 2), 1.78 (C = 4), and c_ff for free ends	Reading	Model	(H4)	Premise of no node	10-05 Kv, 10-11 CFF
[051]	DSV	ΔS⁰_* ≤ 1.4·10⁻² (ratio to 2S₀ ≤ 1.05·10⁻²)	Reading	ħ = 0	(H2)	Premise of no node	10-11 Table 6 DSV
[052]	N2	The constants of route 2 π_*, Λ, C_1D, gap_W, the inner chain of the bridge	Reading	Three points	(H2)	[102]. To the power form of H: does not reach	10-07 [06]
[053]	QIN	The inner chain of the ring q_in ≈ 1.24–1.28	Reading	Four points	(H2)	[101]. To the power form of H: does not reach	10-07 [07]
[054]	EDGE	The boundary stage q ≈ 1.004–1.045	Reading	Four points	(H2)	[101]. To the power form of H: does not reach	10-07 [08]
[055]	ELL	ℓ_min = 38.3 / 121.9 / 406.8	Reading	Three points	(H2)	[089][094]. To the power form of H: reaches	10-09 [08]
[056]	AWV	Upper bound of A_W 1857 / 2794 / 9106, lower bound 1.71 / 1.74 / 2.59	Reading	Three points	(H2)	Premise of no node	10-09 [09]
[057]	ST3	How far strand 3 got (reading 0.54 times, paper upper bound 10³ times)	Reading	Two points	(H2)	Premise of no node	10-09 [23]
[067]	A18	C ≤ 658 (numerical input)	Reading	Six nodes	(H1)	Premise of no node	10-06 Table 2 A18
[089]	S4	(Σ.4) ℓ_min does not depend on k	Reading	Three points	(H2)	[092]. To the power form of H: reaches	10-09 [14]
[094]	AM2	Needed value 25.1 / 90.3 / 312.3	Reading	Three points	(H2)	[097]. To the power form of H: does not reach	10-09 [19]
[097]	ST1	How far strand 1 got (1.4–5.5 times the needed value)	Reading	Three points	(H2)	Premise of no node	10-09 [22]
[102]	AV	A_W of the product form ≈ 2.5·10⁶–4.7·10⁷	Reading	Three points	(H2)	Premise of no node	10-07 [14]
Proved here Rows with proofs (elementary proofs, algebra on named premises) (48 rows)
[058]	A2	Lemma K2 (second-order Taylor of the tilt and the Hölder remainder)	Proved here	Independent of ħ	(H1)	[061]. To the power form of H: reaches	10-06 [02]
[059]	A8	(T2) The marginal of the kept sites is a nearest-neighbour chain	Proved here	Independent of ħ	(H1)	[062]. To the power form of H: reaches	10-06 [11]
[060]	A14	(T5) Decomposition of the variance	Proved here	Independent of ħ	(H1)	[065]. To the power form of H: reaches	10-06 [12]
[061]	MARG	The continuum statement of the margin λ	Proved here	Six nodes	(H1)	[062]. To the power form of H: reaches	10-06 [13]
[062]	A7	Gap on the coarse side ≥ λ (Gershgorin on the ring)	Proved here	Six nodes	(H1)	[065]. To the power form of H: reaches	10-06 [14]
[063]	A11	Nesting λ_S ≥ 2.3×10⁻⁵	Proved here	(0,0.2]	(H1)	[065]. To the power form of H: reaches	10-06 [15]
[064]	A13	(T4) v/ħ ≤ 5888	Proved here	(0,0.2]	(H1)	[065]. To the power form of H: reaches	10-06 [16]
[065]	A16	Algebra of rates C_P ≤ ε/t	Proved here	Six nodes	(H1)	[066][067]. To the power form of H: reaches	10-06 [17]
[066]	A17	Proposition H1: C ≤ 1.6×10¹⁰ (ring version)	Proved here	Six nodes	(H1)	[068]. To the power form of H: reaches	10-06 [18]
[068]	SEG	Conditions (H1), (H1seg): assembly when the B rows hold in uniform form	Proved here	(0,0.2]	(H1)	[075]. To the power form of H: reaches	10-05 [02], 10-11 [03], 10-06 §07
[069]	TP	Lemma TP (two projections)	Proved here	Independent of ħ	(H3)	[072][078][081]. To the power form of H: reaches	10-05 [10], 10-11 [16]
[070]	ESP	Efron–Stein for product measures (martingale differences and Jensen)	Proved here	Independent of ħ	(H3)	[071][075][081]. To the power form of H: reaches	10-11 [17]
[071]	BOX	Product inequality for boxes (conditional independence of even boxes)	Proved here	Independent of ħ	(H3)	[072]. To the power form of H: reaches	10-05 [11], 10-11 [18]
[072]	H3	Proposition H3: C_P ≤ (1+1/n)C_box/(1−c_alt)	Proved here	Independent of ħ	(H3)	[105]. To the power form of H: reaches	10-05 [14], 10-11 [19]
[073]	DEC	Decomposition of the variance and splitting into a product on the fast side	Proved here	Independent of ħ	(H4)	[075]. To the power form of H: reaches	10-05 [12], 10-11 [20]
[074]	KGC	c_kg = C²+π² (algebra of the limit of the closed formula)	Proved here	Independent of ħ	(H4)	[075]. To the power form of H: reaches	10-05 [13], 10-11 [21]
[075]	H4	Proposition H4: C_box ≤ C_loc + (1+χ)C_kg	Proved here	Independent of ħ	(H4)	[104]. To the power form of H: reaches	10-05 [15], 10-11 [31]
[076]	BV	Lemma BV (convexity for k ≤ 7)	Proved here	Independent of ħ	(H2)	[078][081][082]. To the power form of H: reaches	10-11 [22]
[077]	MR	Lemma MR (reduction to the ends)	Proved here	Independent of ħ	(H2)	[078]. To the power form of H: reaches	10-11 [23]
[078]	TB	Lemma TB (two blocks for 8 ≤ k ≤ 14)	Proved here	Independent of ħ	(H2)	[082]. To the power form of H: reaches	10-11 [24]
[079]	G	The ratio of Proposition G (geometric series)	Proved here	Independent of ħ	(H2)	Premise of no node	10-11 [25]
[080]	RR	Example in which two-point quantities cannot bound the alternating maximal correlation	Proved here	Independent of ħ	(H2)	Premise of no node	10-11 [26]
[081]	BET	Inequality of form (β) (k ≥ 15)	Proved here	Independent of ħ	(H2)	[082]. To the power form of H: reaches	10-11 [27]
[082]	CORE3	Proposition CORE3: three stages for the constant of the core	Proved here	Three points	(H2)	[103]. To the power form of H: reaches	10-11 [28]
[083]	PHY	The ends of the core of the sector framework are only on the side of the well	Proved here	Independent of ħ	(H2)	Premise of no node	10-11 [29]
[084]	CLOC	The local term vanishes as ħ→0	Proved here	ħ→0	(H2)	[103]. To the power form of H: reaches	10-11 [30]
[085]	S1	(Σ.1) Sum over sectors	Proved here	Independent of ħ	(H2)	[087]. To the power form of H: reaches	10-09 [10]
[086]	S2	(Σ.2) Gibbs variational inequality	Proved here	Independent of ħ	(H2)	[087]. To the power form of H: reaches	10-09 [11]
[087]	S3	(Σ.3) Localisation component by component	Proved here	Independent of ħ	(H2)	[092]. To the power form of H: reaches	10-09 [12]
[088]	SK	The scalar form is not uniform in k	Proved here	Independent of ħ	(H2)	Premise of no node	10-09 [13]
[090]	R1	Localised Bochner	Proved here	Independent of ħ	(H2)	[094]. To the power form of H: does not reach	10-09 [15]
[091]	R2	Optimisation of the Gibbs tilt	Proved here	Independent of ħ	(H2)	[094]. To the power form of H: does not reach	10-09 [16]
[092]	S5	(Σ.5) Composition and the closing condition	Proved here	Independent of ħ	(H2)	[093][099]. To the power form of H: reaches	10-09 [17], 10-07 [11]
[093]	AMX	The formula for the needed value A_max	Proved here	Independent of ħ	(H2)	[094]. To the power form of H: does not reach	10-09 [18]
[095]	THR	If the thresholds disagree, ℓ = 0	Proved here	Independent of ħ	(H2)	Premise of no node	10-09 [20]
[098]	WALL	At the single site at the top, diagonal dominance fails by ¼	Proved here	Independent of ħ	(H2)	Premise of no node	10-09 [24], 10-07 W
[099]	COREP	A positive lower bound for the gap of the core, uniform in k (sector side)	Proved here	—	(H2)	[103]. To the power form of H: reaches	10-09 [25], 10-07 [15]
[100]	SWB	S_W of the bridge ≤ 1779.6	Proved here	Window	(H2)	[102]. To the power form of H: does not reach	10-07 [12]
[101]	SWR	S_W of the ring ≤ 122745	Proved here	Window	(H2)	Premise of no node	10-07 [13]
[103]	T0P	Row (T0′P): Poincaré for the core, uniform in core length and end values	Proved here	—	(H2)	[104]. To the power form of H: reaches	10-05 [04], 10-07 [16], 10-11 [28][30]
[104]	K4	K₄ does not depend on ħ	Proved here	ħ→0	(H4)	[105]. To the power form of H: reaches	10-11 [32]
[105]	P45	Proposition 4.5: C_P ≤ Kξ²S₀/ħ	Proved here	ħ→0	Conclusion	[110]. To the power form of H: reaches	10-05 [16], 10-11 [33]
[106]	BL	Family of bridges, one-dimensional version: Proposition L (R ≥ 1)	Proved here	Every ħ	Bridge	[110]. To the power form of H: reaches	10-05 [17], 10-04 §04
[107]	GS	Identity of the ground-state transformation	Proved here	Finite spatial lattice	Bridge	[108]. To the power form of H: does not reach	10-01 [11]
[108]	BB	Family of bridges, multi-dimensional version: Proposition B (C_P ≥ κξ²)	Proved here	Continuous time, T=∞	Bridge	[109]. To the power form of H: does not reach	10-01 [12]
[109]	LH	The lower half of the power for the multi-dimensional version	Proved here	ξ > 1	Bridge	Premise of no node	10-01 [17]
[110]	RB	1 ≤ R ≤ K′/ħ	Proved here	ħ→0	Conclusion	[111]. To the power form of H: reaches	10-05 [18]
[111]	PH	The power form of H: ln C_P / ln ξ → 2	Proved here	ħ→0	Conclusion	The final conclusion	10-05 [19]

Counting the rows by grade gives Table 2.

Table 2 The number of rows of Table 1 (by grade; the breakdown in the condition column is counted by rows, not by the names of conditions)
Grade	Rows	Main content
Assumption	30	The common premise P0, (H2^tube), (KG), (X), (MIX_alt), (MIX_core), (ΔS_core), B1–B5 extending (H1) beyond the nodes, the premises of interval arithmetic, the inputs to the sectors, the remaining single proposition (LS_W♭), Proposition P5 (with a table of assumptions) and others
Cited	10	Mobility of kinks, Bakry–Émery on convex domains, Muckenhoupt, MTP₂, Helffer's criterion, Brascamp–Lieb, Bochner, two representations of maximal correlation, the formula for stationary correlations
Computer-assisted	4	The margin of (H1) (six nodes), the gap of two sites, the chain outside the window, the outer chain of the ring
Reading	19	How the correlation length grows, maximal correlations and the values of the stages of the core, the constants of route 2, the inner chain, the rarity exponent, the needed value, the coefficient $K$ of the reduced model and others
Proved here	48	The assembly of Proposition H1, Lemma TP, the product over boxes, Proposition H3, Proposition H4, Proposition CORE3, the five stages of the sectors, Proposition 4.5, Proposition L, the algebra to the power form of H and others
Total	111	Breakdown by condition: (H1) 25, (H2) 57, (H3) 7, (H4) 9, common 1, family of bridges 7, conclusion 4, explanation 1

There are many (H2) rows in Table 2 because the row of the core of (H2) is built from two sides (the three stages on the box side and the five stages on the sector side); it does not mean that (H2) is further along than the others. Conversely, there are few (H3) rows because the construction of Proposition H3 is short and the remaining assumption rows are gathered into one, (MIX_alt). The number of rows counts where there are proofs and where assumptions remain; it does not measure how many of the four conditions are done (§08).

The dependency graph — joining five graphs into one

We turn the 111 rows of Table 1 into a list of nodes in the same format as 10-05 §07. The numbers of the premises to the right of "⟸" are always smaller than the number of the conclusion on the left. There is just one node, [103] (row (T0′_P)), for which either of two ways of support suffices, and there we write "(…) or (…)". The numbers in both brackets are smaller than [103], so the rule works in the same way.

The whole is long, so we first give Figure 1, which extracts only the trunk. The numbers in the trunk are the same as in the whole graph.

Figure 1 The trunk of the integrated graph (of all 111 nodes, only the nodes on the main roads to the conclusion [111]; numbers as in the whole)

[001] ASM P0     common premise (uniqueness, Markov property, extension, limit, regularity)
[002][003][005] ASM (H2tube), (KG), (X)
[006] ASM (MIX_alt)          [007][008] ASM (MIX_core), (ΔS_core)
[012]–[016] ASM B1–B5 ((H1) beyond the nodes, beyond the ends, to scraps)
[026] ASM (LS_W♭) the remaining single proposition
[040][041] CMP margin of (H1), gap of two sites (six nodes, (0,0.2])
[044] RDG ln ξ ≥ s/ħ
[066] PRV Proposition H1 (ring version, six nodes) ⟸ [065] (with [040][041] below it)
[068] PRV condition (H1), (H1seg) ⟸ [066][012][013][014][015][016]
[072] PRV Proposition H3 ⟸ [006][069][071]
[075] PRV Proposition H4 ⟸ [068][002][003][005][030][070][073][074]
[082] PRV Proposition CORE3 (core on the box side) ⟸ [007][046][047] …
[084] PRV the local term vanishes ⟸ [008][044]
[099] PRV lower bound of the core (sector side) ⟸ [026][092][019][018]
[103] PRV row (T0′P) ⟸ ([082][084]) or ([099][018])
[104] PRV K₄ independent of ħ ⟸ [103][075]
[105] PRV Proposition 4.5 ⟸ [030][072][104]
[106] PRV family of bridges, Proposition L (one-dim. version) ⟸ [001]    [108] Proposition B (multi-dim. version)
[110] PRV 1 ≤ R ≤ K′/ħ ⟸ [105][106]
[111] PRV power form of H ⟸ [044][110]

(side road) [042][043] CMP chain outside the window, outer chain of the ring → [100][101] S_W → [102] RDG A_W of the product form (stops here)

Open the whole graph (111 nodes)

[001] ASM P0     uniqueness of the measure at T=∞, Markov property, extension from local functions, the limit step, regularity   ħ: —
[002] ASM TUBE   (H2tube) Poincaré for the tube, uniform in tube length ≤ Cξ   ħ: —
[003] ASM KG     (KG) box gap of the reduced kink gas is of the Glauber type   ħ: —
[004] ASM GLA    closed formula for the gap of the Glauber box with fixed ends (original source bibliographic only)   ħ: —
[005] ASM X      (X) cross term ℰ_Y(E[f|Y]) ≤ (1+χ)ℰ(f), χ uniform   ħ: —
[006] ASM MXA    (MIX_alt) alternating maximal correlation between boxes c_alt < 1 is uniform   ħ: —
[007] ASM MXC    (MIX_core) upper bound for the alternating maximal correlation in the core c̄ < 1 (k ≥ 15)   ħ: —
[008] ASM DSC    (ΔS_core) C_P ≤ c ħ^(−p) e^(ΔS/ħ) for core and window   ħ: —
[009] ASM A5     continuous version of Holley's comparison (the tail lemma)   ħ: six nodes
[010] ASM A10    the Poincaré–Miranda theorem (covering by boxes)   ħ: (0,0.2]
[011] ASM A15    (T5) regularity and density of the functions used   ħ: —
[012] ASM B1     (T1b) neighbour and end values > 2.5   ħ: —
[013] ASM B2     (T1c) ħ between the nodes (in uniform form)   ħ: outside the nodes
[014] ASM B3     (T1c) ħ < 0.005 (in uniform form)   ħ: —
[015] ASM B4     (T3d) end values of the two sites > 4   ħ: —
[016] ASM B5     transfer from the ring to scraps (with end values)   ħ: —
[017] ASM IA     premises of interval arithmetic (IEEE correct rounding, errors of sums, our own exp)   ħ: —
[018] ASM LIM    (lim), (END_rand), regularity at the seam of the ring   ħ: —
[019] ASM SM     the small assumptions of route 4 (inputs to the sectors)   ħ: —
[020] ASM PROD   Proposition LSσ_W (construction of the upper bound for A_W of the product form)   ħ: —
[021] ASM LSWin  input (LS_W) (the form of LSI for the marginals of site windows)   ħ: —
[022] ASM PF     (PF_seg) (locality of volume on the bridge)   ħ: —
[023] ASM BAR    Barta's row κ = 3/1000, b = 493/1000   ħ: independent of ħ
[024] ASM REG    the boundary term of Bochner and regularity of eigenfunctions   ħ: —
[025] ASM PROX   the provisional rows of Proposition P5 (lifting assumption, Spec and others)   ħ: —
[026] ASM LSWb   (LS_W♭) A_W < A_max(ħ): the remaining single proposition of route 5   ħ: —
[027] ASM K3     the next eigenvalue 3/4 of the fluctuation operator (of Pöschl–Teller type)   ħ: independent of ħ
[028] ASM SPEC1  (A1) discreteness of the spectrum, simplicity and positivity of the ground state (finite spatial lattice)   ħ: —
[029] ASM KU     (A3) κ uniform in β (the graduation of the multi-dimensional version)   ħ: —
[030] CIT MOB    mobility of a single kink D = ħ/S₀ (at the level of the process)   ħ: ħ→0
[031] CIT BE     Bakry–Émery on convex domains (Kolesnikov–Milman)   ħ: independent of ħ
[032] CIT A3     Muckenhoupt's bracket B ≤ C_P ≤ 4B   ħ: independent of ħ
[033] CIT A4     correlation inequality for MTP₂ (monotonicity of e, ħκ ≥ 0)   ħ: independent of ħ
[034] CIT A6     Poincaré version of Helffer's criterion (Ledoux Proposition 3.1)   ħ: independent of ħ
[035] CIT A12    Brascamp–Lieb (the cross κ_f, (T4))   ħ: independent of ħ
[036] CIT BOC    integral form of Bochner's formula (Ledoux Proposition 1.3)   ħ: independent of ħ
[037] CIT SV     singular-value representation of maximal correlation (Witsenhausen)   ħ: —
[038] CIT KR     for Gaussians, maximal correlation = linear canonical correlation (Kolmogorov–Rozanov)   ħ: —
[039] CIT CORR   (A2) formula for correlations of the stationary path measure   ħ: T=∞
[040] CMP A1     (T1a) margin ħρ − 2ħκ ≥ 0.067 (neighbour and end in [0,2.5]²)   ħ: six nodes
                 Lean T1_margin_six_nodes (numbers), T1_node_margin (assumption: interval output)
[041] CMP A9     (T3) λ_c ≥ 1.3×10⁻⁴ (ends in [0,4]²)   ħ: (0,0.2]
[042] CMP QF     q_free ≤ 0.998854904 (the chain outside the window) ⟸ [017]   ħ: window
                 Lean win_qfree_window_le_of_interval_table (assumption: the table of interval-arithmetic output)
[043] CMP QO     q_out ≤ 0.998888530 (the outer chain of the ring, pin ≤ 0) ⟸ [017][018]   ħ: window
                 Lean unc_window_lt_one_of_table (assumption: the table of interval-arithmetic output)
[044] RDG XI     ln ξ ≥ s/ħ (ξ ∝ ħ^½ e^(S₀/ħ)), the size of D/(Cξ)²   ħ: three points, leading term
[045] RDG CAL    c_alt = 0.731 / 0.410 / 0.138 (C = 2 / 4 / 8)   ħ: model
[046] RDG MC2    two-point maximal correlation of Stage 2 and B₂ (22.1 / 30.5 / 66.4)   ħ: three points
[047] RDG CB     c̄_(≥15) ≤ 0.535 (measurement of a lower bound)   ħ: three points
[048] RDG BIS    bistability of the core on the box side, the fibres of the binary of the bump   ħ: three points
[049] RDG CTL    positive controls for Proposition H3 (pure Gaussian, Ising)   ħ: —
[050] RDG KV     K ≈ 2.76 / 1.43 (C = 2), 1.78 (C = 4), and c_ff for free ends   ħ: model
[051] RDG DSV    ΔS⁰_* ≤ 1.4·10⁻² (ratio to 2S₀ ≤ 1.05·10⁻²)   ħ: ħ = 0
[052] RDG N2     the constants of route 2 π_*, Λ, C_1D, gap_W, the inner chain of the bridge   ħ: three points
[053] RDG QIN    the inner chain of the ring q_in ≈ 1.24–1.28   ħ: four points
[054] RDG EDGE   the boundary stage q ≈ 1.004–1.045   ħ: four points
[055] RDG ELL    ℓ_min = 38.3 / 121.9 / 406.8   ħ: three points
[056] RDG AWV    upper bound of A_W 1857 / 2794 / 9106, lower bound 1.71 / 1.74 / 2.59   ħ: three points
[057] RDG ST3    how far strand 3 got (reading 0.54 times, paper upper bound 10³ times)   ħ: two points
[058] PRV A2     Lemma K2 (second-order Taylor of the tilt and the Hölder remainder)   ħ: independent of ħ
[059] PRV A8     (T2) the marginal of the kept sites is a nearest-neighbour chain   ħ: independent of ħ
[060] PRV A14    (T5) decomposition of the variance ⟸ [011]   ħ: independent of ħ
[061] PRV MARG   the continuum statement of the margin λ ⟸ [040][058][032][033][009]   ħ: six nodes
                 Lean T1_margin_six_nodes, T1_node_margin
[062] PRV A7     gap on the coarse side ≥ λ (Gershgorin on the ring) ⟸ [034][059][061]   ħ: six nodes
                 Lean ring_gershgorin (assumption: κ ≥ 0)
[063] PRV A11    nesting λ_S ≥ 2.3×10⁻⁵ ⟸ [041][010][035]   ħ: (0,0.2]
[064] PRV A13    (T4) v/ħ ≤ 5888 ⟸ [041][035]   ħ: (0,0.2]
                 Lean T4_paper_numeric (assumption: λ_c ≥ 1.3×10⁻⁴)
[065] PRV A16    algebra of rates C_P ≤ ε/t ⟸ [060][062][063][064]   ħ: six nodes
                 Lean H1_assembly (assumptions: seven named ones)
[066] PRV A17    Proposition H1: C ≤ 1.6×10¹⁰ (ring version) ⟸ [065]   ħ: six nodes
                 Lean H1_rate_paper_six_nodes (numbers)
[067] RDG A18    C ≤ 658 (numerical input) ⟸ [065]   ħ: six nodes
                 Lean H1_rate_numeric_six_nodes (numbers)
[068] PRV SEG    conditions (H1), (H1seg): assembly when the B rows hold in uniform form ⟸ [066][012][013][014][015][016]   ħ: (0,0.2]
[069] PRV TP     Lemma TP (two projections)   ħ: independent of ħ
                 Lean two_proj_var (assumption: A+B ≤ (1+c)V)
[070] PRV ESP    Efron–Stein for product measures (martingale differences and Jensen)   ħ: independent of ħ
[071] PRV BOX    product inequality for boxes (conditional independence of even boxes) ⟸ [001][070]   ħ: independent of ħ
[072] PRV H3     Proposition H3: C_P ≤ (1+1/n)C_box/(1−c_alt) ⟸ [006][069][071]   ħ: independent of ħ
                 Lean box_two_family, box_shift_average
[073] PRV DEC    decomposition of the variance and splitting into a product on the fast side ⟸ [001]   ħ: independent of ħ
[074] PRV KGC    c_kg = C²+π² (algebra of the limit of the closed formula)   ħ: independent of ħ
                 Lean kg_constant (assumption: Cξ ≠ 0)
[075] PRV H4     Proposition H4: C_box ≤ C_loc + (1+χ)C_kg ⟸ [068][002][003][005][030][070][073][074]   ħ: independent of ħ
                 Lean H4_two_scale, H4_gap_form
[076] PRV BV     Lemma BV (convexity for k ≤ 7) ⟸ [031]   ħ: independent of ħ
                 Lean lemma_BV
[077] PRV MR     Lemma MR (reduction to the ends) ⟸ [001]   ħ: independent of ħ
[078] PRV TB     Lemma TB (two blocks for 8 ≤ k ≤ 14) ⟸ [069][076][077]   ħ: independent of ħ
                 Lean tb_far, tb_adjacent, tb_range
[079] PRV G      the ratio of Proposition G (geometric series)   ħ: independent of ħ
                 Lean gauss_mode0, one_sub_phi
[080] PRV RR     example in which two-point quantities cannot bound the alternating maximal correlation   ħ: independent of ħ
                 Lean rareR_pair, rareR_joint
[081] PRV BET    inequality of form (β) (k ≥ 15) ⟸ [001][069][070][076]   ħ: independent of ħ
                 Lean core_uniform_L5 (assumption: the measured c̄)
[082] PRV CORE3  Proposition CORE3: three stages for the constant of the core ⟸ [007][046][047][076][078][081]   ħ: three points
                 Lean three_stage (assumption: the upper bound of each stage)
[083] PRV PHY    the ends of the core of the sector framework are only on the side of the well   ħ: independent of ħ
                 Lean p5_end_not_negative
[084] PRV CLOC   the local term vanishes as ħ→0 ⟸ [008][044]   ħ: ħ→0
                 Lean cloc_term_poly, cloc_term_vanishes
[085] PRV S1     (Σ.1) sum over sectors   ħ: independent of ħ
                 Lean var_split_cells, cell_sum_sup
[086] PRV S2     (Σ.2) Gibbs variational inequality   ħ: independent of ħ
                 Lean gibbs_ln2_cell
[087] PRV S3     (Σ.3) localisation component by component ⟸ [021][085][086]   ħ: independent of ħ
                 Lean comp_sum_le
[088] PRV SK     the scalar form is not uniform in k   ħ: independent of ħ
                 Lean scalar_not_uniform (assumption: p > 0)
[089] RDG S4     (Σ.4) ℓ_min does not depend on k ⟸ [022][055]   ħ: three points
[090] PRV R1     localised Bochner ⟸ [024][036]   ħ: independent of ħ
                 Lean negw_le_localized, bochner_localized
[091] PRV R2     optimisation of the Gibbs tilt   ħ: independent of ħ
                 Lean tilt_cost_le
[092] PRV S5     (Σ.5) composition and the closing condition ⟸ [023][024][036][087][089]   ħ: independent of ħ
                 Lean comp_close (assumptions: Barta, (Σ.3), Bochner)
[093] PRV AMX    the formula for the needed value A_max ⟸ [092]   ħ: independent of ħ
[094] RDG AM2    needed value 25.1 / 90.3 / 312.3 ⟸ [055][090][091][093]   ħ: three points
                 Lean judge_i_inside (assumption: the measured lower bound of ℓ)
[095] PRV THR    if the thresholds disagree, ℓ = 0   ħ: independent of ħ
[096] ASM P5     Proposition P5 (the lower end of the window, with a table of assumptions) ⟸ [025]   ħ: 8 nodes
                 Lean path5_conditional, p5_assembly
[097] RDG ST1    how far strand 1 got (1.4–5.5 times the needed value) ⟸ [094]   ħ: three points
[098] PRV WALL   at the single site at the top, diagonal dominance fails by ¼   ħ: independent of ħ
[099] PRV COREP  a positive lower bound for the gap of the core, uniform in k (sector side) ⟸ [026][092][019][018]   ħ: —
                 Lean comp_close
[100] PRV SWB    S_W of the bridge ≤ 1779.6 ⟸ [042]   ħ: window
[101] PRV SWR    S_W of the ring ≤ 122745 ⟸ [053][054][043]   ħ: window
                 Lean sw_inner_le (assumptions: q_in ≤ 13/10, q_out ≤ 0.998888530)
[102] RDG AV     A_W of the product form ≈ 2.5·10⁶–4.7·10⁷ ⟸ [020][052][100]   ħ: three points
[103] PRV T0P    row (T0′P): Poincaré for the core, uniform in core length and end values ⟸ ([082][084]) or ([099][018])   ħ: —
[104] PRV K4     K₄ does not depend on ħ ⟸ [103][075]   ħ: ħ→0
[105] PRV P45    Proposition 4.5: C_P ≤ Kξ²S₀/ħ ⟸ [030][072][104]   ħ: ħ→0
                 Lean H3_H4_compose (assumptions: (8), (12), D = ħ/S₀, n, ħ, S₀ > 0, c_alt < 1)
[106] PRV BL     family of bridges, one-dimensional version: Proposition L (R ≥ 1) ⟸ [001]   ħ: every ħ
                 Lean local_rayleigh_ratio_le_one (skeleton of the finite sum)
[107] PRV GS     identity of the ground-state transformation ⟸ [028]   ħ: finite spatial lattice
[108] PRV BB     family of bridges, multi-dimensional version: Proposition B (C_P ≥ κξ²) ⟸ [028][039][107]   ħ: continuous time, T=∞
                 Lean cont_ratio_closed, one_sided_bridge
[109] PRV LH     the lower half of the power for the multi-dimensional version ⟸ [029][108]   ħ: ξ > 1
                 Lean power_lower_half_of_bridge
[110] PRV RB     1 ≤ R ≤ K′/ħ ⟸ [105][106]   ħ: ħ→0
[111] PRV PH     the power form of H: ln C_P / ln ξ → 2 ⟸ [044][110]   ħ: ħ→0
                 Lean power_H_of_kink_ratio (assumptions: 0 < K, s, δ; 1 ≤ R ≤ K/ħ; s/ħ ≤ ln ξ)

How to check. There are three steps by which readers can check for themselves. (1) Look one by one at the rows of the whole graph that have "⟸", and check that the numbers on the right are all smaller than the number on the left. At [103], look at both brackets. (2) If this rule is kept in every row, the number strictly decreases each time a premise is followed, so you eventually reach a leaf (a row without "⟸") and never return to the original row. That is all there is to "there is no circle". (3) If even one edge is found that does not keep the rule, it is a candidate for a circle of dependence, and the text has to name which step takes the conclusion of which step as a premise. In the graph of this chapter there was no such edge (all edges of the 111 nodes were checked by comparing numbers).

The assumption rows do not contain the quantity of the conclusion. The rule of numbering does not prevent the form in which the conclusion has slipped into the content of an assumption row (the form that puts the conclusion as a premise). So we read the statements of the assumption rows one by one. The quantities of the conclusion are three: the Poincaré constant $C_P(\mu)$ of the whole measure at $T=\infty$ , the ratio $R=C_P/\xi^2$ , and the power $\ln C_P/\ln\xi$ . The 30 assumption rows fall into (i) properties of the measure ([001], [011], [018], [024]), (ii) constants of partial measures (scraps, tubes, cores, site windows: [002], [008], [012]–[016], [021], [022], [026]), (iii) quantities of correlation ([006], [007]), (iv) reduced models and comparisons of forms ([003], [004], [005]), (v) premises of computation and citation ([009], [010], [017], [019], [020], [023], [025], [096]), and (vi) the multi-dimensional version and explanatory rows ([027], [028], [029]); none of them contains $C_P(\mu)$ , $R$ or the power. The Poincaré constants contained in the rows of (ii) belong to the partial measures of scraps, tubes, cores and windows, not to the whole measure. This check is done by eye; machine checking does not replace it (10-13 §05).

The family of bridges — Proposition L and Proposition B

[106] Proposition L and [108] Proposition B are the one-dimensional and multi-dimensional versions of a sentence of the same form. Both say "for the path measure, the ceiling of the Rayleigh quotient of test functions local in time is the square of the correlation length", and from this come lower bounds for the relaxation time, $C_P\ge\xi^2$ (Proposition L) and $C_P\ge\kappa\xi^2$ (Proposition B).

Table 3 The two versions of the family of bridges
Version	Statement	Premises	Role in this part
One-dimensional version [106]	Proposition L: $R=C_P/\xi^2\ge1$ for the 0+1-dimensional double well	[001] (continuous time, $T\to\infty$ ; proof in 10-04 §04)	The left inequality of (14). Gives the lower half of the power form of H without conditions
Multi-dimensional version [108]	Proposition B: $C_P\ge\kappa\xi^2$ on a finite spatial lattice	[028] assumption on the spectrum, [039] formula for correlations, [107] ground-state transformation (10-01 §06)	[109] the lower half of the power for the multi-dimensional version (with the uniformity of the graduation [029]). Does not enter the road to the conclusion [111] of the first step

Putting the two side by side, one reads in the same form that the content of Assumption H is only "the upper half". The lower half is given automatically by the bridge (the one-dimensional version needs only the premise [001]; the multi-dimensional version needs [028][039] and the uniformity of the graduation [029]), and what conditions (H1)–(H4) take on is the upper half $C_P\le K\xi^2S_0/\hbar$ . For the multi-dimensional version to apply to the four-dimensional Wilson measure, the rows of discrete time, infinite volume and graduation remain ([08][09][10] of the graph of 10-01).

The position of the computer-assisted rows — what is on the road to the conclusion and what is not

For the four "Computer-assisted" rows of Table 1, we look at the road to the conclusion [111].

[040] the margin, [041] the gap of two sites ((H1)). There is a road [061] the continuum statement of the margin → [062], [063], [064] → [065] the algebra of rates → [066] Proposition H1 → [068] condition (H1) → [075] Proposition H4 → … → [111]. But it is only the road on which they join the assumption rows B1–B5 ([012]–[016]) at [068]; there is no road that reaches the conclusion without passing through [068]. The computer assistance at the six nodes becomes a premise of the conclusion only when combined with the assumption rows extending it beyond the nodes, beyond the ends and to scraps.
[042] the chain outside the window, [043] the outer chain of the ring ((H2), route 1 and route 6). [042] → [100] $S_W$ of the bridge → [102] $A_W$ of the product form (Reading) stops there, and [043] → [101] $S_W$ of the ring stops there. Neither is on the road to the conclusion. This is because the value of $A_W$ of the product form lies outside the needed value that the remaining single proposition [026] asks for (10-09 §03).

These two rows turn the contraction of the chains into inequalities over the whole window $\hbar\in[3\cdot10^{-4},3\cdot10^{-3}]$ , and they stand as results of computer assistance within the window in their own right (10-08). But in the present construction they are not used as premises of the conclusion. They enter the road when an upper bound for $A_W$ not of the product form satisfies [026] and the ratio of the chain $q$ enters that upper bound (10-07 §06). Put the other way round, the number of computer-assisted rows does not show how close one is to the conclusion.

There is no $\hbar$ at which all rows are in place

We overlay the range of $\hbar$ of each row on one number line (Figure 2). Assumption rows whose range is "—" ([002], [003], [005], [006] and others, most of the 30 assumption rows) are rows not shown at any $\hbar$ , so they are not drawn; only the rows that have a range are drawn.

Figure 2 Bands of the range of

\hbar

(the horizontal axis is

\log_{10}\hbar

, from

10^{-4}

1

). Solid lines and circles are computer-assisted, dashed lines are assumptions, squares are readings, and small dots are the node values of a proposition with a table of assumptions

There are three things to read from Figure 2. (a) The computer assistance for the margin of (H1) is at six nodes with $\hbar\ge0.005$ , and the smallest node $0.005$ is larger than the upper end of the window $3\cdot10^{-3}$ (the "gap" between the vertical dotted lines in the figure). (b) Proposition P5 is point values at 8 nodes at the lower end of the window, $[3\cdot10^{-4},10^{-3}]$ , and a little beyond $10^{-3}$ the two conditions can no longer hold together in the same window (the reading that they do not hold together at $1.35\cdot10^{-3}$ , 10-09 §05). (c) The six nodes of (H1) and the 8 nodes of P5 do not meet, and there is no node of (H1) inside the window. Moreover, the assumption rows whose range is "—" ((H2^tube), (KG), (X), (MIX_alt) and others) remain assumptions at every $\hbar$ . Therefore there is still not a single $\hbar$ at which all the rows of the four conditions are in place together.

Table 4 Three kinds of range of $\hbar$ (do not mix them; four kinds together with the three points of 10-04 §07)
Kind	Range	Which rows	Grade
The nodes of (H1)	$\{0.2,0.1,0.05,0.02,0.01,0.005\}$	[040], [061]–[066]	Computer-assisted, Proved here (between the nodes and below $0.005$ , Assumption of [013][014])
The computer-assisted window	$[3\cdot10^{-4},3\cdot10^{-3}]$ (25 subintervals)	[042], [043], [100], [101]	Computer-assisted, Proved here
The range of Proposition P5	8 nodes in $[3\cdot10^{-4},10^{-3}]$ (no enclosure between the nodes)	[096]	Assumption (a proposition with a table of assumptions)
The three points of reading	$\hbar=3\cdot10^{-3}／10^{-3}／3\cdot10^{-4}$	[044], [046], [047], [052]–[056] and others	Reading

What is needed to bring them into line. To bring them into line over the same range of $\hbar$ , one of the following is needed.

Extend (H1) to $\hbar\le10^{-3}$ . That is, show row [014] ( $\hbar\lt0.005$ ). The type of computer assistance by subintervals cannot be used, because with a fixed ratio the number of subintervals, $\ln(0.005/\hbar)/\ln r$ , grows without bound as $\hbar\to0$ ; a paper argument uniform as $\hbar\to0$ is needed ((H1-b) of 10-06 §07).
Extend P5 to $\hbar\ge0.005$ . This corresponds to route 7 (outside the window), a route decided to be outside the scope of this part (10-07 §02). The form of P5 itself also stops at $1.35\cdot10^{-3}$ .

Whichever is done, they only come into line over a fixed range. The power form of H is a statement about $\hbar\to0$ , so in the end every row has to be stated in a form uniform as $\hbar\to0$ , and computer assistance in the window alone cannot reach it. Outside the window, paper asymptotics are needed. The assumption rows whose range is "—" remain at the stage before ranges are brought into line: first being shown at a single $\hbar$ .

The rows needed to reach the power form of H — two ways of supporting the row of the core

Following the graph from the conclusion [111] in the direction of the premises picks up all the leaves the conclusion needs. The only fork is the "or" at [103] (row (T0′_P)), so there are two required sets of leaves (Table 5). This applies to the graph of the first step the way of thinking that counts the sets that reach the conclusion when the assumption rows are put as "provisionally true" (for the list of walls on the side of the four-dimensional lattice, see 10-02 §06).

Table 5 The leaves needed for the conclusion [111] (for each way of supporting [103]. In either set, every row listed is needed)
Grade of leaf	Support A: the core on the box side ([082] and [084])	Support B: the core on the sector side ([099])
Assumption	15 rows: [001], [002], [003], [005], [006], [007], [008], [009], [010], [011], [012]–[016]	20 rows: [001], [002], [003], [005], [006], [009], [010], [011], [012]–[016], [018], [019], [021], [022], [023], [024], [026]
Cited	[030], [031], [032], [033], [034], [035]	[030], [032], [033], [034], [035], [036]
Computer-assisted	[040], [041]	[040], [041]
Reading	[044], [046], [047]	[044], [055] (and [089], which depends on it)

What to read from Table 5. (1) The assumption rows common to both ways of support are the common premise [001], the rows inside the box [002][003][005], [006] between boxes, and [009]–[016] extending (H1). These remain whichever road is taken. (2) Support A puts the alternating maximal correlation of the core [007] and the action barrier [008] as assumptions, and needs the readings of Stages 2 and 3, [046][047], to be replaced by upper bounds. Support B puts the remaining single proposition [026] and the inputs to the sectors [019], [021], [022], [024] and Barta's row [023] as assumptions. (3) Both sets still contain "Reading" rows. For the conclusion to become unconditional, every "Assumption" row has to be replaced by a proof, and every "Reading" row by an upper bound (Proved here, Cited or Computer-assisted).

A note on how to read it — a map, not a fraction

The integrated table is a map that shows where in the claim of the first step there are proofs and where assumptions remain. A proportion such as "48 of 111 rows are Proved here" does not show progress. There are two reasons. One is that the rows do not have equal weight (the single row [001] holds everything from the uniqueness of the measure to regularity, while the single row [074] is the algebra of a sum of two terms). The other is that many of the "Proved here" rows are algebra that takes assumption rows as input, and as long as one assumption row remains, the conclusion stays conditional (the same as the note after Table 2 of 10-05).

When reading it as a map, the following order helps. (a) Follow the trunk of Figure 1 from the conclusion [111], (b) look at the required set of leaves in Table 5, and (c) trace the "Assumption" rows in it from the source column of Table 1 to the text of each chapter. What remains and its cost are laid out row by row of this table in 10-15.

This part places Assumption H at the axis of the study, and has built the upper half of the first step by dividing it into four conditions. This map, which puts the whole on one sheet, is also a map within that way of dividing. Other viewpoints are taken up in Part 11.

What this chapter can say

Can say	Cannot say
The integrated table putting the rows of the five chapters of the first step on one sheet (111 rows: Assumption 30, Cited 10, Computer-assisted 4, Reading 19, Proved here 48), and the dependency graph that keeps the rule of numbering on every edge (no circle)	Any of the 30 assumption rows. Hence the conclusion of Proposition 4.5 and the power form of H of the first step
That the statements of the assumption rows do not contain the quantities of the conclusion $C_P(\mu)$ , $R$ or the power (a check by reading the statements)	That the assumption rows are compatible with each other, or that none of them is false
The position of the four computer-assisted rows: the two rows of (H1) become premises of the conclusion only on the road where they join B1–B5, and the two rows of (H2) are not on the road to the conclusion	Carrying the computer-assisted results outside the window or to $\hbar\to0$
That there is no $\hbar$ at which all rows are in place together (by comparing ranges), and the two things needed to bring them into line	Either of the two things to bring them into line. Rows in a form uniform as $\hbar\to0$
That there are two required sets of leaves for the conclusion (Table 5)	Which of the two ways of support is easier

Sources and reproduction

Item	Kind	Source, tool
The statement, grade and range of each row of Table 1	This book	10-05 Table 2, 10-06 Table 2, 10-07 Table 4, 10-09 Table 5, 10-11 Table 6, 10-04 Table 3, 10-01 Table 8. The original sources of the cited theorems are in the source table of each chapter
Edges of the dependency graph	This book	The "⟸" of each chapter's dependency graph copied as it is, with identical rows merged (the rules of §01). The "or" at [103] comes from the notes on correspondence in 10-05, 10-07 and 10-11
Checking the rule of numbering, counting the rows, the required set of leaves	Text processing	A small script that, from data copying out the rows and edges of the table, compares the numbers on every edge, counts rows by grade, and collects leaves from the conclusion in the direction of the premises (not a mathematical computation)
Lean theorem names and assumptions	Lean	Under each row of the graph. The list of statements and the limits of checking are in 10-13

Terms used in this chapter — integrated table, dependency graph, node, leaf, trunk, the rule of numbering, circle of dependence, the form that puts the conclusion as a premise, family of bridges, way of support, required set of leaves, bands of the range of $\hbar$ (nodes, window, the range of P5, the three points of reading). Their meanings are in the A-02 glossary.

Next chapter: 10-13 Lean statements and the limits of machine checking — looks, through the list of bundles and examples, at what machine checking guarantees, "the conclusion follows from the propositions as written", and what it does not guarantee (the truth of the assumptions, the encoding of the objects, closing by putting the conclusion into a definition, circles of dependence).

Revision 2026-10-09: first edition.