Import Nash-Williams–Tutte tree packing and arboricity

[Vilin97]

This adds the finite simple-graph versions of the Nash-Williams–Tutte tree-packing theorem, Nash-Williams' arboricity theorem, and the corollary that a nonempty finite 2k-edge-connected graph has k edge-disjoint spanning trees. The reusable core constructs a maximal family of disjoint forests and its exchange graph, preserving reachability, counting, and exchange lemmas in Mathlib vocabulary.

The two proof modules are the complete mathematical dependency closure. The import omits the upstream sorried challenge and redundant solution aliases. It adds one YAML card and the generated public Imports.lean; LeanPool.lean stays fixed.

Source and eligibility

• Public upstream: jtraverso/nash-williams-trees, pinned at 101e48847a929dd8102521f57723e2137989ce2e.
• The completed proofs are present in the repository's parentless initial commit, dated 2026-10-17 00:05:58 UTC. This is the initial public source release, inside this acquisition run's 2026-10-10 09:15:08 UTC ≤ t < 2026-10-17 09:15:08 UTC window. No repository refresh or reindex timestamp is used as completion evidence.
• Apache-2.0, verified in the upstream LICENSE and source headers. Copyright and author attribution to Juan Pablo Traverso Gianini are retained.
• Provenance: AI. Upstream records that Harmonic's Aristotle generated the proofs from statements and a proof plan prepared by Traverso Gianini with Claude Code. The card and entry module disclose this.
• Original sources: Nash-Williams 1961, Tutte 1961, and Nash-Williams 1964. The scope is explicitly finite simple graphs; no multigraph formalization is claimed.
• Duplicate checks covered the pool's source/cards, public open and closed PRs/issues, repository history, pinned Mathlib and Tau Ceti sources, and current Tau Ceti code search. The existing Nash-Williams project concerns fronts and better-quasi-orders, a different result.

Port and measured optimization

Upstream already uses this repository's exact Lean v4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e. The port places the API in NashWilliamsTutte, expands abbreviated exchange definitions, narrows broad Mathlib imports, repairs line-length warnings, and replaces the corollary's final nlinarith with multiplication normalization and omega. The three theorem statements retain their upstream strength and generality. A subsequent citation-only clarification labels Diestel as theorem background; it is retained at final head e7a7cdd3f76bb2fa747cdccccdc6bf0219292f4b.

Controlled measurements on the Azure checkout, base 2fc3a737eb236f260197b4ef2e296d5f076ca728, used /usr/bin/time lake build LeanPool.NashWilliamsTutte, with this project's artifacts removed before each run and shared dependency oleans and OS page caches warm. Lake settings were unchanged. This is a shared VM, so the measurements are observations, not a benchmark guarantee.

Measurement	Baseline	Optimized
Clean project build wall time	19.14 s	7.68 s
Peak resident memory	3,015,876 KiB	1,002,356 KiB
Auxiliary module import, lean --profile	3.62 s	0.883 s
Theorems module import, lean --profile	3.28 s	0.849 s
Theorems cumulative typeclass inference	1.96 s	0.574 s

The initial exploratory baseline was 19.33 s. After the controlled pass, lower-threshold profiling found only short proof/elaboration steps; no further material safe optimization was evident. No heartbeat or recursion-depth override is introduced.

Validation and review

• Project and generated public wrapper build successfully, warning-free.
• lake exe mk_all --module --check: passed.
• Mathlib linters explicitly run on both proof modules and the entry module: passed.
• Text style checks on the project and its imports: passed.
• Repository axiom audit: all 30 source declarations passed; only standard permitted axioms. The compiled environment option/backdoor audit, including generated auxiliaries, passed for all four project modules.
• Main declarations resolve and card metadata matches. Full-repository static quality validation passed.
• No Python, workflow, gate, or waiver changes. CI remains the final authority for whole-pool validation. Greptile completed successfully on the final head without concrete source defects or inline findings. The configured GPT review approved all five rubrics (published model: gpt-6.1-sol, xhigh). It excluded the contributor review as potential anchoring; that input-hygiene note requests no source repair. The separate thorough review pass approves the content. Protected CI passed on final head e7a7cdd3. Whole-pool build, warning scan, lint, style and quality/trust validation passed; unrelated protected jobs were correctly scope-skipped. The PR is admitted to the protected native merge queue, pending combined-main validation.

