Formalisation and certificates
Parts of the paper are proved in Lean 4 with Mathlib, and several constants and inequalities rest on computer-assisted proofs. This page maps each formalised statement to its Lean theorems, and each computer-assisted statement to its code, in the order of the paper. Appendix B of the paper describes the formal statements, the hypotheses and the differences between the formal and the written proofs. The dependency graph shows how the statements depend on each other and which are formalised.
Lean proofs
A Lean theorem below proves the paper’s statement in the uniform ε–N form described in Appendix B, under the hypotheses listed. The hypotheses are explicit assumptions of the final theorems, not axioms. “Coverage” says which part of the statement is formalised.
| Paper | Lean (namespace CubicPathwidth) |
Hypotheses | Coverage |
|---|---|---|---|
| Theorem 1.1 | C3.c3MainClaimT2.target2a |
H1 | part (a) without hypotheses (as Theorem 8.1); part (b) under H1 (as Theorem 7.1(a)) |
| Theorem 1.3 | T4.target4 |
H3 | the whole statement, under H3 at the triple \(\mathsf{S}\) |
| Corollary 1.4 | T4.target5 |
H3 | the \(\varepsilon\)–\(M\) form of Remark 9.14, which implies the statement, under H3 at the triple \(\mathsf{S}\) |
| Theorem 3.1 | CutSweep.cutSweep |
none | the whole statement, with Lemma 3.2 for every graph |
| Lemma 5.4 | Locality.graph_correlation_lower |
none | the case \(p=3\) |
| Theorem 7.1 | T2.target2aT2.target2bT2.target2c |
H1, H2 | part (a) under H1; parts (b) and (c) under H2 at the pair |
| Theorem 7.2 | T3.target3PT3.target3RT3.target3S |
H3 | the triples \(\mathsf{P}\), \(\mathsf{R}\) and \(\mathsf{S}\), under H3 at the triple |
| Theorem 8.1 | C3.c3MainClaim |
none | the whole statement |
| Theorem 8.2 | Sw4.targetThm62 |
H6, H7 | the whole statement, under H6 and H7 |
| Definition 9.1 | PwSeq.targetRhoForm |
none | the equivalence of its \(\varepsilon\)–\(N\) form with its \(\rho(n)=o(n)\) form |
| Theorem 9.2 | PwSeq.targetThm1CPwSeq.targetThm1FPwSeq.targetThm1PPwSeq.targetThm1RPwSeq.targetThm1SSw4.targetThm1M |
H1, H3, H6, H7 | \(\mathsf{C}\) without hypotheses; \(\mathsf{F}\) under H1; \(\mathsf{P}\), \(\mathsf{R}\) and \(\mathsf{S}\) under H3 at the triple; \(\mathsf{M}\) under H6 and H7 |
| Lemma 9.3 | PwSeq.targetBootstrapLemmaPwSeq.targetLemma2 |
none | its first claim, and the whole lemma when \((a_3,\dots,a_k)\) is a pathwidth sequence |
| Theorem 10.1 | Alg.algoT1ValidAlg.algoT2aValidAlg.algoMixedValidAlg.algoT4ValidAlg.algoT1NoFallbackAlg.algoMixedNoFallbackAlg.algoT4NoFallbackAlg.algoT1WidthAlg.algoT2aWidthAlg.algoMixedWidthAlg.algoT4WidthAlg.algoT1RealizesTheorem1Alg.algoT2aRealizesTheorem2aAlg.algoMixedRealizesTheorem2bAlg.algoMixedRealizesTheorem2cAlg.algoMixedRealizesTheorem3PAlg.algoMixedRealizesTheorem3RAlg.algoMixedRealizesTheorem3SAlg.algoT4RealizesTheorem4Alg.algoT4RealizesCorollary5 |
H1, H2, H3 | for a Lean port of the implementation: every output is a path decomposition; no fallback on the inputs of these cases; the width bounds; and the bounds of Part I attained for some labeling (under the hypotheses of the attained theorem). Not the computation of the labels or the running times |
| Lemma A.28 | Alg.undoWidthAlg.undoNoFallback |
none | for the Lean port of the implementation |
| Lemma A.33 | Alg.connectorLemma10Alg.connectorNoFallback |
none | for the Lean port of the implementation |
| Lemma A.34 | Alg.deletionProcessBound |
none | for the Lean port of the implementation |
Hypotheses
- H1 (
SimplexFourClaim): proved in Mulgund’s separate Lean formalisation (Lean 4.31.0), restated word for word. - H2 (
AdmissiblePair): certified by the computer-assisted proof of Proposition 7.5. - H3 (
AdmissibleTriple): certified by the computer-assisted proof of Proposition 7.5. - H6 (
SwitchMixedClaim): proved in the paper (Lemma A.10, with box certificates); not formalised. - H7 (
SwitchedChargingClaim): proved in the paper (Proposition A.13, a certificate); not formalised.
Build
The Lean project is in lean/: Lean v4.34.0 (lean-toolchain) and Mathlib pinned in lake-manifest.json. It was built from scratch on the machine Serges-MacBook-Pro (16 cores, arm64-apple-darwin24.6.0), not by the site’s build, which renders the pages only. evidence/build-info.txt records the run: commit 3e9f58c of the research repository, Lean 4.34.0, lake build of both libraries with exit code 0 in 165 seconds. The sources on this site are those of commit e1fa7cf, which differs from the built commit only in comments (the export checks this).
To check it yourself:
cd lean
lake exe cache get
lake buildand then, for each theorem of the table, #print axioms in a file that imports CubicPathwidthProofs. evidence/axioms.txt is the report of that run for 46 declarations, 46 of which are linked above; each depends only on Lean’s standard axioms propext, Classical.choice and Quot.sound.
The project has 245 modules, of which lake build builds 244; the module list says which.
Computer-assisted proofs
The code is in ancillary/ under the MIT licence (LICENSE); SHA256SUMS lists checksums, and README.md says how to run each part. The table lists the statements whose proofs use a computation; the paper names further scripts where it uses them, and those names link to the files.