Add classical matching and factor theory collection

[jtraverso]

This adds Classical matching and factor theorems in finite graphs, an integrated collection whose headline results are the Tutte–Berge formula and Tutte's f-factor criterion.

Mathematical scope

• Berge's augmenting-path characterization and the Tutte–Berge matching/barrier identity.
• Kőnig–Egerváry matching–vertex-cover duality for finite bipartite graphs.
• Petersen's theorem for finite bridgeless cubic graphs, including a perfect matching through any prescribed edge.
• Tutte's f-factor criterion via a matching gadget and its necessity/sufficiency proofs.
• Decomposition of a finite 2k-regular graph into k spanning two-factors, including k = 0.
• Dilworth's and Mirsky's finite partition theorems as an order-theoretic companion.

The collection uses Mathlib's SimpleGraph, matching and perfect-matching predicates. Hall's and Tutte's one-factor theorems are imported from Mathlib and are credited as existing inputs. Three short integration interfaces combine maximum-matching certificates and matching–cover optimality. The mathematical results are classical; this submission contributes their integrated Lean formalizations, rather than claiming new mathematics or polynomial-time algorithms.

Source provenance

The 18 Lean files integrate five Apache-2.0 developments registered with Palomar, with original sources pinned in the module documentation:

Development	Frozen source	Palomar registration
Kőnig–Egerváry; Dilworth–Mirsky	konig-edge-colouring, 7c60f7e	PALOMAR-2026-10-15-000019
Berge; Tutte–Berge	berge-matching, b9c91bf	PALOMAR-2026-10-16-000011
Petersen perfect matching	petersen-matching, 77630d6	PALOMAR-2026-10-16-000004
Even-regular two-factors	euler-petersen, 02c3f1a	PALOMAR-2026-10-16-000016
Tutte f-factors	tutte-f-factor, dc3bbce	PALOMAR-2026-10-18-000005

Authorship: Juan Pablo Traverso Gianini. Proof provenance: AI, as declared in the project card. The card and result documentation identify the classical mathematical sources separately from these implementation sources.

Integration and validation

The diff is limited to 18 Lean files and the project YAML card (4,302 physical lines). Import LeanPool.ClassicalMatchingFactors.Imports for the public aggregate. The project has no mathematical dependency on another Lean Pool project; Kőnig edge colouring and copied Vizing infrastructure are outside this submission. Comparison against the relevant Mathlib, Tau Ceti and pool sources was performed; the repository's independent novelty review remains necessary.

Locally checked at e9c09ffe087ab4b110d50f1db19d4c296ec8abfa, based on ae357410e8e2711ccd7fdb77e41859142331d355:

• Project aggregate build under the official Lean 4.35.0-rc3 / Mathlib pins: PASS without warnings.
• Declaration linters, including slow checks: PASS.
• Official project/card quality checks and generated aggregate comparison: PASS.
• Axioms of 134 public declarations and the official compiled-environment audit over all 18 modules: PASS, only the permitted foundational axioms.
• Boundary consumers: empty vertex type, finite-only bipartite interface, two-factor interface without DecidableEq, and zero factors: PASS.
• Official text-linter API over all 18 files, with the standard linters enabled and a positive self-test: PASS.

On this Windows host, the lake exe lint-style executable itself encountered a Lake initialization error (Lake.packageAttr). Its official text-linter functions were checked directly instead; this is not represented as a successful CLI run. The normal Linux CI command, whole-pool checks and independent project reviews are still pending.