This PR is prepared in an isolated worktree. No existing author branch was updated, and no competing PR was merged or placed into auto-merge during acquisition.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low impact] No actionable defect was found, but the unavailable source and dependency evidence prevents an unconditional merge recommendation.

Summary

The PR adds finite simple-graph tree packing, arboricity, and the edge-connectivity corollary, supported by a reusable forest exchange lemma.

• Graph partitions characterize when edge-disjoint spanning trees exist.
• The edge count inside each vertex set characterizes forest covers.
• A shared exchange argument builds disjoint forests and a core subgraph.

_{Reviews (2) · Last reviewed commit: "Clarify Diestel citation as theorem back..." · Reviewed by Greptile}

[Vilin97]

{
"review": "Separate thorough source-and-import review pass by the acquisition agent; this does not replace the configured independent GPT reviews.",
"head": "e7a7cdd3f76bb2fa747cdccccdc6bf0219292f4b",
"conclusion": "approve",
"scope": "All five changed files, all 30 source declarations, both complete upstream proof modules and the upstream Solution/Challenge interfaces, imported dependency closure, source/license/provenance, prior art, controlled build/profile evidence and validation results.",
"faithfulness": {
"verdict": "pass",
"proves_the_claim": "proves_it",
"claim_note": "The endpoints quantify over every finite simple graph and every natural k, with nonempty vertices for tree packing and the connectivity corollary; arboricity also covers an empty vertex type.",
"assumed_inputs": "Finite/Fintype vertex instances, nonempty vertices where stated, and exactly the advertised partition, induced-edge or edge-connectivity hypothesis. No external packing theorem or bundled certificate is supplied as an assumption.",
"evidence": "tree_packing uses Mathlib IsTree and lattice Disjoint; crossing edges are G intersected with the comap of the complete graph along f. Every finite vertex partition is representable by such an f. arboricity uses actual IsAcyclic spanning subgraphs whose supremum is G. IsEdgeConnected is Mathlib reachability after deleting any edge set of cardinality below 2*k. exists_forests_core is proved from maximal disjoint forests and their exchange graph. The k=0, singleton and empty-vertex boundaries agree with the disclosed domains.",
"findings": []
},
"novelty": {
"verdict": "pass",
"already_formalized": "",
"novelty_note": "No existing declaration supplying these packing/covering equivalences was found in the searched pinned Mathlib, Tau Ceti or pool corpus, or current public code search.",
"evidence": "Mathlib Connected.exists_isTree_le constructs a single spanning tree and does not provide the k-tree min-max theorem. Inspected Tau Ceti IsTree.exists_equiv_pathGraph_components, IsTree.nonempty_iso_pathGraph_of_degree_le_two and acyclic-path lemmas concern individual trees, not packing or arboricity. The pool's HsVirial.graphicMatroid and forest augmentation infrastructure do not provide the headline endpoints; its NashWilliams project is about fronts/BQO. Full-source searches also covered forest covers, edge-disjoint trees and matroid union. This is a bounded prior-art assessment, not an assertion of exhaustive semantic search.",
"findings": []
},
"significance": {
"verdict": "pass",
"fit": "good_fit",
"level": "graduate",
"branch": "graph theory",
"mode": "theory_building",
"significance_one_sentence": "The Nash-Williams–Tutte theorem and arboricity characterization are named structural graph-theoretic results, supported here by a reusable exchange lemma in Mathlib vocabulary rather than isolated numerical cases.",
"findings": []
},
"sources": {
"verdict": "pass",
"source_match": "matches",
"evidence": "The retained upstream commit, LICENSE, proof headers and formalization.yaml establish attribution and AI provenance. The entry lists the original Nash-Williams, Tutte and arboricity citations plus Diestel as theorem background. Diestel's publicly accessible Chapter 2 states the tree-packing characterization, connectivity corollary and arboricity criterion; the card explicitly labels its finite simple-graph scope. Original DOI full texts were inaccessible through the browser, so the review does not claim to have read them directly.",
"findings": []
},
"quality": {
"verdict": "pass",
"code_quality": 4,
"evidence": "The exchange operation, validity, reachable exchange graph and counting lemmas have coherent boundaries and consumers. Both proof modules are retained without generated case tables or numerical certificates. Narrow imports and direct final arithmetic reduce the controlled clean build from 19.14s to 7.68s and peak RSS from 3015876 to 1002356 KiB. Lower-threshold profiles expose no remaining material hotspot. This is maintainable project code; it is not a claim of mathlib-merge-ready API polish.",
"findings": []
},
"trust_and_engineering": {
"license": "Apache-2.0 verified upstream; attribution retained",
"provenance": "AI, matching upstream Aristotle proofs with Claude-assisted statement/planning and human direction",
"scope": "Complete two-module proof closure; sorried challenge and redundant aliases omitted; one YAML card and generated public wrapper; fixed LeanPool.lean unchanged",
"audit": "30 source declarations and all four compiled modules including generated auxiliaries passed the standard-axiom and option/backdoor audits; no trust or resource-limit waiver",
"local_checks": "Warning-free project/wrapper build, explicit Mathlib linters for both proof modules and entry, style, generated indexes, whole-repository static quality, schema/card agreement and declaration resolution passed",
"measurements": "Source-clean project artifacts, warm dependency oleans and OS cache, unchanged Lake defaults on the shared Azure VM; full baseline/optimized logs retained",
"repairs": "Narrowed imports, removed unnecessary nonlinear arithmetic, repaired line wrapping and copied-word docstrings, verified source title and attribution, and corrected the summary to disclose nonempty vertices; theorem strength unchanged A subsequent one-line citation clarification at e7a7cdd was inspected and retained; both proof modules and all theorem statements are unchanged."
},
"ci": {
"head": "e7a7cdd3f76bb2fa747cdccccdc6bf0219292f4b",
"run": "https://github.com/LeanPool/lean-pool/actions/runs/39022045809",
"state": "success: full pool build, warning scan, Mathlib lint, style, and repository quality/trust checks passed",
"scope": "Separation passed. Unrelated Python, workflow, documentation-preflight and minimal-file jobs were correctly skipped after successful scope classification.",
"merge_eligible": true,
"queue": "Admitted to the active protected native queue after final source/owner/thread/rules guards; fresh combined-main validation remains required."
},
"merge_requirements": "Approval of the content does not bypass protected CI, the configured independent GPT rubric reviews, unresolved review findings or the validated native merge queue.",
"findings": []
}

