From 23321c3565517a371761eec79d50c335e32aaea4 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Fri, 2 Oct 2026 16:22:38 +0000 Subject: [PATCH] =?UTF-8?q?Cite=20Alexandersson=E2=80=93Leite=20for=20the?= =?UTF-8?q?=20orientation=20and=20minima=20pages?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- RealRooted/Challenges/ChordalClawFreeAcyclicSinks.lean | 4 ++++ RealRooted/Challenges/ClawFreeOrientationSinks.lean | 4 ++++ RealRooted/Challenges/MinimaPolynomial.lean | 4 ++++ RealRooted/Challenges/UnitIntervalAcyclicSinks.lean | 4 ++++ 4 files changed, 16 insertions(+) diff --git a/RealRooted/Challenges/ChordalClawFreeAcyclicSinks.lean b/RealRooted/Challenges/ChordalClawFreeAcyclicSinks.lean index cd0fd1326..d1d0d1d44 100644 --- a/RealRooted/Challenges/ChordalClawFreeAcyclicSinks.lean +++ b/RealRooted/Challenges/ChordalClawFreeAcyclicSinks.lean @@ -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" @@ -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–Seymour](/RealRooted/theorems/chudnovsky-seymour/) and diff --git a/RealRooted/Challenges/ClawFreeOrientationSinks.lean b/RealRooted/Challenges/ClawFreeOrientationSinks.lean index fd8cd95c2..0c8297c90 100644 --- a/RealRooted/Challenges/ClawFreeOrientationSinks.lean +++ b/RealRooted/Challenges/ClawFreeOrientationSinks.lean @@ -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" @@ -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–Seymour](/RealRooted/theorems/chudnovsky-seymour/) and diff --git a/RealRooted/Challenges/MinimaPolynomial.lean b/RealRooted/Challenges/MinimaPolynomial.lean index 902afc8ee..6499da6f2 100644 --- a/RealRooted/Challenges/MinimaPolynomial.lean +++ b/RealRooted/Challenges/MinimaPolynomial.lean @@ -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" @@ -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). diff --git a/RealRooted/Challenges/UnitIntervalAcyclicSinks.lean b/RealRooted/Challenges/UnitIntervalAcyclicSinks.lean index 94dd2ae3a..0a728c0b3 100644 --- a/RealRooted/Challenges/UnitIntervalAcyclicSinks.lean +++ b/RealRooted/Challenges/UnitIntervalAcyclicSinks.lean @@ -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" @@ -64,6 +66,8 @@ weighted form of the [Chudnovsky–Seymour 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–Seymour](/RealRooted/theorems/chudnovsky-seymour/) and