[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 remains in the reviewed changes, but the unverified source, license, novelty, and cost dimensions prevent an unconditional merge recommendation.

Summary

Adds classical matching, factor, and finite-order theorems using Mathlib’s graph and matching predicates.

• Finite graphs now have matching theorems and optimality certificates.
• Bridgeless cubic graphs now have perfect matchings through any chosen edge.
• Tutte’s criterion now characterizes graphs with prescribed degrees.
• Even-regular graphs now split into spanning two-factors.
• Finite posets now have matching chain and antichain partitions.
• One public import brings the classical theorem collection into Lean Pool.

_{Reviews (2) · Last reviewed commit: "Consolidate Euler circuit proof and drop..." · Reviewed by Greptile}

[Vilin97]

{
"summary": "At e9c09ff this is a completed, substantive collection of finite matching and factor theory. The card's ten results agree with the actual matching, odd-component, degree and finite-poset statements. Hall and Tutte's one-factor theorem are disclosed inputs; the augmenting-path, Tutte–Berge, general f-factor, prescribed-edge Petersen and two-factor conclusions are proved in the submitted development. The public aggregate reaches all eighteen modules. Source approval is separate from authored CI, the matching configured review and protected queue validation.",
"assessment": {
"fit": "good_fit",
"level": "graduate",
"branch": "graph theory and finite order theory",
"mode": "theory_building",
"obscure_problem": false,
"code_quality": 3,
"significance_one_sentence": "Tutte–Berge and the full f-factor criterion anchor an integrated development of classical matching, minimax, regular-graph and finite-order theorems.",
"novelty_note": "The inspected pinned Mathlib, TauCeti and current pool candidates do not supply the same headline contracts. Hall and Tutte's one-factor theorem are reused prerequisites; the pool's degree-constrained matching, representation-equivalence, even-cycle and colouring results have different conclusions. This is a bounded source comparison, not an assertion that every possible prior formalization has been excluded.",
"source_note": "The five frozen upstream developments have Apache-2.0 licenses and their authorship and AI proof provenance are consistent with the submission. The Tutte 1954 publisher citation was checked; other inaccessible historical DOI pages remain unverified, with no demonstrated citation mismatch."
},
"verdict": "approve",
"findings": [],
"scope": {
"reviewed_head": "e9c09ffe087ab4b110d50f1db19d4c296ec8abfa",
"source_coverage": "All nineteen added files, including the full eighteen Lean modules, were reviewed by the logical reviewer and independent mathematical peer; no elided diff used for acceptance.",
"mathematical_inputs": "Finite vertex types; actual Mathlib graph/matching predicates; prescribed-edge Petersen assumes cubic and bridgeless. The f-factor inequality is in integers and derives f(v) ≤ degree(v), rather than imposing it silently; the two-factor decomposition includes k=0. No new mathematical or polynomial-time-algorithm claim is made.",
"validation": "The author's local validation remains attributed. Repository CI and its actual applicable protected contexts, the configured exact-head review and native merge-group validation remain required."
},
"advisory": {
"thread": 4309178558,
"disposition": "Nonblocking; no source change required.",
"rationale": "EulerTrail imports EulerCircuit and its stronger prescribed-start theorem uses exists_mem_support_adj_not_mem_edges from the earlier module. Directly deriving the earlier circuit theorem from the later result would create a cycle. Consolidation should first extract the shared trail helpers while preserving the public module API; the current two proofs are acceptable."
}
}

[Vilin97]

/review

Please independently review exact head e9c09ffe087ab4b110d50f1db19d4c296ec8abfa under all five current project rubrics. Authored CI is still running and remains required before protected queue admission.

[Vilin97]

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

Reviewed head: ddc69d46947836112fd62c9cc593a82c4221461c

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

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	All ten card headlines match the Lean statements and definitions, with no undisclosed substantive hypotheses or postulated content found.
Novelty	✅ pass	No headline duplicate was identified in Mathlib or the pool; a complete semantic comparison with Tau Ceti remains unverifiable beyond the inspected declarations and searches.
Significance	✅ pass	The Tutte–Berge formula and Tutte’s f-factor criterion anchor a substantial, completed development that meets the significance bar.
Sources	✅ pass	Tutte’s 1954 paper supports the f-factor criterion, and all five imported Lean developments are credited; some historical-source statements remain unverifiable.
Code quality (advisory)	✅ pass	The proofs are competently organized; repeated unnecessary public tactic imports are minor maintenance debt.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	The stated finiteness, bipartiteness, regularity, bridgelessness, and partial-order hypotheses match the card. Hall’s and Tutte’s one-factor theorems are imported from Mathlib as disclosed; decidability instances impose no additional classical mathematical restriction.
Matches cited source	🟡 unverifiable
Fit	✅ good_fit
Level	graduate
Branch	finite graph theory and order theory
Mode	theory_building
Code quality	3 / 5

Statement check: The Lean proves the Tutte–Berge identity, the full f-factor equivalence for natural-valued degree prescriptions, and the remaining listed matching, factor, and finite-order results, including the zero-factor case.

The Lean develops classical matching and factor theory through augmenting paths, odd-component obstructions, matching gadgets, and regular-graph decompositions, with Dilworth and Mirsky partition theorems as companions.

Code quality findings (1)

• unused-import — LeanPool/ClassicalMatchingFactors/Factors/Defs.lean:13
  All seven Factors modules, Bipartite/MatchingCover, Matching/Berge, Matching/Petersen, and Order/ChainPartitions repeat this broad tactic import block. Neither FinCases nor GCongr has a tactic invocation anywhere in the collection; Defs contains only oddCount. These public imports obscure actual dependencies and unnecessarily widen the foundational module's import surface. Trim imports per module and keep proof-only tactic imports private where possible.
  Evidence: public import Mathlib.Tactic.FinCases
  public import Mathlib.Tactic.GCongr

noncomputable def oddCount (G : SimpleGraph V) (f : V → ℕ) (S T : Finset V) : ℕ :=
Nat.card {c : (G.induce ((S ∪ T : Finset V) : Set V)ᶜ).ConnectedComponent //
Odd (∑ w ∈ univ.filter (fun w : ↥(((S ∪ T : Finset V) : Set V)ᶜ) =>
(G.induce ((S ∪ T : Finset V) : Set V)ᶜ).connectedComponentMk w = c),
(f w + #{t ∈ T | G.Adj w t}))}

---

Tokens: 10,392,237 in / 39,261 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $42.1579 (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.

[Vilin97]

{
"summary": "At ddc69d4 the complete three-file delta removes redundant Euler counting/existence proofs and an unnecessary f-factor helper premise. The shared parity proof genuinely produces the circuit theorem; both public import paths and all150 written declaration names remain. The unchanged collection still proves the ten matching, factor, regular-graph and finite-order contracts reviewed at its frozen parent. Source approval remains separate from matching configured review, current-main qualification and protected queue integration.",
"assessment": {
"fit": "good_fit",
"level": "graduate",
"branch": "graph theory and finite order theory",
"mode": "theory_building",
"obscure_problem": false,
"code_quality": 4,
"significance_one_sentence": "Tutte–Berge and the full f-factor criterion anchor an integrated development of classical matching, minimax, regular-graph and finite-order theorems.",
"novelty_note": "The inspected pinned Mathlib, TauCeti and current pool candidates do not supply the same headline contracts. Hall and Tutte's one-factor theorem are reused prerequisites; the pool's degree-constrained matching, representation-equivalence, even-cycle and colouring results have different conclusions. This is a bounded source comparison, not an assertion that every possible prior formalization has been excluded.",
"source_note": "The five frozen upstream developments have Apache-2.0 licenses and their authorship and AI proof provenance are consistent with the submission. The Tutte 1954 publisher citation was checked; other inaccessible historical DOI pages remain unverified, with no demonstrated citation mismatch."
},
"verdict": "approve",
"findings": [],
"scope": {
"reviewed_head": "ddc69d46947836112fd62c9cc593a82c4221461c",
"source_coverage": "All19 current file identities/modes authenticated:16 literal bodies retain the complete parent review; all274 lines of the complete three-file native delta, both whole current Euler modules and the full changed f-factor helper/caller proofs were read. Independent mathematical/API review agrees; no elided diff is used for acceptance.",
"mathematical_inputs": "Finite vertex types; actual Mathlib graph/matching predicates; prescribed-edge Petersen assumes cubic and bridgeless. The f-factor inequality is in integers and derives f(v) ≤ degree(v), rather than imposing it silently; the two-factor decomposition includes k=0. No new mathematical or polynomial-time-algorithm claim is made.",
"validation": "This is the exact-head source verdict. Actual applicable authored CI, a matching current-head configured review, qualified current-main CI and normal protected native-group checks remain required before merge. The earlier e9c configured result is historical for this head.",
"intentional_API_changes": "Removing hT strengthens the f-factor auxiliary helper. The compatibility extension lemma keeps its mathematical Type but renames hp to _hp; external named-argument calls using hp := could need the new spelling. No such internal caller exists; no blanket compiled-API identity claim is made."
},
"advisory": {
"disposition": "Both earlier maintenance findings are repaired.",
"rationale": "EulerTrail now owns the shared support/count helpers and unchanged parity producer; EulerCircuit publicly reexports it. Circuit existence is a corollary at a vertex supplied by connectedness. The old extension helper validly returns its existing circuit-existence disjunct, without circularity. The redundant hT premise and corresponding F1 argument are removed; F3 retains its genuine witness assumptions."
}
}

[Vilin97]

/review

Please independently review exact head ddc69d46947836112fd62c9cc593a82c4221461c under all five current project rubrics. The Euler consolidation and f-factor helper cleanup have received a new exact-head source approval. The parent-head review is historical; authored CI, current-main CI and protected native queue validation remain separate requirements.