Blueprint: Monotone Local Search with Sample-Dependent Running Times

Serge Gaspers

This blueprint lists the statements of the paper that are formalised in Lean, with the paper’s numbering, and their dependencies. Each statement links to its Lean declarations; each proof links to the paper. Green means that the statement is proved in Lean. Statements whose Lean proof covers only part of the claim say which part.

3 Monotone Local Search with sample-dependent running times

Theorem 3.5 Exponential-moment Monotone Local Search

Let $\Phi $ be an implicit set system and let $\mathcal{A}$ solve $\Phi $-Extension with running-time exponent $g$. Let $\psi \ge 0$, $\Gamma \ge 1$ and $\kappa {\gt}0$ be numbers that can be computed from $(I,k)$ in time $N^{O(1)}$ and whose values are at most $N^{O(1)}$. With any cap $\Theta $ and trial counts $m_{t,\theta }$ satisfying (2), Algorithm MLS-$\theta $$(\psi ,\Gamma ,\kappa )$, given $I$ and $k\le n$,

(i): runs in time $2^{\psi n}N^{O(1)}$ and in space $N^{O(1)}$ plus the space of $\mathcal{A}$;
(ii): answers no if $\mathcal{F}_I$ contains no set of size at most $k$;
(iii): answers yes with probability at least $1-e^{-\kappa }$ if $\mathcal{F}_I$ contains a set $S$ with $|S|=k$ that satisfies

\begin{equation*} \max _{0\le t\le k}\frac{\mu _t(S)}{\binom nt}\ \ge \ \frac{2^{-\psi n}}{\Gamma }. \tag {$\star $} \end{equation*}

Condition ($\star $) holds in particular if $W_S(y)\ge (1+y)^n\, 2^{-\psi n}/\Gamma $ for some $y\ge 0$.

Lean covers 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.

Proof ▶

See the proof of Theorem 3.5 in the paper. 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 eq:fw-params are not covered for the uniform samples of Algorithm MLS-$\theta $: budgeted_success_of_admissible (thm:fw-budgeted) covers them for abstract trials, but the step from uniform samples to (T3) is not formalised.

Lemma 3.8 Threshold selection

✓

Let $\xi $ be a random variable with values in $[0,\infty ]$ and $\Pr [\xi {\lt}\infty ]{\gt}0$, so that $\mathbb {E}[2^{-\xi }]{\gt}0$.

(a): If $\Theta \ge 0$ is an integer with $2^{-\Theta }\le \mathbb {E}[2^{-\xi }]/2$, then some $\theta \in \{ 0,\dots ,\Theta \} $ satisfies $\Pr [\xi \le \theta ]\, 2^{-\theta }\ge \mathbb {E}[2^{-\xi }]/(4(\Theta +1))$.
(b): Conversely, $\Pr [\xi \le \theta ]\, 2^{-\theta }\le \mathbb {E}[2^{-\xi }]$ for every integer $\theta $.

Proof ▶

See the proof of Lemma 3.8 in the paper. $\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 {\lt}\infty ]{\gt}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 Generating function versus exponential moments

For every instance $I$, running-time exponent $g$ and solution $S$ with $|S|=k$, the moments $\mu _t(S)$ with $0\le t\le k$ are positive, since $g$ is finite, and

\[ \min _{0\le t\le k}\frac{\binom nt}{\mu _t(S)}\ \le \ \inf _{y\ge 0}\frac{(1+y)^n}{W_S(y)}\ \le (n+1)\min _{0\le t\le k}\frac{\binom nt}{\mu _t(S)} . \]

Lean covers the first inequality, in the form used later: a lower bound $W_S(y)\ge (1+y)^n2^{-\psi n}/\Gamma $ for some $y\ge 0$ gives condition $(\star )$; and the second inequality in pointwise form: for each $t\le k$ some $y\ge 0$ 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)$.

Proof ▶

See the proof of Lemma 3.9 in the paper. The infimum form of the second inequality follows from fw_gf_upper by dividing by $\mu _t(S){\gt}0$ and $W_S(y){\gt}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 Necessity of ($\star $)

Let $k\le n$ be an integer, fix $S\in \mathcal{F}_I$ with $|S|\le k$ and run Algorithm MLS-$\theta $$(\psi ,\Gamma ,\kappa )$ on $(I,k)$. The expected number of trials that run $\mathcal{A}$ on a subset of $S$ is at most

\[ P_{\mathrm{nec}}\cdot 2^{\psi n}\max _{0\le t\le |S|}\frac{\mu ^{(k)}_t(S)}{\binom nt}, \]

where $P_{\mathrm{nec}}=8\Gamma (k+1)(\Theta +1)\bigl(\kappa (\Theta +1)+1\bigr)\le N^{O(1)}$ and $\Theta $ is the cap used. In particular, if $\max _{t\le |S|}\mu ^{(k)}_t(S)/\binom nt\le 2^{-\psi n}/(4P_{\mathrm{nec}})$, the probability that some trial runs $\mathcal{A}$ on a subset of $S$ is at most $1/4$.

Lean covers 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 \ge 0$, $\Gamma \ge 1$, $\kappa {\gt}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.

Proof ▶

See the proof of Proposition 3.10 in the paper. 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 Budgeted trials

Let $\Phi $ be an implicit set system, and let $\mathrm{Tr}$ and the index sets $\mathcal{T}=\mathcal{T}_{I,k}$ be as in Algorithm 3.13, such that $\mathcal{T}_{I,k}$ can be listed in time $N^{O(1)}$. Suppose that there is a polynomial $p$ such that for every instance $I$, every integer $k\le n$, every $\iota \in \mathcal{T}_{I,k}$ and every integer $\theta \ge 0$

(T1): $\mathrm{Tr}_{\iota ,\theta }$ runs in time $2^\theta p(N)$ and in space $p(N)$ plus $\mathrm{sp}$, where $\mathrm{sp}\ge 0$ depends only on $I$ (for example, the space of an extension algorithm on $I$), and
(T2): $\mathrm{Tr}_{\iota ,\theta }$ rejects if $\mathcal{F}_I$ contains no set of size at most $k$.

Fix $I$ and $k$, let $S\in \mathcal{F}_I$ with $|S|=k$, and suppose that for each $\iota \in \mathcal{T}$ there is a random variable $\xi _{\iota }$ with values in $[0,\infty ]$, whose distribution may depend on $S$ but not on $\theta $, such that

(T1): $\Pr [\mathrm{Tr}_{\iota ,\theta }\text{ accepts}]\ge \Pr [\xi _{\iota }\le \theta ]$ for every integer $\theta \ge 0$.

Let $\psi $, $\Gamma $, $\kappa $ be as in Theorem 3.5. Then Algorithm 3.13, run with these trials and parameters, runs in time $2^{\psi n}N^{O(1)}$ and space $N^{O(1)}+\mathrm{sp}$, answers no if $\mathcal{F}_I$ contains no set of size at most $k$, and answers yes with probability at least $1-e^{-\kappa }$ if

\[ \max _{\iota \in \mathcal{T}}\mathbb {E}[2^{-\xi _{\iota }}]\ \ge \ \frac{2^{-\psi n}}\Gamma . \]

Lean covers soundness (every YES answer, on every outcome, under (T2)) and the success probability $\ge 1-e^{-\kappa }$ under (T3) and the moment condition, for any cap and trial counts within the ranges of eq:fw-params.

Proof ▶

