Add chordal separators and Dirac theorems

[jtraverso]

Summary

• define chordal graphs via the cycle-and-chord characterization
• state heredity directly through SimpleGraph.comap and derive induced-subgraph heredity
• prove that every minimal vertex separator in a chordal graph is a clique
• formalize Dirac's simplicial-vertex theorem and its two-nonadjacent-vertices strengthening
• expose the finite results over [Finite V], constructing implementation-level decidability only inside proofs

This is a reusable formalization byproduct accompanying Paper II, Complete-Split Extremizers for a Fractional Triangle-Cover Functional on Chordal Graphs. The source metadata now links to the exact frozen Contrib/Submission/Chordal.lean artifact in Paper II v1.2.

This revision responds to the significance/API review by folding the former heredity layer into the full minimal-separator/Dirac development. In particular, IsChordal.comap now literally concludes (G.comap f).IsChordal; it no longer duplicates SimpleGraph.Embedding data as a Function.Embedding plus a separate adjacency equivalence.

Local checks

• lake build LeanPool.Erdos81PaperIIContrib — completed successfully (1082 jobs)
• lake exe runLinter LeanPool.Erdos81PaperIIContrib — pass
• lake exe lint-style LeanPool.Erdos81PaperIIContrib — pass
• lake exe mk_all --check — pass
• explicit axiom audit:
  • IsChordal.comap, IsChordal.induce: [propext, Quot.sound]
  • separator and Dirac theorems: [propext, Classical.choice, Quot.sound]

The expanded source is kernel-clean and the project remains a draft while CI and review assess the larger port. The build currently reports advisory proof-style warnings inherited from the verified Aristotle-generated development; no linter has been disabled or suppressed.

[github-actions]

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 14.78 s (= 0.25 min) — user 4.98 s, sys 3.53 s.

This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget.

Total heartbeats: 22 maxHeartbeats units across 2 files (95 added LOC).

Sum of lean --profile: 2568.6 ms (= 2.57 s). Import-excluded time: 438.6 ms (= 0.44 s).

Count-heartbeats wall-clock total: 4.39 s. Repeated import cost inside lean --profile: 2130.0 ms (= 2.13 s).

Heartbeat values come from Mathlib's linter.countHeartbeats and are already in maxHeartbeats units. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

LOC counts added lines in the profiled Lean files from this PR diff.

File	LOC	Heartbeats (maxHB)	Count wall (s)	lean --profile (s)	Without import (s)	Import (s)	Decls	Errors
LeanPool/Erdos81PaperIIContrib/Chordal.lean	70	22	2.22	1.33	0.27	1.06	6	0
LeanPool/Erdos81PaperIIContrib.lean	25	0	2.17	1.24	0.17	1.07	0	0
Total	95	22	4.39	2.57	0.44	2.13	6	0

Aggregate phase totals

Phase	Time
import	2130.0 ms (= 2.13 s)
interpretation	281.0 ms (= 0.28 s)
initialization	71.5 ms (= 0.07 s)
tactic execution	20.1 ms (= 0.02 s)
elaboration	19.4 ms (= 0.02 s)
tacticAnalysis	11.7 ms (= 0.01 s)
linting	5.9 ms (= 0.01 s)
typeclass inference	5.6 ms (= 0.01 s)
simp	5.3 ms (= 0.01 s)
type checking	5.2 ms (= 0.01 s)
parsing	3.9 ms (= 0.00 s)
overlappingInstancesLinter	3.4 ms (= 0.00 s)

Slowest changed modules (from lake build)

Changed module	Lake time
LeanPool.Erdos81PaperIIContrib.Chordal	3.00 s
LeanPool.Erdos81PaperIIContrib	1.30 s

Per-file `lean --profile` output

LeanPool/Erdos81PaperIIContrib.lean

import took 1.07s
cumulative profiling times:
	elaboration 0.261ms
	import 1.07s
	initialization 41.3ms
	interpretation 126ms
	linting 0.415ms
	module linting 0.00184ms
	overlappingInstancesLinter 0.855ms
	parsing 0.0506ms
	tacticAnalysis 1.47ms
real 1.92
user 1.05
sys 0.89

LeanPool/Erdos81PaperIIContrib/Chordal.lean

