[Rule] DecisionMinimumVertexCover to DecisionMaximumLeafSpanningTree

Source

Decision<MinimumVertexCover<SimpleGraph, One>>, registered as
DecisionMinimumVertexCover/graph=SimpleGraph/weight=One.

Given an undirected graph with vertices V={0,...,n-1}, an indexed list of m
edge occurrences, and a signed bound k, decide whether a vertex cover of
cardinality at most k exists. A witness is a length-n Boolean selection
vector. Every edge must have a selected endpoint. The repository's graph
representation also permits loops and repeated edge occurrences; a loop
requires its sole endpoint to be selected. Both decision values are Or.

Target

Decision<MaximumLeafSpanningTree<SimpleGraph>>, registered by the accompanying
implementation as DecisionMaximumLeafSpanningTree/graph=SimpleGraph.

Given a graph H and a signed bound b, decide whether H has a spanning tree
with at least b degree-one vertices. A witness is a Boolean vector over the
indexed target edges. The existing maximum-leaf model is retained; its
mechanical Decision wrapper is supporting infrastructure, not a second
scientific contribution. The bare optimization pair would have incompatible
minimization/maximization witness value types, so the rule uses the decision
variants explicitly.

Endpoint registration dependency. This exact target Decision variant was
absent from the inspected main baseline. The implementation includes its
mechanical registry entry. The repository's shipping workflow expects both
endpoints already on main; maintainers must triage the dependency and agree
the integration order before the rule PR is described as merge-ready.
The issue proposes that prerequisite; it does not count it as another credit.

Motivation

This adds a direct incoming NP-hardness route to maximum-leaf spanning tree
through the already registered decision vertex-cover problem. The baseline
graph has a route from 3-SAT to unit DecisionMinimumVertexCover, while the
maximum-leaf decision wrapper and this edge were absent. The construction is
linear in the source graph and decodes a cover directly from tree degrees.

No dedicated proposal of this exact pair was located in the public all-state
history captured on 2026-10-13. The related
#910 proposes
DominatingSet to MaximumLeafSpanningTree, which has a different source. This
negative history search is not a claim of originality in the literature.

Reference

Paul Bonsma, Max-Leaves Spanning Tree is APX-hard for Cubic Graphs, Journal of
Discrete Algorithms 12, 14–23 (2012),
DOI 10.1016/j.jda.2011.06.005,
primary preprint.

The introduction, final paragraph before Section 2, was read. It describes
the classical universal-root/subdivision reduction from cubic vertex cover.
The proof below states the full repository-domain extension explicitly,
including two forced root leaves, arbitrary input graphs, loops, repeated
edges, empty inputs and signed bounds. No claim is made that this extension is
new in the mathematical literature.

Reduction Algorithm

Write the indexed source edge list as e_j=(u_j,v_j), 0≤j<m.

1. Keep original vertices 0,...,n-1. For each edge occurrence create a
   subdivision vertex a_j=n+j.
2. Add a root r=n+m and private vertices p=r+1, q=r+2.
3. In this exact edge order, insert all (r,v) for v=0,...,n-1, then
   (u_j,a_j),(v_j,a_j) for each source edge occurrence, then (r,p),(r,q).
   For a source loop the two incidence edge occurrences are retained.
4. Let N=n+m+3, M=n+2m+2, normalize k'=min(n,max(-1,k)), and set
   the target leaf bound to b=N-1-k'.
5. After validating a target decision witness, return exactly the original
   vertices having degree at least two in its selected spanning tree.

Forward. Suppose C covers the source graph and |C|≤k. Select every
root-to-original edge and both private-leaf edges. For each a_j, select
exactly one incidence edge to an endpoint in C. The result is connected with
N-1 edges, hence is a spanning tree. Its internal vertices are contained in
{r}∪C, so it has at least N-1-|C| leaves. If k≤n, this is at least b;
if k>n, use |C|≤n=k' instead. For k<0 there is no source witness.

Backward. In any target spanning tree, both private-leaf edges must be
selected, so r is internal. For a source edge occurrence e_j, consider
the path from a_j to r. Its first original vertex is an endpoint of e_j
and is internal on that path, so it has tree degree at least two. Thus the
extracted set C covers every source edge, including loops. If the tree has
L≥b leaves, then |C|≤N-L-1≤k'. For k≥0, this gives |C|≤k. For k<0,
the target bound is N; a tree on N≥3 vertices cannot have N leaves, so
both instances are NO. This proves YES/NO equivalence on the entire domain.

The same inequalities also give the exact optimization relation
maximum_leaves(H)=n+m+2-minimum_cover(G). This relation justifies the decision
threshold; the implementation does not register an unsupported bare
minimization-to-maximization witness rule.

Complexity and numeric boundaries. Construction and extraction take
O(n+m) time and space, beyond target validation. The graph is connected even
for n=m=0, when it is a three-vertex path. All size additions, multiplication
by two, and conversions used by the target bound are checked; normalizing k
first avoids negating the minimum signed integer. Unrepresentable derived
sizes return the library's explicit reduction error rather than wrapping.