See the proof of Theorem 3.14 in the paper. (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.

4 Corollaries: mean exponents, linear savings and product form

Theorem 4.1 Mean-exponent Monotone Local Search

Let $t(I,k)\in \{ 0,\dots ,k\} $ and $\lambda (I,k)\ge 0$ be computable in time $N^{O(1)}$, with values $\lambda (I,k)\le N^{O(1)}$, such that for every instance $I$, every $k\le n$ and every $S\in \mathcal{F}_I$ with $|S|=k$, writing $t=t(I,k)$,

\begin{equation} \mathbb {E}_X\bigl[g(I,X,k)\bigr]\le \lambda (I,k),\qquad X\text{ uniform in }\binom {S}{t}. \end{equation}

Then there is a randomized algorithm that, given $I$ and $k\le n$, runs in time

\[ \frac{\binom nt}{\binom kt}\, 2^{\lambda (I,k)}\, N^{O(1)} \]

and in space $N^{O(1)}$ plus the space of $\mathcal{A}$. It answers no if $\mathcal{F}_I$ contains no set of size at most $k$, and it answers yes with probability at least $1-1/e$ if $\mathcal{F}_I$ contains a set of size exactly $k$. Running it for $k=0,1,\dots ,n$ decides $\Phi $-Subset as in Remark 3.6.

Lean covers the Jensen step of the proof and the success probability it gives through Algorithm MLS-$\theta $.

Proof ▶

See the proof of Theorem 4.1 in the paper. The direct algorithm with the Markov cutoff (rem:co-markov) is not formalised; running time and space are not modelled.

Corollary 4.3 Linear mean savings

Let $\beta =\beta (I,k)$, $\rho =\rho (I,k)$ and $C=C(I,k)$ be nonnegative reals computable from $(I,k)$ in time $N^{O(1)}$, with $\beta n+C\le N^{O(1)}$. Let $I$ be an instance and $k$ an integer with $\sigma =k/n\in (0,1)$ such that for every $t\in \{ 0,\dots ,k\} $ and every $S\in \mathcal{F}_I$ with $|S|=k$,

\begin{equation} \mathbb {E}_X\bigl[g(I,X,k)\bigr]\le \beta n-\rho t+C,\qquad X\text{ uniform in }\binom St . \end{equation}

Let $F^*(\sigma )$ be as in (6), and let $\kappa {\gt}0$ be as in Theorem 3.5. Then:

(1): Every such $S$ satisfies $G(S)\le 2^{C+nF^*(\sigma )}$. Algorithm MLS-$\theta $ with $\Gamma =1$, confidence $\kappa $ and a rate computable from $(I,k)$ in time $N^{O(1)}$ gives a randomized algorithm that, given $I$ and $k$, runs in time $2^{\max (0,\, C+nF^*(\sigma ))}N^{O(1)}$, answers no if $\mathcal{F}_I$ contains no set of size at most $k$, and answers yes with probability at least $1-e^{-\kappa }$ if $\mathcal{F}_I$ contains a set of size $k$.
(2): $F^*(\sigma ){\lt}\beta $ if and only if $\rho {\gt}\log (1/\sigma )$.

Lean covers the inequality of part (1), and part (2).

Proof ▶

See the proof of Corollary 4.3 in the paper. Part (2) is the last clause of one_sample_size. The algorithm of part (1) is not formalised.

Remark 4.4 One sample size

The algorithm of Theorem 4.1 at a single sample size $t$ with the mean bound $\beta n-\rho t+C$ of (7) runs in time $\binom nt\binom kt^{-1}2^{\beta n-\rho t+C}N^{O(1)}$, and

\begin{equation} \binom nt\binom kt^{-1}2^{\beta n-\rho t}=2^{\beta n}\prod _{i=0}^{t-1}\frac{n-i}{2^{\rho }(k-i)} . \end{equation}

The factor with index $i$ weighs the two effects of sampling one more element: the probability that the sample lies inside a fixed solution of size $k$ is divided by $(n-i)/(k-i)$, and the running-time bound $2^{\beta n-\rho t+C}$ of the extension call is divided by $2^{\rho }$. As $n\ge k$, the factors are nondecreasing in $i$, and with $p=2^{-\rho }$ the factor with index $i$ is below $1$ exactly when $(1-p)i{\lt}k-pn$. So the best sample size is the number of factors below $1$, and sampling at all beats $t=0$ exactly when the first factor $n/(2^{\rho }k)=p/\sigma $ is below $1$, that is $\sigma {\gt}p$, the condition of Corollary 4.3(2).

By the entropy estimates (1), the running time above is at most $(k+1)2^{C}2^{nf_\sigma (\tau )}N^{O(1)}$ with $\tau =t/n$ and

\begin{equation} f_\sigma (\tau )=H(\tau )-\sigma H(\tau /\sigma )+\beta -\rho \tau \qquad (0\le \tau \le \sigma ),\qquad p=2^{-\rho }. \end{equation}

Expanding the entropies gives $H(\tau )-\sigma H(\tau /\sigma )=-(1-\tau )\log (1-\tau )+(\sigma -\tau )\log (\sigma -\tau )-\sigma \log \sigma $, so on $[0,\sigma )$ the derivative is $f_\sigma '(\tau )=\log \frac{1-\tau }{\sigma -\tau }-\rho $, the logarithm of the factor of (8) with index $i=\tau n$. It is strictly increasing in $\tau $, so $f_\sigma $ is convex on $[0,\sigma ]$. If $\sigma \le p$ (which includes $\rho =0$), then $f_\sigma '(\tau )\ge f_\sigma '(0)=\log \frac1\sigma -\rho \ge 0$, and the minimum of $f_\sigma $ over $[0,\sigma ]$ is $f_\sigma (0)=\beta =F^*(\sigma )$. If $\sigma {\gt}p$ (so $p{\lt}1$), then $f_\sigma '$ vanishes exactly at $\tau ^*=\frac{\sigma -p}{1-p}\in (0,\sigma )$, the unique minimizer. With $A=\frac{1-\sigma }{1-p}$ we have $1-\tau ^*=A$, $\sigma -\tau ^*=pA$ and $-\rho =\log p$, so

\[ f_\sigma (\tau ^*)=-(1-p)A\log A+pA\log p+\tau ^*\log p-\sigma \log \sigma +\beta =\beta +\sigma \log \frac p\sigma +(1-\sigma )\log \frac{1-p}{1-\sigma }=F^*(\sigma ), \]

using $(1-p)A=1-\sigma $ and $pA+\tau ^*=\sigma $. In both cases the minimum of $f_\sigma $ over $[0,\sigma ]$ is $F^*(\sigma )$. Since $H(\tau )-\sigma H(\tau /\sigma )$ is nondecreasing on $[0,\sigma ]$ (its derivative is $\log \frac{1-\tau }{\sigma -\tau }\ge 0$), the single-size algorithm run at $t=\lfloor \tau ^*n\rfloor $ (with $\tau ^*=0$ if $\sigma \le p$) attains the exponent $C+nF^*(\sigma )$ of Corollary 4.3(1) up to the factors $2^{\rho }$ and $k+1$. Algorithm RS (Section 6), the black-box barrier (Appendix D.6) and the two-class family of Appendix A use $f_\sigma $ in this form.

Lean covers the minimisation: $f_\sigma $ is strictly convex on $[0,\sigma ]$, and its minimum $F^*(\sigma )$ is attained exactly at $\tau ^*$ with the closed forms.

Proof ▶

See the proof of Remark 4.4 in the paper. 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.

5 Connected Dominating Set and Max Leaf Spanning Tree

Lemma 5.1 Max leaf and connected domination

Let $G$ be a connected graph with $n$ vertices. If $n\ge 3$, the maximum number of leaves of a spanning tree of $G$ equals $n-\gamma _{\mathrm{c}}(G)$, and a spanning tree with at least $n-|S|$ leaves can be computed in polynomial time from any connected dominating set $S$. If $n\le 2$, the only spanning tree of $G$ is $G$ itself, with no leaf if $n=1$ and two leaves if $n=2$.

Lean covers both sentences, with the spanning tree shown to exist: for $n\ge 3$ 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\le 2$, $G$ is a tree and its only spanning tree, with no leaf if $n=1$ and two leaves if $n=2$ (maxLeaf_small).

Proof ▶

See the proof of Lemma 5.1 in the paper. The polynomial-time computation is not modelled (existence only).

Lemma 5.2 First accepted size

Let $\Phi $ be an implicit set system and let $I$ be an instance of $\Phi $ with a universe of $n$ elements whose family $\mathcal{F}_I$ of solutions is nonempty and does not contain the empty set; let $\operatorname {opt}(I)\in \{ 1,\dots ,n\} $ be the least size of a solution. Let $\mathrm{Dec}$ be a procedure which, on input $(I,s)$ with $1\le s\le n$, runs in time $T$ and space $\mathrm{Sp}$ and rejects if $\mathcal{F}_I$ contains no set of size at most $s$. Then running $\mathrm{Dec}$ on $(I,1),(I,2),\dots ,(I,n)$ and outputting the first accepted $s$, or $n$ if none is accepted, runs in time $nT$ and space $\mathrm{Sp}$ and never outputs a value below $\operatorname {opt}(I)$; if $\mathrm{Dec}$ accepts $(I,\operatorname {opt}(I))$ with probability at least $p$, the output is $\operatorname {opt}(I)$ with probability at least $p$ (deterministic form: $p=1$). For $\Phi _{\mathrm{CDS}}$ (Definition 5.7), a connected graph $G$ and $\operatorname {opt}(G)=\gamma _{\mathrm{c}}(G)$, the same procedure solves Max Leaf Spanning Tree within the same bounds, by Lemma 5.1, where graphs with $n\le 2$ vertices are handled directly in constant time.

Lean covers 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.

Proof ▶

See the proof of Lemma 5.2 in the paper. Running time and space are not modelled. The Max Leaf Spanning Tree clause for $\Phi _{\mathrm{CDS}}$ is covered through cor:cds-budgeted (cds_budgeted_maxLeaf) for $n\ge 3$ and through lem:cds-maxleaf (maxLeaf_small) for $n\le 2$. Proofs in MaxLeafFormal/Budget.lean.

Lemma 5.3 Vertex-weighted directed Steiner tree

For $\vec G$, $n$, $r$, $K$ and $\varphi $ as above, $\operatorname {OPT}_\varphi (\vec G,r,K)$ can be computed deterministically in time $2^{|K|}(n+\varphi _{\max })^{O(1)}$ and space $(n+\varphi _{\max })^{O(1)}$.

Lean covers 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).

Proof ▶

See the proof of Lemma 5.3 in the paper. 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 Directed Steiner encoding

Let $J=(\mathcal{D},B,R)$ be a state of an $n$-vertex graph $G$ and $\varphi \colon B\to \{ 0,1,\dots ,\varphi _{\max }\} $. If $C_1\in \mathcal{D}$, then $\operatorname {OPT}_\varphi (J)=\operatorname {OPT}_\varphi (\vec G_J,\hat C_1,K_1)$ for $K_1=\{ \hat C:C\in \mathcal{D}\setminus \{ C_1\} \} \cup \check R$. Consequently, for every state $J$ of $G$, $\operatorname {OPT}_\varphi (J)$ can be computed deterministically in time $2^{|\mathrm{T}(J)|}(n+\varphi _{\max })^{O(1)}$ and space $(n+\varphi _{\max })^{O(1)}$.