import took 1.06s
cumulative profiling times:
	attribute application 0.0515ms
	congr simp thm 0.311ms
	elaboration 19.1ms
	fix level params 0.518ms
	import 1.06s
	initialization 30.2ms
	instantiate metavars 0.732ms
	interpretation 155ms
	let-to-have transformation 0.0381ms
	linting 5.44ms
	module linting 0.00163ms
	overlappingInstancesLinter 2.57ms
	parsing 3.81ms
	process pre-definitions 2.32ms
	share common exprs 1.77ms
	simp 5.31ms
	tactic execution 20.1ms
	tacticAnalysis 10.2ms
	type checking 5.2ms
	typeclass inference 5.6ms
real 1.96
user 1.13
sys 0.90

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.

[github-actions]

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

Reviewed head: e19f221565c33da53e92c940f7655d62da95f328

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

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	Each headline matches the corresponding Lean theorem, including its finiteness, nonemptiness, connectedness, and non-completeness conditions.
Novelty	✅ pass	No Mathlib declaration or pooled project in the supplied prior-art search already proves any of the five headline chordal-graph results.
Significance	✅ pass	The PR develops a self-contained chordal-graph theory culminating in named Dirac theorems and the clique theorem for minimal separators.
Sources	✅ pass	The frozen GitHub artifact is not inspectable from the diff, but the cited Dirac variants are explicitly labelled and no source inconsistency is demonstrated.
Code quality (advisory)	✅ pass	The long argument is factored into narrowly scoped private helpers with visible consumers, while the public API keeps finiteness and decidability assumptions localized.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	Chordality is assumed throughout; IsChordal.comap also takes an injective map, minimalSeparator_isClique takes minimal-separator evidence, and the existence results take the finiteness, nonemptiness, connectedness, and non-completeness hypotheses stated in the card.
Matches cited source	🟡 unverifiable
Fit	✅ good_fit
Level	graduate
Branch	graph theory
Mode	theory_building
Code quality	4 / 5

Statement check: The declarations prove chordality under comap and induce, cliquehood of a finite minimal separator, existence of a simplicial vertex in a nonempty finite chordal graph, and two distinct non-adjacent simplicial vertices in the connected non-complete finite case.

The contribution formalizes induced-subgraph heredity, clique minimal separators, existence of simplicial vertices, and the connected non-complete two-simplicial-vertex conclusion for finite chordal graphs.

---

Tokens: 116,348 in / 7,312 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $0.4006
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]

I reviewed head 5bec2cc4eb0283ff5542cf477933b71dca721291. The definitions and heredity proofs appear correct, and the Paper II manuscript does list induced-subgraph heredity as a standard chordal-graph fact. The blocker is standalone significance, not correctness.

This PR contains only about 70 implementation lines / 95 profiled Lean LOC. Its substantive result is the elementary pullback of chordality along an induced embedding; IsChordal.induce is then a one-line specialization. That falls below the repository's 250-LOC candidate baseline and the significance rubric's graduate/research-level threshold. The PR body says the larger Dirac/minimal-separator development is forthcoming. Please bundle this layer with that work, where heredity becomes infrastructure supporting a significant theorem.

Chordal.lean:40–49 also introduces IsSimplicial, Separates, and IsMinimalSeparator, but none is consumed here. Merging now would freeze an unexercised public API before the separator proofs validate its generality.

When revising the API, use Mathlib's bundled graph embedding (f : H ↪ɢ G) or state the actual comap theorem (G.comap f).IsChordal. The current Function.Embedding plus a separate adjacency equivalence is exactly the data already packaged by SimpleGraph.Embedding, while a theorem named comap should preferably mention comap.

All checks are green, and performance is excellent—22 max-heartbeat units and 0.44s import-excluded time—but that confirms this is a tiny preliminary layer. I would not merge it as a standalone Lean Pool project; I would welcome it folded into the promised chordal-graph development.

[jtraverso]

Implemented the requested direction in commit 58695bd: the PR now includes the minimal-separator clique theorem and both Dirac simplicial-vertex theorems (854 changed lines), and the comap API now states the actual G.comap f theorem using Mathlib's graph embedding. Source metadata points to the exact Paper II v1.2 frozen artifact. Local build, module linter, style linter, generated-root check, and explicit axiom audit all pass. I have kept the PR in draft while CI/review evaluates the expanded development; generated-proof style warnings are disclosed rather than suppressed.