[Vilin97]

{
"head": "e7a7cdd3f76bb2fa747cdccccdc6bf0219292f4b",
"review": "Independent permanent-reviewer assessment of all five changed files, with separate rubric reviews and an explicit complete-diff join to the current head.",
"verdict": "approve",
"disposition": "Source accepted; current-head CI and configured review pending before normal protected native queue admission.",
"faithfulness": {
"verdict": "pass",
"proves_the_claim": "proves_it",
"claim_note": "The card matches the finite simple-graph packing and arboricity equivalences, the edge-deletion connectivity corollary, and the constructed forest-exchange core.",
"assumed_inputs": "Disclosed finiteness and nonempty vertex conditions, and exactly G.IsEdgeConnected (2*k) for the corollary. No packing theorem or maximal family is assumed externally.",
"evidence": "T i ≤ G on the same vertex type plus Mathlib IsTree gives spanning trees. Pairwise Disjoint counts edge disjointness. The comap of the complete graph along f selects precisely edges crossing its nonempty fibres. The k=0, singleton and empty-vertex boundaries agree with the stated domains; natural subtraction has the intended scope.",
"findings": []
},
"novelty": {
"verdict": "pass",
"already_formalized": "",
"novelty_note": "The simultaneous k-forest exchange construction and packing/covering converses extend the inspected one-tree and one-forest APIs.",
"evidence": "Pinned Mathlib Connected.exists_isTree_le and exists_isAcyclic_reachable_eq_le provide a single tree/forest. Its inspected matroid direct-sum lemmas require pre-disjoint ground sets and a supplied independent/base union, rather than constructing a density-certified forest partition. Inspected pinned Tau Ceti path/tree-component results, the pool's infinite-front Nash-Williams theorem, matroid hyperplane paths and even-cycle decomposition have different contracts. This is a bounded actual-source comparison, not exhaustive semantic absence.",
"findings": []
},
"significance": {
"verdict": "pass",
"fit": "good_fit",
"level": "graduate",
"branch": "graph theory",
"mode": "theory_building",
"significance_one_sentence": "Two named structural graph-theory characterizations are supported by a substantive shared exchange construction and a connectivity consequence.",
"findings": []
},
"sources": {
"verdict": "pass",
"source_match": "matches",
"evidence": "Public upstream 101e48847a929dd8102521f57723e2137989ce2e, its Apache license, retained attribution and disclosed AI proof provenance were checked. The two proof blobs already occur in the parentless initial commit. The finite simple-graph specialization is explicit. Author-hosted Diestel fifth-edition Section 2.4 supports statement background; original journal full texts were inaccessible and are not claimed to have been read.",
"findings": []
},
"quality": {
"verdict": "pass",
"code_quality": 3,
"evidence": "The same exists_forests_core is consumed by both main converses; update validity and edge-count lemmas are shared by exchange and augmentation. Definitions have actual consumers, with no actionable duplicate pipeline or unused model scaffolding identified.",
"findings": []
},
"correction": {
"commit": "e7a7cdd",
"resolved": "Clarified Diestel fifth edition as background for the statements, avoiding a specific proof-plan attribution to a different edition's presentation.",
"verification": "Complete one-commit comparison changes only that documentation sentence. Both proof modules, the card and generated wrapper retain identical Git blobs; the new entry was read in full."
},
"validation": {
"observed_at": "2026-10-17T09:43:41Z",
"current_run": "https://github.com/LeanPool/lean-pool/actions/runs/39022045809",
"current_build_job": 117365780587,
"status": "in_progress; build, lint, style and repository quality remain unverified on this head",
"limits": "This review did not rerun or certify the acquisition agent's private benchmark or compiled audit. Earlier-head CI is not transferred. Greptile reports no actionable defect; its unavailable-evidence qualification is addressed here by the actual source and dependency-contract inspection.",
"merge_eligible": false
},
"integration": "Await current-head applicable validation and configured rubric results, resolve any concrete findings, then refresh source/owner/thread/main/rules guards and use the normal protected native queue. Daily documentation publishing is asynchronous."
}