Lean covers correctness: eq:cds-dir-match 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).

Proof ▶

See the proof of Lemma 5.6 in the paper. 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 Steiner extension

For every state $J$ of an $n$-vertex graph, $\operatorname {OPT}(J)$ can be computed deterministically in time $2^{|\mathrm{T}(J)|}n^{O(1)}$ and polynomial space. Consequently, the algorithm $\mathcal{A}_{\mathrm{St}}$ of Definition 5.7 solves $\Phi _{\mathrm{CDS}}$-Extension in polynomial space, and

\[ g(G,X,k)=|\mathrm{T}(J_X)|=n-|N[X]|+\operatorname {comp}(G[X]) \]

is a running-time exponent for it in the sense of Definition 3.2, with values in $\{ 0,\dots ,n\} $.

Lean covers correctness: $\mathcal A_{\mathrm{St}}$, which tests $\mathrm{OPT}(J_X)\le k-|X|$ with the value computed as in lem:cds-dir-steiner, solves $\Phi _{\mathrm{CDS}}$-Extension for every $X$ and $k$ (aSt_iff_ext), and rejects when $k{\lt}|X|$; $J_X$ is a state whose solutions are the sets $Y$ disjoint from $X$ with $X\cup Y$ a connected dominating set; eq:cds-TX (terminals_JX).

Proof ▶

See the proof of Corollary 5.8 in the paper. 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 thm:rsc 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 Tree inequality

Let $F$ be a tree and let $X\subseteq V(F)$ be nonempty. Then

\[ |N_F[X]|-\operatorname {comp}(F[X])\ \ge \ 1+\sum _{x\in X}\bigl(d_F(x)-1\bigr), \]

with equality if and only if $F\{ X\} $ is connected.

Lean covers the inequality; the equality case is not formalised.

Proof ▶

See the proof of Lemma 5.9 in the paper.

Lemma 5.10 Pointwise form

✓

Let $G$ be a connected graph with $n\ge 2$ vertices and let $S$ be a connected dominating set of $G$. Let $F$ be a spanning tree of $G$ in which every vertex of $V\setminus S$ is a leaf; one exists, by the construction in the proof of Lemma 5.1, which needs only $n\ge 2$. Put $w(u)=d_F(u)-1$ for $u\in S$. Then $\sum _{u\in S}w(u)=n-2$, and for every nonempty $X\subseteq S$,

\[ |N[X]|-\operatorname {comp}(G[X])\ \ge \ 1+\sum _{x\in X}w(x). \]

Proof ▶

See the proof of Lemma 5.10 in the paper.

Lemma 5.11 Mean number of terminals

✓

Let $G$ be a connected graph with $n\ge 2$ vertices, let $S$ be a connected dominating set of $G$ with $|S|=s$, let $1\le t\le s$ and let $X$ be uniform in $\binom St$. Then

\[ \mathbb {E}\bigl[|N[X]|-\operatorname {comp}(G[X])\bigr]\ \ge \ 1+\frac{t(n-2)}s, \qquad \text{equivalently}\qquad \mathbb {E}\, |\mathrm{T}(J_X)|\ \le \ n-1-\frac{t(n-2)}s . \]

Proof ▶

See the proof of Lemma 5.11 in the paper. That this formula counts the terminals of the Steiner instance $J_X$ (eq:cds-TX) is SteinerCDS.terminals_JX, listed under cor:cds-steiner; the two are not combined in one theorem.

6 Warm-up: sampling a connected dominating set with the mean running-time exponent

Proposition 6.1 Certified rate of RS

✓

Let $F^*$ be the function of (14).

(a): For every $\sigma \in (0,1)$, $F^*(\sigma ){\lt}H(\sigma )\le 1$, and the minimum of $f_\sigma $ over $[0,\sigma ]$ is attained exactly at $\tau ^*(\sigma )=\dfrac {\sigma -2^{-1/\sigma }}{1-2^{-1/\sigma }}\in (0,\sigma )$.
(b): At $\sigma =\frac12$: $\tau ^*=\frac13$ and $F^*(\frac12)=\frac12\log 3$, so the base $2^{F^*(1/2)}$ is exactly $\sqrt3$.
(c): $F^*(\sigma )\le \log 1.744835$ for every $\sigma \in (0,1]$. Moreover $F^*(\sigma )\le 0.7807$ for $\sigma \in (0,0.31]$ and $F^*(\sigma )\le 0.7802$ for $\sigma \in [0.54,1]$.

Proof ▶

See the proof of Proposition 6.1 in the paper. 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 Closed-form moment bound

✓

Let $G$ be a connected graph with $n$ vertices and let $S$ be a connected dominating set of $G$ with $|S|=s$ and $\sigma =s/n$. Then, for the running-time exponent $g(X)=|\mathrm{T}(J_X)|$ of Corollary 5.8,

\[ \max _{0\le t\le s}\frac{\mu _t(S)}{\binom nt}\ \ge \ \frac{2^{-nF^*(\sigma )}}2 . \]

Proof ▶

See the proof of Corollary 6.2 in the paper. $g$ is RateAssembly.gT. Proved from lem:cds-C (CDS.mean_terminals) and the linear-savings bound of part 1B. Standard axioms only.

Theorem 6.4 Algorithm RS

For every constant $\kappa {\gt}0$, Algorithm RS runs in time $O(1.7449^n)$ and polynomial space. It never outputs a value below $\gamma _{\mathrm{c}}(G)$, and it outputs $\gamma _{\mathrm{c}}(G)$ with probability at least $1-e^{-\kappa }$. Consequently Connected Dominating Set and Max Leaf Spanning Tree (by Lemma 5.1, and directly when $n\le 2$) can be solved by a randomized algorithm with one-sided error (one-sided Monte Carlo) in time $O(1.7449^n)$ and polynomial space.

Lean covers the completeness inequality of the proof: (⋆) with $\Gamma =2$ and $\psi _{\mathrm{RS}}=0.80309062$ for every connected dominating set, and $\log 1.744835{\lt}0.80309062$ with $1.744835\le 2^{0.80309062}{\lt}1.744836$.

Proof ▶

See the proof of Theorem 6.4 in the paper. The algorithm, its running time and space, and the composition with thm:fw-main are not formalised here. Standard axioms only.

7 Exponential moments of the Steiner extension: Algorithm RS-$\theta $

Theorem 7.2 Algorithm RS-$\theta $

For every constant $\kappa {\gt}0$, Algorithm RS-$\theta $ runs in time $O^{*}(2^{\psi ^*n})$, where $2^{\psi ^*}=1.7203\ldots {\lt}1.7204$, and in polynomial space. It never outputs a value below $\gamma _{\mathrm{c}}(G)$, and it outputs $\gamma _{\mathrm{c}}(G)$ with probability at least $1-e^{-\kappa }$. Consequently Connected Dominating Set, and Max Leaf Spanning Tree (by Lemma 5.1, and directly when $n\le 2$), can be solved by a randomized algorithm with one-sided error (one-sided Monte Carlo) in time $O(1.7204^n)$ and polynomial space.

Lean covers the constants only: $2^{\psi ^*}\in [1.7203,1.7204)$ for $\psi ^*=0.7827016$, together with $0.7807{\lt}\psi ^*$ and $H(0.2){\lt}0.7802$ (used in the proof of prop:rst-rate).

Proof ▶

See the proof of Theorem 7.2 in the paper. The algorithm and its running time are not formalised; prop:rst-rate 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 Tree reduction

✓

Let $G$ be a connected graph, let $S$ be a connected dominating set of $G$, let $F$ be a spanning tree of $G[S]$ and let $o$ be an owner map with counts $\nu $. Then for every $X\subseteq S$,

\[ |\mathrm{T}(J_X)|\ \le \ \Pi _{F,\nu }(X). \]

Equality holds for every $X\subseteq S$ if $G[S]=F$ and every vertex of $V\setminus S$ has exactly one neighbor in $S$. Consequently $W_S(y)\ge W_{F,\nu }(y)$ for every $y\ge 0$.

Proof ▶

See the proof of Lemma 7.3 in the paper.

Lemma 7.4 Tree recursion

✓

Let $y\ge 0$, and let the messages $\mathrm{msg}_v$ be defined by (18) for any order of the children. Then every $\mathrm{msg}_v$ has nonnegative entries and $W_{F,\nu }(y)=\mathrm{fin}(\mathrm{msg}_r)$.

Proof ▶

See the proof of Lemma 7.4 in the paper. 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 Antinorm certificate

✓

Let $y\ge 0$ and $e_1,e_2{\gt}0$, and let $Z\subseteq \mathbb {R}^3_{\ge 0}$ be finite and nonempty with

(a): $z\circ z'\in \mathcal P_Z$ for all $z,z'\in Z$, and
(b): $\mathrm{Init}_y(j)\in e_1e_2^{\, j}\, \mathcal P_Z$ for every integer $j\ge 0$.

