feat(Combinatorics/SimpleGraph/LapMatrix): bound Laplacian eigenvalues by `|V|` by hasjack · Pull Request #43953 · leanprover-community/mathlib4

hasjack · 2026-09-18T21:20:50Z

Prove that every Laplacian eigenvalue of a finite simple graph is at most
the number of vertices, via comparison of the Rayleigh quotient with the
complete graph. Also record the underlying quadratic-form bound
xᵀ L x ≤ |V| · ‖x‖².

Adds dotProduct_mulVec_lapMatrix_le_card and eigenvalues_lapMatrix_le_card
in LapMatrix.lean only. The claim is the uniform bound λ ≤ |V| for every
indexed eigenvalue; it does not assert |V| ∈ spectrum for every graph.
Searched existing LapMatrix API (PSD, zero_mem_spectrum_lapMatrix,
lapMatrix_top) and did not find a card upper bound under another name.
Happy to rename if a preferred lemma already exists.

…s by |V| Prove that every eigenvalue of the Laplacian of a finite simple graph is at most the number of vertices, via complete-graph comparison of the Rayleigh quotient. Also record the underlying quadratic-form bound.

github-actions · 2026-09-18T21:21:39Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to Zulip and join the Lean community.
Thank you again for joining our community.

github-actions · 2026-09-18T21:22:29Z

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

github-actions · 2026-09-18T21:23:13Z

PR summary 5945e6f8cd

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

+ dotProduct_mulVec_lapMatrix_le_card
+ eigenvalues_lapMatrix_le_card
+ lapMatrix_toLinearMap₂'_mono

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 5945e6f).

+3 new declarations
−0 removed declarations

+SimpleGraph.dotProduct_mulVec_lapMatrix_le_card
+SimpleGraph.eigenvalues_lapMatrix_le_card
+SimpleGraph.lapMatrix_toLinearMap₂'_mono

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 5945e6f8cd
Reference commit b1007d8abf

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Prove the eigenvalue card bound via HasEigenvalue/Rayleigh using only APIs already imported by LapMatrix, avoiding Analysis.Matrix.Spectrum (+599 transitive imports) and PiL2.

SnirBroshi · 2026-09-18T21:42:23Z

Welcome!
Could you try generalizing beyond Reals? What assumptions of the real numbers are you using?
Also could you please comment on if and how you're using LLMs for this PR?

…ld bounds Extract `lapMatrix_toLinearMap₂'_mono` for `G ≤ H`, rewrite the card bound via `le_top`, and state the quadratic-form / eigenvalue inequalities over a linearly ordered field (same style as `posSemidef_lapMatrix`).

…emma Inline the Rayleigh argument into `eigenvalues_lapMatrix_le_card` and delete `eigenvalue_lapMatrix_le_card`, keeping a single HasEigenvalue API. Deletions: - SimpleGraph.eigenvalue_lapMatrix_le_card

…card bound Apply Snir review suggestions: binder/simp/zero_le_two/Fintype.card notation, and replace the mono+complete-graph calc with a one-line grw.

Apply remaining Snir suggestion: `dotProduct_mulVec_lapMatrix_le_card G x`.

… G on hquad G is a section variable, so `dotProduct_mulVec_lapMatrix_le_card G x` mis-applies G as a Type argument. Call with `(R := R) x` instead.

Elaboration expects explicit G after R; Snir's `G x` needs `(R := R)` first so G is not consumed as a Type.

hasjack · 2026-09-18T23:57:01Z

-awaiting-author

SnirBroshi · 2026-09-19T00:05:40Z

Could you please comment on LLM-use as I've asked above? Thanks!

hasjack · 2026-09-19T00:16:03Z

Could you please comment on LLM-use as I've asked above? Thanks!

I used an LLM (Grok) to check whether LapMatrix.lean already had a card bound (it did not) and to sketch the complete-graph / Rayleigh argument. I wrote and compiled the Lean in this file myself, including the ordered-field change, the G ≤ H lemma, dropping the extra eigenpair spelling, and the (R := R) G x binder fix.

R and G are explicit section variables; matches lapMatrix_toLinearMap₂' R G x.

Keep only eigenvalues_lapMatrix_le_card as a new main result; mono and form bound stay as lemmas but drop out of the module header.

Restructure dotProduct_mulVec_lapMatrix_le_card and eigenvalues_lapMatrix_le_card with backwards reasoning so the mono / Rayleigh steps land as goals instead of textbook haves.

Form bound via convert/simp; eigenvalues via term-mode hxpos then rw + exact. Drops nested have/show scaffolding.

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

SnirBroshi · 2026-09-19T13:20:20Z

@Parcly-Taxel Why LLM-generated? They said

I wrote and compiled the Lean in this file myself

hasjack · 2026-09-19T21:38:47Z

-awaiting-author

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Sep 18, 2026

github-actions Bot added t-combinatorics Combinatorics large-import Automatically added label for PRs with a significant increase in transitive imports labels Sep 18, 2026

hasjack changed the title ~~feat(Combinatorics/SimpleGraph/LapMatrix): bound Laplacian eigenvalues by |V|~~ feat(Combinatorics/SimpleGraph/LapMatrix): bound Laplacian eigenvalues by |V| Sep 18, 2026

feat(Combinatorics/SimpleGraph/LapMatrix): drop Spectrum/PiL2 imports

a5d9fc1

Prove the eigenvalue card bound via HasEigenvalue/Rayleigh using only APIs already imported by LapMatrix, avoiding Analysis.Matrix.Spectrum (+599 transitive imports) and PiL2.

