Formalisation and certificates
Parts of the paper are proved in Lean 4 with Mathlib, and several constants rest on computer certificates. This page maps each formalised statement to its Lean declarations and each certified statement to its files, in the order of the paper. The dependency graph shows how the formalised statements depend on each other.
Lean proofs
“Proved” means that the Lean theorem states the paper’s claim, under the modelling choices in the note, and proves it. “Partly proved” means that Lean covers the part named. Every declaration below was checked, and its axioms printed, in the author’s fresh Lean build of this release; the release page gives the axiom audit and the commands to repeat the check.
| Paper | Lean (namespace MaxLeafFormal) |
Coverage |
|---|---|---|
| Theorem 3.5 | MLS.mls_soundMLS.mls_successMLS.mls_budget |
partly proved: item (ii) (soundness, on every outcome); item (iii) (success probability) for the cap \(\Theta=\lceil\psi n+\log\Gamma\rceil+1\) and the trial counts \(m_{t,\theta}=\lceil M_{t,\theta}\rceil\); and the arithmetic of item (i) (the total time budget) for the same choice. The model fixes one instance and replaces the extension algorithm by its specification; running time and space are not modelled beyond the budget arithmetic. Independent trials are a product measure over all trial slots. The other admissible caps and trial counts of (2) are not covered for the uniform samples of Algorithm MLS-\(\theta\): budgeted_success_of_admissible (Theorem 3.14) covers them for abstract trials, but the step from uniform samples to (T3) is not formalised. |
| Lemma 3.8 | Budget.integral_twoPowNeg_posBudget.threshold_probBudget.threshold_prob_upper |
proved: the whole lemma: \(\mathbb E[2^{-\xi}]>0\) and parts (a) and (b), for a measurable \(\xi\) with values in \([0,\infty]\) on any probability space, with \(\Pr[\xi<\infty]>0\). \(\Theta\) in (a) is a natural number and \(\theta\) in (b) any integer, as in the paper. threshold_prob_aux proves (a) without the hypothesis \(\Pr[\xi<\infty]>0\). The earlier finite form (a random variable uniform over finitely many values, the case that Algorithm MLS-\(\theta\) uses) is MLS.threshold_selection and MLS.threshold_upper. Proofs in MaxLeafFormal/Budget.lean. |
| Lemma 3.9 | MLS.star_of_WMLSNec.fw_gf_upperMLSNec.mu_mul_pow_le_WMLSNec.pow_le_choose_mul |
partly proved: the first inequality, in the form used later: a lower bound \(W_S(y)\ge(1+y)^n2^{-\psi n}/\Gamma\) for some \(y\ge0\) gives condition \((\star)\); and the second inequality in pointwise form: for each \(t\le k\) some \(y\ge0\) has \(\mu_t(S)(1+y)^n\le(n+1)\binom nt W_S(y)\) (fw_gf_upper), for any real exponent \(g\) and any \(S\) with \(|S|=k\), with its two steps \(W_S(y)\ge\mu_t(S)y^t\) and \((1+y)^n\le(n+1)\binom nty^t\) at \(y=t/(n-t)\). The infimum form of the second inequality follows from fw_gf_upper by dividing by \(\mu_t(S)>0\) and \(W_S(y)>0\); that step is not in Lean. fw_gf_upper and its two steps are from run fa-pd-rest, accepted 2026-10-30, kernel-checked with the standard axioms only (no native_decide). |
| Proposition 3.10 | MLSNec.mls_necessaryMLSNec.Pnec |
partly proved: the probability form, for the cap \(\Theta=\lceil\psi n+\log\Gamma\rceil+1\) and the trial counts \(m_{t,\theta}=\lceil M_{t,\theta}\rceil\): for \(k\le n\), \(\psi\ge0\), \(\Gamma\ge1\), \(\kappa>0\) and \(|S|\le k\), the probability that some trial runs the extension algorithm on a subset of \(S\) is at most \(P_{\mathrm{nec}}2^{\psi n}B\) for every \(B\ge\max_{t\le|S|}\mu^{(k)}_t(S)/\binom nt\), which gives the bound \(\frac14\) of the last sentence. The expected-count display, other admissible caps and trial counts, and \(P_{\mathrm{nec}}\le N^{O(1)}\) are not stated. The exponent \(g\) is any real function and \(S\) any set of size at most \(k\). Run fa-pd-rest, accepted 2026-10-30. Kernel-checked with the standard axioms only (no native_decide). Proofs in MaxLeafFormal/MLSNec.lean. |
| Theorem 3.14 | Budget.budgeted_soundBudget.budgeted_successBudget.budgeted_success_of_admissible |
partly proved: soundness (every YES answer, on every outcome, under (T2)) and the success probability \(\ge1-e^{-\kappa}\) under (T3) and the moment condition, for any cap and trial counts within the ranges of (2). (T1) and the running-time and space bound are not modelled. Trials are abstract probability spaces with an acceptance event, run independently (a product measure over all trial slots); the index set is any finite type. budgeted_success assumes only the lower bounds on \(\Theta\) and \(m\) and does not mention \(S\), so it implies the paper’s statement; budgeted_success_of_admissible restates it with the full ranges. Proofs in MaxLeafFormal/Budget.lean. |
| Theorem 4.1 | MLS.mu_ge_of_meanMLS.mls_success_of_mean |
partly proved: the Jensen step of the proof and the success probability it gives through Algorithm MLS-\(\theta\). The direct algorithm with the Markov cutoff (Remark 4.2) is not formalised; running time and space are not modelled. |
| Corollary 4.3 | MLS.linear_savings_WMLS.one_sample_size |
partly proved: the inequality of part (1), and part (2). Part (2) is the last clause of one_sample_size. The algorithm of part (1) is not formalised. |
| Remark 4.4 | MLS.one_sample_size |
partly proved: the minimisation: \(f_\sigma\) is strictly convex on \([0,\sigma]\), and its minimum \(F^*(\sigma)\) is attained exactly at \(\tau^*\) with the closed forms. Lean proves strict convexity from a strictly increasing derivative, then the minimum by monotonicity on \([0,\tau^*]\) and \([\tau^*,\sigma]\); the paper argues through the Kullback–Leibler identity. |
| Lemma 5.1 | CDS.maxLeaf_eqCDS.spanningTree_of_CDSCDS.maxLeaf_small |
partly proved: both sentences, with the spanning tree shown to exist: for \(n\ge3\) the maximum number of leaves of a spanning tree is \(n-\gamma_c(G)\) (maxLeaf_eq) and every connected dominating set \(S\) gives a spanning tree with at least \(n-|S|\) leaves (spanningTree_of_CDS, for every \(n\)); for \(n\le2\), \(G\) is a tree and its only spanning tree, with no leaf if \(n=1\) and two leaves if \(n=2\) (maxLeaf_small). The polynomial-time computation is not modelled (existence only). |
| Lemma 5.2 | Budget.first_accepted |
partly proved: the claims about the output: it is never below \(\operatorname{opt}(I)\), and it equals \(\operatorname{opt}(I)\) with at least the probability that the run at \(\operatorname{opt}(I)\) accepts. Running time and space are not modelled. The Max Leaf Spanning Tree clause for \(\Phi_{\mathrm{CDS}}\) is covered through Corollary 8.5 (cds_budgeted_maxLeaf) for \(n\ge3\) and through Lemma 5.1 (maxLeaf_small) for \(n\le2\). Proofs in MaxLeafFormal/Budget.lean. |
| Lemma 5.3 | SteinerDir.steinerAlg_eqSteinerDir.bIE_countSteinerDir.bw_countSteinerDir.bw_memSteinerDir.bw_zeroSteinerDir.bw_posSteinerDir.feasible_of_walkSteinerDir.walk_of_feasible |
partly proved: correctness: for every finite digraph, root \(r\), terminal set \(K\) and weights \(\varphi\), the algorithm of the proof (inclusion–exclusion over branching-walk counts, with the least-length rule) returns \(\mathrm{OPT}_\varphi(\vec G,r,K)\), and \(\infty\) if no feasible set exists (steinerAlg_eq). Running time and space are not modelled. The procedure is fixed as the Lean definition steinerAlg and pinned by rfl examples, so the theorem is about the paper’s algorithm, not only its output. The hypothesis \(r\notin K\) is not needed. Run cds-maxleaf-rsc-steiner, accepted 2026-10-30. Proofs in MaxLeafFormal/SteinerDir.lean. |
| Lemma 5.6 | SteinerCDS.optSt_eq_optDirSteinerCDS.isState_JbSteinerCDS.optSt_eq_inf_JbSteinerCDS.stateAlg_eq |
partly proved: correctness: (25) for every state \(J\) and every \(C_1\in\mathcal D\) (optSt_eq_optDir), the reduction for \(\mathcal D=\emptyset\) (optSt_eq_inf_Jb), and that the combined computation on the directed encoding returns \(\mathrm{OPT}_\varphi(J)\) for every state (stateAlg_eq). Running time and space are not modelled. stateAlg picks \(C_1\) by choice, so it is a mathematical function, not a program; optSt_eq_optDir holds for every \(C_1\). Run cds-maxleaf-rsc-steiner, accepted 2026-10-30. Proofs in MaxLeafFormal/SteinerCDS.lean. |
| Corollary 5.8 | SteinerCDS.aSt_iff_extSteinerCDS.aSt_iff_extYesSteinerCDS.not_aSt_of_ltSteinerCDS.isSol_JX_iffSteinerCDS.isState_JXSteinerCDS.terminals_JXSteinerCDS.optSt_J0 |
partly proved: correctness: \(\mathcal A_{\mathrm{St}}\), which tests \(\mathrm{OPT}(J_X)\le k-|X|\) with the value computed as in Lemma 5.6, solves \(\Phi_{\mathrm{CDS}}\)-Extension for every \(X\) and \(k\) (aSt_iff_ext), and rejects when \(k<|X|\); \(J_X\) is a state whose solutions are the sets \(Y\) disjoint from \(X\) with \(X\cup Y\) a connected dominating set; (13) (terminals_JX). Running time and space are not modelled. No Lean function returns a connected dominating set or a spanning tree; RSCSteiner.rscAcceptSt_witness and rscAcceptSt_witness_min state only that they exist. RSCSteiner.rsc_success_of_data_st and rsc_maxLeaf_of_data_st are CO-6 and CO-8 of Theorem 8.1 with this computation in place of the specification of \(\mathcal A_{\mathrm{St}}\). Run cds-maxleaf-rsc-steiner, accepted 2026-10-30. Proofs in MaxLeafFormal/SteinerCDS.lean and MaxLeafFormal/RSCSteiner.lean. |
| Lemma 5.9 | CDS.tree_inequality |
partly proved: the inequality; the equality case is not formalised. |
| Lemma 5.10 | CDS.pointwise |
proved: the whole lemma. |
| Lemma 5.11 | CDS.mean_terminals |
proved: the average bound, with the terminal count defined by the formula \(n-|N[X]|+\mathrm{comp}(G[X])\). That this formula counts the terminals of the Steiner instance \(J_X\) (13) is SteinerCDS.terminals_JX, listed under Corollary 5.8; the two are not combined in one theorem. |
| Proposition 6.1 | RSRateAB.rs_rate_aRSRateAB.rsfσ_min_eqRSRateAB.rs_rate_bRSRateAB.rs_rate_b_argminRSRateAB.rs_base_denomRSRateAB.rs_baseRSRateAB.rsfσ_eq_fσRSRateAB.rsTau_eq_τstarRSRate.rs_rate_cRSRate.rsF_oneRSRate.rsF_eq_Fstar |
proved: (a): for every \(\sigma\in(0,1)\), \(F^*(\sigma)<H(\sigma)\le1\), and \(f_\sigma\) has its unique minimum over \([0,\sigma]\) at \(\tau^*\in(0,\sigma)\) with value \(F^*(\sigma)\); (b): at \(\sigma=\frac12\), \(\tau^*=\frac13\) and \(F^*(\frac12)=\frac12\log3\), base \(\sqrt3\); (c): \(F^*(\sigma)\le\log1.744835\) for every \(\sigma\in(0,1]\), \(F^*\le0.7807\) on \((0,0.31]\) and \(F^*\le0.7802\) on \([0.54,1]\), with \(F^*\) given by (14). Parts (a) and (b) are RSRateAB (run rs-rate-ab, accepted 2026-10-30); rsfσ_eq_fσ and rsTau_eq_τstar identify its rsfσ and rsTau with MLS.fσ and MLS.τstar at \(\beta=1\), \(\rho=1/\sigma\). rs_base_denom states the denominator \(\sigma^\sigma(1-\sigma)^{1-\sigma}=2^{-H(\sigma)}\) of the base. Part (c): rsF_eq_Fstar identifies rsF with MLS.Fstar at \(\beta=1\), \(\rho=1/\sigma\); rsF_one gives \(F^*(1)=0\); the interval covers RSCover0–21 are exported by export_rs_cover.py and re-checked in Lean. Kernel-checked with the standard axioms only (decide +kernel and norm_num; no native_decide). |
| Corollary 6.2 | RateAssembly.rs_moments |
proved: the whole corollary, for the running-time exponent \(g(X)=|\mathrm{Tm}(J_X)|\), as (⋆) with \(\Gamma=2\) and \(\omega=F^*(s/n)\). \(g\) is RateAssembly.gT. Proved from Lemma 5.11 (CDS.mean_terminals) and the linear-savings bound of part 1B. Standard axioms only. |
| Theorem 6.4 | RateAssembly.rs_starRSRate.rs_constants |
partly proved: the completeness inequality of the proof: (⋆) with \(\Gamma=2\) and \(\psi_{\mathrm{RS}}=0.80309062\) for every connected dominating set, and \(\log1.744835<0.80309062\) with \(1.744835\le2^{0.80309062}<1.744836\). The algorithm, its running time and space, and the composition with Theorem 3.5 are not formalised here. Standard axioms only. |
| Theorem 7.2 | RSThetaRate.rst_rates |
partly proved: the constants only: \(2^{\psi^*}\in[1.7203,1.7204)\) for \(\psi^*=0.7827016\), together with \(0.7807<\psi^*\) and \(H(0.2)<0.7802\) (used in the proof of Proposition 7.8). The algorithm and its running time are not formalised; Proposition 7.8 is now in Lean (RateAssembly.rst_rate). Kernel-checked with the standard axioms only (decide +kernel and norm_num; no native_decide). |
| Lemma 7.3 | CDS.tree_reductionCDS.moment_bound_of_tree_boundCDS.rstheta_moment_bound_0CDS.rstheta_moment_bound_1LobsterGraph.tree_reduction_eq |
proved: the inequality and its consequence for \(W_S(y)\); the equality clause, for every \(X\subseteq S\) when \(F=G[S]\) and every vertex outside \(S\) has exactly one neighbour in \(S\) (tree_reduction_eq, which does not assume that \(G\) is connected, that \(S\) is a connected dominating set or that \(F\) is a tree); with the certificates, the two moment bounds that RS-\(\theta\) feeds to the main theorem. |
| Lemma 7.4 | Antinorm3.triple_singleAntinorm3.triple_splitAntinorm3.treeW_eq_fin |
proved: the identity \(W_{F,\nu}(y)=\mathrm{fin}(\mathrm{msg}_r)\) through the base case and the merge step of the recursion; the messages are defined in closed form, so they do not depend on the order of the children. The nonnegativity of the messages is proved as Antinorm3.triple_nonneg, which is built in the release build but not linked, because axioms.txt, the audit of the linked declarations, does not list it. |
| Lemma 7.5 | Antinorm3.merge_mem_smul_PZAntinorm3.init_allAntinorm3.triple_D_memAntinorm3.tree_bound_of_certificate |
proved: the whole lemma: under (a) and (b), \(W_{F,\nu}(y)\ge c_Ze_1^{\,s}e_2^{\,\nu(F)}\) for every tree and every \(\nu\) (tree_bound_of_certificate, through triple_D_mem), and the tail claim (init_all); Antinorm3.merge_mem_smul_PZ is the merge step of the proof. |
| Proposition 7.7 | RSThetaCert.cert0_ZRSThetaCert.cert0_pairsRSThetaCert.cert0_initsRSThetaCert.cert1_ZRSThetaCert.cert1_pairsRSThetaCert.cert1_initsAntinorm3.tree_bound_of_checksrstheta_tree_bound_0rstheta_tree_bound_1RSThetaRate.rst_ratesRSThetaRate.rst_rates_detail |
proved: both certificates, checked in the Lean kernel on exact rationals (decide +kernel), and the two tree bounds they give; and the numerical claims of the display: each ten-decimal coefficient of \(\psi_0,\psi_1\) within \(\frac12\cdot10^{-10}\) of the exact one, \(\sigma_\times\in[0.4172629270,0.4172629271)\), the maximum of the display (as an IsGreatest of the union of the two images) in \([0.78270151357,0.78270151358)\), and \(\psi_0,\psi_1<0.78270152<\psi^*=0.7827016\) on their intervals. The certificate data in RSThetaCert.lean is exported from cert_final_0.json and cert_final_1.json; RSThetaRate reuses the same constants. The paper writes the proved value as \(0.78270151357\ldots\), which lies in \([0.78270151357,0.78270151358)\). Kernel-checked with the standard axioms only (decide +kernel and norm_num; no native_decide). |
| Proposition 7.8 | RateAssembly.rst_rate |
proved: the whole proposition, as (⋆) with \(\Gamma=2\) and \(\psi^*=0.7827016\), for every connected graph and every connected dominating set. Combines Corollary 6.2 and Proposition 6.1(c) outside \((0.31,0.54)\) with the two RS-θ certificates (Proposition 7.7) inside. Standard axioms only. |
| Proposition 7.9 | Lobster.u_eqLobster.M_mulVecLobster.lobster_lowerLobster.lobster_upperLobsterGraph.LamLobsterGraph.SstarLobsterGraph.lobW_eq_matrixLobsterGraph.mu_mul_pow_le_WLobsterGraph.pow_le_choose_mulLobsterGraph.lob_moments_upperLobsterGraph.lob_moments_lowerLobsterGraph.rst_caterpillar_cLobsterGraph.rst_caterpillar_c_of_agree |
partly proved: the two displayed bounds of part (c), for every \(L\ge1\), with \(\Lambda_L\) the graph LobsterGraph.Lam on \(\mathrm{Fin}\,L\times\mathrm{Fin}\,7\) and \(S^*\) = LobsterGraph.Sstar: \(\mu_t(S^*)/\binom nt\le(n+1)\,1.71927^{-n}\) for \(0\le t\le n=7L\), and \(\binom nt\le C\cdot1.71928^n\mu_t(S^*)\) for some \(t\le3L\), with one \(C>0\) for all \(L\) (the paper’s \(\min_t\binom nt/\mu_t(S^*)\le C\cdot1.71928^n\)); the same two bounds for every graph on the same vertices whose edges at \(S^*\) are those of \(\Lambda_L\) (rst_caterpillar_c_of_agree); on the way, the identity \(W_{S^*}(y)=f^{\mathsf T}\mathbf M_y^{L-1}\mathbf u_y\) for every real \(y\) (lobW_eq_matrix) and the two certified matrix inequalities (Lobster.lobster_lower, Lobster.lobster_upper), with \(\mathbf u_y\), \(\mathbf M_y\) the recursion of Lemma 7.4. Not claimed: parts (a) and (b), the last sentence of (c) (the bracketing up to the factors \((n+1)^{1/n}\) and \(C^{1/n}\), and the numerical limit \(1.7192725\ldots\)), the consequence, and the step from “unique maximum-leaf spanning tree \(\Lambda_L\)” to agreement at \(S^*\). \(\Lambda_L\) is one fixed labelling of the uniform \((2,2)\)-lobster. The cell data (LobsterData.lean) are exported by export_lobster_cells.py and re-checked in Lean. Run rst-caterpillar-rest, accepted 2026-10-30, on top of Appendix G part 8H. Kernel-checked with the standard axioms only (decide +kernel and norm_num; no native_decide). Proofs in MaxLeafFormal/Lobster.lean and MaxLeafFormal/LobsterGraph.lean. |
| Theorem 8.1 | RSCHeadline.rsc_successRSCTrials.rsc_success_of_boundRSCCompose.rsc_success_of_dataRSCCompose.rsc_maxLeaf_of_dataRSCCompose.rsc_rho_ltRSCCompose.Wcl_eq |
partly proved: the probability part for a connected graph \(G\): Algorithm RSC, with the parameters of the paper and any cap and trial counts meeting the lower bounds of (2), never outputs a value below \(\gamma_c(G)\) and outputs \(\gamma_c(G)\) with probability at least \(1-e^{-\kappa}\), both for the ancillary certificate with no data hypotheses (RSCHeadline.rsc_success, with the compiler trust of Proposition D.5.23) and for any certificate satisfying conditions (C1), (C2), (C4), (C5) with \(c_Z>0.6060\) (rsc_success_of_data, standard axioms only); under conditions (C1), (C2), (C4), (C5) with \(c_Z>0.6060\) and for \(n\ge3\), the output \(n-s\) is the maximum number of leaves of a spanning tree with the same probability (rsc_maxLeaf_of_data, the Max Leaf clause); also \(1.6990<\varrho<1.6991\) (rsc_rho_lt), and the form conditional on Proposition 8.6 alone (rsc_success_of_bound). RSCHeadline.rsc_success instantiates rsc_success_of_data with the certificate of Proposition D.5.23, so it is unconditional but not kernel-only: it inherits the native_decide trust of Proposition D.5.23 (see there). The Max Leaf clause is in Lean only in its conditional form (rsc_maxLeaf_of_data). The running time and polynomial space are not covered. These theorems use the specification of the Steiner extension; the paper’s computation is proved to accept exactly the same samples (RSCSteiner.rscAcceptSt_eq, Corollary 5.8), and RSCSteiner.rsc_success_of_data_st and rsc_maxLeaf_of_data_st state the two conditional results with it. The two Lean definitions of \(W^{\mathrm{cl}}_S\) are proved equal (RSCCompose.Wcl_eq). Proofs in MaxLeafFormal/RSCTrials.lean, MaxLeafFormal/RSCCompose.lean, MaxLeafFormal/RSCHeadline.lean and MaxLeafFormal/RSCSteiner.lean. |
| Lemma 8.4 | RSCTrials.rsc_trials_T2RSCTrials.rsc_trials_T3RSCTrials.rsc_trials_W |
partly proved: the soundness part of (a) (an accepting trial for \(s\) gives \(\gamma_c(G)\le s\)) and all of (b): (T3) for every connected dominating set \(S\) with \(\lvert S\rvert=s\), and \(W^{\mathrm{cl}}_S(y)\le(1+y)^n\max_{0\le t\le\lvert S\rvert}\mathbb E[2^{-\xi_t}]\) for every \(y\ge0\). The running time of (a) is not modelled. The closed-sample distribution is modelled exactly; the Steiner extension is replaced by its specification, and \(\lvert\mathrm{Tm}(J_X)\rvert\) by the formula of (13). The inequality is proved for every \(S\subseteq V\). Proofs in MaxLeafFormal/RSCTrials.lean. With the Steiner computation itself (Corollary 5.8), the same acceptance rule is RSCSteiner.rscAcceptSt (rscAcceptSt_eq), and that (13) gives the terminal count is SteinerCDS.terminals_JX. |
| Corollary 8.5 | Budget.cds_budgetedBudget.cds_budgeted_maxLeaf |
partly proved: everything except running time and space: under (T2) for every \(s\) and (T3) with the moment condition at \(s=\gamma_c(G)\), the output is never below \(\gamma_c(G)\) and equals \(\gamma_c(G)\) with probability at least \(1-e^{-\kappa}\); for \(n\ge3\), \(n\) minus the output is the maximum number of leaves of a spanning tree with the same probability. (T1), running time and space are not modelled. Trials are abstract probability spaces, independent across all runs; the lower bounds on the cap and trial counts are assumed for every \(s\). Proofs in MaxLeafFormal/Budget.lean. |
| Proposition 8.6 | RSCGraph.rsc_bound_of_dataRSCGraph.rsc_bound_of_data'RSCCompose.rsc_bound_trials |
partly proved: the bound, conditional on the certificate conditions (C1), (C2), (C4), (C5); the primed form also assumes \(c_Z>0.6060\). The conditions are proved for the ancillary certificate in Proposition D.5.23 (RSCFinal, with native_decide and so with compiler trust); the bound for that certificate is not restated as one theorem here, but RSCHeadline.rsc_success (Theorem 8.1) uses it. Proofs in MaxLeafFormal/RSCGraph.lean. RSCCompose.rsc_bound_trials restates the bound for the definition of \(W^{\mathrm{cl}}_S\) used in Theorem 8.1 (MaxLeafFormal/RSCCompose.lean). |
| Lemma 10.1 | DetRate.det_cert |
proved: the whole lemma: for every \(u\in[0.15,0.85]\) some \(y\in\{\frac{1+\sqrt5}8,\frac12,\frac5{16},\frac14,\frac{27}{128},\frac{29}{160}\}\) has \(\chi_y(u)\le\log(\sqrt5-\frac12)\), including the algebraic interval \(a=2\). Kernel-checked with the standard axioms only (decide +kernel and norm_num; no native_decide). |
| Lemma 11.2 | CCGibbs.cc_gibbsCCGibbs.Zpart_isoCCGibbs.spr_eigenCCGibbs.spr_factsCCGibbs.eIn_eq_induce |
proved: the whole lemma: for every finite tree \(F\) and every \(\zeta>0\), \(\mathcal Z_F(\zeta)\ge\min(1,\zeta)\,\lambda_{\max}(M_\zeta)^{|V(F)|-1}\), with \(\lambda_{\max}(M_\zeta)\) in its closed form (CCRate.spr); spr_eigen shows that the closed form is the largest eigenvalue of \(M_\zeta\) and the largest modulus of a root of its characteristic polynomial, both eigenvalues being real and nonnegative for \(\zeta\ge0\). Proved by a subtree recursion with a logarithmic potential, not by the paper’s Markov-chain route; only the statement is fixed. spr_eigen speaks of the roots of the characteristic polynomial, not of Mathlib’s spectrum. eIn_eq_induce identifies the edge count with the induced subgraph. Run component-count-gibbs, accepted 2026-10-30. Kernel-checked with the standard axioms only (no native_decide). Proofs in MaxLeafFormal/CCGibbs.lean. |
| Lemma 11.3 | CCGibbs.cc_pathCCGibbs.cc_path_min |
proved: the whole lemma: for every \(k\ge1\), every graph isomorphic to the path on \(k\) vertices and every \(\zeta\ge0\), \(\mathcal Z_{P_k}(\zeta)\le(1+\zeta)\lambda_{\max}(M_\zeta)^{k-1}\le2\lambda_{\max}(M_\zeta)^k\); with Lemma 11.2, paths minimize \(\mathcal Z_F\) among trees on the same number of vertices up to the factor \(\min(1,\zeta)/(1+\zeta)\) (cc_path_min). Run component-count-gibbs, accepted 2026-10-30. Kernel-checked with the standard axioms only (no native_decide). Proofs in MaxLeafFormal/CCGibbs.lean. |
| Corollary 11.5 | CCT.cc_T_aCCT.cc_T_a_of_hasCCBoundCCT.cc_T_a_of_gibbsCCT.W_ge_Z |
partly proved: part (a): for every set \(S\) with \(|S|=k\) and a tree \(F\) on \(S\) satisfying (20) with \(c\ge1\), for every \(y>0\) the chain \(W_S(y)\ge2^{-\gamma}c^{-k}\mathcal Z_F(cy/2)\ge2^{-\gamma}\min(1,\zeta)\lambda^{-1}(\lambda/c)^k\) with \(\zeta=cy/2\), \(\lambda=\lambda_{\max}(M_\zeta)\), and \((1+y)^n/W_S(y)\le2^{\gamma}\frac{\lambda}{\min(1,\zeta)}2^{n\phi_{c,\sigma}(y)}\) with \(\sigma=k/n\) (cc_T_a); the global form under Definition 11.4 (cc_T_a_of_hasCCBound). Parts (b) and (c) are not formalised. The hypotheses \(\gamma\ge0\), \(S\in\mathcal F_I\) and \(g\ge0\) are not needed and are omitted, and \(g\) is used in the remaining-budget convention of MLS.W. W_ge_Z (the first inequality, for \(y\ge0\) and any graph) and cc_T_a_of_gibbs (conditional on the Gibbs bound) are intermediate forms. Run component-count-cc-T-a, accepted 2026-10-30. Kernel-checked with the standard axioms only (no native_decide). Proofs in MaxLeafFormal/CCT.lean. |
| Lemma 11.12 | CCRate.cc_certCCRate.spr_root |
proved: the whole lemma: every \(\sigma\in(0,1]\) satisfies (R1), (R2) or (R3) with \(c=2\), \(\psi=0.71755\), \(\Gamma_0=16\), and \(0.71755<\log1.6444\). \(\lambda_{\max}\) is the paper’s closed form; the proof of this lemma uses only CCRate.spr_root (it is a root of \(x^2-(1+2\zeta)x+\zeta\)). Its link to \(M_\zeta\) is CCGibbs.spr_eigen: the characteristic polynomial of \(M_\zeta\) is \(x^2-(1+2\zeta)x+\zeta=(x-\lambda_{\max})(x-\zeta/\lambda_{\max})\) with \(0\le\zeta/\lambda_{\max}\le\lambda_{\max}\), and every complex root has modulus at most \(\lambda_{\max}\), so \(\lambda_{\max}\) is the largest eigenvalue and the spectral radius. Nothing else about the spectrum of \(M_\zeta\) (eigenvectors, Perron–Frobenius) is formalised. The interval data (CCData.lean) are exported by export_cc_cert.py and re-checked in Lean. CCRate.cc_c3 also checks the \(c=3\) facts: \(\lambda_{\max}(M_{6/5})=3\) with the side conditions of Corollary 11.5(b) at \(c=3\), \(3^{64}<5^{45}\) (Lemma D.9.8), and \(\log\frac95<H(26/45)\). Kernel-checked with the standard axioms only (decide +kernel and norm_num; no native_decide). |
| Theorem 12.8 | DSTCert.dst_ratesDSTCert.dst_certs_exactDSTGraph.fa_dst_WS_minimum |
partly proved: the constants of the proof only: \(0.457<\log1.3727\), \(2^{0.457}\in[1.37268,1.37269)\), and (from Proposition D.11.17) \(c_{Z_j}e_{2,j}\ge1/100\) and the exponent bound below \(0.457\). The algorithm and its running time are not formalised. The checked step is DSTGraph.fa_dst_WS_minimum: for a minimum Steiner set and each certificate \(j\), \(c_{Z_j}e_{2,j}e_{1,j}^{\,s}e_{2,j}^{\,p}\le W_S(y_j)\), the middle inequality of the proof times \((1+y_j)^{n_U}\), which uses (38), Lemma D.11.16 and Lemma D.11.15 (formalised as DSTCert.dst_rec). The first inequality of Lemma 3.9 and the step to the running time are not combined with it in Lean. Kernel-checked with the standard axioms only (decide +kernel and norm_num; no native_decide). |
| Theorem 12.10 | PDRate.pd_constantsPDGraph.pd_starPDGraph.pd_success |
partly proved: the constants of the proof: \(\psi_{\mathrm{pr}}<0.70502\) and \(2^{0.70502}<1.6302\) (the base of the stated \(O(1.6302^n)\)), and \(2^{\psi_{\mathrm{pr}}}\in[1.6301556,1.6301557)\); condition \((\star)\) of Theorem 3.5 at rate \(0.70502\) and \(\Gamma=1\) for every paired dominating set \(S\), with \(k=|S|\) (pd_star); and the success bound for \(k=|S|\) when the extension algorithm is replaced by its specification: Algorithm MLS at that rate, with the cap \(\Theta=\lceil\psi n+\log\Gamma\rceil+1\) and the trial counts \(m_{t,\theta}=\lceil M_{t,\theta}\rceil\) for \(\Gamma=1\) and any \(\kappa>0\), accepts with probability at least \(1-e^{-\kappa}\) (pd_success). The algorithm, its running time and the Tutte-matrix finishing step (Lemma 12.9) are not formalised. The paper’s algorithm uses that one-sided-error extension, so by Corollary 3.15 it runs MLS with the cap and trial counts for \(2\Gamma=2\); its success bound, which goes through the halved acceptance probability of Corollary 3.15, is not covered: pd_success is the exact-extension form at \(\Gamma=1\), and pd_star gives the condition \((\star)\) with \(\Gamma=1\) that Corollary 3.15 needs. That a graph without isolated vertices has a paired dominating set is PDGraph.exists_pairedDom. Proposition 12.11 has its own entry. Run fa-pd-rest, accepted 2026-10-30, and the certificates run. Kernel-checked with the standard axioms only (decide +kernel and norm_num; no native_decide). |
| Proposition 12.11 | PDGraph.fa_pd_tightPDGraph.pd_tight_critPDGraph.pd_tight_minPDGraph.pd_tight_argminPDGraph.pd_tight_uniquePDGraph.Sstar_subsetPDGraph.pd_tight_WPDGraph.pd_tight_ratioPDGraph.pd_tight_W_lePDGraph.pd_tight_momentsPDGraph.pd_tight_acceptsPDGraph.pd_tight_prob |
partly proved: all three sentences, the last one in the trial model: \(y^*\) is the only critical point of \(h_6\) in \((0,\infty)\) and \(\min_{y\ge0}h_6(y)=h_6(y^*)\), with \(y^*\) the only minimizer on \([0,\infty)\) (pd_tight_argmin); the centers form the only paired dominating set \(S^*\) of \(G_L\) of size at most \(2L\), and \(|S^*|=2L\); and for fixed \(0\le\psi'<\psi_{\mathrm{pr}}\), \(\Gamma\ge1\) and \(\kappa>0\), the probability that Algorithm MLS accepts \(k=2L\) on \(G_L\) tends to \(0\) as \(L\to\infty\), for the cap \(\Theta=\lceil\psi' n+\log\Gamma\rceil+1\) and the trial counts \(m_{t,\theta}=\lceil M_{t,\theta}\rceil\), with the extension algorithm replaced by its specification; on the way, the intermediate claims of the proof (every paired dominating set of \(G_L\) contains the centers, \(W_{S^*}(y)=(y^2+\frac y2+\frac1{64})^L\), \((1+y)^n/W_{S^*}(y)=2^{n\,h_6(y)}\), the moment bound, and that an accepting trial whose sample has its nominal size samples inside \(S^*\)). The paper’s algorithm, with the one-sided-error extension of Lemma 12.9, uses the cap and trial counts for \(\Gamma=2\) (Corollary 3.15 doubles the \(\Gamma=1\) of Theorem 12.10); the statement holds for every fixed \(\Gamma\ge1\), so it covers that instance. The success bound of that instance is not covered (see Theorem 12.10). That an extension algorithm with one-sided error and its own independent coins accepts only where its specification holds is argued in the specification, not in Lean; the Lean step this needs, that the samples have their nominal sizes almost surely, is MLSNec.trialMeasure_card_null. Other admissible caps and trial counts, and \(\Gamma,\kappa\) that depend on \(L\), are not covered. Run fa-pd-rest, accepted 2026-10-30. Kernel-checked with the standard axioms only (no native_decide). Proofs in MaxLeafFormal/PDGraph.lean and MaxLeafFormal/MLSNec.lean. |
| Lemma D.4.1 | Antinorm3.merge_Kcum_leftAntinorm3.merge_Kcum_rightAntinorm3.fin_nonneg_of_KcumAntinorm3.PZ_add_KcumAntinorm3.smul_PZ_add_KcumAntinorm3.smul_PZ_mono |
proved: parts (a) and (b), for the cone \(\mathcal K_{\mathrm{cum}}\); PZ_add_Kcum, smul_PZ_add_Kcum and Antinorm3.smul_PZ_mono are the instance of Lemma D.4.2(a) used with it. |
| Lemma D.5.1 | RSCGraph.rsc_mono |
proved: the lemma as stated, with \(|\mathrm{Tm}(J_X)|\) given by the formula \(n-|N[X]|+\mathrm{comp}(G[X])\) of (13). Proofs in MaxLeafFormal/RSC/Mono.lean. |
| Lemma D.5.2 | RSCGraph.rsc_modelRSCTree.monotone_coupling |
proved: the inequality as stated, for \(0\le p_2\le p_3\le1\) and \(y\ge0\) (rsc_model); monotone_coupling is the coupling step of its proof. Proofs in MaxLeafFormal/RSC/Model.lean, MaxLeafFormal/RSC/Measure.lean. |
| Lemma D.5.4 | RSCGraph.rsc_pointwise |
proved: all parts, including the asymmetry between \(X'\) and \(X\) in (v). Proofs in MaxLeafFormal/RSC/Pointwise.lean. |
| Lemma D.5.6 | RSCGraph.rsc_jensenRSCGraph.EQ3RSCGraph.EQ2RSCGraph.EQexRSCGraph.rsc_jensen_nonneg |
proved: the inequality and its “in particular” clause (rsc_jensen_nonneg, whose hypotheses hco and hex are the paper’s “all these expectations are nonnegative”). Proofs in MaxLeafFormal/RSC/Jensen.lean, MaxLeafFormal/RSC/Expect.lean. |
| Lemma D.5.8 | RSCTree.rsc_recursionRSCTree.rsc_recursion_fin |
proved: the ten-state recursion with forcings. Proofs in MaxLeafFormal/RSC/TreeCore.lean, MaxLeafFormal/RSC/GenInst.lean, MaxLeafFormal/RSCTreeGen.lean. |
| Lemma D.5.9 | RSCRec.rsc_messages |
proved: parts (a)–(d), for every node of every ordered labelled tree and every forcing. Proofs in MaxLeafFormal/RSCRec.lean. |
| Lemma D.5.11 | RSCGraph.rsc_jlemma |
proved: the statement, with \(T_u\) the union of the paths. Proofs in MaxLeafFormal/RSC/JLemma.lean, MaxLeafFormal/RSC/Bridge.lean. |
| Lemma D.5.12 | RSCTree.rsc_oddsRSCTree.odds1 |
proved: the odds inequality, and (31) for every \(w\ne o\). Proofs in MaxLeafFormal/RSC/Odds.lean, MaxLeafFormal/RSCTreeModel.lean. |
| Lemma D.5.13 | RSCGraph.rsc_creditRSCGraph.rsc_credit_ex |
proved: the credit inequality (rsc_credit) and its consequence (rsc_credit_ex). The positivity \(\Pr_{\mathrm{tm}}(o\notin X)>0\) is proved in Lean from the positive weight of \((\emptyset,\emptyset)\), as in the paper. Proofs in MaxLeafFormal/RSC/Odds.lean, MaxLeafFormal/RSCGraph.lean. |
| Lemma D.5.14 | RSCGraph.rsc_leaf |
proved: the statement as in the paper. Proofs in MaxLeafFormal/RSC/Leaf.lean. |
| Corollary D.5.17 | RSCGraph.rsc_reductionRSCGraph.rsc_reduction_ofRSCGraph.exists_ownerOK |
proved: the corollary as stated, for every owner map that follows the owner rule (rsc_reduction): \((F,\nu,c_2,c_3)\) is admissible, \(s+\sum_v\nu_v=n\) and \(W^{\mathrm{cl}}_S(y)\ge W^{\mathrm{tm}}(F,\nu,c)\). That owner-rule maps exist is RSCGraph.exists_ownerRule; it is not linked because axioms.txt, the audit of the linked declarations, does not list it, but scripts/AxiomsRSCTree.lean prints its axioms in the release build (the three standard ones). rsc_reduction_of proves the same for a weaker owner condition, and exists_ownerOK gives such a map. Proofs in MaxLeafFormal/RSCGraph.lean. |
| Lemma D.5.18 | RSCTree.rsc_relaxed |
proved: both claims: \(W^{\mathrm{tm}}\ge\widetilde W\) and \(\widetilde W=\widetilde{\mathrm{fin}}(\widetilde M_r)\), for any root and any order of the children. Proofs in MaxLeafFormal/RSC/RelaxedLe.lean, MaxLeafFormal/RSC/TreeCore.lean, MaxLeafFormal/RSC/GenInst.lean, MaxLeafFormal/RSCTreeGen.lean. |
| Lemma D.5.19 | RSCCert.rsc_cone_aRSCCert.rsc_cone_bRSCCert.rsc_cone_c |
proved: parts (a), (b) and (c): \(\mathcal K_{\mathrm{pos}}\) is a closed convex cone containing the orthant and generated by the fourteen vectors; merging with a nonnegative message on either side preserves it; \(\widetilde{\mathrm{fin}}\ge0\) on it. Stated for the graded eight-state merge with \(0<p_2\le p_3<1\) (MaxLeafFormal/RSCCert.lean). |
| Lemma D.5.20 | RSCCert.certificate_conditionsRSCCert.certificate_conditions_ofRSCCert.C5_of_stagesRSCFinal.rsc_tree_boundRSCTree.rsc_relaxed |
proved: both inequalities, as separate results: the first is rsc_relaxed (Lemma D.5.18), and the second, in recursion form \(\widetilde{\mathrm{fin}}(\widetilde M_r)\ge c_Z\hat e^{s+\nu(F)}\) for every admissible labelled rooted tree and every order of the children under (C1)–(C6), is certificate_conditions; also the staged-chain criterion for (C5). Children are merged left to right. With Lemma D.5.18 (below), the first inequality follows as well. For the ancillary certificate, RSCFinal.rsc_tree_bound gives \(\widetilde{\mathrm{fin}}(\widetilde M_r)\ge0.6060\,\hat e^{s+\nu(F)}\) for every admissible tree, from Proposition D.5.23 (with its compiler trust, see there). |
| Lemma D.5.21 | RSCParams.rsc_lightpairsRSCParams.rsc_C3 |
proved: the six light pairs, and (C3) for the \(d_{\min}\) functions of Proposition D.5.23. Logarithms are Mathlib’s Real.log, bounded by series with explicit error terms (MaxLeafFormal/RSCParams.lean). |
| Lemma D.5.22 | RSCParams.rsc_rsccredits |
proved: \(1\le\varpi_\tau\le2q_\tau\) and (30) for the RSC parameters. Margins exceed \(6\cdot10^{-9}\) and \(5\cdot10^{-9}\) (as in the proof of Lemma D.5.22); proved with rational bounds on the logarithms. |
| Proposition D.5.23 | RSCFinal.rsc_cert_fullRSCFinal.certZ_cZ_eqRSCFinal.certZ_cZ_digitsRSCFinal.rsc_j_oneRSCCert.IsStagesRSCCert.isStages_C5RSCFinal.rsc_certRSCFinal.certZ_cZRSCFinal.certZ_C1RSCFinal.certZ_C2RSCFinal.certZ_C4RSCFinal.certZ_C5 |
proved: the proposition as stated and used (rsc_cert_full): a set \(Z\) of \(1024\) nonnegative rational points (the points of the ancillary certificate) with \(c_Z>0.6060\) satisfying (C1)–(C6) of Lemma D.5.20 for the stated parameters, with (C5) proved directly for every chain of the required length \(j\) of nonnegative points of \(\mathcal P_Z\), the form that Lemma D.5.20 uses; for the same \(Z\), nonnegative rational stage sets of the stated sizes (\(62\) for \((1;0,1)\); \(62\) and \(304\) for \((1;1,0)\); \(61\), \(62\) and \(62\) for \((2;1,0)\), \((2;1,1)\), \((2;2,0)\)) that satisfy the stage relations, with the chain lengths \(j\) of (C5); and the scalar hypotheses of Lemma D.5.20. For the certificate’s point set, \(c_Z=123019910197327428728743/202985322574630920671369\) exactly, so \(0.60605<c_Z<0.60606\) (certZ_cZ_eq, certZ_cZ_digits), and \(j=1\) for all other pairs (rsc_j_one). Not kernel-only: 472 generated shard theorems are decided by native_decide (run A’s 466 in MaxLeafFormal/RSCData, and six in MaxLeafFormal/RSCData/Extras/Shards.lean for the exact \(c_Z\) and the stage sizes), so the theorems that use the data also trust the Lean compiler (#print axioms lists one auxiliary axiom per shard theorem; rsc_cert_full has 471 of them). The checkers’ soundness theorems (RSCCheck, RSCCheckExtras) and everything outside the data use the standard axioms only. Modelling choices: the stages include the stage relations that the proof uses (RSCCert.IsStages), which is what makes the clause say something about \(Z\) (PD1 of the amendment); a set of \(62\) points means \(62\) distinct points (PD3); the scalar hypotheses of Lemma D.5.20 are an added last conjunct, taken from the proof of the proposition and from its use in the proof of Proposition 8.6 (PD10); \(P\ge0\) is a hypothesis of isStages_C5, which derives (C5) at the start point from the stages. RSCFinal.rsc_cert is the form without the stage clause and the scalar conjunct (PD2). The data modules are generated from rsc-certificate.json.gz by formal/scripts/export_rsc_cert.py and formal/scripts/export_rsc_extras.py (hashes in RSCData/MANIFEST.sha256 and RSCData/Extras/MANIFEST.sha256) and are not imported by MaxLeafFormal.lean. Proofs in MaxLeafFormal/RSCFinal.lean, RSCFinalExtras.lean, RSCStages.lean, RSCCheck.lean and RSCCheckExtras.lean. |
| Lemma D.9.8 | CCRate.cc_c3 |
partly proved: the final inequality of the proof only: \(3^{64}<5^{45}\), equivalent to \(\sigma^*\ln3>\ln1.8\). The infimum and its attainment are not formalised. Kernel-checked with the standard axioms only (decide +kernel and norm_num; no native_decide). |
| Lemma D.11.14 | DSTGraph.fa_dst_pointDSTGraph.fa_dst_point_eqDSTGraph.fa_dst_W |
proved: the whole lemma, \(g(X)\le\Psi_A(X)\) for every \(X\subseteq S\) with equality if \(\vec G[\bar K_X]=A[\bar K_X]\), and its consequence (38), \(W_A(y)\le W_S(y)\) for \(y\ge0\); stated for every \(S\subseteq U\) and every out-arborescence \(A\) of \(\vec G[\{r\}\cup K\cup S]\) rooted at \(r\) (the paper fixes \(S\) inclusion-minimal rooted), with \(W_A\) defined on the digraph (DSTGraph.WAg). DSTGraph.exists_rtree identifies WAg with the tree function DSTCert.WA of Lemma D.11.15 and Lemma D.11.16. The rooted-set facts of further.tex (steiner_of_rooted, reachPart_rooted, rooted_minimal_of_minimal_steiner, minimum_steiner_rooted_minimal) and the composites fa_dst_WS_cert and fa_dst_WS_minimum are in the same file. Run fa-dst-ws-wa, accepted 2026-10-30. Kernel-checked with the standard axioms only (no native_decide). Proofs in MaxLeafFormal/DSTGraph.lean. |
| Lemma D.11.15 | DSTCert.dst_rec |
proved: \(W_A(y)=(\mathrm{msg}_r)_1\) for every real \(y\) and every out-arborescence rooted at \(r\), with the children merged in list order. \(\Psi_A\) and \(W_A\) (Lemma D.11.14’s count and (38)) are defined on the positions of an RTree Kind; Lean examples compare \(W_A\) with hand values on small trees. Kernel-checked with the standard axioms only (no native_decide). |
| Lemma D.11.16 | DSTCert.dst_tree_bound_WADSTCert.dst_tree_bound |
proved: the bound \(c_Ze_1^{\,s}e_2^{\,p+1}\le W_A(y)\) under (C1)–(C3), for every out-arborescence rooted at \(r\) with no Steiner leaf, where \(W_A\) is the sum of (38). dst_tree_bound_WA is dst_tree_bound combined with dst_rec (Lemma D.11.15); dst_tree_bound states the bound for \((\mathrm{msg}_r)_1\) of the two-state recursion, for every rooted tree with no Steiner leaf and any root label, which is more general than the lemma. The tree is an RTree Kind whose nodes are addressed by their positions. Kernel-checked with the standard axioms only (decide +kernel and norm_num; no native_decide). |
| Proposition D.11.17 | DSTCert.dst_certs_exactDSTCert.checkCert_soundDSTCert.dst_rates |
proved: the exact claims: the three rational certificates satisfy (C1)–(C3), \(|Z_j|=27,10,28\), \(c_{Z_j}e_{2,j}\ge0.40,0.41,0.011\), \(\lambda_j\ge0\) with \(\sum_j\lambda_j=1\); and the display: \(\max_i\sum_j\lambda_j\alpha_{j,i}\in[0.4569669,0.4569670)\), so below \(0.457\). The approximate table values are not claims. The certificate data (DSTData.lean) are generated from dst_certificates.json by export_dst_cert.py; that the Lean data are the data of that file rests on the exporter (re-running export_dst_cert.py on the committed dst_certificates.json reproduces DSTData.lean byte for byte, and its SHA-256 stamp f0ca3bd5… equals ancillary/SHA256SUMS), while the existence of certificates with these properties is kernel-checked either way. Kernel-checked with the standard axioms only (decide +kernel and norm_num; no native_decide). |
| Lemma D.11.18 | PDGraph.pd_pointPDGraph.pd_point_factorPDGraph.card_eq_sum_pairsPDGraph.pairing_of_matchingPDGraph.matching_of_pairingPDGraph.exists_anchorPDGraph.Ωpair_amgm |
proved: the whole lemma: \(|\operatorname{und}(X)|\le|\{v\notin S:\mathrm{anc}(v)\notin X\}|+2\,|\{uv\in M:u,v\notin X\}|\) for every \(X\subseteq S\), and \(W_S(y)\ge\prod_{uv\in M}\Omega_{uv}(y)\) for \(y\ge0\), for every finite simple graph, every pairing of \(S\) and every choice of anchors; also the factorization behind it, an identity for every real \(y\) (pd_point_factor), \(\sum_{uv\in M}n_{uv}=n\) (card_eq_sum_pairs), and the AM–GM consequence \(\Omega_{uv}(y)\ge y^2+4\cdot2^{-n_{uv}/2}y+2^{-n_{uv}}\) for \(y\ge0\) (Ωpair_amgm). The perfect matching \(M\) of \(G[S]\) enters as an oriented list of pairs; pairing_of_matching and matching_of_pairing link it edge by edge to Mathlib’s SimpleGraph.Subgraph.IsMatching, through which PDGraph.IsPairedDom defines paired dominating sets. The AM–GM consequence after the lemma holds for \(y\ge0\) (for \(y<0\) only when \(d_u=d_v\)), which is where the paper uses it. Run fa-pd-rest, accepted 2026-10-30. Kernel-checked with the standard axioms only (no native_decide). Proofs in MaxLeafFormal/PDGraph.lean. |
| Lemma D.11.19 | PDRate.pd_ratePDGraph.pd_rate_W |
proved: both claims: \(h_{\bar n}(y^*)\le h_6(y^*)=\psi_{\mathrm{pr}}\) for every integer \(\bar n\ge2\), with \(y^*=(3\sqrt3-1)/16\) and \(\psi_{\mathrm{pr}}\in[0.7050097,0.7050098)\); and \(W_S(y^*)\ge(1+y^*)^n2^{-\psi_{\mathrm{pr}}n}\) for every finite graph without isolated vertices and every paired dominating set \(S\) (pd_rate_W). The first claim is from the certificates run (decide +kernel and norm_num), the second from run fa-pd-rest, accepted 2026-10-30, through Lemma D.11.18. PDGraph.noIsolated_of_pairedDom shows that the hypothesis ‘no isolated vertex’ follows from the existence of a paired dominating set. Kernel-checked with the standard axioms only (no native_decide). |
Build
Download: everything needed for checking (the Lean project and the ancillary files, with instructions) or the Lean project alone.
The Lean project is in lean/: Lean v4.35.0 (lean-toolchain) and Mathlib v4.35.0 (lakefile.toml, pinned in lake-manifest.json). To check it:
cd lean
lake exe cache get
lake build
lake env lean CheckDecls.leanCheckDecls.lean checks that every declaration linked from the paper in the default target exists and prints its axioms. Every one of them relies only on Lean’s standard axioms propext, Classical.choice and Quot.sound; their certificate checks (in Antinorm3, Lobster, DSTCert and the other certificate modules) run in the kernel (decide +kernel).
The Lean check of the RSC certificate data is a separate target: its data files are generated from ancillary/rsc/rsc-certificate.json.gz, and its generated theorems are decided by native_decide, so they trust the Lean compiler as well as the kernel. Their declarations depend, besides the standard axioms, on the auxiliary axioms that native_decide adds for those generated theorems only. ancillary/README.md says how to generate the files and build the target (in the author’s release build on 8 cores, both targets together took 117 minutes); CheckDeclsData.lean then checks its linked declarations. The site’s build runs neither Lean target.
The top-level modules of both targets (the proofs of the RSC reduction are in the modules MaxLeafFormal.RSC.* that they import, and the RSC data modules are generated): MaxLeafFormal.Antinorm3, MaxLeafFormal.Antinorm8, MaxLeafFormal.Budget, MaxLeafFormal.CCData, MaxLeafFormal.CCGibbs, MaxLeafFormal.CCRate, MaxLeafFormal.CCT, MaxLeafFormal.CDS, MaxLeafFormal.DSTCert, MaxLeafFormal.DSTData, MaxLeafFormal.DSTGraph, MaxLeafFormal.DetRate, MaxLeafFormal.Enclose, MaxLeafFormal.EncloseH, MaxLeafFormal.Lobster, MaxLeafFormal.LobsterData, MaxLeafFormal.LobsterGraph, MaxLeafFormal.MLS, MaxLeafFormal.MLSNec, MaxLeafFormal.PDGraph, MaxLeafFormal.PDRate, MaxLeafFormal.RSCCert, MaxLeafFormal.RSCCheck, MaxLeafFormal.RSCCheckExtras, MaxLeafFormal.RSCCompose, MaxLeafFormal.RSCFinal, MaxLeafFormal.RSCFinalExtras, MaxLeafFormal.RSCGraph, MaxLeafFormal.RSCGraphDefs, MaxLeafFormal.RSCHeadline, MaxLeafFormal.RSCParams, MaxLeafFormal.RSCRec, MaxLeafFormal.RSCStages, MaxLeafFormal.RSCSteiner, MaxLeafFormal.RSCTreeDefs, MaxLeafFormal.RSCTreeGen, MaxLeafFormal.RSCTreeModel, MaxLeafFormal.RSCTrials, MaxLeafFormal.RSCheck, MaxLeafFormal.RSCover0, MaxLeafFormal.RSCover1, MaxLeafFormal.RSCover10, MaxLeafFormal.RSCover11, MaxLeafFormal.RSCover12, MaxLeafFormal.RSCover13, MaxLeafFormal.RSCover14, MaxLeafFormal.RSCover15, MaxLeafFormal.RSCover16, MaxLeafFormal.RSCover17, MaxLeafFormal.RSCover18, MaxLeafFormal.RSCover19, MaxLeafFormal.RSCover2, MaxLeafFormal.RSCover20, MaxLeafFormal.RSCover21, MaxLeafFormal.RSCover3, MaxLeafFormal.RSCover4, MaxLeafFormal.RSCover5, MaxLeafFormal.RSCover6, MaxLeafFormal.RSCover7, MaxLeafFormal.RSCover8, MaxLeafFormal.RSCover9, MaxLeafFormal.RSRate, MaxLeafFormal.RSRateAB, MaxLeafFormal.RSThetaCert, MaxLeafFormal.RSThetaRate, MaxLeafFormal.RSXConst, MaxLeafFormal.RateAssembly, MaxLeafFormal.Rooted, MaxLeafFormal.SteinerCDS, MaxLeafFormal.SteinerDir.
Computer certificates
The ancillary files are in ancillary/ (download them with the checking bundle above) under the MIT licence (LICENSE); SHA256SUMS lists their checksums. Appendix F of the paper says what each one certifies and how to run it.
To run the checks, use ./verify_all.sh in ancillary/ (quick mode, about a minute) or ./verify_all.sh --full (full mode, one to two hours with 4 processes); requirements.txt pins the Python environment. The two modes certify different things: the quick mode checks every certificate below except that of Proposition D.5.23 (the RSC antinorm certificate), which only the full mode verifies, with two independent programs. The evidence release gives the commands, running times, memory and checksums.