2026-10-09 · chapter Yang–Mills and the mass gapPart 10 Towards a proof of the mass gap — building the first step of the staircaseLean, #print axioms, encoding of statements · Kiichi, Shiori and Rin

The whole book　Contents and reading orders

Lean statements and the limits of machine checking

What this chapter shows — We confirm, with the list of bundles of the first step, the convention that what machine checking (Lean) guarantees is only that "the conclusion follows from the propositions as written (the list of assumptions)", and that it guarantees neither that the assumptions are true nor that the real numbers inside Lean represent physical quantities. We look, through examples with their sources withheld, at two types that cannot be detected even when #print axioms stays within the three standard axioms (putting the conclusion into a definition, and a circle of dependence), and we give a procedure by which readers can inspect statements themselves.

Prerequisite chapters — A-04 Lean and machine checking (the meaning of the label "Lean"), 10-12 §03 (the dependency graph and the rule of numbering), 10-08 §08 (assemblies that put the output of interval arithmetic as an assumption). For how to read Lean itself, see the Lean guide.

Said first — The level is [Y2]–[Y3]. §01–§02 and §06 can be read at [Y2]. This part places Assumption H at the axis of the study, and Lean is used as a tool to check the algebraic steps of its construction. This chapter shows neither the mass gap nor the continuum limit.

The order of this chapter

What machine checking guarantees — the arrow from a list of assumptions to a conclusion (example: the composition of Proposition 4.5)
The three axioms and #print axioms — the criterion of cleanness, why native_decide is not used
The bundles of the first step — the number of theorems in each bundle, what algebra it is, how the assumptions are put (Table 1), the side of the four-dimensional lattice (Table 2)
Assumptions next to theorem names — the discipline of reading, and the fact that the layer of interval arithmetic is outside Lean
Four limits — the truth of the assumptions, the encoding of the objects, putting the conclusion into a definition, circles of dependence (Table 3)
A procedure for readers to inspect for themselves — six questions
Translating conventions — places where the same letter or the same name refers to different quantities (Table 4)
How the bundles are divided — by article, paper and subject

What machine checking guarantees — the arrow from a list of assumptions to a conclusion

Lean is a system in which a mathematical statement is written as a type and its proof as a term of that type, and a small core (the kernel) mechanically checks that the proof matches the statement (Lean guide 01). The rows in this book labelled "Lean" refer to theorems that have passed that check. The label guarantees only one thing.

The convention of this book

What is guaranteed in a row labelled "Lean" is that if all the assumptions written in the statement of the theorem hold, then the conclusion written there holds. It is not guaranteed that the assumptions hold, that the symbols in the statement represent the quantities of the text, or that the statement means the same as the claim in the text.

As an example, we copy the statement of the theorem for the composition of Proposition 4.5 (10-05 §04 Step 3).

theorem H3_H4_compose (CP Cbox n ca K4 C ξ D hbar S0 : ℝ) (hn : 0 < n) (hca : ca < 1)
    (hh : 0 < hbar) (hS : 0 < S0) (hD : D = hbar / S0)
    (hH3 : CP ≤ (1 + 1 / n) * Cbox / (1 - ca)) (hH4 : Cbox ≤ K4 * (C * ξ) ^ 2 / D) :
    CP ≤ (1 + 1 / n) * K4 * C ^ 2 / (1 - ca) * (ξ ^ 2 * S0 / hbar)

How to read it. Everything in the brackets of the first line is a real number (ℝ); CP and ξ are just real numbers with names. hH3 takes the conclusion of Proposition H3, $C_P\le(1+1/n)C_{\rm box}/(1-c_{\rm alt})$ , and hH4 the conclusion of Proposition H4, $C_{\rm box}\le K_4(C\xi)^2/D$ , as assumptions. What the theorem checked is the algebra by which (13) $C_P\le K\xi^2S_0/\hbar$ follows from these two and $D=\hbar/S_0$ . That CP is the Poincaré constant of the path measure at $T=\infty$ , and that the conclusions of Propositions H3 and H4 actually hold (that is, conditions (H1)–(H4) and the premise rows), are outside Lean.

This character of "only the arrow" is not a weakness but a premise of how it is used. Many of the "Proved here" nodes in the dependency graph (10-12 §03) are algebra that takes assumption rows as input, and Lean checks that this algebra has no copying errors or sign errors. Because what enters as an assumption is named in the statement, it can be cross-checked against the list of assumption rows (the integrated table).

The three axioms and `#print axioms`