Then for every tree $F$ with $s$ vertices and every $\nu :V(F)\to \mathbb Z_{\ge 0}$, writing $\nu (F)=\sum _{v\in V(F)}\nu _v$, we have $W_{F,\nu }(y)\ge c_Z\, e_1^{\, s}e_2^{\, \nu (F)}$. If $e_2\le 1$, then (b) holds for all $j$ as soon as it holds for $j\le j_0$ and $(y/2,0,0)\in e_1e_2^{\, j_0+1}\mathcal P_Z$.

Proof ▶

See the proof of Lemma 7.5 in the paper.

Proposition 7.7 Antinorm certificates

✓

For $i\in \{ 0,1\} $, the data $(y_i,e_{1,i},e_{2,i},Z_i)$ of certificate $i$ (Appendix F.2) are rational and satisfy the hypotheses of Lemma 7.5, with $j_0=30$ and $e_{2,i}{\lt}1$:

$i$	$y_i$	$e_{1,i}$	$e_{2,i}$	$\|Z_i\|$	$c_{Z_i}\ge $	$\psi _i(\sigma )$
$0$	$\frac{69}{200}$	$\frac{747593601}{960952792}$	$\frac{512099210}{652701491}$	$27$	$0.6212$	$0.7776061742+0.0122113367\, \sigma $
$1$	$\frac{17}{50}$	$\frac{248231700}{312721579}$	$\frac{568097827}{739289481}$	$29$	$0.6293$	$0.8022330021-0.0468085913\, \sigma $

Here $\psi _i$ is the rate function $\psi _{\mathrm{cert}}$ of Corollary 7.6, with coefficients rounded to ten decimals. The two lines cross at $\sigma _\times =0.4172629270\ldots $, and

\[ \max \Bigl(\max _{\sigma \in [0.31,\, 0.4172629]}\psi _0(\sigma ),\ \max _{\sigma \in [0.4172629,\, 0.54]}\psi _1(\sigma )\Bigr) =0.78270151357\ldots {\lt}\psi ^* . \]

Proof ▶

See the proof of Proposition 7.7 in the paper. 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 Rate of RS-$\theta $

✓

For every connected graph $G$ and every connected dominating set $S$ of $G$,

\[ \max _{0\le t\le |S|}\frac{\mu _t(S)}{\binom nt}\ \ge \ \frac{2^{-\psi ^*n}}{2} . \]

Proof ▶

See the proof of Proposition 7.8 in the paper. Combines cor:rs-moments and prop:rs-rate(c) outside $(0.31,0.54)$ with the two RS-θ certificates (prop:rst-certs) inside. Standard axioms only.

Proposition 7.9 Uniform $(2,2)$-lobsters

Let $L\ge 1$, let $n=7L$ be the number of vertices of $\Lambda _L$, and let $S^*$ be the set of its spine vertices and legs. Then:

(a): $S^*$ is the unique minimum connected dominating set of $\Lambda _L$; so $\gamma _{\mathrm{c}}(\Lambda _L)=3L$ and $\sigma =3/7$.
(b): Run Algorithm RS-$\theta $ with any rate $\psi \ge 0$ in place of $\psi ^*$ (and the corresponding cap and trial counts). For $s=\gamma _{\mathrm{c}}(\Lambda _L)$, the probability that $s$ is accepted is at most $P_{\mathrm{nec}}\, 2^{\psi n}\max _t\mu _t(S^*)/\binom nt$, where $P_{\mathrm{nec}}\le n^{O(1)}$ is the polynomial factor of Proposition 3.10 (with $\Gamma =2$).
(c): For all $L\ge 1$ and $0\le t\le n$, $\mu _t(S^*)/\binom nt\le (n+1)\, 1.71927^{-n}$. Conversely, $\min _t\binom nt/\mu _t(S^*)\le C\cdot 1.71928^{n}$ for a constant $C$ and all $L\ge 1$. So $\bigl(\min _t\binom nt/\mu _t(S^*)\bigr)^{1/n}$ lies in $[1.71927,1.71928]$ up to factors $(n+1)^{1/n}$ and $C^{1/n}$; numerically its limit is $1.7192725\ldots $, attained near $y^*=0.3453$ in the generating-function form.

Consequently, RS-$\theta $ run with a rate $\psi $ in place of $\psi ^*$ outputs $\gamma _{\mathrm{c}}(\Lambda _L)$ with probability bounded away from $0$ on all $\Lambda _L$ only if $2^{\psi }\ge 1.71927$; so the certified base $1.7204$ exceeds the least base with which this algorithm succeeds on all $\Lambda _L$ by at most $0.0012$.

Lean covers the two displayed bounds of part (c), for every $L\ge 1$, 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\cdot 1.71928^n\mu _t(S^*)$ for some $t\le 3L$, with one $C{\gt}0$ for all $L$ (the paper’s $\min _t\binom nt/\mu _t(S^*)\le C\cdot 1.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 lem:rst-treerec.

Proof ▶

See the proof of Proposition 7.9 in the paper. 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.

8 Closure sampling under exponential moments: Algorithm RSC

Theorem 8.1 Algorithm RSC

For every constant $\kappa {\gt}0$, Algorithm RSC (Algorithm 8.2) runs in time $O^{*}\bigl(\varrho ^{\, n}\bigr)$, where $\varrho =1.6990\ldots {\lt}1.6991$, and in polynomial space, on every connected graph $G$ with $n$ vertices. It never outputs a value below $\gamma _{\mathrm{c}}(G)$, and it outputs $\gamma _{\mathrm{c}}(G)$ with probability at least $1-e^{-\kappa }$. Consequently Connected Dominating Set, and Max Leaf Spanning Tree (by Lemma 5.1, and directly when $n\le 2$), can be solved by a randomized algorithm with one-sided error (one-sided Monte Carlo) in time $O(1.6991^n)$ and polynomial space.

Lean covers 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 eq:fw-params, 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 prop:rsc-cert) and for any certificate satisfying conditions (C1), (C2), (C4), (C5) with $c_Z{\gt}0.6060$ (rsc_success_of_data, standard axioms only); under conditions (C1), (C2), (C4), (C5) with $c_Z{\gt}0.6060$ and for $n\ge 3$, 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{\lt}\varrho {\lt}1.6991$ (rsc_rho_lt), and the form conditional on prop:rsc-bound alone (rsc_success_of_bound).

Proof ▶

See the proof of Theorem 8.1 in the paper. RSCHeadline.rsc_success instantiates rsc_success_of_data with the certificate of prop:rsc-cert, so it is unconditional but not kernel-only: it inherits the native_decide trust of prop:rsc-cert (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, cor:cds-steiner), 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 The trials of RSC

Let $G$ be a connected graph with $n$ vertices and let $1\le s\le n$. For $t\in \{ 0,\dots ,s\} $ and an integer $\theta \ge 0$, let $\mathrm{Tr}_{t,\theta }$ be one execution of steps (a)–(c) of Algorithm 8.2 for $s$, with any rational $0\le p_2\le p_3\le 1$.

(a): $\mathrm{Tr}_{t,\theta }$ runs in time $2^\theta r_0(n)$ and space $r_0(n)$ for a polynomial $r_0$ that depends only on $p_2$ and $p_3$, not on $G$, $s$, $t$ or $\theta $, and it rejects if $\gamma _{\mathrm{c}}(G){\gt}s$.
(b): Let $S$ be a connected dominating set of $G$ with $|S|=s$. Let $\xi _t=|\mathrm{T}(J_X)|$ if $X\subseteq S$ and $\xi _t=\infty $ otherwise, where $X=X'\cup \Upsilon $ is the closed sample of the trial. Then the distribution of $\xi _t$ does not depend on $\theta $, $\Pr [\mathrm{Tr}_{t,\theta }\text{ accepts}]\ge \Pr [\xi _t\le \theta ]$ for every $\theta $, and $W^{\mathrm{cl}}_S(y)\le (1+y)^n\max _{0\le t\le s}\mathbb {E}\bigl[2^{-\xi _t}\bigr]$ for every $y\ge 0$.

Lean covers 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\ge 0$.

Proof ▶

See the proof of Lemma 8.4 in the paper. 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 eq:cds-TX. The inequality is proved for every $S\subseteq V$. Proofs in MaxLeafFormal/RSCTrials.lean. With the Steiner computation itself (cor:cds-steiner), the same acceptance rule is RSCSteiner.rscAcceptSt (rscAcceptSt_eq), and that eq:cds-TX gives the terminal count is SteinerCDS.terminals_JX.

Corollary 8.5 Budgeted trials for connected domination

Let $\psi \ge 0$ be a real constant that can be approximated to within $2^{-b}$ in time $b^{O(1)}$ for every integer $b\ge 1$, let $\Gamma _n\ge 1$ be computable in time $n^{O(1)}$ with $\Gamma _n\le n^{O(1)}$, and let $\kappa {\gt}0$ be a constant. Suppose that there are a randomized algorithm $\mathrm{Tr}$ with inputs $(G,s,t,\theta )$, written $\mathrm{Tr}_{t,\theta }$ when $G$ and $s$ are fixed, and a polynomial $r_0$ such that for every connected graph $G$ with $n$ vertices, every $s\in \{ 1,\dots ,n\} $, every $t\in \{ 0,\dots ,s\} $ and every integer $\theta \ge 0$:

