Repository navigation
Classical graph colouring: lists, orientations and spectra - #687
Conversation
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Medium impact] No blocking defect was established, but external source and license checks remain incomplete. SummaryAdds classical graph-colouring results through list colouring, directed paths, and eigenvalues. The latest change replaces the ratio-bound citation with Haemers (2021), Theorem 1.
Reviews (6) · Last reviewed commit: "Cite Haemers for Hoffman's independent-s..." · Reviewed by Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
Proof profile (new / modified Lean files)
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: 201,498 maxHeartbeats units across 9 valid files (1,412 added LOC). Sum of Count-heartbeats wall-clock total: 55.93 s. Repeated import cost inside Heartbeat values sum disjoint root command traces with LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.ClassicalGraphColouring.Spectrum.Bounds |
7.10 s |
LeanPool.ClassicalGraphColouring.Galvin.Kernel |
5.70 s |
LeanPool.ClassicalGraphColouring.Orientations.GallaiRoy |
5.30 s |
LeanPool.ClassicalGraphColouring.Galvin.GaleShapley |
5.20 s |
LeanPool.ClassicalGraphColouring.Konig.Basic |
3.70 s |
LeanPool.ClassicalGraphColouring.Galvin.Galvin |
2.70 s |
LeanPool.ClassicalGraphColouring.Galvin.Orientation |
2.00 s |
LeanPool.ClassicalGraphColouring |
1.50 s |
LeanPool.ClassicalGraphColouring.Imports |
1.50 s |
Per-file `lean --profile` output
LeanPool/ClassicalGraphColouring.lean
import took 3.24s
cumulative profiling times:
attribute application 0.0209ms
elaboration 15.4ms
fix level params 0.0758ms
import 3.24s
initialization 41.4ms
instantiate metavars 0.0386ms
interpretation 252ms
let-to-have transformation 0.04ms
linting 3.64ms
module linting 0.00148ms
overlappingInstancesLinter 3.48ms
parsing 1.83ms
process pre-definitions 0.424ms
share common exprs 0.207ms
tacticAnalysis 7.6ms
type checking 5.91ms
typeclass inference 11.7ms
real 4.20
user 1.49
sys 1.29
LeanPool/ClassicalGraphColouring/Galvin/GaleShapley.lean
import took 1.38s
cumulative profiling times:
attribute application 0.0433ms
congr simp thm 0.101ms
elaboration 14.3ms
fix level params 0.606ms
import 1.38s
initialization 37.1ms
instantiate metavars 0.76ms
interpretation 260ms
let-to-have transformation 0.0488ms
linting 9.29ms
module linting 0.00157ms
overlappingInstancesLinter 2.98ms
parsing 7.22ms
process pre-definitions 2.55ms
share common exprs 1.18ms
tactic execution 43.1ms
tacticAnalysis 24.1ms
type checking 6.2ms
typeclass inference 25.8ms
real 2.40
user 1.44
sys 1.10
LeanPool/ClassicalGraphColouring/Galvin/Galvin.lean
import took 1.38s
cumulative profiling times:
attribute application 0.033ms
compilation (IR) 0.0967ms
compilation (LCNF base) 0.566ms
compilation (LCNF impure) 0.521ms
compilation (LCNF mono) 0.543ms
congr simp thm 4.11ms
elaboration 14.6ms
fix level params 0.407ms
import 1.38s
initialization 37.6ms
instantiate metavars 0.835ms
interpretation 263ms
let-to-have transformation 0.0537ms
linting 9.52ms
module linting 0.00156ms
overlappingInstancesLinter 3.69ms
parsing 5.63ms
process pre-definitions 2.29ms
share common exprs 1.65ms
simp 217ms
tactic execution 56.9ms
tacticAnalysis 20.7ms
type checking 11.4ms
typeclass inference 682ms
real 3.32
user 2.32
sys 1.11
LeanPool/ClassicalGraphColouring/Galvin/Kernel.lean
import took 1.37s
cumulative profiling times:
attribute application 0.029ms
congr simp thm 1.18ms
elaboration 14.9ms
fix level params 0.743ms
import 1.37s
initialization 29.8ms
instantiate metavars 1.37ms
interpretation 262ms
let-to-have transformation 0.0429ms
linting 13.8ms
module linting 0.00134ms
overlappingInstancesLinter 3.57ms
parsing 5.71ms
process pre-definitions 2.73ms
share common exprs 1.72ms
simp 41.5ms
tactic execution 76.3ms
tacticAnalysis 22.2ms
type checking 22.1ms
typeclass inference 59.1ms
real 2.52
user 1.53
sys 1.10
LeanPool/ClassicalGraphColouring/Galvin/Orientation.lean
import took 1.39s
cumulative profiling times:
attribute application 0.199ms
congr simp thm 3.69ms
elaboration 91.5ms
fix level params 2.61ms
import 1.39s
initialization 30.5ms
instantiate metavars 4.17ms
interpretation 384ms
let-to-have transformation 0.279ms
linting 32.1ms
module linting 0.00158ms
overlappingInstancesLinter 11.8ms
parsing 18.6ms
process pre-definitions 11.9ms
share common exprs 6.62ms
simp 154ms
tactic execution 223ms
tacticAnalysis 58.4ms
type checking 116ms
typeclass inference 373ms
real 2.82
user 2.49
sys 1.12
LeanPool/ClassicalGraphColouring/Imports.lean
import took 1.41s
cumulative profiling times:
elaboration 0.0813ms
import 1.41s
initialization 33.4ms
interpretation 202ms
linting 0.269ms
module linting 0.00157ms
overlappingInstancesLinter 0.115ms
parsing 0.00181ms
tacticAnalysis 0.449ms
real 2.35
user 1.28
sys 1.11
LeanPool/ClassicalGraphColouring/Konig/Basic.lean
import took 728ms
cumulative profiling times:
attribute application 0.1ms
congr simp thm 4.92ms
elaboration 42.6ms
fix level params 2.07ms
import 728ms
initialization 30ms
instantiate metavars 3.11ms
interpretation 251ms
let-to-have transformation 0.119ms
linting 22.6ms
module linting 0.00178ms
overlappingInstancesLinter 5.73ms
parsing 15ms
process pre-definitions 8.05ms
share common exprs 4.54ms
simp 76.5ms
tactic execution 352ms
tacticAnalysis 52.7ms
type checking 163ms
typeclass inference 282ms
real 1.89
user 1.91
sys 0.80
LeanPool/ClassicalGraphColouring/Orientations/GallaiRoy.lean
import took 1.37s
cumulative profiling times:
attribute application 0.0996ms
congr simp thm 0.893ms
elaboration 38.1ms
fix level params 0.815ms
import 1.37s
initialization 29.3ms
instantiate metavars 1.37ms
interpretation 307ms
let-to-have transformation 0.0855ms
linting 16.6ms
module linting 0.00168ms
overlappingInstancesLinter 3.95ms
parsing 13.7ms
process pre-definitions 12.5ms
share common exprs 2.43ms
simp 31.7ms
tactic execution 98.1ms
tacticAnalysis 34.3ms
type checking 60.6ms
typeclass inference 135ms
real 2.45
user 1.78
sys 1.10
LeanPool/ClassicalGraphColouring/Spectrum/Bounds.lean
import took 1.42s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 238ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 114ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 321ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 395ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 463ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 358ms
cumulative profiling times:
attribute application 0.186ms
congr simp thm 17.2ms
elaboration 142ms
fix level params 5.41ms
import 1.42s
initialization 35.2ms
instantiate metavars 9.02ms
interpretation 2.72s
let-to-have transformation 0.359ms
linting 50.4ms
module linting 0.00188ms
norm_num 52.7ms
overlappingInstancesLinter 12ms
parsing 24.1ms
process pre-definitions 29.1ms
ring 81.1ms
share common exprs 27ms
simp 721ms
tactic execution 567ms
tacticAnalysis 111ms
type checking 178ms
typeclass inference 1.66s
real 5.52
user 7.34
sys 1.18
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"overall_verdict": "approve",
"reviewed_head": "28b74d8a8b6d4528c766f4ad4e529076c37e6b38",
"review_kind": "Independent complete-source content review; protected CI and configured review remain separate",
"coverage": "Read all nine Lean files and the complete project card at this head, including the three-file repair from ba44f806. Checked producer proofs, all 14 card statements, the existing Vizing and Digraph interfaces, and the frozen-source/provenance and nearest-library comparisons.",
"faithfulness": {
"verdict": "pass",
"bottom_line": "The 14 card statements are supported by the actual proofs, with the finite simple-graph specialization and positive-degree restriction disclosed.",
"proves_the_claim": "proves_it",
"claim_note": "The code proves bipartite Δ-edge/list colouring, finite stable matching and Dinitz, both orientation/path implications, the five spectral bounds and two interface corollaries.",
"assumed_inputs": "Bipartiteness, finite vertex sets, strict injective preference rankings, and the stated edge/nonempty/positive regular-degree conditions. The Hermitian adjacency-matrix argument is an exposed matrix-symmetry hypothesis, not an assumed spectral bound. The kernel, Kempe extension and spectral hard steps are constructed in the development.",
"findings": []
},
"novelty": {
"verdict": "pass",
"bottom_line": "The checked existing contracts do not subsume these headline results.",
"already_formalized": "",
"novelty_note": "The existing Vizing development supplies Δ+1 edge colouring; this adds the bipartite Δ and arbitrary-list existence proofs. Checked Mathlib graph-colouring/adjacency/spectral APIs and pinned Tau Ceti acyclic-path, path-graph and finite graph-interval declarations are prerequisites or different contracts, not these headlines. Existing matching/poset/equitable developments are not copied. Broader semantic novelty outside these bounded comparisons remains unverifiable.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "A completed collection of named graph-colouring theorems with reusable matching, kernel, orientation and spectral infrastructure is a good pool fit.",
"fit": "good_fit",
"level": "graduate",
"branch": "graph colouring and spectral graph theory",
"mode": "theory_building",
"significance_one_sentence": "The collection joins König/Galvin/Dinitz, Gallai–Hasse–Roy–Vitaver, and Wilf/Hoffman through substantive proofs rather than isolated utility corollaries.",
"findings": []
},
"sources": {
"verdict": "pass",
"bottom_line": "The four frozen upstream developments are credited, and the multigraph paper is explicitly labelled as a finite simple-graph specialization.",
"source_match": "matches",
"findings": [],
"verification_limits": "Frozen proof producers, Apache-2.0 licences and disclosed AI provenance are authenticated. Galvin's publisher abstract confirms the multigraph theorem; Roy's original scan confirms both orientation/path directions. Gale–Shapley and Wilf publisher metadata were checked. Complete Gale–Shapley/Wilf/Hoffman/Collatz–Sinogowitz original statements, other historical orientation papers, registry pages and exhaustive priority remain unverifiable.",
"primary_source_checks": [
{
"topic": "Galvin 1995",
"url": "https://www.sciencedirect.com/science/article/pii/S0095895685710118",
"scope": "Publisher abstract; finite simple-graph specialization disclosed"
},
{
"topic": "Roy 1967",
"url": "https://www.numdam.org/article/M2AN_1967__1_5_129_0.pdf",
"scope": "Original scan, Theorems 1–2; paths count vertices"
},
{
"topic": "Gale–Shapley 1962",
"url": "https://www.tandfonline.com/doi/abs/10.1080/00029890.1962.11989827",
"scope": "Publisher bibliographic identity"
},
{
"topic": "Wilf 1967",
"url": "https://londmathsoc.onlinelibrary.wiley.com/doi/10.1112/jlms/s1-42.1.330",
"scope": "Publisher bibliographic identity"
}
]
},
"quality": {
"verdict": "pass",
"bottom_line": "Competent modular proofs with consumers for the stable-matching, kernel, Kempe and Rayleigh infrastructure; the three concrete advisory findings have been repaired.",
"code_quality": 3,
"findings": []
},
"advisory_reconciliation": [
"The Hoffman ratio card now requires positive degree, matching hk : 1 ≤ k.",
"GallaiRoy.isDirectedPath_iff_isSimplePath connects the relation predicate to the existing Digraph API.",
"The converse orientation theorem no longer advertises acyclicity in its exported conclusion."
],
"trust_and_validation": "Static full-source inspection found ordinary closed proofs and no hidden structure field asserting a headline. This source verdict does not claim that the live authored CI, canonical required contexts or environment/axiom audit have completed.",
"merge_eligibility": "Source recommendation approved at the recorded head. Wait for successful applicable authored validation, matching configured review, fresh current-main qualification and normal native queue protections. Do not transfer results from cancelled ba44 CI.",
"performance": "The updated advisory proof-profile comment reports 29.20 s for the changed-module build and 201,501 maxHeartbeats units across the current 1,410 Lean lines. These are published hosted measurements, not an independently reproduced benchmark or a protected-CI pass."
}
The unused-argument linter identified this instance as unused. Keep the theorem conclusion and proof unchanged while permitting the empty vertex type.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"overall_verdict": "approve",
"reviewed_head": "cc25bccb916257b3494debf51bd5212255bc4173",
"review_kind": "Exact-child source delta review after the unused-argument lint repair; prior complete source review retained through an exact tree join",
"coverage": "The complete nine-Lean-file/project-card source review at 28b74d8a remains the baseline (review 5571013338). The child commit removes exactly one unused [Nonempty V] binder from exists_orientation_of_wilf_bound; all proof and conclusion bytes and all other source paths are preserved. The one-line change received independent delta review.",
"faithfulness": {
"verdict": "pass",
"bottom_line": "The 14 card statements are supported by the actual proofs, with the finite simple-graph specialization and positive-degree restriction disclosed.",
"proves_the_claim": "proves_it",
"claim_note": "The code proves bipartite Δ-edge/list colouring, finite stable matching and Dinitz, both orientation/path implications, the five spectral bounds and two interface corollaries.",
"assumed_inputs": "The unchanged hypotheses documented in the baseline review apply. The Wilf-to-orientation corollary now also permits an empty vertex type: its existing producer proofs do not require Nonempty V. The Hoffman corollary retains its Nonempty V hypothesis.",
"findings": []
},
"novelty": {
"verdict": "pass",
"bottom_line": "The checked existing contracts do not subsume these headline results.",
"already_formalized": "",
"novelty_note": "The existing Vizing development supplies Δ+1 edge colouring; this adds the bipartite Δ and arbitrary-list existence proofs. Checked Mathlib graph-colouring/adjacency/spectral APIs and pinned Tau Ceti acyclic-path, path-graph and finite graph-interval declarations are prerequisites or different contracts, not these headlines. Existing matching/poset/equitable developments are not copied. Broader semantic novelty outside these bounded comparisons remains unverifiable.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "A completed collection of named graph-colouring theorems with reusable matching, kernel, orientation and spectral infrastructure is a good pool fit.",
"fit": "good_fit",
"level": "graduate",
"branch": "graph colouring and spectral graph theory",
"mode": "theory_building",
"significance_one_sentence": "The collection joins König/Galvin/Dinitz, Gallai–Hasse–Roy–Vitaver, and Wilf/Hoffman through substantive proofs rather than isolated utility corollaries.",
"findings": []
},
"sources": {
"verdict": "pass",
"bottom_line": "The four frozen upstream developments are credited, and the multigraph paper is explicitly labelled as a finite simple-graph specialization.",
"source_match": "matches",
"findings": [],
"verification_limits": "Frozen proof producers, Apache-2.0 licences and disclosed AI provenance are authenticated. Galvin's publisher abstract confirms the multigraph theorem; Roy's original scan confirms both orientation/path directions. Gale–Shapley and Wilf publisher metadata were checked. Complete Gale–Shapley/Wilf/Hoffman/Collatz–Sinogowitz original statements, other historical orientation papers, registry pages and exhaustive priority remain unverifiable.",
"primary_source_checks": [
{
"topic": "Galvin 1995",
"url": "https://www.sciencedirect.com/science/article/pii/S0095895685710118",
"scope": "Publisher abstract; finite simple-graph specialization disclosed"
},
{
"topic": "Roy 1967",
"url": "https://www.numdam.org/article/M2AN_1967__1_5_129_0.pdf",
"scope": "Original scan, Theorems 1–2; paths count vertices"
},
{
"topic": "Gale–Shapley 1962",
"url": "https://www.tandfonline.com/doi/abs/10.1080/00029890.1962.11989827",
"scope": "Publisher bibliographic identity"
},
{
"topic": "Wilf 1967",
"url": "https://londmathsoc.onlinelibrary.wiley.com/doi/10.1112/jlms/s1-42.1.330",
"scope": "Publisher bibliographic identity"
}
]
},
"quality": {
"verdict": "pass",
"bottom_line": "The source remains modular; the only hosted lint failure was an unused instance in the Wilf interface corollary and has been removed without suppressing a linter.",
"code_quality": 3,
"findings": []
},
"advisory_reconciliation": [
"The Hoffman ratio card now requires positive degree, matching hk : 1 ≤ k.",
"GallaiRoy.isDirectedPath_iff_isSimplePath connects the relation predicate to the existing Digraph API.",
"The converse orientation theorem no longer advertises acyclicity in its exported conclusion.",
"Actual authored job118035442806 passed compilation and index checks, then failed unused-argument lint at ClassicalGraphColouring.lean:55. This commit removes that binder; no proof, theorem conclusion, workflow or gate changes."
],
"trust_and_validation": "Source acceptance is for the recorded child commit after verifying the exact repair and unchanged source-tree entries. Old-head compilation/index passed, but old-head lint failed; text style and repository quality were skipped. Those results are not a CI pass at this new head. Fresh applicable authored CI, configured review and protected queue validation remain required.",
"merge_eligibility": "Source recommendation approved at this exact head. Current-main9fa7 still awaits its proper applicable own PUSH validation. Preserve the infrastructure priority hold until qualified, then require matching authored checks, configured review and normal native queue protections. No queue entry or auto-merge was enabled.",
"performance": "The prior28b advisory profile remains historical scoped evidence only. No new benchmark or current-head protected pass is claimed."
}Generate the entry card from the existing project YAML and preserve the mathematical overview separately.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Source review for dd5a81836cbe5757471fdab67eb4f087b73974c4: the generated project card now matches the unchanged YAML. The mathematical overview is preserved as a separate module docstring.
I compared the complete published delta against cc25bccb916257b3494debf51bd5212255bc4173: only this entry file’s module comments changed. Copyright, imports, theorem statements, assumptions and proof bodies are unchanged; the other nine PR files, including the YAML card, are unchanged. The exact current card checker rejects the previous card and accepts this one.
The complete mathematical/provenance review and the inspected unused-instance repair remain accepted through this explicit comment-only delta: faithfulness, novelty, significance and sources PASS; code quality PASS with advisory score 3/5. No new source finding.
Fresh exact-head CI, the matching configured review, current-main qualification and normal protected queue checks remain required. The previous head’s quality failure is not treated as a pass.
The current advisory reports no new actionable issue. Its source/license/novelty verification limits remain covered by the retained independent review; compile-cost profiling remains advisory.
Use a compact representative declaration/tag list for the generated card. Preserve all fourteen detailed main results, the complete mathematical overview, and every theorem, proof, import and gate.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Source review at baed8b105bd5fe72c50bb5f0962ade93a7d8a58b: the canonical-card regeneration introduced two overlong metadata lines, which caused the warning-free build gate to reject the previous head. This child fixes those lines through the project card data and regenerates the matching entry comment.
The compact card now selects Galvin and Hoffman as representative declarations and uses a shorter tag list. König, Gallai–Roy and the other results remain in the complete fourteen-result metadata and their original modules. All fourteen detailed contracts, mathematical overview, imports, theorem statements and proof bodies are unchanged. The exact published comparison contains only the YAML and generated comment changes.
The current card renderer/checker accepts the regenerated card; the changed lines are 70 and 87 characters. Its list-driven declaration-presence check now targets the two selected representatives rather than four. The repository-wide every-declaration axiom/environment audit is unchanged. No checker, renderer, workflow, option, waiver or proof was modified.
The retained complete mathematical/provenance review remains accepted through this inspected metadata-only delta: faithfulness, novelty, significance, sources and code quality PASS; advisory quality 3/5, no new mathematical finding.
Source recommendation approved at this exact head. Fresh authored CI, the matching configured review and normal protected queue validation remain required. The previous build-step failure and its skipped lint/style/quality stages are not transferred as successful checks.
|
/review Please run the configured five-rubric review for exact head |
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
All 14 card headlines match the Lean; full CI remains pending, and no local rebuild was run because dependencies are absent. |
| Novelty | ✅ pass |
No duplicate headline was established in the pinned Mathlib or pool; the broader Tau Ceti comparison remains unverifiable beyond the inspected declarations. |
| Significance | ✅ pass |
The proved Galvin, Gallai–Roy and Hoffman theorems make this a substantial graduate-level graph-colouring development. |
| Sources | ✅ pass |
No source inconsistency found: Haemers’s Theorem 1 supports the ratio bound and the upstream Lean developments are credited, though some historical full texts remain unverifiable. |
| Code quality (advisory) | ✅ pass |
The proofs use focused helpers and existing graph infrastructure, with no material maintenance issues found; full CI remains pending. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | The card discloses the substantive bipartiteness, strict-preference, list-size, path-bound, colouring, edge-existence and positive-degree hypotheses; spectral declarations additionally receive a Hermitian witness for the real adjacency matrix and require nonempty vertices where needed. Stable matchings, kernels and spectral inequalities are proved rather than postulated. |
| Matches cited source | 🟡 unverifiable |
| Fit | ✅ good_fit |
| Level | graduate |
| Branch | graph theory |
| Mode | theory_building |
| Code quality | 3 / 5 |
Statement check: The results concern finite simple graphs and finite matching/array instances, count directed paths by vertices, and restrict Hoffman's ratio bound to positive regular degree.
The development derives bipartite list edge colouring and Dinitz's theorem through stable matchings and kernels, and establishes the Gallai–Hasse–Roy–Vitaver characterization alongside Wilf and Hoffman spectral bounds.
Tokens: 5,936,841 in / 33,433 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $24.2489 (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.
Point the independent-set ratio result to Haemers2021 Theorem1. Keep Hoffman's1970 reference for the chromatic bound and preserve all theorem statements, proofs and other project metadata.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"review_kind": "Exact-head citation-only source-delta review",
"reviewed_commit": "9866b02d9e00445c9ea4816f92fa8a289a90fef9",
"summary": "Corrected the independent-set ratio-bound citation, which the earlier card review missed.",
"verdict": "approve",
"citation": "Haemers (2021), Theorem 1 states Hoffman's ratio bound for regular graphs. The Lean positive-degree inequality for every independent set matches that nondegenerate form. Hoffman's 1970 reference remains attached to the distinct chromatic bound.",
"verification_scope": "The child of baed changes only main_results[11].source_ref in the project YAML. Parsed comparison preserves all fourteen result contracts and every other metadata value. Full published-blob readback and the one-file commit comparison preserve all Lean source, proofs, imports, generated entry and gates. Independent schema/rendering verification confirms no index or entry regeneration is needed.",
"prior_assessment": "Retain the prior complete mathematical/provenance/significance/novelty assessment through this inspected citation-only child. Configured2222's Sources block was valid at baed and is addressed here; its historical verdict is not relabeled.",
"assessment": {
"maintainability": "improved",
"brittleness": "unchanged",
"risk": "low",
"introduces_tech_debt": false
},
"findings": [],
"validation_scope": "This source acceptance does not transfer baed's successful CI or configured review to this new head. Its applicable checks and matching configured review must pass independently. Current main remains unqualified, so the infrastructure hold remains and no queue admission or automatic merge is enabled."
}
|
/review Current head: |
2 participants
Contribution
Add a classical graph-colouring collection linking three complementary proof methods:
Two short corollaries connect the orientation and spectral results. The collection contains 14 documented results across four previously registered Palomar sources (K19, K29, 000015 and K16). It imports Lean Pool's existing Vizing infrastructure directly. Matching-cover, Dilworth/Mirsky, and equitable-colouring material already in the pool is not copied.
Validation
lake build LeanPool.ClassicalGraphColouring.Importspasses on Lean 4.35.0-rc3 and the repository's pinned Mathlib.git diff --checkpasses.#print axiomsfor the principal results and both interface corollaries reports onlypropext,Classical.choice, andQuot.sound.The full repository index and lint gates will run in CI. Local full-repository quality checks are not meaningful in this sparse worktree.