On top of the type theory of Lean's kernel, the standard toolkit adds three axioms: propositional extensionality propext (equivalent propositions are equal), soundness of quotients Quot.sound (equivalent elements are equal in the quotient), and choice Classical.choice (extracting an element from a proof of existence). Which axioms a theorem depends on is listed by the command #print axioms theorem_name.

In the bundles of this book, we put #print axioms for the main theorems at the end of each file, and our criterion of cleanness is that every line of its output is a subset of the three axioms. Using sorry, which skips a proof, adds sorryAx to the list, and declaring an axiom oneself adds its name, so this criterion is a mechanical confirmation that "the proof has no hole and no arbitrary axiom has been added". In every bundle of Table 1 (the "copy of the axiom output" column of Table 1; including the copies retaken on a second machine on 2026-10-09), we reread that there is not a single axiom name other than the three. Some theorems do not use Classical.choice among the three (for example, tb_range uses only propext and Quot.sound).

Detour native_decide: why it is not used

decide checks a proposition decided by finite case analysis by computation inside the kernel. native_decide translates the same computation into a Lean program, runs it as machine code, and trusts the answer. It is fast, but in exchange the range of trust widens from the kernel to the translator and the execution environment, and that trust appears in the list as an additional axiom (depending on the version, an axiom with a different name appears for each declaration). In the bundles of this book we do not use native_decide, and we put the criterion of cleanness as "every line of the list is a subset of the three axioms". Looking for the presence or absence of a particular axiom name would miss things when the naming changes between versions.

The bundles of the first step — what algebra was checked

The Lean theorems of the first step are divided into files (bundles) by subject. Table 1 lists the main bundles in the order of the chapters that cite them in the text. "Number of theorems" is the number of theorem / lemma declarations in the file, and the column "Representative theorem" gives the theorem name with that theorem's assumptions in the same column.

