Appendix F Computer certificates
Several constants in the bases of our running times rest on finite computations. The first table lists every ancillary file that a proof in the paper depends on, together with what it certifies and the arithmetic it uses; Appendices F.1, F.2, F.3, F.4, F.5, F.6, F.7 and F.8 describe, result by result, what is checked and how. Every check is either in exact rational arithmetic or, for logarithms, exponentials and square roots, in ball arithmetic with outward rounding (Arb (Johansson 2017), through python-flint, at \(256\) bits): each operation returns a ball that provably contains the exact real result, and an inequality is accepted only if it holds for the whole ball. Inputs such as decimal endpoints and parameters are read as exact rationals. So each certificate is a proof, up to the correctness of the software.
Files that a proof depends on
| File | Certifies | Arithmetic |
|---|---|---|
rs_closed_form_interval.py |
the constant \(1.744835\) of RS and the two bounds on \(F^*\) used by RS-\(\theta\) (Proposition 6.1(c)), by adaptive bisection into \(9608\), \(60\) and \(73\) intervals | exact rationals; Arb |
cert_final_0.json, cert_final_1.json, verify_cert.py, verify_cert_indep.py, v_cert_primal.py, cz_bounds.py |
the two antinorm certificates of RS-\(\theta\) (Proposition 7.7), checked three independent ways, and the bounds on \(c_{Z_i}\) | exact rationals |
rst_rate_interval.py |
the rates of the RS-\(\theta\) certificates at the endpoints of their ranges and \(2^{\psi^*}<1.7204\) (Propositions 7.7 and 7.8) | exact rationals; Arb |
lobster_rate_certificate.py |
the bounds \(1.71927\) and \(1.71928\) for the uniform lobsters (Proposition 7.9(c)), on \(4764\) intervals | exact rationals |
rsc/rsc-certificate.json.gz, rsc/rsc-verify.py (with rsc_verify_core.py and rsc_modelg.py in rsc/), rsc/rsc-credits.py, rsc/rsc-verify-independent.py |
the antinorm certificate of RSC (Proposition D.5.23), checked by two independent programs, and the credit inequalities of Lemma D.5.22 | exact rationals |
rates.py (part 4), v_rates.py (part V1) |
the inequalities at the ten endpoints of the five intervals of the deterministic rate certificate (Lemma 10.1) | exact rationals |
component_count_rate_interval.py |
the constant \(1.6444\) for Graph Motif, Connected Vertex Cover and its variants (Lemma 11.12, with the rate \(0.71755<\log1.6444\)) | exact rationals, including Collatz–Wielandt bounds on spectral radii; Arb |
dst_certificates.json, dst_certificate_verify.py, cz_bounds.py |
the three certificates, the bounds on \(c_{Z_j}e_{2,j}\) and the constant \(1.3727\) for Directed Steiner Tree (Proposition D.11.17) | exact rationals; Arb for logarithms |
paired_rate_certificate.py |
the constant \(1.6302\) for Paired Domination (Lemma D.11.19) | Arb |
The programs that produce the data files search in floating-point or decimal arithmetic; only the checks in the table are used (of these producers, only dst_certificate_build.py is included). The second table lists the programs behind the numerical statements of the paper. Each of these statements is marked as numerical where it is made, and no proof uses them.
Numerical evidence, not used in any proof
| File | Computes |
|---|---|
rs_closed_form_interval.py (numerical part) |
the maximum of the closed form \(F^*\) for RS, about \(0.8030893\), so that the constant \(1.744835\) of Proposition 6.1(c) exceeds the base \(2^{\max F^*}\) by less than \(2\cdot10^{-6}\) |
orthant/orthant_try.py |
the orthant antinorm search for RS-\(\theta\) that did not close (Remark D.4.3) |
lower_bound_caterpillar.py |
the finite values for uniform lobsters (Proposition 7.9) |
families.py, v_extremal.py |
the bases of stars of stars and paths, and the search over \(58\,800\) periodic families (Section 7.6) |
v_rates.py (part V5: \(1.9440\) at \(\sigma=0.4172629\), the value used in the text, and \(1.9443\) at \(\sigma=0.4176\), as in rates.py part 3) |
the black-box lower bound of about \(1.9440^n\) for RS-\(\theta\) (Theorem 9.4) |
rates.py (part 4, grid), v_rates.py (part V2; floating point, tolerance \(10^{-11}\)) |
numerical evidence that other choices of \(y\) would not lower the bound of Lemma 10.1: \(\max_{u}\inf_{y>0}\chi_y(u)\approx0.795823\), with grid maximizer \(u\approx0.436\) |
size_demo.py |
the sizes of the balanced product families for \(n\le20\) and block lengths \(4\) to \(6\): they contain 80–90% of all \(t\)-sets (Appendix D.7) |
motif_path_extremal.py |
\(\mathcal Z_F\ge\mathcal Z_{\text{path}}\) on trees with at most \(8\) vertices (after Theorem 11.13) |
wcds_spider.py |
the spider values after Proposition D.11.10 (Appendix F.5) |
dst_obstruction.py |
the bound \(\Omega(1.3716^n)\) for a family of instances of Directed Steiner Tree (Section 12.5) |
maxleaf-measure/optimise.py, maxleaf-measure/sensitivity.py |
the measure optimization for the algorithm of Binkele-Raible and Fernau (after Proposition C.4) |
The files of the measure optimization, of the orthant search for RS-\(\theta\) and of RSC are in the subfolders maxleaf-measure/, orthant/ and rsc/ of the ancillary folder; the tables give the paths of these files. All other files are at its top level. Each program is run as python3 <program> from the folder that contains it, with the data files of its table row as arguments where it reads them. verify_cert.py, verify_cert_indep.py and v_cert_primal.py take cert_final_0.json and cert_final_1.json; rsc-verify.py and rsc-verify-independent.py take rsc-certificate.json.gz and an optional number of processes; and dst_certificate_build.py takes dst_certificate_params.json. The other programs find their data themselves. The output of each program is recorded in the file of the same name with extension .out. For RSC, the outputs are rsc-verify.out, rsc-verify-independent.out (with rsc-verify-independent-negative.out for the perturbed copies) and rsc-credits.out. The programs need Python 3 with python-flint (tested with version \(0.9.0\)); some also need NumPy and SciPy. The file SHA256SUMS lists the SHA-256 checksums of all ancillary files; the certificate of RSC, rsc/rsc-certificate.json.gz, has SHA-256 checksum 9465bd0f7f74dc3a 6376724645bfbde9 7b417035583c89ba 787e347813177651. This file (\(45\) MB) is not among the ancillary files on arXiv, which would store it unpacked; it is in the archived copy of this release (Gaspers 2026) and on the companion site, at the same path. The script verify_all.sh checks the checksums and runs every program of the first table except the two that check the certificate of RSC with one command; with the option –full it also runs these two, which took about \(46\) and \(16\) minutes with four processes in our runs, while all other checks together took about a minute and a half on one core. The file README.md lists which file checks which statement. The ancillary files are released under the MIT license (file LICENSE).
F.1 The closed form of RS
For Proposition 6.1(c), the program rs_closed_form_interval.py covers \([0.2,0.8]\) by \(9608\) closed intervals with exact rational endpoints, obtained by adaptive bisection, and encloses \(F^*\) on each of them in ball arithmetic; every enclosure lies below the enclosure of \(\log1.744835\). The largest upper bound obtained is \(0.80309061427\) (rounded up), while \(\log1.744835=0.80309061469\ldots\), a margin above \(4.2\cdot10^{-10}\). The same program shows \(F^*\le0.7807\) on \([0.15,0.31]\) and \(F^*\le0.7802\) on \([0.54,0.8]\) in the same way, by two further coverings of these intervals, with \(60\) and \(73\) intervals, separate from the first one because the targets are lower; Proposition 6.1(c) states all three bounds, and RS-\(\theta\) uses the last two (Table 3).
F.2 The certificates of RS-\(\theta\)
For \(i\in\{0,1\}\), the file cert_final_\(i\).json stores the data \((y_i,e_{1,i},e_{2,i},Z_i)\) of certificate \(i\) of Proposition 7.7. Three independent programs check the hypotheses of Lemma 7.5 for both certificates in exact rational arithmetic: verify_cert.py, verify_cert_indep.py, which uses linear programming duality instead of the stored convex combinations, and v_cert_primal.py. The program cz_bounds.py computes \(c_{Z_i}=\min_{z\in Z_i}\mathrm{fin}(z)\) exactly, using the code of verify_cert.py, and checks the bounds \(c_{Z_0}\ge0.6212\) and \(c_{Z_1}\ge0.6293\) of Proposition 7.7 (the values are \(0.62120\ldots\) and \(0.62935\ldots\)), hence \(c_{Z_i}\ge0.62\), the bound used in Proposition 7.8. The program rst_rate_interval.py encloses the coefficients of \(\psi_0\) and \(\psi_1\) and their values at the four endpoints \(0.31\), \(0.4172629\) (twice) and \(0.54\) in ball arithmetic, starting from the exact rationals \(y_i,e_{1,i},e_{2,i}\); every enclosure lies below \(0.78270152<\psi^*\), with a margin \(\psi^*-\max>8\cdot10^{-8}\). It also checks \(2^{\psi^*}<1.7204\).
F.3 Uniform lobsters
For Proposition 7.9(c), the program lobster_rate_certificate.py produces the \(4764\) intervals \([a,b]\) covering \([0,\frac34]\), the rational vectors \(w>0\) and the rationals \(\lambda>0\), and the rational data \(v>0\) and \(\lambda'>0\) at \(y^*=0.3453\), and checks all the inequalities stated in the proof of Proposition 7.9 for these data in exact rational arithmetic.
The following computations are in floating point and are not used in any proof. The minimum over \(y>0\) of \(\log(1+y)-\frac17\log\lambda_{\max}(\mathbf M_y)\), for the nonnegative matrix \(\mathbf M_y\) of the proof of Proposition 7.9 and its largest real eigenvalue \(\lambda_{\max}(\mathbf M_y)\), which is its spectral radius by the Perron–Frobenius theorem, is \(0.7817982553\) at \(y^*=0.34531\), which gives the numerical value \(1.7192725\ldots\) of Proposition 7.9(c). The programs families.py and v_extremal.py compute the bases of stars of stars and of paths stated after the proof, and search \(58\,800\) periodic families; none has a larger base than \(\Lambda_L\).
F.4 The certificate of RSC
The data of Proposition D.5.23 are stored in rsc/rsc-certificate.json.gz. The points of \(Z\) and of the stages are stored as exact rationals. For each vector \(P\) whose membership in \(\mathrm{conv}(\mathcal Y)+\mathcal K_{\mathrm{pos}}\) is asserted, the file lists the points \(z_i\) and stores the weights \(\alpha_i\) as floating-point numbers, which the checking program converts to rationals with denominators at most \(10^{12}\) (the closest such rationals, by Fraction.limit_denominator), dropping nonpositive weights; these rationals are the coefficients \(\alpha_i\) of the proof of Proposition D.5.23, and the program checks exactly that \(\sum_i\alpha_i\ge1\) and that \(P\succeq\sum_i\alpha_iz_i\), the latter by evaluating all up-set sums; the poset cone has \(43\) nonempty up-sets. There are \(1024^2=1{,}048{,}576\) pair conditions for (C1); \(26\) conditions for (C2); \(1848\) conditions for (C4) (\(4\le\nu\le36\), for the points \((0,c_3)\) and the hull vertices with \(c_2\ge1\) of the lattice for \(\nu-1\), which the program recomputes exactly); and \(1962\) staged chains for (C5) (the points \((0,c_3)\), \(1\le c_3\le\nu\), and the hull vertices with \(c_2\ge1\) of the lattice for \(\nu\), \(1\le\nu\le36\)), with \(2{,}636{,}800\) conditions \(x\circ z\) in these chains. The file stores the values of \(d^{(3)}_{\min}(\nu)\) and \(d^{(2)}_{\min}(\nu)\) stated in Proposition D.5.23 for \(1\le\nu\le4\), and the value \(0\) for \(5\le\nu\le36\), where Proposition D.5.23 states the value \(1\); the proof of Proposition D.5.23 shows that both values give the same conditions. The check also confirms that all points of \(Z\) are nonnegative and that \(d^{(3)}_{\min}\le d^{(2)}_{\min}\), and it computes \(c_Z=0.60605\ldots\) exactly. Both programs described below also check exactly the inequality \((q_3/\hat e)^{37}\ge\hat e^{-25}\) of (C6), which covers the tail \(\nu>36\).
The checking program (rsc/rsc-verify.py, with rsc_verify_core.py and rsc_modelg.py in the same folder) works in rational arithmetic throughout; it also evaluates the inequalities of Definition D.5.10 and (30) in \(60\)-digit decimal arithmetic; this evaluation is not used, since Lemmas D.5.21 and D.5.22 prove these inequalities. The truncated-series bounds in the proof of Lemma D.5.22 are evaluated exactly by rsc/rsc-credits.py, which also rechecks the light pairs of Lemma D.5.21. A second program (rsc/rsc-verify-independent.py), written from the definitions of Section 8 without reusing any code of the first, re-derives the eight-state recursion, checks it exactly against a brute-force enumeration of the relaxed model and checks \(\widetilde W\le W^{\mathrm{tm}}\) on random trees, recomputes the lattice hulls, confirms that all \(613\) stage points are nonnegative, and verifies the same certificate in rational arithmetic, with rigorous rational bounds for the logarithms in Definition D.5.10 and (30); perturbed copies of the certificate are rejected by it at the expected condition. The first program checks every relation with the rationals above as the coefficients \(\alpha_i\) of the proof. The second accepts a relation if it holds with these rationals or with the exact binary values of the stored weights; either set of nonnegative coefficients proves the relation, so both programs confirm the same relations, possibly with different coefficients.
The points were found by an iterative floating-point search and then rounded to rationals; only the exact check is used.
F.5 The deterministic rate certificate
For Lemma 10.1, the inequalities between rational numbers at the ten endpoints of the five rational intervals, against \(\log\frac{1736}{1000}\), are checked in exact rational arithmetic by rates.py (part 4) and, independently, by v_rates.py (part V1).
Separately, for the spiders of Proposition D.11.10, the program wcds_spider.py computes \(\beta_s\), the largest value of \(\bigl(\inf_{y>0}(1+y)^n/W_S(y)\bigr)^{1/n}\) over \(d_1,\dots,d_s\in\{2,3\}\), by one-dimensional minimization over \(y\) in floating point. It gives \(\beta_{50}=1.743507\), \(\beta_{200}=1.737898\) and \(\beta_{1000}=1.736432\), decreasing toward \(\sqrt5-\frac12=1.736068\ldots\). These values are numerical evidence and are not used in any proof.
F.6 The component-count certificate
For Lemma 11.12, the program component_count_rate_interval.py checks the inequalities (o)–(iii) of its proof with exact rational parameters and ball arithmetic for the logarithms. In (iii), \(\lambda_{\max}(M_{y_j})\) is bracketed between rationals by the Collatz–Wielandt inequalities \(\min_i(M_{y_j}v)_i/v_i\le\lambda_{\max}(M_{y_j})\le\max_i(M_{y_j}v)_i/v_i\) for positive vectors \(v\), evaluated exactly; the lower bracket enters \(\phi_{2,\sigma}(y_j)\), which is decreasing in \(\lambda_{\max}(M_{y_j})\), and the upper one the prefactor. Part B of the same program rechecks the identities and the inequality behind the value \(1.8\) (Corollary 11.5 and Lemma D.9.8), including \(5^{45}>3^{64}\) in exact integer arithmetic; the proofs of these statements do not use it. The largest value of \(\max\bigl(\phi_{2,\sigma^-_j}(y_j),\phi_{2,\sigma^+_j}(y_j)\bigr)\) in (iii) is \(0.7174350\ldots\), against \(\psi=0.71755\) and \(\log1.6444=0.7175613\ldots\); the largest prefactor \(\lambda_{\max}(M_{y_j})/\min(1,y_j)\) is at most \(5.933\). The program motif_path_extremal.py checks the inequality \(\mathcal Z_F\ge\mathcal Z_{\text{path}}\) raised after Theorem 11.13 for all trees on at most \(8\) vertices at \(\zeta\in\{\frac18,\frac14,\frac12,1,2,4\}\) in exact rational arithmetic; this is evidence only.
F.7 Directed Steiner Tree
The file dst_certificates.json stores the three certificates of Proposition D.11.17 and the weights \(\lambda_j\). The program dst_certificate_verify.py checks the hypotheses (C1)–(C3) in exact rational arithmetic and that the weights \(\lambda_j\) are nonnegative and sum to \(1\). The program cz_bounds.py computes \(c_{Z_j}\) exactly (\(0.52305\ldots\), \(0.53544\ldots\) and \(0.02153\ldots\)) and checks \(c_{Z_j}e_{2,j}\ge0.40\), \(0.41\) and \(0.011\) (Proposition D.11.17), so \(c_{Z_j}e_{2,j}\ge1/100\) for every \(j\), as the proof of Theorem 12.8 uses. Membership of a point \(x\) in \(\mathcal R_Z\) is certified by a witness, a point of \(Z\) or a rational convex combination of two points of \(Z\) that lies coordinatewise below \(x\); in the plane such a witness exists whenever \(x\in\mathcal R_Z\). The logarithms in \(\boldsymbol\alpha_j\) and the weighted sums \(\sum_j\lambda_j\alpha_{j,i}\) are enclosed by the same program in ball arithmetic, starting from the exact rationals \(y_j,e_{1,j},e_{2,j},\lambda_j\); the enclosure of their maximum \(0.4569669\ldots\) lies more than \(3.3\cdot10^{-5}\) below \(0.457\), and \(0.457<\log1.3727\) is checked in the same arithmetic. The program dst_obstruction.py computes, in floating point, the value \(1.37168\ldots\) behind the bound \(\Omega(1.3716^n)\) stated after Theorem 12.8; this is evidence only. The family consists of a directed path \(r\to p_1\to\dots\to p_{2L}\) in which each odd \(p_{2i-1}\) has one terminal out-neighbor of out-degree \(0\) and one further out-neighbor with two such terminals, each even \(p_{2i}\) has two such terminals, and \(\lfloor\varkappa L\rfloor\) padding vertices have arcs to and from both terminals of \(p_2\). The spine and its further out-neighbors form the only Steiner set of size at most \(3L\), and as \(L\to\infty\) the bound \(\bigl(\min_t\binom{n_U}{t}/\mu_t(S^*)\bigr)^{1/n}\) for this set is largest at \(\varkappa\approx2.9663\), where it equals \(2^{5/(8+\varkappa)}=1.37168\ldots\).
F.8 Paired Domination
For the first claim of Lemma D.11.19, the program paired_rate_certificate.py encloses \(y^*\) and \(h_{\bar n}(y^*)\) for \(2\le\bar n\le40\) in ball arithmetic and checks \(h_6(y^*)-h_{\bar n}(y^*)>0.00297\) for \(\bar n\neq6\), and it checks the tail bound \(\log(1+y^*)+\frac2{41}\log\frac1{y^*}<0.431<h_6(y^*)\) in the same arithmetic, starting from \(y^*=(3\sqrt3-1)/16\). It also checks \(h_6(y^*)<0.70502\) and \(2^{0.70502}<1.6302\), the two inequalities used in the proof of Theorem 12.10.
F.9 Formal verification
Part of the analysis is also checked in Lean 4 with Mathlib. Except for the data of the RSC certificate (see the end of this subsection), it is checked by the Lean kernel, using only the standard axioms (propositional extensionality, choice and quotient soundness) and without compiled evaluation (native_decide). The statements below refer to the Lean files in the folder formal/ of the ancillary files, a copy of the development as of 1 November 2026; the files lean-toolchain and lake-manifest.json there pin the versions of Lean and Mathlib. They cover the following statements.
Soundness and success probability, items (ii) and (iii), of Theorem 3.5, for the cap and trial counts stated after Algorithm 3.4; Lemma 3.8; and soundness and success probability of Theorem 3.14 for abstract trials. Also both inequalities of Lemma 3.9: the first in the form of the last sentence of Theorem 3.5, the second in the pointwise form of its proof; and Proposition 3.10 for the same cap and trial counts, with the probability that some trial runs \(\mathcal{A}\) on a subset of \(S\) in place of the expected number of such trials.
The Jensen step of the proof of Theorem 4.1 and the success probability it gives; the minimization in Remark 4.4 (\(f_\sigma\) is strictly convex on \([0,\sigma]\) and attains its minimum exactly at \(\tau^*\)); the inequality of part (1) of Corollary 4.3, and its part (2).
Lemma 5.1, with the spanning tree shown to exist rather than computed; Lemmas 5.10 and 5.11; the inequality of Lemma 5.9, without its equality case; the claims of Lemma 5.2 about the output; and Corollary 8.5 except (T1), running time and space, for abstract trials, with its claim for Max Leaf Spanning Tree when \(n\ge3\).
For RS-\(\theta\): Lemmas 7.3, 7.4, D.4.1 and 7.5; both certificates of Proposition 7.7, checked in exact rational arithmetic, with the numerical claims of Proposition 7.7 and \(2^{\psi^*}<1.7204\); the constants of Theorem 7.2; and Proposition 7.8.
For RS: Proposition 6.1, with part (c) by interval covers checked in exact rational arithmetic; Corollary 6.2; and the moment bound in the proof of Theorem 6.4, with \(\log1.744835<\psi_{\mathrm{RS}}\).
For RSC: Proposition 8.6 from conditions (C1), (C2), (C4) and (C5) of a certificate with \(c_Z>0.6060\), through all statements of Appendix D.5 except Proposition D.5.23; the claim of Lemma 8.4(a) that a trial rejects if \(\gamma_{\mathrm{c}}(G)>s\), and Lemma 8.4(b); and, from the same conditions, that the output of Theorem 8.1 is never below \(\gamma_{\mathrm{c}}(G)\), its success probability, and its claim for Max Leaf Spanning Tree when \(n\ge3\). The bound \(\varrho<1.6991\) is checked as an exact rational comparison. The two Lean definitions of the closure generating function of Definition 8.3 that these results use are proved equal.
For the Steiner extension: the correctness of the computed value in Lemmas 5.3 and 5.6 and Corollary 5.8, that is, the inclusion–exclusion over branching walks on the directed encoding returns \(\operatorname{OPT}(J)\) for every state \(J\), and \(\mathcal{A}_{\mathrm{St}}\) solves \(\Phi_{\mathrm{CDS}}\)-Extension. So the acceptance test of step (c) of Algorithm 8.2, as the algorithm computes it, accepts exactly the samples that its specification accepts, and the two RSC results above are also proved for that test. No Lean function returns a connected dominating set or a spanning tree.
Lemma 10.1; Lemma 11.12, with \(\lambda_{\max}(M_\zeta)\) given by its closed form in Definition 11.1; Lemma 11.2 for every finite tree and Lemma 11.3 for paths, both with the same closed form, which is proved to be the largest eigenvalue of \(M_\zeta\); part (a) of Corollary 11.5; the final inequality \(5^{45}>3^{64}\) in the proof of Lemma D.9.8; Proposition D.11.17, Lemmas D.11.14, D.11.15 and D.11.16 and equation (38), which give the lower bound on \(W_S(y_j)\) in the proof of Theorem 12.8, and the constants of that proof; Lemmas D.11.18 and D.11.19, the constants of Theorem 12.10 and condition (\(\star\)) for every paired dominating set, and Proposition 12.11, whose last claim is checked for the cap and trial counts stated after Algorithm 3.4 and an extension algorithm that accepts exactly the yes-instances (the step to the algorithm of Lemma 12.9 is not in Lean: that algorithm accepts only yes-instances, so a run with it accepts only on samples on which the run with the exact algorithm accepts); and the two bounds of part (c) of Proposition 7.9, for \(\Lambda_L\) and for every graph that has the same edges as \(\Lambda_L\) at the vertices of \(S^*\).
The data of the RSC certificate are checked in Lean as well, but not by the kernel alone. The program formal/scripts/export_rsc_cert.py translates rsc/rsc-certificate.json.gz into Lean data files. Checking functions written in Lean, whose correctness is proved in the kernel with the standard axioms, are evaluated on these data by compiled code (native_decide, in \(472\) generated theorems). From this Lean proves Proposition D.5.23 as stated: the \(1024\) points of \(Z\) satisfy (C1)–(C6), and for the same \(Z\) there are nonnegative rational stages of the stated sizes that satisfy the relations defining stages. The same theorem contains the conditions on the parameters in Lemma D.5.20, which the proof of Proposition D.5.23 checks. Lean also proves the exact value of \(c_Z\), a fraction equal to \(0.60605\ldots\), and proves (C5) directly for every sequence of the required length, the form that Lemma D.5.20 uses. With the RSC item above, this gives the success probability in Theorem 8.1 with no assumption on the certificate. This check trusts the Lean compiler in addition to the kernel; it is a third check of the data, beside the two programs of Appendix F.4. The large generated data files (about \(170\) MB) are not included: the program regenerates them, and formal/MaxLeafFormal/RSCData/MANIFEST.sha256 lists the SHA-256 checksums of the files that Lean checked. Files regenerated with the exporter shipped here differ from those only in one header comment, the checksum of the exporter; the README.md of the ancillary files shows how to restore it, after which all checksums match.
Not checked in Lean are running times and space bounds, the algorithms other than the Steiner tree computation, parts (b) and (c) of Corollary 11.5, parts (a) and (b) of Proposition 7.9, the last sentence of its part (c) (the bracketing up to factors and the numerical limit) and the consequence stated after it, and the graph-theoretic parts of the other applications.