[jtraverso]

Fixed the final CI issue in commit 9fa6394 by regenerating the Paper II project card from projects.yml. The canonical card now includes the induced-subgraphs tag and the generated Main declarations formatting. The targeted card-current check passes, lake exe mk_all --check reports no update necessary, and the diff is limited to LeanPool/Erdos81PaperIIContrib.lean; no Lean definitions or proofs changed. This push reruns the authoritative full quality gate.

[jtraverso]

Resolved the remaining long-line CI warning in commit afef4c5. The generated project card now has a single headline declaration, SimpleGraph.IsChordal.exists_two_nonadj_isSimplicial; all other public results remain unchanged and continue to be documented under main_results. Targeted validation passes: 1082-job build with no warnings, runLinter, lint-style, project-card current check, and mk_all --check. No proof code changed.

[jtraverso]

@Vilin97 Ready for maintainer re-review at exact head 4b2042f. The original significance/API concerns are now addressed by the minimal-separator clique theorem, both Dirac simplicial-vertex theorems, and the actual SimpleGraph comap API. The Aristotle cleanup preserves all public statements and axiom footprints while removing the generated-proof warnings. The project card now uses the strongest Dirac theorem as its headline, with the remaining public results retained in main_results. Exact-head CI is fully green, including Build pool, Build project, linters, repository-quality checks, separation guard, and documentation.

[greptile-apps]

Greptile Summary

The PR adds a reusable chordal-graph formalization and integrates it into Lean Pool.

• Defines chordality, simplicial vertices, and fixed-endpoint vertex separators.
• Proves chordality under comaps and induced subgraphs.
• Establishes the clique property for finite minimal separators of fixed vertex pairs and finite forms of Dirac’s simplicial-vertex results.
• Registers and imports the new Paper II contribution.

Important Files Changed

Filename	Overview
LeanPool/Erdos81PaperIIContrib/Chordal.lean	Adds the chordal-graph definitions and separator and Dirac theorems; the repaired separator documentation now matches the theorem’s finite, fixed-endpoint scope.
LeanPool/Erdos81PaperIIContrib.lean	Adds the project entry module with an overview that accurately qualifies the separator result.
LeanPool/projects.yml	Registers the contribution and accurately describes the separator theorem as applying to finite minimal separators of fixed vertex pairs.
LeanPool.lean	Exposes the new Paper II contribution through the repository root imports.

_{Reviews (27): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger Greptile}

[jtraverso]

@Vilin97 The branch is now synchronized with current main at exact head d27dcdc6. The merge only incorporates the upstream README statistics refresh; the four Paper II contribution files are unchanged. All review threads remain resolved. Could you please perform the final maintainer re-review when convenient?

[jtraverso]

@Vilin97 The branch is updated to current main at head bebf7655. For final re-review, every blocker in the original review of 5bec2cc4 is now addressed:

• Standalone significance: the preliminary ~95-LOC heredity layer is now a 957-line chordal-graph development proving the finite fixed-endpoint minimal-separator clique theorem and both parts of Dirac's theorem.
• Previously unexercised API: IsSimplicial, Separates, and IsMinimalSeparator are now consumed by the public separator and Dirac results.
• Graph embedding/comap API: SimpleGraph.IsChordal.comap now states (G.comap f).IsChordal and its proof uses SimpleGraph.Embedding.comap.
• Claim scope: the catalog, module overview, and theorem docstring consistently say “finite minimal separators of fixed vertex pairs.”

All review threads are resolved, and the exact-head CI is rerunning after the base update. GitHub still carries the old CHANGES_REQUESTED review, so please re-review and approve or dismiss that stale review when convenient.

[greptile-apps]

Want your agent to iterate on Greptile's feedback? Try greploops.

[Vilin97]

Reviewed exact head 822738f3089d92c5e65a6bfb8c88c992e4699167. The earlier review on 5bec2cc4 is stale: this revision now has 957 lines of substantive chordal-graph development, consumes the separator/simplicial API, uses the actual comap construction, builds and lints locally, and has green exact-head CI. Those original blockers are resolved.

