feat: Add structural analysis for Erdős-Gyárfás conjecture

inprogress/31-Erdos-Gyarfas/31-Erdos-Gyarfas-FR.tex

@@ -0,0 +1,90 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[utf8]{inputenc}
+\usepackage[french]{babel}
+\usepackage{amsmath, amssymb, amsthm}
+\usepackage{geometry}
+\geometry{margin=1in}
+
+\title{Analyse Structurale et Stratégie de Preuve Constructive de la Conjecture d'Erd\H{o}s-Gy\'{a}rf\'{a}s}
+\author{Charles EDOU NZE\thanks{Charles EDOU NZE, chercheur indépendant}}
+\date{}
+
+\newtheorem{theorem}{Théorème}[section]
+\newtheorem{lemma}[theorem]{Lemme}
+\newtheorem{definition}[theorem]{Définition}
+\newtheorem{conjecture}[theorem]{Conjecture}
+
+\begin{document}
+\maketitle
+
+\begin{abstract}
+Ce document présente une formulation axiomatique, une revue de la littérature et une architecture de preuve structurée pour la conjecture d'Erd\H{o}s-Gy\'{a}rf\'{a}s en théorie des graphes. La conjecture stipule que tout graphe dont le degré minimum est d'au moins 3 contient un cycle dont la longueur est une puissance de 2. Nous décomposons le problème en plusieurs lemmes intermédiaires et fournissons une architecture adaptée à la vérification formelle dans Lean 4.
+\end{abstract}
+
+\section{Introduction et Définitions Axiomatiques}
+La conjecture d'Erd\H{o}s-Gy\'{a}rf\'{a}s est un problème ouvert fondamental en théorie des graphes extrémaux. Soit $G = (V, E)$ un graphe simple, fini et non orienté. Soit $\delta(G)$ le degré minimum des sommets dans $G$.
+
+\begin{definition}[Graphe et Degré Minimum]
+Soit $V$ un ensemble fini et $E \subseteq \binom{V}{2}$ l'ensemble des arêtes. Le degré minimum est défini par :
+\[
+\delta(G) = \min_{v \in V} \deg(v)
+\]
+où $\deg(v) = |\{u \in V \mid \{u, v\} \in E\}|$.
+\end{definition}
+
+\begin{conjecture}[Erd\H{o}s-Gy\'{a}rf\'{a}s, 1995]
+Si $G = (V, E)$ est un graphe avec $\delta(G) \ge 3$, alors $G$ contient un cycle $C_k$ de longueur $k$ tel que $k = 2^m$ pour un certain entier $m \ge 1$.
+\end{conjecture}
+
+\section{Littérature Contextuelle et Analogies}
+Le problème se situe à l'intersection de la théorie des graphes extrémaux et de la combinatoire additive. Il est structurellement similaire aux questions concernant l'existence de longueurs de cycles spécifiques dans les graphes denses (par exemple, les théorèmes de Bondy et Simonovits sur les cycles de longueur paire).
+
+Nous dressons une analogie avec la preuve de l'existence de cycles pairs dans des graphes de densité suffisante, où l'on construit typiquement un chemin maximal et étudie le voisinage de ses extrémités. Ici, nous cherchons à affiner le processus de construction du chemin en exploitant la condition sur le degré pour forcer des cycles de longueurs spécifiques.
+
+\section{Stratégie de Preuve et Lemmes}
+
+Nous décomposons la conjecture en sous-problèmes structurés.
+
+\begin{lemma}[Voisinage du Chemin Maximal]
+\label{lem:longest_path}
+Soit $P = v_1 v_2 \dots v_l$ un chemin maximal dans un graphe $G$ avec $\delta(G) \ge 3$. Alors tous les voisins de $v_1$ doivent se trouver sur $P$.
+\end{lemma}
+
+\begin{proof}
+Supposons qu'il existe un voisin $u$ de $v_1$ tel que $u \notin V(P)$. Alors le chemin $u v_1 v_2 \dots v_l$ a une longueur $l+1$, contredisant l'hypothèse selon laquelle $P$ est un chemin maximal. Ainsi, $N(v_1) \subseteq V(P)$.
+\end{proof}
+
+\begin{lemma}[Formation de Cycles]
+\label{lem:cycle_lengths}
+Soit $P = v_1 v_2 \dots v_l$ un chemin maximal dans $G$ avec $\delta(G) \ge 3$. Soient $v_{i_1}, v_{i_2}, \dots, v_{i_k}$ les voisins de $v_1$ sur $P$, ordonnés tels que $2 = i_1 < i_2 < \dots < i_k \le l$. Puisque $\delta(G) \ge 3$, $k \ge 3$. Les arêtes $\{v_1, v_{i_j}\}$ créent des cycles $C^{(j)}$ de longueur $i_j$.
+\end{lemma}
+
+\begin{proof}
+Le segment de chemin $v_1 \dots v_{i_j}$ a une longueur $i_j - 1$. L'ajout de l'arête $\{v_1, v_{i_j}\}$ complète un cycle de longueur $(i_j - 1) + 1 = i_j$.
+\end{proof}
+
+\section{Architecture de Formalisation Lean 4}
+Pour autoformaliser cette preuve, nous esquissons les structures Lean 4.
+
+\begin{verbatim}
+import Mathlib.Combinatorics.SimpleGraph.Basic
+import Mathlib.Combinatorics.SimpleGraph.Connectivity
+
+variable {V : Type*} [Fintype V] [DecidableEq V]
+variable (G : SimpleGraph V)
+
+def min_degree_at_least (k : \mathbb{N}) : Prop :=
+  \forall v : V, G.degree v \ge k
+
+def has_cycle_power_of_two : Prop :=
+  \exists (c : G.Walk v v), c.IsCycle \land \exists (m : \mathbb{N}), c.length = 2^m
+
+theorem erdos_gyarfas (h : min_degree_at_least G 3) :
+  has_cycle_power_of_two G := by
+  sorry
+\end{verbatim}
+
+\section{Conclusion}
+La décomposition structurelle fournie sert d'étape fondamentale vers la résolution de la conjecture d'Erd\H{o}s-Gy\'{a}rf\'{a}s, la préparant pour la vérification formelle.
+
+\end{document}

inprogress/31-Erdos-Gyarfas/31-Erdos-Gyarfas.tex

@@ -0,0 +1,89 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[utf8]{inputenc}
+\usepackage{amsmath, amssymb, amsthm}
+\usepackage{geometry}
+\geometry{margin=1in}
+
+\title{Structural Analysis and Constructive Proof Strategy for the Erd\H{o}s-Gy\'{a}rf\'{a}s Conjecture}
+\author{Charles EDOU NZE\thanks{Charles EDOU NZE, chercheur indépendant}}
+\date{}
+
+\newtheorem{theorem}{Theorem}[section]
+\newtheorem{lemma}[theorem]{Lemma}
+\newtheorem{definition}[theorem]{Definition}
+\newtheorem{conjecture}[theorem]{Conjecture}
+
+\begin{document}
+\maketitle
+
+\begin{abstract}
+This document presents an axiomatic formulation, literature review, and a structured proof architecture for the Erd\H{o}s-Gy\'{a}rf\'{a}s conjecture in graph theory. The conjecture states that every graph with minimum degree at least 3 contains a cycle whose length is a power of 2. We decompose the problem into several intermediate lemmata and provide an architecture suitable for formal verification in Lean 4.
+\end{abstract}
+
+\section{Introduction and Axiomatic Definitions}
+The Erd\H{o}s-Gy\'{a}rf\'{a}s conjecture is a fundamental open problem in extremal graph theory. Let $G = (V, E)$ be a simple, finite, undirected graph. Let $\delta(G)$ denote the minimum degree of the vertices in $G$.
+
+\begin{definition}[Graph and Minimum Degree]
+Let $V$ be a finite set and $E \subseteq \binom{V}{2}$ be the edge set. The minimum degree is defined as:
+\[
+\delta(G) = \min_{v \in V} \deg(v)
+\]
+where $\deg(v) = |\{u \in V \mid \{u, v\} \in E\}|$.
+\end{definition}
+
+\begin{conjecture}[Erd\H{o}s-Gy\'{a}rf\'{a}s, 1995]
+If $G = (V, E)$ is a graph with $\delta(G) \ge 3$, then $G$ contains a cycle $C_k$ of length $k$ such that $k = 2^m$ for some integer $m \ge 1$.
+\end{conjecture}
+
+\section{Contextual Literature and Analogies}
+The problem lies at the intersection of extremal graph theory and additive combinatorics. It is structurally similar to questions concerning the existence of specific cycle lengths in dense graphs (e.g., theorems of Bondy and Simonovits on cycles of even length).
+
+We draw an analogy with the proof of the existence of even cycles in graphs of sufficient density, where one typically constructs a longest path and studies the neighborhood of its endpoints. Here, we aim to refine the path-building process by exploiting the degree condition to force cycles of specific lengths.
+
+\section{Proof Strategy and Lemmata}
+
+We decompose the conjecture into structured sub-problems.
+
+\begin{lemma}[Longest Path Neighborhood]
+\label{lem:longest_path}
+Let $P = v_1 v_2 \dots v_l$ be a longest path in a graph $G$ with $\delta(G) \ge 3$. Then all neighbors of $v_1$ must lie on $P$.
+\end{lemma}
+
+\begin{proof}
+Suppose there exists a neighbor $u$ of $v_1$ such that $u \notin V(P)$. Then the path $u v_1 v_2 \dots v_l$ has length $l+1$, contradicting the assumption that $P$ is a longest path. Thus, $N(v_1) \subseteq V(P)$.
+\end{proof}
+
+\begin{lemma}[Cycle Formation]
+\label{lem:cycle_lengths}
+Let $P = v_1 v_2 \dots v_l$ be a longest path in $G$ with $\delta(G) \ge 3$. Let $v_{i_1}, v_{i_2}, \dots, v_{i_k}$ be the neighbors of $v_1$ on $P$, ordered such that $2 = i_1 < i_2 < \dots < i_k \le l$. Since $\delta(G) \ge 3$, $k \ge 3$. The edges $\{v_1, v_{i_j}\}$ create cycles $C^{(j)}$ of length $i_j$.
+\end{lemma}
+
+\begin{proof}
+The path segment $v_1 \dots v_{i_j}$ has length $i_j - 1$. Adding the edge $\{v_1, v_{i_j}\}$ completes a cycle of length $(i_j - 1) + 1 = i_j$.
+\end{proof}
+
+\section{Lean 4 Formalization Architecture}
+To autoformalize this proof, we outline the Lean 4 structures.
+
+\begin{verbatim}
+import Mathlib.Combinatorics.SimpleGraph.Basic
+import Mathlib.Combinatorics.SimpleGraph.Connectivity
+
+variable {V : Type*} [Fintype V] [DecidableEq V]
+variable (G : SimpleGraph V)
+
+def min_degree_at_least (k : \mathbb{N}) : Prop :=
+  \forall v : V, G.degree v \ge k
+
+def has_cycle_power_of_two : Prop :=
+  \exists (c : G.Walk v v), c.IsCycle \land \exists (m : \mathbb{N}), c.length = 2^m
+
+theorem erdos_gyarfas (h : min_degree_at_least G 3) :
+  has_cycle_power_of_two G := by
+  sorry
+\end{verbatim}
+
+\section{Conclusion}
+The structural decomposition provided serves as a foundational step towards resolving the Erd\H{o}s-Gy\'{a}rf\'{a}s conjecture, preparing it for formal verification.
+
+\end{document}

inprogress/31-Erdos-Gyarfas/README.fr.md

@@ -0,0 +1,7 @@
+# 31-Erdos-Gyarfas
+
+## Conjecture d'Erdős-Gyárfás
+
+**Statut**: En cours
+
+La conjecture d'Erdős-Gyárfás stipule que tout graphe ayant un degré minimum d'au moins 3 contient un cycle de longueur $2^k$ pour un certain entier $k \ge 1$.

inprogress/31-Erdos-Gyarfas/README.md

@@ -0,0 +1,7 @@
+# 31-Erdos-Gyarfas
+
+## Erdős-Gyárfás Conjecture
+
+**Status**: In Progress
+
+The Erdős-Gyárfás conjecture states that every graph with minimum degree at least 3 contains a cycle of length $2^k$ for some integer $k \ge 1$.