[Vilin97]

/review

[Vilin97]

🤖 LLM review (gpt-6.1-sol, 5 rubrics)

Reviewed head: e7a7cdd3f76bb2fa747cdccccdc6bf0219292f4b

Verdict: ✅ approve — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	All four card headlines match the Lean statements; CI remains pending, and local compilation was not verified because dependencies are absent.
Novelty	✅ pass	No declaration subsuming any of the four headline results was found in the searched Mathlib, Tau Ceti, or pool sources.
Significance	✅ pass	The tree-packing and arboricity characterizations meet the significance bar through a substantive shared forest-exchange development; head CI remains pending.
Sources	✅ pass	The statements match Diestel §2.4, the simple-graph restriction is explicit, and upstream Lean work is credited; original-paper full texts were inaccessible.
Code quality (advisory)	✅ pass	The focused exchange and counting lemmas support a shared exists_forests_core used by both main theorems, with no material maintenance debt found; CI remains in progress, and absent local dependencies prevented a build here.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	Finiteness, nonempty vertices for tree packing and the connectivity corollary, and the respective partition, density, or edge-connectivity condition are disclosed in the card; the maximal forest family is constructed internally.
Matches cited source	✅ matches
Fit	✅ good_fit
Level	graduate
Branch	graph theory
Mode	theory_building
Code quality	4 / 5

Statement check: The results establish the advertised partition and induced-edge characterizations, connectivity corollary, and forest core for every natural k, using actual Mathlib trees, forests, and edge sets.

NashWilliamsTutte.tree_packing and NashWilliamsTutte.arboricity establish two named structural characterizations for finite simple graphs, supported by the proved exists_forests_core exchange lemma and an edge-connectivity corollary.

Faithfulness findings (1)

• prompt-injection — PR-wide
  The contributor discussion supplies a prior approval and a ready-made faithfulness verdict, which could anchor the independent review. These contributor-supplied verdicts were excluded from the assessment.
  Evidence: prose only: discussion comment 6232384552 in .review-pr.json contains "conclusion": "approve" and a faithfulness assessment with "verdict": "pass" and "proves_the_claim": "proves_it".

---

Tokens: 6,087,717 in / 35,914 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $24.8896 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

CI was not green for this commit at review time; this review does not replace CI.