Appendix B Formal verification
Several results of Part I, among them Theorem 3.1, have formal proofs in the Lean 4 proof assistant (version 4.34.0) with the Mathlib library (commit 5ed2965). In addition, a Lean port of the implementation of the algorithms of Theorem 1.5, for the cases described in Appendix B.1, is proved to output path decompositions that attain the bounds of Theorems 8.1, 7.1, 7.2 and 1.3 and Corollary 1.4 for suitable labelings, under the same hypotheses. The development is part of the accompanying code, and the driver script of Appendix A.2.6 has a third mode, lean, that rebuilds the formal proof of Theorem 8.1. Table 8 lists the formal proofs; the text after the table states the hypotheses they assume, describes the formal statements and what is not formalized, and records where the formal proofs follow other routes than the written ones. Appendix B.1 describes the implementation, its tests and its Lean port. No result of Part II or of Appendices A.7, C and D is formalized.
What each result rests on.
The results rest on three kinds of evidence, and we say for each headline result which kind it needs.
(a) Theorem 1.1(a), Corollary 1.2 and the switch lemma behind them (Lemma 8.9) use no computation; their written proof uses the case \(d=3\) of Lemma 6.5, which is a case of Mulgund’s theorem (Mulgund 2026) and also has an elementary proof (Remark 6.6). Theorem 8.1, which is Theorem 1.1(a), has a complete formal proof in Lean, without hypotheses. Its written proof takes Section 8.1 to Section 8.5 and lemmas from Sections 3, 4, 5, 6 and 7; the formal proof follows it with the differences listed under “Routes” below.
(b) Theorem 1.1(b) uses two inputs. The first is, for vertices of degree \(4\), the extremality of the regular simplex among four Gaussian variables, which is a case of Mulgund’s theorem (Mulgund 2026) and also follows from the four-cap theorem of Fejes Tóth (Fejes Tóth 1950) ((Böröczky 2004 Theorem 5.6.2)). The second is a certified enclosure of \(F_4\) (Proposition 6.9).
(c) Theorem 1.3 and Corollary 1.4 are derived from the triple \((\frac5{32},\frac14,\frac{11}{32})\) for maximum degree \(5\) (Theorem 7.2). This triple rests on a computer-assisted charging certificate, verified in ball arithmetic and exact rational arithmetic (Proposition 7.5), and on the case of five variables of the simplex theorem. That case is Mulgund’s theorem (Mulgund 2026), proved in a preprint with a Lean formalization that we compiled and checked against the inequality we use (see H1 below). Theorem 7.1(b),(c) are restrictions of triples of Theorem 7.2 and rest on the same certificate.
The bootstrap from degree \(5\) to all degrees (Lemma 9.3) is a combinatorial induction without computation. Theorem 8.2 rests on two further computer-assisted certificates. Theorem 1.1(b), Theorem 1.3, Corollary 1.4 and Theorems 7.2 and 8.2 also have formal proofs in Lean, conditional on the certified and external inputs named above.
For every entry of Table 8, the final Lean theorem has no hypotheses beyond those of the written statement and those listed, and Lean’s #print axioms reports only the three standard axioms propext, Classical.choice and Quot.sound. The development contains no unproved steps (sorry), no additional axioms and no trusted native computation. The last column of the table says what each formal statement was checked against: the written statement it formalizes, and for the implementation also the code it ports.
Since Mathlib has no notion of pathwidth, the development defines path decompositions directly: a path decomposition is a nonempty finite sequence of bags that covers every vertex and every edge, such that the bags containing any vertex are consecutive. Graphs are Mathlib’s simple graphs on the vertex set \(\{0,\dots,n-1\}\), and a bound \(\mathop{\mathrm{pw}}(G)\le w\) means that \(G\) has a path decomposition whose bags have at most \(w+1\) vertices. Treewidth is not formalized. Unless said otherwise below, a formal statement is the uniform \(\varepsilon\)–\(N\) form of the written one: for every real \(\varepsilon>0\) there is \(N\) such that every graph of the class with \(n\ge N\) vertices satisfies \(\mathop{\mathrm{pw}}(G)\le\beta(G)+\varepsilon n\), where \(\beta\) is the bound without its remainder. All theorem names below live in the Lean namespace CubicPathwidth.
Table 8: The formal proofs. “Axioms” lists what #print axioms reports beyond the three standard axioms, which every entry uses. The hypotheses H1, H2, H3, H6 and H7 are stated, with their status, after the table.
| Result | Lean theorem | Hypotheses | Axioms | Checked against |
|---|---|---|---|---|
| Theorem 8.1, that is Theorem 1.1(a) | C3.c3MainClaim, proving the proposition C3MainClaim |
none | none | Theorem 8.1 |
| Theorem 3.1 | CutSweep.cutSweep, proving the proposition CutSweepClaim |
none | none | Theorem 3.1 and Lemma 3.2 |
| Lemma 5.4 for \(p=3\) | Locality.``graph_correlation_lower |
none | none | a lemma inside the development of Theorem 8.1; not separately checked |
| Theorem 7.1(a) | T2.target2a |
H1 | none | Theorem 7.1 |
| Theorem 7.1(b), (c) | T2.target2b, T2.target2c |
H2 at the pair | none | Theorem 7.1 |
| Theorem 7.2, triples \(\mathsf{P}\), \(\mathsf{R}\), \(\mathsf{S}\) | T3.target3P, T3.target3R, T3.target3S |
H3 at the triple | none | Theorem 7.2 |
| Theorem 1.3; Corollary 1.4 | T4.target4; T4.target5 |
H3 at \(\mathsf{S}\) | none | Theorem 1.3; Corollary 1.4 |
| Definition 9.1 (its \(\varepsilon\)–\(N\) form is equivalent to its \(\rho(n)=o(n)\) form); Lemma 9.3: its first claim; the whole lemma when \((a_3,\dots,a_k)\) is a pathwidth sequence | PwSeq.targetRhoForm; PwSeq.targetBootstrapLemma; PwSeq.targetLemma2 |
none | none | Definition 9.1 and Lemma 9.3 |
| Theorem 9.2 for \(\mathsf{C}\), \(\mathsf{F}\), \(\mathsf{P}\), \(\mathsf{R}\), \(\mathsf{S}\) | PwSeq.targetThm1C, targetThm1F, targetThm1P, targetThm1R, targetThm1S |
none for \(\mathsf{C}\); H1 for \(\mathsf{F}\); H3 at the triple for \(\mathsf{P}\), \(\mathsf{R}\), \(\mathsf{S}\) | none | Theorem 9.2 |
| Theorem 8.2; Theorem 9.2 for \(\mathsf{M}\) | Sw4.targetThm62; Sw4.targetThm1M |
H6 and H7 | none | Theorem 8.2; Theorem 9.2 |
| Implementation of Appendix B.1: every output is a path decomposition | Alg.algoT1Valid, algoT2aValid, algoMixedValid, algoT4Valid |
none | none | the Lean port against the implementation, and the statements against Appendix B.1 |
| Implementation: no fallback on the inputs of these cases of Theorem 10.1; the width bounds of Lemmas A.33 and A.28 and of Lemma A.34 for the bootstrap of \(\mathsf{S}\); the bounds of Part I attained for some labeling | Alg.``algoT1RealizesTheorem1, …, Alg.``algoT4RealizesCorollary5, with \(29\) statements in all |
those of the attained theorem (none, H1, H2, H3) | none | the statements against Appendix B.1 and the theorems they realize |
The hypotheses and their status.
The five hypotheses are mathematics established outside the development, stated as explicit hypotheses of the final theorems rather than as axioms.
- H1
-
(
SimplexFourClaim) The case \(d=4\) of Lemma 6.5, written exactly as the theoremFSC.cdf_simplex_leof Mulgund’s formalization (Mulgund 2026) for four variables. Status: proved in that formalization, by the author of (Mulgund 2026). We compiled it at the commit its author designates as certified, and checked that its main theorem depends only on the three standard axioms and that, for \(n\in\{3,4,5\}\) variables and after the substitution \(X=-U\), its statement is exactly the inequality of Lemma 6.5. The distribution in that statement is Mathlib’s multivariate Gaussian measure, which for a positive semidefinite matrix is the centered Gaussian distribution with that covariance, singular matrices included. The reproducibility package does not rebuild this formalization. It uses Lean 4.31.0 and another version of Mathlib, so our development cannot import it; H1 therefore restates the theorem word for word. The written proof uses the same theorem. - H2
-
(
AdmissiblePair, at \((F_3,0.2575)\) and at \((\frac5{32},\frac14)\)) Admissibility for \(D=\{3,4\}\) as in Definition 7.3, with the exact center bounds; these pairs are the restrictions of \(\mathsf{P}\) and \(\mathsf{S}\) noted after Proposition 7.5. Status: certified by the computer-assisted proof of Proposition 7.5 in ball arithmetic and exact rational arithmetic (Appendix A.2). The computation is not repeated inside Lean, because that would require verified enclosures of \(\Phi\), of the simplex functions \(S_d\) and of Owen’s \(T\) function on about a thousand cells. - H3
-
(
AdmissibleTriple, at \(\mathsf{P}\), \(\mathsf{R}\) and \(\mathsf{S}\)) Proposition 7.5 as stated. Status: as for H2. The written method of this certificate uses the cases \(d=4\) and \(d=5\) of Lemma 6.5, which rest on Mulgund’s preprint (Remark 6.6). The simplex theorem for five variables enters the formal proofs only through this certificate. - H6
-
(
SwitchMixedClaim) Lemma A.10 as stated, for centered Gaussian vectors described by their correlation matrices and for the bounds in every order, with \(\Psi\) written as the expectation \(\mathbb{E}[\mathbf{1}\{Y_0\le0\}\lceil N/2\rceil]\), where \(N\) counts the neighbors with positive label. Status: proved in the paper by a coupling reduction and the box certificates of Appendix A.3.2 in ball arithmetic; not formalized. - H7
-
(
SwitchedChargingClaim) Proposition A.13 with \(c_{3}\) exact and the center bounds of H2 and H3. Status: a further problem of the certificate of Proposition 7.5 (Appendix A.2); not formalized.
The formal statements.
C3MainClaim is the uniform \(\varepsilon\)–\(N\) form of Theorem 8.1 with \(c_{3}\) written as the exact real expression \(\frac3{4\pi}\arccos\frac56\): for every real \(\varepsilon>0\) there is \(N\) such that for every \(n\ge N\), every simple graph on the vertex set \(\{0,\dots,n-1\}\) all of whose degrees are at most \(3\) has a path decomposition in which every bag has at most \((c_{3}+\varepsilon)n+1\) vertices. The proposition also contains the inequality \(c_{3}<2c_*/(1+6c_*)\approx0.16443\), where \(c_*=\frac3{2\pi}\arccos\frac{2\sqrt2}3\) is the constant of Theorem 3.1; this compares \(c_{3}\) with a weaker coefficient proved earlier in the same development and plays no role here. The statement graph_correlation_lower is the inequality \(\mathop{\mathrm{Corr}}(Y_u,Y_v)\ge r_*(1-\frac1R)\) for every graph of maximum degree at most \(3\), every radius \(R\ge1\) and every edge \(uv\).
In the statements for Theorem 7.1 and Theorem 7.2, \(F_4\) and \(F_3\) are defined as the suprema over the threshold of the ideal star functions (2.2), and Theorem 7.1(a) is stated in the form \(\mathop{\mathrm{pw}}(G)\le F_4n+o(n)\). The formal target for Corollary 1.4 is the \(\varepsilon\)–\(M\) form of Remark 9.14, which implies Corollary 1.4: for every \(\varepsilon>0\) there is \(M\) such that every graph with \(m\ge M\) edges, on any number of vertices, satisfies \(\mathop{\mathrm{pw}}(G)\le(\frac7{48}+\varepsilon)m\). It implies the \(o(n)\) form: Lemma 3.2 gives \(\mathop{\mathrm{pw}}(G)\le m\), as at most \(m\) edges leave any prefix of an ordering, and \(\mathop{\mathrm{pw}}(G)\le n-1<\frac7{48}m\) if \(m>\frac{48}7n\), so \(\mathop{\mathrm{pw}}(G)\le\frac7{48}m+\max\{M,\frac{48}7\varepsilon n\}\) for every graph.
The formal definition of a pathwidth sequence is the finite-tuple phrasing given after Definition 9.1, for tuples \((a_3,\dots,a_k)\) with \(k\in\{3,4,\dots\}\cup\{\infty\}\), with the remainder in uniform \(\varepsilon\)–\(N\) form: for every \(\varepsilon>0\) there is \(N\) such that every graph with \(n\ge N\) vertices satisfies \(\mathop{\mathrm{pw}}(G)\le\sum_{d=3}^ka_dn_d+\sum_{d>k}n_d+\varepsilon n\). The theorem PwSeq.targetRhoForm proves this equivalent to the form of Definition 9.1 with one remainder function \(\rho(n)=o(n)\). The statements for Theorem 9.2 bound every graph, with coefficient \(1\) for each vertex of degree greater than \(k\). CutSweepClaim states Theorem 3.1 in four parts: \(c_*=\frac3{2\pi}\arcsin\frac13\) for \(c_*\) written as \(\frac3{2\pi}\arccos\frac{2\sqrt2}3\); \(c_*<\frac16\); \(\mathop{\mathrm{pw}}(G)\le w\) whenever some ordering of \(V(G)\) has at most \(w\) edges leaving each of its prefixes, for every graph (the generality of Lemma 3.2); and the uniform \(\varepsilon\)–\(N\) form of \(\operatorname{cw}(G)\le c_*n+o(n)\) for maximum degree at most \(3\).
What is not formalized.
The following are not formalized: Corollary 1.2; Theorem 3.6; Corollary 9.5; Corollary 9.15; the enclosures of Proposition 6.9; the certificates behind H2, H3, H6 and H7; the explicit remainders of Lemma 4.5 and (9.4); the explicit threshold \(n\ge2^{46}\) and the explicit constants of the proof of Theorem 3.1; the computation of the labels (Appendices A.5.2, A.5.3, A.5.4 and A.5.5) and the running times of Theorem 10.1; Corollary 10.2 and Theorem 10.3; and treewidth.
Routes.
Each formal proof follows the written proof, with the following differences. The formal proof of Theorem 8.1 proves the switch lemma (Lemma 8.9) by a different deformation than Lemma 8.11: it rotates one vector of the residual configuration at a time, controls each rotation by a Plackett-type derivative computation, and reaches a planar configuration after finitely many rotations by a potential-function argument; this route exists only in the formal development. It also proves the case \(d=3\) of Lemma 6.5 directly, by the elementary argument of Remark 6.6, instead of taking it from Mulgund’s theorem. All formal proofs prove only \(o(n)\) remainders, so they choose their parameters from \(\varepsilon\), replace explicit rates by continuity or elementary estimates (for Theorems 7.1 and 7.2, they also prove the inequalities \(5\Phi(-3)\le\frac1{50}\le F_3\le\frac{103}{400}\) by elementary estimates instead of the certified values of Proposition 6.9), and, except for Theorem 3.1, bound the expected total absolute deviation of all counts instead of applying Chebyshev’s inequality to each count. For vertices of degree at most \(2\), the formal proofs of Theorems 7.1, 7.2, 8.2 and 1.3 do not follow Lemma 4.5: they keep a smallest set of vertices to which every component of the rest, of treewidth at most \(2\), attaches at most twice, and lift the decomposition by a torso construction, with the remainder \(12\sqrt n+1\). The formal bootstrap proves \(\sigma_d\le a_d\) through the conserved deficit \(d(1-\sigma_d)+(1-\sigma_{d-1})=\frac{129}{32}\) instead of Lemma 9.12; with base degree \(k\ge3\) in place of \(5\) it proves Lemma 9.3, and with it Theorem 9.2 for \(\mathsf{C}\), \(\mathsf{F}\), \(\mathsf{P}\), \(\mathsf{R}\) and \(\mathsf{S}\), and for \(\mathsf{M}\) under H6 and H7 with the base of Theorem 8.2.
B.1 The implementation
The accompanying code implements the randomized algorithms of the cubic, padded, mixed and general cases of Theorem 10.1, with floating-point labels, and its outputs were valid path decompositions on all test inputs; for the sweeps, the widths were between \(1.19\) and \(1.63\) times the bounds without remainder at \(n\le2000\). A Lean port of these algorithms, which agrees with the implementation on \(16{,}650\) test calls, is proved to output path decompositions that, for suitable labelings, attain Theorems 8.1, 7.1, 7.2 and 1.3 and Corollary 1.4 under the hypotheses of their formal proofs.