github-actions Bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Sep 18, 2026

SnirBroshi reviewed Sep 18, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean Outdated

SnirBroshi reviewed Sep 18, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean Outdated

SnirBroshi added the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Sep 18, 2026

hasjack added 2 commits September 18, 2026 21:50

feat(Combinatorics/SimpleGraph/LapMatrix): drop redundant eigenpair l…

4433fc5

…emma Inline the Rayleigh argument into `eigenvalues_lapMatrix_le_card` and delete `eigenvalue_lapMatrix_le_card`, keeping a single HasEigenvalue API. Deletions: - SimpleGraph.eigenvalue_lapMatrix_le_card

SnirBroshi reviewed Sep 18, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean Outdated

hasjack added 4 commits September 18, 2026 22:56

feat(Combinatorics/SimpleGraph/LapMatrix): style cleanup and grw for …

368fd2c

…card bound Apply Snir review suggestions: binder/simp/zero_le_two/Fintype.card notation, and replace the mono+complete-graph calc with a one-line grw.

style(Combinatorics/SimpleGraph/LapMatrix): drop explicit R on hquad

686254a

Apply remaining Snir suggestion: `dotProduct_mulVec_lapMatrix_le_card G x`.

fix(Combinatorics/SimpleGraph/LapMatrix): restore R and drop spurious…

0b7e9a3

… G on hquad G is a section variable, so `dotProduct_mulVec_lapMatrix_le_card G x` mis-applies G as a Type argument. Call with `(R := R) x` instead.

fix(Combinatorics/SimpleGraph/LapMatrix): pass G after (R := R) on hquad

a5148ae

Elaboration expects explicit G after R; Snir's `G x` needs `(R := R)` first so G is not consumed as a Type.

github-actions Bot removed the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Sep 18, 2026

SnirBroshi added the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Sep 19, 2026

SnirBroshi reviewed Sep 19, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean Outdated

hasjack added 2 commits September 19, 2026 00:23

fix(Combinatorics/SimpleGraph/LapMatrix): call card bound as R G x

3fcc8e9

R and G are explicit section variables; matches lapMatrix_toLinearMap₂' R G x.

docs(Combinatorics/SimpleGraph/LapMatrix): slim Main definitions list

a770edd

Keep only eigenvalues_lapMatrix_le_card as a new main result; mono and form bound stay as lemmas but drop out of the module header.

hasjack added 2 commits September 19, 2026 01:11

refactor(Combinatorics/SimpleGraph/LapMatrix): goal-first card bounds

be3535b

Restructure dotProduct_mulVec_lapMatrix_le_card and eigenvalues_lapMatrix_le_card with backwards reasoning so the mono / Rayleigh steps land as goals instead of textbook haves.

refactor(Combinatorics/SimpleGraph/LapMatrix): one by per card bound

4964c73

Form bound via convert/simp; eigenvalues via term-mode hxpos then rw + exact. Drops nested have/show scaffolding.

SnirBroshi reviewed Sep 19, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean Outdated

Update Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

07766ce

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

SnirBroshi reviewed Sep 19, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean Outdated

SnirBroshi reviewed Sep 19, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean Outdated

Update Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

918f85f

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

SnirBroshi reviewed Sep 19, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean Outdated

SnirBroshi reviewed Sep 19, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean Outdated

hasjack and others added 2 commits September 19, 2026 03:15

Update Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

684ed54

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

Update Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

31b5142

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

SnirBroshi reviewed Sep 19, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

SnirBroshi reviewed Sep 19, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean Outdated

Update Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

a6c244b

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

SnirBroshi reviewed Sep 19, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean Outdated

SnirBroshi reviewed Sep 19, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean Outdated

hasjack and others added 2 commits September 19, 2026 03:36

Update Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

b76037d

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

Update Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

a098818

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

SnirBroshi reviewed Sep 19, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean Outdated

Update Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

5655d23

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

SnirBroshi changed the title ~~feat(Combinatorics/SimpleGraph/LapMatrix): bound Laplacian eigenvalues by |V|~~ feat(Combinatorics/SimpleGraph/LapMatrix): bound Laplacian eigenvalues by |V| Sep 19, 2026

Parcly-Taxel added the LLM-generated PRs with substantial input from LLMs - review accordingly label Sep 19, 2026

SnirBroshi added awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. and removed LLM-generated PRs with substantial input from LLMs - review accordingly labels Sep 19, 2026

Jack Pickett added 2 commits September 19, 2026 21:15

style: drop explicit binders on lapMatrix mono grw

7b5696a

Merge branch 'master' into feat/eigenvalues-lapMatrix-le-card

024bc1e

github-actions Bot removed the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Sep 19, 2026

Merge branch 'master' into feat/eigenvalues-lapMatrix-le-card

5945e6f

Conversation

hasjack commented Sep 18, 2026 • edited by SnirBroshi Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Sep 18, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented Sep 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

✅ PR Title Formatted Correctly

Uh oh!

github-actions Bot commented Sep 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 5945e6f8cd

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

SnirBroshi commented Sep 18, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

hasjack commented Sep 18, 2026

Uh oh!

SnirBroshi commented Sep 19, 2026

Uh oh!

Uh oh!

hasjack commented Sep 19, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

SnirBroshi commented Sep 19, 2026

Uh oh!

hasjack commented Sep 19, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

hasjack commented Sep 18, 2026 •

edited by SnirBroshi

Loading

github-actions Bot commented Sep 18, 2026 •

edited

Loading

github-actions Bot commented Sep 18, 2026 •

edited

Loading