Skip to content

Cite Alexandersson鈥揕eite for the orientation and minima pages #1103

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We鈥檒l occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
PerAlexandersson wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Cite Alexandersson鈥揕eite for the orientation and minima pages #1103

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions RealRooted/Challenges/ChordalClawFreeAcyclicSinks.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@ import RealRooted.Graph.ChordalAcyclicSink
version = 1
section = "families"
slug = "chordal-claw-free-acyclic-sinks"
authors = ["Alexandersson", "Leite"]
years = [2026]

[[definitions]]
name = "RealRooted.Graph.ordinaryAcyclicSinkPolynomial"
Expand Down Expand Up @@ -63,6 +65,8 @@ For the refined polynomial of natural unit interval graphs, see

## References

P. Alexandersson and L. Saud Maia Leite, unpublished manuscript (2026).

The theorem was formalized in RealRooted issue #677. For the claw-free
background, see the
[Chudnovsky鈥揝eymour](/RealRooted/theorems/chudnovsky-seymour/) and
Expand Down
4 changes: 4 additions & 0 deletions RealRooted/Challenges/ClawFreeOrientationSinks.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@ import RealRooted.Graph.AllOrientationSinkIdentity
version = 1
section = "families"
slug = "claw-free-orientation-sinks"
authors = ["Alexandersson", "Leite"]
years = [2026]

[[definitions]]
name = "RealRooted.Graph.allOrientationSinkPolynomial"
Expand Down Expand Up @@ -60,6 +62,8 @@ For acyclic orientations, see the pages on

## References

P. Alexandersson and L. Saud Maia Leite, unpublished manuscript (2026).

The counting identity was proved with Aristotle (Harmonic). For the claw-free
background, see the
[Chudnovsky鈥揝eymour](/RealRooted/theorems/chudnovsky-seymour/) and
Expand Down
4 changes: 4 additions & 0 deletions RealRooted/Challenges/MinimaPolynomial.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@ import RealRooted.Graph.MinimaForest
version = 1
section = "families"
slug = "minima-polynomial"
authors = ["Alexandersson", "Leite"]
years = [2026]

[[definitions]]
name = "RealRooted.Graph.LocalOrder"
Expand Down Expand Up @@ -86,6 +88,8 @@ For sinks of acyclic orientations, see the pages on

## References

P. Alexandersson and L. Saud Maia Leite, unpublished manuscript (2026).

The counting identity was proved with Aristotle (Harmonic).
<!-- /realrooted-catalog-content -->

Expand Down
4 changes: 4 additions & 0 deletions RealRooted/Challenges/UnitIntervalAcyclicSinks.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@ import RealRooted.UnitIntervalGraph.AcyclicSink
version = 1
section = "families"
slug = "unit-interval-acyclic-sinks"
authors = ["Alexandersson", "Leite"]
years = [2026]

[[definitions]]
name = "RealRooted.UnitIntervalGraph.Data"
Expand Down Expand Up @@ -64,6 +66,8 @@ weighted form of the [Chudnovsky鈥揝eymour theorem](/RealRooted/theorems/chudnov

## References

P. Alexandersson and L. Saud Maia Leite, unpublished manuscript (2026).

The orientation theorem was formalized in RealRooted issue #639. For the
claw-free background, see the
[Chudnovsky鈥揝eymour](/RealRooted/theorems/chudnovsky-seymour/) and
Expand Down
Loading