Corner cases. For an edgeless source, selecting no vertices gives a star
with N-1=n+2 leaves. A source loop forces its original vertex internal in
every target spanning tree, exactly matching the cover requirement. Separate
subdivision vertices preserve repeated edge occurrences. Disconnected sources
and isolated vertices need no preprocessing.

Size Overhead

Here n and m are the registered source parameters num_vertices and
num_edges. Decision bounds are input data, not additional registered size
parameters. The target graph is bipartite with parts {r}∪{a_j} and
V∪{p,q}.

Validation Method

Local engineering checkpoint. Production code 650a8023 passed fmt,
complete clippy, 6,980 ordinary tests and 149 doctests in a separate retry.
The original Cargo command was interrupted by RAM exhaustion in doctest
compilation, not recorded as exit zero. Test-only HEAD a4b8cba0 changes no
production code and passed fresh fmt (4.566 s), clippy (45.973 s), and all
eight focused rule-05 tests. CLI round trips/default solve, four exporters,
full manual and topology passed. 89 new rule tests were measured below
five seconds: 88 earlier tests (maximum 4.7597 s including startup) plus
the allocation regression (0.017 s). Final new-production coverage PASS:
1,223/1,233 instrumented added lines, 99.189%; every rule exceeds 95%.
The audit excludes 814 added lines with no DA record explicitly; ten
instrumented lines remain uncovered. The focused instrumented extension
passed 8/8 tests. Human scientific review and maintainer approval remain
pending.

All mathematical counts below are local evidence. Proof sources, constructor,
independent adversarial and cross-check scripts are prepared locally and can
accompany a later implementation PR; they are not public certificate URLs.

The general proof above establishes correctness. Finite checks independently
search for counterexamples and audit construction/extraction.

• Constructor: 9,783,487 checks / 8,600 instances, seed 2026101303,
  including all 1,100 simple graphs through five vertices, every constructed
  target spanning tree via a complete structured enumeration, generic
  edge-subset cross-checks on smaller graphs, and signed/loop/multilist cases.
• Independent adversary, written from the proof: 789,445 checks / 4,781
  instances, including two Hypothesis strategies with 300 examples each;
  zero failures.
• Cross-comparison: 6,600 simple and 500 multilist targets identical,
  21,875 tree checks, 1,198 cross-extractions, zero disagreements.
• Rust: 7 rule tests and 16 model/wrapper tests passed. Tests exercise the
  canonical example, signed bounds, empty inputs, loops, repeated edges,
  malformed witnesses and parameter predictions. Formatting passed.

Counts are assertions and instance executions, not independent statistical
samples. Local evidence is under research/coauthorship-2026-10-13/ in
proofs/graph_vertexcover_leafspanningtree.typ,
verification/graph_vertexcover_leafspanningtree_constructor.py,
adversary/adv_vertexcover_leafspanningtree_report.json, and
verification/cross_vertexcover_leafspanningtree_report.json. These are not
public certificate URLs yet.

Example

Source. Take the four-cycle with indexed edges
[(0,1),(1,2),(2,3),(3,0)]. A minimum vertex cover is {0,2} of size two;
the disjoint edges (0,1) and (2,3) prove that no smaller cover exists.

Construction and target. Vertices 4,5,6,7 subdivide those four edges;
the root is 8 and the two private leaves are 9,10. The complete ordered
target edge list is

[(8,0),(8,1),(8,2),(8,3),
 (0,4),(1,4),(1,5),(2,5),(2,6),(3,6),(3,7),(0,7),
 (8,9),(8,10)].

There are N=11 vertices and M=14 edges. Select

[true,true,true,true,true,false,false,true,true,false,false,true,true,true].

Its degree vector is (3,1,3,1,1,1,1,1,6,1,1), so it has eight leaves. The
extraction is [true,false,true,false], selecting {0,2}.

For source bound k=2, the target bound is b=10-2=8, and both instances are
YES. For k=1, the bound is nine. A nine-leaf target tree would extract a
cover of size at most one, contradicting the two disjoint source edges;
therefore both instances are NO.

Suboptimal underlying spanning trees are visible too: keep all root edges but
attach edge vertices (4,5,6,7) respectively to (0,1,2,0) to obtain seven
leaves, or to (0,1,2,3) to obtain six. They fail the eight-leaf bound and
prevent a test from accepting an arbitrary spanning tree as a valid target
decision witness.

BibTeX

@article{Bonsma2012MaxLeaves,
  author = {Bonsma, Paul},
  title = {Max-leaves spanning tree is {APX}-hard for cubic graphs},
  journal = {Journal of Discrete Algorithms},
  volume = {12},
  pages = {14--23},
  year = {2012},
  doi = {10.1016/j.jda.2011.06.005},
  eprint = {0912.0226},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/0912.0226}
}

Attribution and submission status

Responsible human contributor: Thiago Costa
(@ThiagoCAltoe). Discovery, proofs, drafting,
implementation and automated adversarial checking were assisted by Codex AI
agents. Human scientific review is pending. Maintainers decide
nontriviality, acceptance and any coauthorship credit; no such result is
claimed. The Decision wrapper is not counted separately.