One source/scope blocker remains. The project summary and mathematical overview say the development formalizes “both parts of Dirac’s theorem,” but SimpleGraph.IsChordal.exists_two_nonadj_isSimplicial assumes hconn : G.Connected. Dirac’s standard second theorem is for every finite non-complete chordal graph, without connectedness. The cited frozen artifact confirms only the same connected special case, so it does not support the broader “both parts” wording.

Please either prove the full non-complete theorem, or consistently label this result in the title/card/module prose as the connected special case and avoid claiming that both parts of Dirac’s theorem are formalized. The exact theorem-level informal statement is already accurate; the blocker is the broader attribution and project summary.

[Vilin97]

Supplementary provenance finding for the current head 822738f3089d92c5e65a6bfb8c88c992e4699167: the cited source artifact header says it is released under Apache-2.0 “as described in LICENSE,” but the cited repository’s root LICENSE is CC BY-NC 4.0. Lean Pool requires Apache-2.0 or MIT-compatible licensing. Please provide an explicit, unambiguous Apache-2.0 license grant for this imported artifact (or point the source card to a compatible commit/path) before merge. This is in addition to the theorem-scope/source-card correction in the formal review.

[jtraverso]

@Vilin97 Addressed both remaining blockers at exact head 9a28038c.

Dirac scope: the project title is now “Chordal graphs: minimal separators and simplicial vertices.” The catalog and generated module overview now say precisely that the development proves Dirac's simplicial-vertex theorem and the connected non-complete case of the two-vertex conclusion. The public theorem docstring has likewise been changed from “Dirac's theorem, second part” to “Connected case of Dirac's two-vertex conclusion.” The exact theorem-level informal statement remains unchanged and accurate. No declaration or proof body changed.

License provenance: the source card now points to the immutable source at commit 822738f3 in jtraverso/lean-pool, whose repository license is unambiguously Apache-2.0:

• source: https://github.com/jtraverso/lean-pool/blob/822738f3089d92c5e65a6bfb8c88c992e4699167/LeanPool/Erdos81PaperIIContrib/Chordal.lean
• license: https://github.com/jtraverso/lean-pool/blob/822738f3089d92c5e65a6bfb8c88c992e4699167/LICENSE

Local validation on the updated branch:

• lake exe mk_all --check: PASS
• lake build LeanPool.Erdos81PaperIIContrib: PASS (1082 jobs)
• lake exe runLinter LeanPool.Erdos81PaperIIContrib: PASS
• lake exe lint-style LeanPool.Erdos81PaperIIContrib: PASS
• git diff --check: PASS

Please re-review this exact head when convenient.

[Vilin97]

Maintainer decision required

Reviewed exact head d489b021917dbfd63414e2eda826cd04fbb068c0. The prior scope and provenance requests are resolved: the title/card/module now consistently identify the connected non-complete case of Dirac's two-vertex conclusion, and the cited frozen artifact sits in an Apache-2.0 repository. All five main-result informals match the Lean statements, no searched Mathlib or Lean Pool declaration duplicates them, exact-head CI and Greptile are green, and all review threads are resolved. A targeted local build completed in 10.26s; the headline declarations use only the allowed axioms.

The remaining boundary is maintainability. The exact-head quality review rates the code 2/5 because the 957-line module carries parallel Set-based, Finset-based, and induced-set reachability/separator layers plus conversion glue; it also retains three unused tactic imports. The mathematics is a significant, reusable chordal-graph development, and the duplicate machinery is private, so this is not an established faithfulness or correctness failure. A maintainer must decide whether to accept the imported proof structure at Lean Pool's bar or require consolidation around one reachability/separator representation before merge.

Quality evidence: #349 (comment)

[jtraverso]

Removed the remaining tactic-import residue at exact head a72c5d1f: Aesop, Mathlib.Tactic.Cases, Mathlib.Tactic.Linarith, and Mathlib.Tactic.Tauto are no longer imported. No declaration, proof body, or project metadata changed.

Local validation:

• lake build LeanPool.Erdos81PaperIIContrib: PASS (995 jobs; previously 1082 with the broader imports)
• lake exe runLinter LeanPool.Erdos81PaperIIContrib: PASS
• lake exe lint-style LeanPool.Erdos81PaperIIContrib: PASS
• lake exe mk_all --check: PASS
• git diff --check: PASS

I have intentionally not changed the private Set/Finset/induced-set proof architecture without a maintainer request, since that would be a substantially higher-risk proof refactor rather than a cleanup.