(T1): $\mathrm{Tr}_{t,\theta }$ runs in time $2^\theta r_0(n)$ and space $r_0(n)$,
(T2): $\mathrm{Tr}_{t,\theta }$ rejects if $\gamma _{\mathrm{c}}(G){\gt}s$, and
(T3): if $s=\gamma _{\mathrm{c}}(G)$, then there are random variables $\xi _t$ with values in $[0,\infty ]$, whose distributions do not depend on $\theta $, such that $\Pr [\mathrm{Tr}_{t,\theta }\text{ accepts}]\ge \Pr [\xi _t\le \theta ]$ for all $t$ and $\theta $, and $\max _{0\le t\le s}\mathbb {E}[2^{-\xi _t}]\ge 2^{-\psi n}/\Gamma _n$.

Then the algorithm that, for $s=1,\dots ,n$ in turn, runs Algorithm 3.13 on $(G,s)$ with the index set $\{ 0,\dots ,s\} $, these trials, rate $\psi $, loss factor $\Gamma _n$, confidence $\kappa $ and a cap and trial counts within the ranges (2), and outputs the first accepted $s$, or $n$ if none, runs in time $2^{\psi n}n^{O(1)}$ and polynomial space, never outputs a value below $\gamma _{\mathrm{c}}(G)$, outputs $\gamma _{\mathrm{c}}(G)$ with probability at least $1-e^{-\kappa }$, and, when $n\ge 3$, solves Max Leaf Spanning Tree within the same bounds.

Lean covers 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\ge 3$, $n$ minus the output is the maximum number of leaves of a spanning tree with the same probability.

Proof ▶