Table 1 The main bundles of the first step (the number of theorems is the number of declarations. Copy of the axiom output: ○ = the output of `#print axioms` at the end remains separately, and we reread that every line is a subset of the three axioms. Includes the copies retaken on a second machine on 2026-10-09)
Bundle	Number of theorems	What algebra	Representative theorem (assumptions)	Chapter	Copy of the axiom output
`LatticeGaugeOneScale`	12	H↑, H↓ and the rereading of mass (the equality version)	`hup_is_gap_positivity` ( $0\lt m$ , $C_P=1/m^2$ , $C_P\le K\xi^2$ )	10-01	○
`LatticeGaugeHupBridge`	18	The one-sided bridge, the lower half of the power, negative controls	`hup_is_gap_positivity_of_lower` ( $0\lt m_{\rm lat}$ , $\kappa/m_{\rm lat}^2\le C_P$ , $C_P\le K\xi^2$ ), `first_power_does_not_bridge` (negative control)	10-01	○
`LatticeGaugeDoubleWellTestbed`	7	The skeleton of the finite sum of Proposition L	`local_rayleigh_ratio_le_one` ( $0\lt m$ , $a_k\ge m$ , $c_k\ge0$ , $\sum c_ka_k\gt0$ )	10-04	○
`LatticeGaugeTwoScalePoincare`	8	Splitting of the variance, curvature of the convex core, values of the reduced two-state model, the band ratio of Glauber	`split_poincare_le` (the splitting formula, two local Poincaré inequalities, the mean difference, additivity of forms, non-negative constants)	10-04, 10-05	○
`LatticeGaugeDoubleWellKramers`	10	From the bracketing of the ratio to the power form of H	`power_H_of_kink_ratio` ( $0\lt K,s,\delta$ , $1\le R\le K/\hbar$ , $s/\hbar\le\ln\xi$ )	10-04, 10-05	○
`LatticeGaugeH1Assembly`	17	The algebra of rates of Proposition H1, the arithmetic of the margin at six nodes, Gershgorin on the ring	`H1_assembly` (seven named ones: decomposition, the fine side, Helffer's criterion, the margin, $0\lt\lambda$ , (T4), the condition on rates)	10-06	○
`LatticeGaugeCoarseSideUniform`	20	Arithmetic of (T4), the two-sided form of Muckenhoupt	`T4_paper_numeric` ( $\lambda_c\ge1.3\times10^{-4}$ )	10-06	○
`LatticeGaugeIntervalQfreeWindow`	150	The linear-fractional map of Lemma TAU, the identity of the tilt, from covering to window, recomputation of the rate-limiting cells	`win_qfree_window_le_of_interval_table` (the table of interval-arithmetic output)	10-08	○
`LatticeGaugeRingUnconditionedWindow`	20	Assembly of the window for the outer chain of the ring	`unc_window_lt_one_of_table` (the table of interval-arithmetic output)	10-07, 10-08	○
`LatticeGaugeRingInnerChain`	22	The ratio at the corner of the wall, $S_W$ of the ring	`sw_inner_le` ( $q_{\rm in}\le13/10$ , $q_{\rm out}\le0.998888530$ )	10-07	○
`LatticeGaugePartitionFramework`	14	Sum over sectors, the Gibbs step, composition and the closing condition	`comp_close` ( $X\gt0$ , $b,A\ge0$ , $\ell\gt0$ , and the three inequalities of Barta, (Σ.3) and Bochner)	10-09	○
`LatticeGaugeRemVProxy`	23	Assembly of Proposition P5	`path5_conditional` (with the remainder inequality, the proxy ratio, rarity and the arithmetic margin named)	10-09	○
`LatticeGaugeDetourKills`, `…2`	17, 16	The arithmetic of "the line that killed it" for the detour plans	Lemmas for each type (10-10 Table 4)	10-10	○
`LatticeGaugeBoxReduction`	23	Lemma TP, even and odd boxes, averaging over shifts, positive and negative controls	`box_shift_average` (the two-family inequality for each shift, $C_{\rm box}\ge0$ , the sum over overlaps $\le\mathcal E$ )	10-05, 10-11	○
`LatticeGaugeBoxGap`	18	Proposition H4, the algebra of $c_{\rm kg}$ , the composition of H3 and H4	`H3_H4_compose` (the statement of §01)	10-05, 10-11	○
`LatticeGaugeCoreMixing`, `CoreMaxCorr`, `CoreThreeStage`	15, 20, 18	The three stages of the core (Lemma BV, Proposition G, Lemma TB, combining the three stages)	`three_stage` (the upper bound of each stage)	10-11	○
`LatticeGaugeCoreActionGap`	15	The vanishing of the local term, drawing the line at the ends	`cloc_term_vanishes` ((ΔS_core), the reading of $\xi$ , $\Delta S_*\lt2S_0$ )	10-11	○
`LatticeGaugeGlobalLyapunov`	21	The algebra of the Lyapunov criterion and the positive control of the one-dimensional Gaussian	`gauss1d_bbcg`, `gauss1d_equality` (no assumptions)	10-14	○

The theorems of Table 1 are all inequalities and equalities on real numbers, finite sums and sequences. There is no theorem that has measures, operators or spaces of paths as types. The bundle of interval arithmetic (most of the 150 declarations of IntervalQfreeWindow) recomputes the formula for the upper bound of the last step cell by cell in rational numbers; there are many declarations, but the content is arithmetic. The index of all bundles is shared with Appendix A-04.

The side of the four-dimensional lattice. The theorems of the roads tried on the four-dimensional lattice (10-02 §07 Table 4), divided by the type of the object their statements speak about directly, are as in Table 2.

Table 2 The type of object and the character of the theorems on the side of the four-dimensional lattice (rows are theorems; the character symbols correspond to the classification of Table 4 of 10-02: R = reproof, A = arrangement, C = conditional, N = negative control, M = lattice theorem)
Type of object	Number of theorems	Examples
Real numbers (and natural numbers) only	23	`chain_band`, `drain_exponent`
Sequences, real functions	11	`S4_two_sided`, `conditional_scale_bound`
Sums over finite sets and finite groups	8	`intact_frac_le`, `meff_ge_of_corr`
Operators on an inner-product space	1	`tau_int_le`
Lattice gauge fields (quaternions, Haar measure)	3	`one_link`, `hess_gauge`
Total	46	Counted by character (41 rows, counting two paired theorems as one row): R 11, A 15, C 7, N 5, M 3

There are three theorems that have lattice gauge fields as a type, and there is no theorem about expectations, correlations or gaps of the Wilson measure. As for the correspondence of characters, "reproof, arrangement, conditional, negative control, lattice theorem" of Table 4 of 10-02 correspond one to one to R, A, C, N, M of this table.

Assumptions next to theorem names

In the text and tables of this part, when we write a theorem name, we list the assumptions of that theorem in the same column (example: H1_assembly (assumptions: seven named ones)). If only the theorem name is written, it is read at the stage of summary as "settled in Lean", and conditional algebra swells into an unconditional result. In the integrated table (10-12), too, we wrote the theorem names and assumptions under each node of the graph.

In the computer-assisted rows, the Lean column splits into three layers (10-08 §08): (1) the algebraic core (monotonicity of the linear-fractional map, the identity of the tilt, the algebra from covering to window); (2) recomputation of the rate-limiting cells and of randomly chosen cells (not all cells); (3) the assembly that puts the table of interval-arithmetic output as an assumption and derives the conclusion for the whole window. Interval arithmetic itself (interval evaluation of the map of a step, quadrature, invariant sets, the conventions of rounding) is outside Lean, and its correctness rests on cross-checks and control tests (10-08 §07). The label of a theorem that puts the table as an assumption is read as "if the output of interval arithmetic is correct, the conclusion for the whole window is correct as algebra".

Four limits — what cannot be detected even within the three axioms

Even for a theorem that meets the criterion of cleanness (§02), the following four are not guaranteed. The first two restate the convention of §01; the last two are types in which the way the statement is written itself empties the conclusion.

(1) The truth of the assumptions. A theorem does not prove a single step of its assumptions. If hH4 of H3_H4_compose is false, the conclusion says nothing.

(2) The encoding of the objects. CP inside Lean is a real number with a name, and that it is the Poincaré constant of the path measure is a reading of the text. The check passes even if the same name refers to a different quantity in another bundle. For example, a theorem named measured_ratio exists in two bundles of the first step (CoreActionGap and HierarchicalLink), and they are statements about different quantities in different namespaces. A name is no guarantee of content.

(3) Putting the conclusion into a definition. If the desired property is written as it is inside a definition and that definition is taken as an assumption, the conclusion becomes a copy of the assumption, and the proof closes in one line. The following is pseudo-Lean showing only the type.

Putting the conclusion into a definition closes anything (pseudo-Lean, an example of the type)

def InSpectrum (E : ℝ) : Prop := E = 0 ∨ c ≤ E          -- write the desired property into the definition of "spectrum"
theorem gap (E : ℝ) (h : InSpectrum E) : E = 0 ∨ c ≤ E := h   -- just returns the assumption as it is
def massGap : ℝ := 1 / 2                                  -- put the value literally, and positivity closes too

All three lines pass the check, and the list from #print axioms is either empty or within the three axioms. Even so, "spectrum" is not tied to the spectrum of any operator, so there is no mathematical content. One document wrote one of the conjuncts of its main theorem in this type, and another as a number put literally. It is an example in which the theorem name contains "mass gap" and every check passes, yet the statement does not encode the object.

(4) A circle of dependence. Lean checks theorems one at a time. Even if theorem A takes the conclusion of B as an assumption and theorem B takes the conclusion of A as an assumption, both pass the check. Neither conclusion has been derived unconditionally, yet putting the two side by side makes it look "shown". The same holds when proofs are written in prose: one document put the final conclusion, that the gap is positive, as a premise of intermediate steps (clustering, uniqueness of the vacuum), "to be shown later". Drawn as a dependency graph, an edge goes back from a conclusion with a large number to a step with a small number, and the rule of numbering (10-12 §03) is broken.

Table 3 The four limits, and how this book guards against them
Limit	Visible to the check?	How this book guards against it
(1) The truth of the assumptions	Not visible (assumptions are arguments)	Write the assumptions next to the theorem name (§04); count the assumption rows one by one in the integrated table (10-12 Table 1)
(2) The encoding of the objects	Not visible (it only gives names to real numbers)	State the types of the Lean objects in the text ("real numbers, finite sums" of §03); translate conventions (§07); write, chapter by chapter, the correspondence between the quantities of the text and the symbols of the theorem statements
(3) Putting the conclusion into a definition	Not visible (stays within the three axioms)	Copy the theorem statement into the text and read the definitions back (questions 3 and 4 of §06); give negative-control theorems (examples that collapse when an assumption is removed)
(4) A circle of dependence	Not visible (theorems are checked one at a time)	The rule of numbering of the dependency graph; checking that the assumption rows do not contain the quantity of the conclusion (10-12 §03)

Negative-control theorems work as a guard against (3). For example, no_bound_when_c_one (if the two $\sigma$ -algebras are the same, $c=1$ , the reduction to the box says nothing) and first_power_does_not_bridge (with the first power, the bridge cannot be built) show that the conclusion collapses when an assumption is removed, confirming that the assumption is not decoration but acts on the conclusion.

A procedure for readers to inspect for themselves — six questions

When reading a claim labelled Lean, ask the following six in order. They apply equally to the theorems of this book and to theorems of other documents.

Cleanness. Is every line of the output of #print axioms a subset of propext, Classical.choice, Quot.sound? If you do not have the output at hand, it is "unconfirmed".
The list of assumptions. Write out all the brackets before the colon in the theorem statement (the arguments whose types are propositions). Does a claim that the text calls "unconditional" still have propositional arguments?
Trace back the definition of the conclusion. Open the definitions of the names that appear in the conclusion (such as InSpectrum), and see whether they contain the same sentence as the conclusion. Are the assumption and the conclusion unfoldings of the same proposition?
The type of the object. Do the objects the claim should speak about (measures, operators, fields) appear as types in the theorem statement? If what appears is only real numbers, natural numbers and finite sums, the tie to the objects lies in the reading of the text.
The direction of dependence. If the claim joins several theorems, arrange as numbered nodes which theorem takes the conclusion of which theorem as an assumption, and see whether the numbers of premises can be placed smaller than the numbers of conclusions. If not, it is a candidate for a circle.
Negative control. Is an example given in which the conclusion collapses when one assumption is removed? If not, check for yourself whether that assumption acts on the conclusion.

Example. Applied to H3_H4_compose of §01: (1) a subset of the three axioms; (2) the propositional arguments are the seven hn, hca, hh, hS, hD, hH3, hH4; (3) the conclusion is an inequality of real numbers and no tracing back of definitions is needed; (4) the objects are all real numbers; (5) hH3 and hH4 are the conclusions of Propositions H3 and H4, and in the integrated graph [072], [075] and [104] are smaller than [105]; (6) no_bound_when_c_one shows that at $c_{\rm alt}=1$ the reduction to the box says nothing (hca is not decoration). The answer is "if Propositions H3 and H4 hold, the inequality of Proposition 4.5 follows as algebra", and no more.

Translating conventions — places where the same letter or the same name refers to different quantities

Lean theorems do not know the meaning of symbols, so the check passes even if the same letter refers to different quantities in different files. Table 4 translates the conventions inside the theorems into the notation table of this book (Appendix A-01) and writes discrepancies as discrepancies. The upper six rows are on the side of the four-dimensional lattice, the lower five on the side of the first step.

Table 4 Conventions inside Lean and the notation of this book
Quantity	Inside Lean	This book	Discrepancy
$\beta$	One-link integration $e^{\beta\langle u,M\rangle}$ , $\langle u,M\rangle=\tfrac12{\rm Re\,tr}(UM^\dagger)$	$\beta=2N/g^2$	None ( $\beta=4/g^2$ at $N=2$ ). Against the convention of Shen–Zhu–Zhu, $\beta=4\beta_{\rm SZZ}$
tr and angle	Link angle $U=e^{i\vartheta\cdot\sigma}$	$T^a=\sigma^a/2$ , $U=e^{i\theta^aT^a}$	$\theta=2\vartheta$ , $C_P^{(\theta)}=4C_P^{(\vartheta)}$ . A constant factor, so it does not affect the power
$a$	`a` of `drain_exponent`	Lattice spacing	Lean's $a$ is the reciprocal of the bookkeeping length, $1/\xi_{\rm RG}$
$\eta$	The static exponent, the exponent of susceptibility, the exponent of overlap	$\eta_s$ and $\eta_{\rm dyn}$ separated by subscripts	Present (the same letter for three quantities)
$\kappa$	The one-loop slope, the coefficient of a model, the coefficient of the Casimir term, the contribution of faces sharing no edge	Only the one-loop slope $11/(3\pi^2)$	Present (the same letter for four quantities)
$C_P$ (four dimensions)	A real number with a name	The Poincaré constant of Langevin. The normalisation is named	With the normalisations of the field $A$ and the angle $\vartheta$ , $C_P^{(A)}=\beta C_P^{(\vartheta)}$
$\hbar$ and $\varepsilon$	`hbar` (a real number). The lattice spacing enters as a number	$\mathcal E(f)=(\hbar/\varepsilon)\sum_i\mathbb E\|\partial_if\|^2$ , $\varepsilon=\tfrac12$	None. The conversion between the readings at $\varepsilon=0.25$ and at $\varepsilon=\tfrac12$ is not written (10-14 §05)
The graduation of $C_P$ for the core	$C_P$ of the theorems of the stages of the core	10-11 uses the convention of $\mathcal E$ , 10-09 the convention of $\hbar\int\|\nabla g\|^2$	$C^{(10\text{-}09)}=C/\varepsilon=2C$ (10-11 §05)
$K$	`K` of `power_H_of_kink_ratio`	$K$ of Proposition 4.5 and $K'=KS_0$	Lean's $K$ is $K'$ of the text (10-05 Step 5)
Theorem names	`measured_ratio`	—	Different theorems with the same name in two bundles ((2) of §05)
Reading values	Numerical theorems such as `K_ff_C2`, `three_stage_3em4`	Reading	Arithmetic with measured values put as assumptions. The grade of the values stays "Reading" (it does not become "Proved here" through the Lean label)

How the bundles are divided — by article, paper and subject

The bundles (files) are divided by subject (one proposition and its lemmas). It is usual for the theorems cited by one chapter or article to span several bundles, and the "Chapter" column of Table 1 gives the correspondence. There are four disciplines for dividing them.

One subject per bundle. Even mutually dependent subjects such as Proposition H3 and Proposition H4 are put in separate bundles, and the composition goes into a bundle of its own. The boundaries between bundles become the boundaries between nodes of the dependency graph, and one can follow which bundle takes the conclusion of which bundle as an assumption.
#print axioms at the end. At the end of each bundle we put #print axioms for the main theorems, and keep the output under the same name as the bundle (the "copy of the axiom output" of Table 1).
No internal names in names. Bundle names and theorem names are given by mathematical content (LatticeGauge… followed by the name of the subject), and names visible to readers do not contain working names or names of people.
Decide the bundles handed to articles and papers. When an article or paper cites theorems of some bundle, the list of the bundles containing the cited theorems is also placed on the article's side, together with the version of the bundles (the output of which check). If a bundle is later corrected, the list on the side of the citing article is corrected too.

This part places Assumption H at the axis of the study, and Lean was used for the algebraic steps of the construction of the first step. The viewpoint of doing proof checking in another form (for example, a formalisation that makes the objects themselves types) is taken up in Part 11.

What this chapter can say

Can say	Cannot say
Lean The theorems of the bundles of Table 1 pass machine checking in a form that makes the assumptions explicit as arguments. In every bundle of Table 1, every line of the remaining `#print axioms` output is a subset of the three axioms	The truth of the assumption rows. A check of reading Lean's real numbers as quantities of the path measure itself
The Lean theorems of the first step are all statements on real numbers, finite sums and sequences; there is no theorem that has measures or operators as types	A formalisation that makes measures and operators types
The four limits and how to guard against them (Table 3), the six questions for inspection	That a claim that has passed the six questions is true (the questions are necessary checks, not sufficient ones)
That the layer of interval arithmetic is outside Lean, and only the assembly that puts the table as an assumption is inside Lean	Formal verification of the implementation of interval arithmetic

Sources and reproduction

Item	Kind	Source, tool
The declarations and numbers of the theorems of the bundles	Lean	We read the declarations of the source of each bundle (Lean 4, Mathlib) and counted the `theorem` / `lemma` lines. Theorem names and assumptions are in each row of the text
Copy of the axiom output	Lean	We read the copy of the `#print axioms` output of each bundle and counted the absence of axiom names other than the three (`sorryAx` and others), after confirming with a control copy that contains such a name that it would be detected
The three axioms and `#print axioms`	Cited	J. Avigad, L. de Moura, S. Kong, S. Ullrich et al., "Theorem Proving in Lean 4", chapter Axioms and Computation
The layers of type and the characters on the side of the four-dimensional lattice (Table 2)	This book	10-02 §07 and the count in the correspondence table of the old version (the same 46 theorems)
Examples of the type that puts the conclusion into a definition and the type of a circle of dependence	This book	A reading of two external documents that claim a construction or a proof (the sources are withheld and only the types are written; no judgement is made on whether the documents are right or wrong)

Terms used in this chapter — machine checking, bundle, the criterion of cleanness, the three axioms, #print axioms, native_decide, encoding of the objects, putting the conclusion into a definition, circle of dependence, negative-control theorem, translating conventions. Their meanings are in the A-02 glossary.

Next chapter: 10-14 Reconciliation — the numbers of the record and the known numbers — lays out, row by row against the numbers of the record, the distance between each condition of the first step and the nearest known theorem, a summary of the bibliographic checks, and the known numbers used for positive controls.

Revision 2026-10-09: first edition.
2026-10-09: for the four bundles whose "copy of the axiom output" in Table 1 was △ (HupBridge, RemVProxy, DetourKills, GlobalLyapunov), #print axioms was retaken on another computer and they were changed to ○.