See the proof of Corollary 8.5 in the paper. (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 Closure generating function of a minimum solution

Let $p_2=0.07$, $p_3=0.077$, $y=31/100$ and $\hat e=145729958/189014575$. For every connected graph $G$ with $n$ vertices and every connected dominating set $S$ of $G$ with $|S|=\gamma _{\mathrm{c}}(G)$,

\[ W^{\mathrm{cl}}_S(y)\ \ge \ 0.6060\, \hat e^n . \]

Lean covers the bound, conditional on the certificate conditions (C1), (C2), (C4), (C5); the primed form also assumes $c_Z{\gt}0.6060$.

Proof ▶

See the proof of Proposition 8.6 in the paper. The conditions are proved for the ancillary certificate in prop:rsc-cert (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 (thm:rsc) uses it. Proofs in MaxLeafFormal/RSCGraph.lean. RSCCompose.rsc_bound_trials restates the bound for the definition of $W^{\mathrm{cl}}_S$ used in thm:rsc (MaxLeafFormal/RSCCompose.lean).

10 Deterministic algorithms in polynomial space

Lemma 10.1 Rate certificate

✓

For every $u\in [0.15,0.85]$ there is $y\in \{ \frac{1+\sqrt5}8,\frac12,\frac5{16},\frac14,\frac{27}{128},\frac{29}{160}\} $ with $\chi _y(u)\le \log (\sqrt5-\frac12)$.

Proof ▶

See the proof of Lemma 10.1 in the paper. Kernel-checked with the standard axioms only (decide +kernel and norm_num; no native_decide).

11 Component-count running times

Lemma 11.2 Gibbs bound, after Csikvári and Lin

✓

For every tree $F$ with $k\ge 1$ vertices and every $\zeta {\gt}0$,

\[ \mathcal Z_F(\zeta )\ \ge \ \min (1,\zeta )\, \lambda _{\max }(M_\zeta )^{k-1}. \]

Proof ▶

See the proof of Lemma 11.2 in the paper. 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 Paths

✓

For a path $F$ with $k\ge 1$ vertices and every $\zeta \ge 0$, $\mathcal Z_F(\zeta )\le (1+\zeta )\, \lambda _{\max }(M_\zeta )^{k-1}\le 2\lambda _{\max }(M_\zeta )^k$.

Proof ▶

See the proof of Lemma 11.3 in the paper. 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 Generating function of a component-count running time

Let $g$ have a component-count bound with constants $(c,\gamma )$, let $S\in \mathcal{F}_I$ with $|S|=k\ge 1$, let $F$ be a tree for $S$ as in Definition 11.4, and put $\sigma =k/n$.

(a)

For every $y{\gt}0$, with $\zeta =cy/2$,

\[ W_S(y)\ \ge \ 2^{-\gamma }c^{-k}\mathcal Z_F(\zeta )\ \ge \ 2^{-\gamma }\, \frac{\min (1,\zeta )}{\lambda _{\max }(M_\zeta )} \Bigl(\frac{\lambda _{\max }(M_\zeta )}{c}\Bigr)^{k}, \]

and therefore

\[ \frac{(1+y)^n}{W_S(y)}\le 2^\gamma \, \frac{\lambda _{\max }(M_\zeta )}{\min (1,\zeta )}\, 2^{n\phi _{c,\sigma }(y)} . \]

(b)

Put $y^*=\frac{2(c-1)}{2c-1}$ and $\zeta ^*=cy^*/2=\frac{c(c-1)}{2c-1}$. Then $\lambda _{\max }(M_{\zeta ^*})=c$, and if $c{\gt}1$,

\[ W_S(y^*)\ \ge \ 2^{-\gamma }\, \frac{\min (1,\zeta ^*)}{c},\qquad \frac{(1+y^*)^n}{W_S(y^*)}\le \frac{2^\gamma c}{\min (1,\zeta ^*)}\Bigl(\frac{4c-3}{2c-1}\Bigr)^n . \]

(c)

$W_S(0)=\mu _0(S)\ge 2^{-\gamma }c^{-k}$ and $\mu _k(S)\ge 2^{-1-\gamma }$.

Lean covers part (a): for every set $S$ with $|S|=k$ and a tree $F$ on $S$ satisfying eq:cc-bound with $c\ge 1$, for every $y{\gt}0$ the chain $W_S(y)\ge 2^{-\gamma }c^{-k}\mathcal Z_F(cy/2)\ge 2^{-\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)\le 2^{\gamma }\frac{\lambda }{\min (1,\zeta )}2^{n\phi _{c,\sigma }(y)}$ with $\sigma =k/n$ (cc_T_a); the global form under def:cc-bound (cc_T_a_of_hasCCBound).

Proof ▶

See the proof of Corollary 11.5 in the paper. Parts (b) and (c) are not formalised. The hypotheses $\gamma \ge 0$, $S\in \mathcal F_I$ and $g\ge 0$ 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\ge 0$ 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 Rate certificate for $c=2$

✓

Every $\sigma \in (0,1]$ satisfies (R1), (R2) or (R3) of Corollary 11.6 with $c=2$, $\psi =0.71755$ and $\Gamma _0=16$. Moreover $0.71755{\lt}\log 1.6444$, so $2^{0.71755n}n^{O(1)}=O(1.6444^n)$.

Proof ▶

See the proof of Lemma 11.12 in the paper. $\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 cor:cc-T(b) at $c=3$, $3^{64}{\lt}5^{45}$ (lem:cc-inf), and $\log \frac95{\lt}H(26/45)$. Kernel-checked with the standard axioms only (decide +kernel and norm_num; no native_decide).

12 Further applications

Theorem 12.8 Directed Steiner Tree

Directed Steiner Tree on digraphs with $n$ vertices can be solved by a randomized algorithm with one-sided error in time $2^{0.457n}n^{O(1)}=O(1.3727^n)$ and polynomial space.

Lean covers the constants of the proof only: $0.457{\lt}\log 1.3727$, $2^{0.457}\in [1.37268,1.37269)$, and (from prop:fa-dst-certs) $c_{Z_j}e_{2,j}\ge 1/100$ and the exponent bound below $0.457$.

Proof ▶

See the proof of Theorem 12.8 in the paper. 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 eq:fa-dst-W, lem:fa-dst-cert and lem:fa-dst-rec (formalised as DSTCert.dst_rec). The first inequality of lem:fw-gf 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 Paired Domination

For graphs $G$ with $n$ vertices and no isolated vertex, $\gamma _{\mathrm{pr}}(G)$ can be computed by a randomized algorithm with one-sided error in time $O(1.6302^n)$ and polynomial space.

Lean covers the constants of the proof: $\psi _{\mathrm{pr}}{\lt}0.70502$ and $2^{0.70502}{\lt}1.6302$ (the base of the stated $O(1.6302^n)$), and $2^{\psi _{\mathrm{pr}}}\in [1.6301556,1.6301557)$; condition $(\star )$ of thm:fw-main 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 {\gt}0$, accepts with probability at least $1-e^{-\kappa }$ (pd_success).

Proof ▶

See the proof of Theorem 12.10 in the paper. The algorithm, its running time and the Tutte-matrix finishing step (lem:fa-pd-ext) are not formalised. The paper’s algorithm uses that one-sided-error extension, so by cor:fw-onesided it runs MLS with the cap and trial counts for $2\Gamma =2$; its success bound, which goes through the halved acceptance probability of cor:fw-onesided, is not covered: pd_success is the exact-extension form at $\Gamma =1$, and pd_star gives the condition $(\star )$ with $\Gamma =1$ that cor:fw-onesided needs. That a graph without isolated vertices has a paired dominating set is PDGraph.exists_pairedDom. prop:fa-pd-tight 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 Tightness

The only critical point of $h_6$ in $(0,\infty )$ is $y^*$, and $\min _{y\ge 0}h_6(y)=h_6(y^*)$. Let $G_L$ be the disjoint union of $L$ double stars, each an edge $uv$ with two pendant vertices at $u$ and two at $v$. Then the centers form the only paired dominating set $S^*$ of $G_L$ of size at most $2L$, and if Algorithm MLS-$\theta $ of Theorem 12.10 is run with a rate $\psi '{\lt}\psi _{\mathrm{pr}}$, it accepts $k=2L$ with probability tending to $0$ as $L\to \infty $.

Lean covers 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\ge 0}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 '{\lt}\psi _{\mathrm{pr}}$, $\Gamma \ge 1$ and $\kappa {\gt}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^*$).

Proof ▶

See the proof of Proposition 12.11 in the paper. The paper’s algorithm, with the one-sided-error extension of lem:fa-pd-ext, uses the cap and trial counts for $\Gamma =2$ (cor:fw-onesided doubles the $\Gamma =1$ of thm:fa-pd); the statement holds for every fixed $\Gamma \ge 1$, so it covers that instance. The success bound of that instance is not covered (see thm:fa-pd). 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.

D Deferred proofs

Lemma D.4.1 Closure facts

✓

(a): If $Q\in \mathbb {R}^3_{\ge 0}$ and $\Delta \in \mathcal K_{\mathrm{cum}}$, then $\Delta \circ Q\in \mathcal K_{\mathrm{cum}}$ and $Q\circ \Delta \in \mathcal K_{\mathrm{cum}}$.
(b): $\mathrm{fin}(\Delta )\ge 0$ for every $\Delta \in \mathcal K_{\mathrm{cum}}$.

Proof ▶

See the proof of Lemma D.4.1 in the paper.

Lemma D.5.1 Monotonicity of the number of terminals

✓

For $X\subseteq Y\subseteq V$ we have $|\mathrm{T}(J_Y)|\le |\mathrm{T}(J_X)|$.

Proof ▶

See the proof of Lemma D.5.1 in the paper. Proofs in MaxLeafFormal/RSC/Mono.lean.

Lemma D.5.2 Closure tree model

✓

For $0\le p_2\le p_3\le 1$ and $y\ge 0$,

\[ W^{\mathrm{cl}}_S(y)\ \ge \ \sum _{X'\subseteq S}\ \sum _{\Upsilon \subseteq C_F(X')} y^{|X'|}\, \pi _{X'}(\Upsilon )\, 2^{-\Psi _F(X'\cup \Upsilon )}\prod _{u\in O}h_u(X',X'\cup \Upsilon ). \]

Proof ▶

See the proof of Lemma D.5.2 in the paper. Proofs in MaxLeafFormal/RSC/Model.lean, MaxLeafFormal/RSC/Measure.lean.

Lemma D.5.4 Pointwise bound

✓

Let $0{\lt}p_2\le p_3{\lt}\frac12$, let $o$ be an owner map, let $u\in O$ have the owner $o=o(u)$, and let $X'\subseteq X\subseteq S$. Then $h_u(X',X)\ge \bar h_u(X)$ whenever $o\notin X$, and:

(i): if $u$ is private, then $h_u(X',X)\ge \bar h_u(X)$;
(ii): if $u$ is shared of type $\tau $, then $h_u(X',X)\ge \bar h_u(X)\, q_\tau ^{\mathbf1[o\in X]}$;
(iii): if $u$ is shared of type $\tau $, $o\notin X$ and $N'_u\cap X\ne \emptyset $, then $h_u(X',X)\ge e^{\delta _\tau }\, \bar h_u(X)$;
(iv): if $u$ is shared of type $3$, then $\ln \bigl(h_u(X',X)/\bar h_u(X)\bigr)\ge \mathbf1_u\bigl(\delta _3\, \mathbf1[o\notin X]-\varepsilon _3\, \mathbf1[o\in X]\bigr)$;
(v): if $u$ is shared of type $2$, then $\ln \bigl(h_u(X',X)/\bar h_u(X)\bigr)\ge \mathbf1_u\bigl(\delta _2\, \mathbf1[o\notin X]-\varepsilon _2\, \mathbf1[o\in X']\bigr)$.

Proof ▶

See the proof of Lemma D.5.4 in the paper. Proofs in MaxLeafFormal/RSC/Pointwise.lean.

Lemma D.5.6 Exposures, credits and the Jensen correction

✓

Let $0{\lt}p_2\le p_3{\lt}\frac12$, $y\ge 0$ and $\varpi _2,\varpi _3\ge 1$. In the setting of Definition D.5.5,

\[ W^{\mathrm{cl}}_S(y)\ \ge \ W^{\mathrm{tm}}\exp \Bigl(\sum _{u\in O^{\mathrm{co}}}\mathbb {E}_{\mathrm{tm}}[\ln \tilde h_u] +\sum _{u\in O^{\mathrm{ex}}}\mathbb {E}_{\mathrm{tm}}[\ln \tilde h^{\mathrm{ex}}_u]\Bigr). \]

In particular, if all these expectations are nonnegative, then $W^{\mathrm{cl}}_S(y)\ge W^{\mathrm{tm}}$.

Proof ▶

See the proof of Lemma D.5.6 in the paper. Proofs in MaxLeafFormal/RSC/Jensen.lean, MaxLeafFormal/RSC/Expect.lean.

Lemma D.5.8 Ten-state recursion

✓

Let $M_v$, $v\in S$, be the messages of Definition D.5.7, for any orders of the children. Then every $M_v$ is nonnegative, and with the weights $\mathrm{wt}$ of Definition D.5.5

\begin{align*} A_r& =\sum _{(X',\Upsilon )\models f,\ r\in X'}\mathrm{wt}(X’,\Upsilon ),\\ (C_2)_r+\lambda (C_3)_r& =\sum _{(X',\Upsilon )\models f,\ r\in \Upsilon }\mathrm{wt}(X’,\Upsilon ),\\ \tfrac 12(O_{00})_r+(O_{01})_r+(O_1)_r+q_2(O_2)_r+q_3(O_3)_r& =\sum _{(X',\Upsilon )\models f,\ r\notin X}\mathrm{wt}(X’,\Upsilon ), \end{align*}

where $M_r=(A_r,\dots ,(O_3)_r)$ and $(X',\Upsilon )\models f$ ranges over the pairs with $X'\subseteq S$ and $\Upsilon \subseteq C_F(X')$ that respect the forcing. In particular $\mathrm{fin}(M_r)$ is the sum of $\mathrm{wt}$ over these pairs, and $\mathrm{fin}(M_r)=W^{\mathrm{tm}}$ for the empty forcing.

Proof ▶

See the proof of Lemma D.5.8 in the paper. Proofs in MaxLeafFormal/RSC/TreeCore.lean, MaxLeafFormal/RSC/GenInst.lean, MaxLeafFormal/RSCTreeGen.lean.

Lemma D.5.9 Message inequalities

✓

Let $F$ be rooted anywhere and let $f$ be a forcing. Then the messages $M_v=(A,C_0,\dots ,O_3)$ of Definition D.5.7 satisfy:

(a): $C_0\ge \frac{p_2}2(O_{00}+O_{01})$ and $C_j\ge \frac{p_2}2O_j$ for $j=1,2,3$, for every $v$ with $f(v)\ne \mathsf{excl}$;
(b): $C_0+C_1+C_2+C_3\le \frac{p_2}y\, A$, for every $v$ with $f(v)\ne \mathsf{out}$ none of whose children is excluded;
(c): $\chi _{\mathsf S}(M_v)\le \mathsf b\, \chi _{\mathsf O}(M_v)$, for every $v$ with $f(v)\ne \mathsf{out}$ none of whose children is excluded;
(d): $\chi _{\mathsf S}(M_v)\ge \chi _{\mathsf O}(M_v)$ for every $v$ with $f(v)\ne \mathsf{excl}$, and $\chi _{\mathsf S}(M_v)\ge q_3\, \chi _{\mathsf O}(M_v)$ for every $v$ with $f(v)=\mathsf{excl}$.

Proof ▶

See the proof of Lemma D.5.9 in the paper. Proofs in MaxLeafFormal/RSCRec.lean.

Lemma D.5.11 Nonnegative correction at light owners

✓

Under the standing assumptions of Appendix D.5.3 (in particular $y{\gt}0$), in the setting of Definition D.5.5, let $u$ be a shared vertex of type $\tau $ whose owner $o=o(u)$ is $\tau $-light and is a leaf of $T_u$. Then $\mathbb {E}_{\mathrm{tm}}[\ln \tilde h_u]\ge 0$.

Proof ▶

See the proof of Lemma D.5.11 in the paper. Proofs in MaxLeafFormal/RSC/JLemma.lean, MaxLeafFormal/RSC/Bridge.lean.

Lemma D.5.12 Odds of being sampled

✓

In the setting of Definition D.5.5, let $U\subseteq S$ and $w\in S\setminus U$ with $|U\cap N_F(w)|\le 1$, and let $E$ be the event that $U\cap X=\emptyset $. Then

\[ \Pr _{\mathrm{tm}}\bigl(E,\ w\in X'\bigr)\ \ge \ \frac y2\, q_3^{|U\cap N_F(w)|}\, \Pr _{\mathrm{tm}}\bigl(E,\ w\notin X\bigr). \]

Proof ▶

See the proof of Lemma D.5.12 in the paper. Proofs in MaxLeafFormal/RSC/Odds.lean, MaxLeafFormal/RSCTreeModel.lean.

Lemma D.5.13 Credits

✓

Put $\vartheta =\frac y2q_3$ and $\rho _1=(1+\vartheta )^{-1}$. Under the standing assumptions of Appendix D.5.3, in the setting of Definition D.5.5, let $u$ be an exposed vertex of type $\tau $ with owner $o$. Then

\[ \Pr _{\mathrm{tm}}\bigl(N'_u\cap X\ne \emptyset \bigm |o\notin X\bigr)\ \ge \begin{cases} 1-\rho _1& \text{if }\tau =2,\\ 1-\rho _1^2& \text{if }\tau =3. \end{cases} \]

Consequently, if

\begin{equation} \ln \varpi _2\le (1-\rho _1)\, \delta _2\qquad \text{and}\qquad \ln \varpi _3\le (1-\rho _1^2)\, \delta _3 , \end{equation}

then $\mathbb {E}_{\mathrm{tm}}[\ln \tilde h^{\mathrm{ex}}_u]\ge 0$ for every exposed vertex $u$.

Proof ▶

See the proof of Lemma D.5.13 in the paper. The positivity $\Pr _{\mathrm{tm}}(o\notin X){\gt}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 Private neighbors of leaves

✓

If $S$ is a minimum connected dominating set with $|S|\ge 2$, then every leaf $v$ of $F$ has a private neighbor, that is, some $u\in O$ with $N_S(u)=\{ v\} $.

Proof ▶

See the proof of Lemma D.5.14 in the paper. Proofs in MaxLeafFormal/RSC/Leaf.lean.

Corollary D.5.17 Reduction to the tree model

✓

Assume the standing assumptions of Appendix D.5.3 (in particular $y{\gt}0$). Let $\varpi _2,\varpi _3$ satisfy $1\le \varpi _\tau \le 2q_\tau $ and (30), let $S$ be a minimum connected dominating set with $|S|=s$, and let $o$, $O^{\mathrm{co}}$, $O^{\mathrm{ex}}$, $\nu $, $c_2$, $c_3$ be given by Definition D.5.16. Then $(F,\nu ,c_2,c_3)$ is admissible, $s+\sum _{v\in S}\nu _v=n$, and $W^{\mathrm{cl}}_S(y)\ge W^{\mathrm{tm}}(F,\nu ,c)$.

Proof ▶

See the proof of Corollary D.5.17 in the paper. 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 The relaxed recursion

✓

Under the standing assumptions of Appendix D.5.3, for every tree $F$ and every choice of the root $r$, $\widetilde W(F,\nu ,c)\le W^{\mathrm{tm}}(F,\nu ,c)$ and $\widetilde W(F,\nu ,c)=\widetilde{\mathrm{fin}}(\widetilde M_r)$.

Proof ▶

See the proof of Lemma D.5.18 in the paper. Proofs in MaxLeafFormal/RSC/RelaxedLe.lean, MaxLeafFormal/RSC/TreeCore.lean, MaxLeafFormal/RSC/GenInst.lean, MaxLeafFormal/RSCTreeGen.lean.

Lemma D.5.19 The poset cone

✓

Let $0{\lt}p_2\le p_3{\lt}1$. The cone $\mathcal K_{\mathrm{pos}}$ defined above, together with the eight-state merge $\circ $ and the functional $\mathrm{fin}$, has the following properties.

(a): $\mathcal K_{\mathrm{pos}}$ is a closed convex cone containing $\mathbb {R}^8_{\ge 0}$, and it is the convex cone generated by the eight unit vectors $e_{\mathsf x}$ and the six vectors $e_{\mathsf x'}-e_{\mathsf x}$ for the covering pairs $\mathsf x'\succ \mathsf x$ displayed above.
(b): If $Q\in \mathbb {R}^8_{\ge 0}$ and $\Delta \in \mathcal K_{\mathrm{pos}}$, then $\Delta \circ Q\in \mathcal K_{\mathrm{pos}}$ and $Q\circ \Delta \in \mathcal K_{\mathrm{pos}}$.
(c): $\mathrm{fin}(\Delta )\ge 0$ for every $\Delta \in \mathcal K_{\mathrm{pos}}$.

Proof ▶

See the proof of Lemma D.5.19 in the paper. Stated for the graded eight-state merge with $0{\lt}p_2\le p_3{\lt}1$ (MaxLeafFormal/RSCCert.lean).

Lemma D.5.20 Certificate conditions

✓

Let $0{\lt}p_2\le p_3{\lt}\frac12$, $y{\gt}0$, $1\le \varpi _\tau \le 2q_\tau $ and $0{\lt}\hat e{\lt}q_3$. Let $Z\subseteq \mathbb {R}^8_{\ge 0}$ be finite and nonempty, let $\nu _0\ge 0$ and $\nu _E\ge 1$ be integers, and let $d^{(3)}_{\min },d^{(2)}_{\min }:\{ 1,\dots ,\nu _E\} \to \mathbb Z_{\ge 1}$ with $d^{(3)}_{\min }\le d^{(2)}_{\min }$; put $j_\tau (\nu )=\max (1,d^{(\tau )}_{\min }(\nu )-1)$. Suppose that:

(C1): $z\circ z'\in \mathcal P_Z$ for all $z,z'\in Z$;
(C2): $\mathrm{Init}(\nu )\in \hat e^{1+\nu }\mathcal P_Z$ for $0\le \nu \le \nu _0$, and $\mathrm{Init}(\infty )\in \hat e^{\nu _0+2}\mathcal P_Z$;
(C3): for $1\le \nu \le \nu _E$ and $\tau \in \{ 2,3\} $, every pair $(\nu ,d)$ with $1\le d{\lt}d^{(\tau )}_{\min }(\nu )$ is $\tau $-light;
(C4): for $2\le \nu \le \nu _E$: if $d^{(3)}_{\min }(\nu )\le 1$, then $\mathrm{Init}(\nu ;0,c_3)\in \hat e^{1+\nu }\mathcal P_Z$ for $1\le c_3\le \nu -1$, and if moreover $d^{(2)}_{\min }(\nu )\le 1$, then $\mathrm{Init}(\nu ;c_2,c_3)\in \hat e^{1+\nu }\mathcal P_Z$ for all $(c_2,c_3)\in L(\nu -1)$ with $c_2\ge 1$;
(C5): for $1\le \nu \le \nu _E$ and $(c_2,c_3)\in L(\nu )$, with $j=j_3(\nu )$ if $c_2=0$ and $j=j_2(\nu )$ if $c_2\ge 1$: $\hat e^{-1-\nu }\mathrm{Init}(\nu ;c_2,c_3)\circ Q_1\circ \cdots \circ Q_j\in \mathcal P_Z$ (merged from left to right) for all $Q_1,\dots ,Q_j\in \mathcal P_Z\cap \mathbb {R}^8_{\ge 0}$;
(C6): $(q_3/\hat e)^{\nu _E+1}\ge \hat e^{-(\nu _0+1)}$.

Then every admissible quadruple $(F,\nu ,c_2,c_3)$ in which $F$ has $s$ vertices satisfies, with $\nu (F)=\sum _{v\in V(F)}\nu _v$,

\[ W^{\mathrm{tm}}(F,\nu ,c)\ \ge \ \widetilde W(F,\nu ,c)\ \ge \ c_Z\, \hat e^{\, s+\nu (F)} . \]

Proof ▶

See the proof of Lemma D.5.20 in the paper. Children are merged left to right. With lem:rsc-relaxed (below), the first inequality follows as well. For the ancillary certificate, RSCFinal.rsc_tree_bound gives $\widetilde{\mathrm{fin}}(\widetilde M_r)\ge 0.6060\, \hat e^{s+\nu (F)}$ for every admissible tree, from prop:rsc-cert (with its compiler trust, see there).

Lemma D.5.21 Light pairs for RSC

✓

For $p_2=0.07$, $p_3=0.077$ and $y=31/100$ the pairs $(1,1)$, $(1,2)$, $(2,1)$ and $(3,1)$ are $3$-light, and the pairs $(1,3)$ and $(2,2)$ are $2$-light.

Proof ▶

See the proof of Lemma D.5.21 in the paper. Logarithms are Mathlib’s Real.log, bounded by series with explicit error terms (MaxLeafFormal/RSCParams.lean).

Lemma D.5.22 Credits for RSC

✓

For $p_2=0.07$, $p_3=0.077$, $y=31/100$, $\varpi _2=\frac{272657}{250000}=1.090628$ and $\varpi _3=\frac{288677}{250000}=1.154708$, we have $1\le \varpi _\tau \le 2q_\tau $ and (30) holds.

Proof ▶

See the proof of Lemma D.5.22 in the paper. Margins exceed $6\cdot 10^{-9}$ and $5\cdot 10^{-9}$ (as in the proof of lem:rsc-rsccredits); proved with rational bounds on the logarithms.

Proposition D.5.23 The certificate

✓

Let $p_2=0.07$, $p_3=0.077$, $y=31/100$, $\varpi _2=272657/250000$, $\varpi _3=288677/250000$, $\hat e=145729958/189014575$, $\nu _0=24$, $\nu _E=36$, $d^{(3)}_{\min }(1)=3$, $d^{(3)}_{\min }(2)=d^{(3)}_{\min }(3)=2$, $d^{(2)}_{\min }(1)=4$, $d^{(2)}_{\min }(2)=3$, $d^{(2)}_{\min }(3)=2$ and $d^{(3)}_{\min }(\nu )=d^{(2)}_{\min }(\nu )=1$ for $4\le \nu \le 36$. There is a set $Z$ of $1024$ nonnegative rational points with $c_Z{\gt}0.6060$, and there are nonnegative rational stages for (C5), namely for $\nu =1$ a set $Y_1$ of $62$ points for $(c_2,c_3)=(0,1)$ and sets $Y_1$, $Y_2$ of $62$ and $304$ points for $(1,0)$, and for $\nu =2$ sets $Y_1$ of $61$, $62$ and $62$ points for $(1,0)$, $(1,1)$ and $(2,0)$, such that conditions (C1)–(C6) of Lemma D.5.20 hold.

Proof ▶

See the proof of Proposition D.5.23 in the paper. 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 lem:rsc-cert are an added last conjunct, taken from the proof of the proposition and from its use in the proof of prop:rsc-bound (PD10); $P\ge 0$ 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 The critical fraction for $c=3$

For $\sigma ^*=26/45$, $\inf _{y\ge 0}\phi _{3,\sigma ^*}(y)=\log 1.8$, attained at $y=4/5$.

Lean covers the final inequality of the proof only: $3^{64}{\lt}5^{45}$, equivalent to $\sigma ^*\ln 3{\gt}\ln 1.8$.

Proof ▶

See the proof of Lemma D.9.8 in the paper. 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 Pointwise bound

✓

For every $X\subseteq S$,

\[ g(X)\ \le \ \Psi _A(X):=\bigl|\{ u\in K\cup X:\ \mathrm{par}(u)\notin \bar K_X\} \bigr| . \]

Equality holds if $\vec G[\bar K_X]=A[\bar K_X]$.

Proof ▶

See the proof of Lemma D.11.14 in the paper. DSTGraph.exists_rtree identifies WAg with the tree function DSTCert.WA of lem:fa-dst-rec and lem:fa-dst-cert. 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 Two-state recursion

✓

Let $y\ge 0$, and let the vectors $\mathrm{msg}_v$ be defined with this $y$ and any order of the children. Then $W_A(y)=(\mathrm{msg}_r)_1$.

Proof ▶

See the proof of Lemma D.11.15 in the paper. $\Psi _A$ and $W_A$ (lem:fa-dst-point’s count and eq:fa-dst-W) 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 Certificate

✓

Let $y\ge 0$, $e_1,e_2{\gt}0$, and let $Z\subseteq \mathbb {R}^2_{\ge 0}$ be a finite set whose points have positive first coordinate, with

(C1): $z\circ z'\in \mathcal R_Z$ for all $z,z'\in Z$;
(C2): $(1,0)\in e_2\mathcal R_Z$;
(C3): $(y,1)\circ z\in e_1\mathcal R_Z$ for all $z\in Z$.

Then $W_A(y)\ge c_Z\, e_1^{\, s}e_2^{\, p+1}$ for every out-arborescence $A$ as above, that is, rooted at $r$, with $s$ vertices in $S$, $p$ terminals, and no leaf in $S$.

Proof ▶

See the proof of Lemma D.11.16 in the paper. dst_tree_bound_WA is dst_tree_bound combined with dst_rec (lem:fa-dst-rec); 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 Certificates for Directed Steiner Tree

✓

The certificates of Appendix F.7 are three rational certificates $(y_j,e_{1,j},e_{2,j},Z_j)$, $j=0,1,2$, each of which satisfies (C1)–(C3) with $y=y_j$, $e_1=e_{1,j}$, $e_2=e_{2,j}$ and $Z=Z_j$, and rational weights $\lambda _j\ge 0$ with $\sum _j\lambda _j=1$. With the exponent vectors $\boldsymbol \alpha _j=(\alpha _{j,1},\alpha _{j,2},\alpha _{j,3})=\bigl(\log (1+y_j)-\log e_{1,j},\ -\log e_{2,j},\ \log (1+y_j)\bigr)$, the data are, approximately,

$j$	$\lambda _j\approx $	$y_j\approx $	$e_{1,j}\approx $	$e_{2,j}\approx $	$\|Z_j\|$	$c_{Z_j}e_{2,j}\ge $	$(\alpha _{j,1},\alpha _{j,2},\alpha _{j,3})\approx $
$0$	$0.7458$	$0.45494$	$1.003883$	$0.78$	$27$	$0.40$	$(0.535367,\, 0.358454,\, 0.540958)$
$1$	$0.0858$	$0.48223$	$1.041122$	$0.78$	$10$	$0.41$	$(0.509635,\, 0.358454,\, 0.567774)$
$2$	$0.1684$	$0.02$	$0.963015$	$0.52$	$28$	$0.011$	$(0.082938,\, 0.943416,\, 0.028569)$

and

\[ \max _{i\in \{ 1,2,3\} }\ \sum _{j=0}^2\lambda _j\alpha _{j,i}\ =\ 0.4569669\ldots \ {\lt}\ 0.457 . \]

Proof ▶

See the proof of Proposition D.11.17 in the paper. 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 Pointwise certificate

✓

For every $X\subseteq S$,

\[ |\operatorname {und}(X)|\ \le \ \bigl|\{ v\notin S:\mathrm{anc}(v)\notin X\} \bigr|+2\, \bigl|\{ uv\in M:u,v\notin X\} \bigr| , \]

and consequently, for every $y\ge 0$,

\[ W_S(y)=\sum _{X\subseteq S}y^{|X|}2^{-|\operatorname {und}(X)|}\ \ge \ \prod _{uv\in M}\Omega _{uv}(y),\qquad \Omega _{uv}(y)=y^2+y\bigl(2^{-d_u}+2^{-d_v}\bigr)+2^{-n_{uv}} . \]

Proof ▶

See the proof of Lemma D.11.18 in the paper. 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\ge 0$ (for $y{\lt}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 Rate

✓

The functions $h_{\bar n}$ and the point $y^*$ defined above satisfy

\[ \max _{\bar n\in \{ 2,3,\dots \} }h_{\bar n}(y^*)=h_6(y^*)=\psi _{\mathrm{pr}}=0.7050097\ldots , \]

and for every graph $G$ without isolated vertices and every paired dominating set $S$ of $G$,

\[ W_S(y^*)\ \ge \ (1+y^*)^n\, 2^{-\psi _{\mathrm{pr}}n} . \]

Proof ▶

See the proof of Lemma D.11.19 in the paper. 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 lem:fa-pd-point. 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).

\(i\)	\(y_i\)	\(e_{1,i}\)	\(e_{2,i}\)	\(\|Z_i\|\)	\(c_{Z_i}\ge \)	\(\psi _i(\sigma )\)
\(0\)	\(\frac{69}{200}\)	\(\frac{747593601}{960952792}\)	\(\frac{512099210}{652701491}\)	\(27\)	\(0.6212\)	\(0.7776061742+0.0122113367\, \sigma \)
\(1\)	\(\frac{17}{50}\)	\(\frac{248231700}{312721579}\)	\(\frac{568097827}{739289481}\)	\(29\)	\(0.6293\)	\(0.8022330021-0.0468085913\, \sigma \)

\(j\)	\(\lambda _j\approx \)	\(y_j\approx \)	\(e_{1,j}\approx \)	\(e_{2,j}\approx \)	\(\|Z_j\|\)	\(c_{Z_j}e_{2,j}\ge \)	\((\alpha _{j,1},\alpha _{j,2},\alpha _{j,3})\approx \)
\(0\)	\(0.7458\)	\(0.45494\)	\(1.003883\)	\(0.78\)	\(27\)	\(0.40\)	\((0.535367,\, 0.358454,\, 0.540958)\)
\(1\)	\(0.0858\)	\(0.48223\)	\(1.041122\)	\(0.78\)	\(10\)	\(0.41\)	\((0.509635,\, 0.358454,\, 0.567774)\)
\(2\)	\(0.1684\)	\(0.02\)	\(0.963015\)	\(0.52\)	\(28\)	\(0.011\)	\((0.082938,\, 0.943416,\, 0.028569)\)

Blueprint: Monotone Local Search with Sample-Dependent Running Times

3 Monotone Local Search with sample-dependent running times

4 Corollaries: mean exponents, linear savings and product form

5 Connected Dominating Set and Max Leaf Spanning Tree

6 Warm-up: sampling a connected dominating set with the mean running-time exponent

7 Exponential moments of the Steiner extension: Algorithm RS-\(\theta \)

8 Closure sampling under exponential moments: Algorithm RSC

10 Deterministic algorithms in polynomial space

11 Component-count running times

12 Further applications

D Deferred proofs