Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

adjacency_matrix_ty

AdjacencyMatrix : ∀ {V} [Fintype V], SimpleGraph V → Matrix V V Real The adjacency matrix of a graph.

app

app2

app3

arrow

bool_ty

build_graph_theory_env

Build the graph theory environment, registering all axioms and theorems.

bvar

cayley_graph_ty

CayleyGraph : ∀ (G : Group) (S : Finset G), SimpleGraph G The Cayley graph Cay(G, S) with vertex set G and edges from S-generating set.

cheeger_constant_ty

CheegerConstant : ∀ {V} [Fintype V], SimpleGraph V → Real The Cheeger constant (edge expansion ratio) of a graph.

cheeger_inequality_ty

CheegerInequality : ∀ {V} [Fintype V] (G : SimpleGraph V), λ₂/2 ≤ h(G) ≤ √(2·d·λ₂) The Cheeger inequality connecting spectral gap λ₂ to edge expansion h(G).

chromatic_number_ty

chromatic_number : ∀ {V} [Fintype V], SimpleGraph V → Nat

chromatic_polynomial_ty

ChromaticPolynomial : ∀ {V} [Fintype V], SimpleGraph V → (Nat → Int) P(G, k) = number of proper k-colorings of G.

clique_cover_number_ty

CliqueCoverNumber : ∀ {V} [Fintype V], SimpleGraph V → Nat The minimum number of cliques needed to cover all vertices.

connectivity_threshold_ty

ConnectivityThreshold : Nat → Real The threshold probability p_c = ln(n)/n for G(n,p) connectivity.

crossing_number_ty

CrossingNumber : ∀ {V} [Fintype V], SimpleGraph V → Nat The crossing number cr(G): minimum crossings in any planar drawing.

cst

deletion_contraction_tutte_ty

DeletionContractionTutte : ∀ {V} [Fintype V] (G : SimpleGraph V) (e : Edge V), TuttePolynomial G = TuttePolynomial (Delete G e) + TuttePolynomial (Contract G e) Deletion-contraction recurrence for the Tutte polynomial.

digraph_adj_ty

digraph_adj : ∀ {V}, Digraph V → V → V → Bool

digraph_ty

Digraph V = { adj : V → V → Bool }

dynamic_graph_ty

DynamicGraph : Type → Type A dynamic graph supporting incremental/decremental edge updates.

edge_connectivity_ty

EdgeConnectivity : ∀ {V} [Fintype V], SimpleGraph V → Nat λ(G) = minimum number of edges whose removal disconnects G.

edge_expansion_ty

EdgeExpansion : ∀ {V}, SimpleGraph V → Real → Prop Cheeger constant h(G) = min over S of |∂S|/min(|S|,|V\S|).

eigenvalue_interlacing_ty

EigenvalueInterlacing : ∀ {V} [Fintype V] (G H : SimpleGraph V), IsInducedSubgraph H G → InterlacesEigenvalues (Laplacian G) (Laplacian H) Cauchy’s eigenvalue interlacing theorem for graph Laplacians.

erdos_renyi_graph_ty

ErdosRenyiGraph : Nat → Real → SimpleGraph The Erdős-Rényi G(n,p) random graph model.

euler_formula_ty

Euler’s formula: V - E + F = 2 for connected planar graphs

eulerian_circuit_thm_ty

Eulerian circuit theorem: G has Eulerian circuit ↔ G is connected ∧ all degrees even

excluded_minor_characterization_ty

ExcludedMinorCharacterization : ∀ {V}, SimpleGraph V → Type A graph class is characterized by a finite set of forbidden minors.

four_color_theorem_ty

Four Color Theorem: χ(G) ≤ 4 for any planar graph G

fractional_chromatic_number_ty

FractionalChromaticNumber : ∀ {V} [Fintype V], SimpleGraph V → Real χ_f(G) = inf { k/d : G has a (k:d)-coloring }.

fully_dynamic_connectivity_ty

FullyDynamicConnectivity : ∀ {V} [Fintype V], DynamicGraph V → Prop A data structure supporting edge insertions, deletions, and connectivity queries.

genus_ty

Genus : ∀ {V} [Fintype V], SimpleGraph V → Nat The genus of a graph: minimum genus of orientable surface for embedding.

graph_homomorphism_ty

GraphHomomorphism : ∀ {V W}, SimpleGraph V → SimpleGraph W → Type A graph homomorphism f : V → W preserving adjacency.

graph_laplacian_ty

GraphLaplacian : ∀ {V} [Fintype V], SimpleGraph V → Matrix V V Real L = D - A where D is degree matrix, A is adjacency matrix.

graph_minor_ty

GraphMinor : ∀ {V W}, SimpleGraph V → SimpleGraph W → Prop H is a minor of G if H can be obtained from a subgraph of G by contracting edges.

graphon_cut_distance_ty

GraphonCutDistance : Graphon → Graphon → Real The cut distance between two graphons.

graphon_ty

Graphon : Type A graphon is a symmetric measurable function W : [0,1]² → [0,1].

halls_theorem_ty

Hall’s theorem: bipartite graph G=(A∪B, E) has perfect matching ↔ for all S ⊆ A, |N(S)| ≥ |S|

homomorphism_duality_ty

HomomorphismDuality : ∀ {V W} (H : SimpleGraph V) (G : SimpleGraph W), ¬ (Hom H G) ↔ ∃ (D : Digraph), DualObstruction D G Homomorphism duality: absence of H-homomorphism characterized by dual.

hypergraph_coloring_ty

HypergraphColoring : ∀ {V}, Hypergraph V → Nat → Prop A proper k-coloring of a hypergraph: each hyperedge has at least 2 colors.

hypergraph_turan_ty

HypergraphTuran : ∀ (r k n : Nat), TuranDensity r k n Turán-type density results for hypergraphs.

hypergraph_ty

Hypergraph : Type → Type A hypergraph on vertex type V: a collection of hyperedges (subsets of V).

ihara_zeta_function_ty

IharaZetaFunction : ∀ {V} [Fintype V], SimpleGraph V → (Complex → Complex) The Ihara zeta function Z_G(u) = ∏_p (1 - u^{|p|})^{-1} over prime cycles p.

impl_pi

incremental_connectivity_ty

IncrementalConnectivity : ∀ {V} [Fintype V], DynamicGraph V → Prop An online connectivity structure supporting only edge insertions.

is_bipartite_ty

IsBipartite : ∀ {V}, SimpleGraph V → Prop

is_eulerian_ty

IsEulerian : ∀ {V}, SimpleGraph V → Prop A graph has an Eulerian circuit iff every vertex has even degree and graph is connected

is_hamiltonian_ty

IsHamiltonian : ∀ {V}, SimpleGraph V → Prop A graph has a Hamiltonian cycle visiting each vertex exactly once

is_perfect_graph_ty

IsPerfectGraph : ∀ {V}, SimpleGraph V → Prop A graph is perfect if χ(H) = ω(H) for every induced subgraph H.

is_perfect_matching_ty

IsPerfectMatching : ∀ {V} [Fintype V], SimpleGraph V → Matching → Prop

is_planar_ty

IsPlanar : ∀ {V}, SimpleGraph V → Prop

is_tree_ty

IsTree G ↔ Connected G ∧ acyclic G

kruskal_mst

Minimum spanning tree via Kruskal’s algorithm (weighted undirected graph).

kuratowski_theorem_ty

Kuratowski’s theorem: G is planar ↔ G has no K₅ or K₃₃ subdivision

lovasz_theta_ty

LovaszThetaFunction : ∀ {V} [Fintype V], SimpleGraph V → Real The Lovász theta function ϑ(G), sandwiched between ω(G) and χ(G̅).

matching_polynomial_ty

MatchingPolynomial : ∀ {V} [Fintype V], SimpleGraph V → (Real → Real) μ(G, x) = ∑_k (-1)^k m_k(G) x^{n-2k} where m_k = number of k-matchings.

matching_ty

Matching G = Set of independent edges

max_flow

Max-flow via Ford-Fulkerson with BFS (Edmonds-Karp).

max_flow_min_cut_ty

MaxFlowMinCut : ∀ (n : Nat) (s t : Nat) (cap : Nat → Nat → Real), MaxFlow n s t cap = MinCutCapacity n s t cap Max-flow min-cut theorem for real-valued capacities.

mengers_theorem_ty

MengersThm : ∀ {V} [Fintype V] (G : SimpleGraph V) (s t : V), MaxDisjointPaths G s t = MinVertexCut G s t Menger’s theorem: max number of vertex-disjoint s-t paths = min vertex cut size.

nat_ty

pathwidth_ty

Pathwidth : ∀ {V} [Fintype V], SimpleGraph V → Nat pw(G) = min over path decompositions of (max bag size - 1).

phase_transition_ty

PhaseTransition : ∀ (n : Nat) (p : Real), p > 1/n → GiantComponentExists (ErdosRenyi n p) Phase transition at p = 1/n: a giant component emerges.

pi

prop

real_ty

robertson_seymour_wqo_ty

RobertsonSeymourWQO : ∀ {V} (seq : Nat → SimpleGraph V), ∃ i j, i < j ∧ Minor (seq i) (seq j) The Robertson-Seymour theorem: graphs are well-quasi-ordered under the minor relation.

semi_streaming_sketch_ty

SemiStreamingSketch : ∀ {V} [Fintype V], SimpleGraph V → Type A semi-streaming sketch using O(n · polylog n) space for n = |V|.

simple_graph_adj_ty

SimpleGraph.adj : ∀ {V}, SimpleGraph V → V → V → Prop

simple_graph_connected_ty

SimpleGraph.Connected : ∀ {V}, SimpleGraph V → Prop

simple_graph_degree_ty

SimpleGraph.degree : ∀ {V} [Fintype V] [DecidableEq V], SimpleGraph V → V → Nat

simple_graph_ty

SimpleGraph V = { adj : V → V → Prop // sym, irrefl }

sketched_connectivity_ty

SketchedConnectivity : ∀ {V} [Fintype V], SemiStreamingSketch → Prop Determine connectivity from a semi-streaming sketch.

spectral_gap_ty

SpectralGap : ∀ {V} [Fintype V], SimpleGraph V → Real The spectral gap λ₂ = second smallest eigenvalue of the normalized Laplacian.

strong_perfect_graph_thm_ty

StrongPerfectGraphThm : ∀ {V} (G : SimpleGraph V), IsPerfect G ↔ (NoOddHole G ∧ NoOddAntihole G) The strong perfect graph theorem (Chudnovsky-Robertson-Seymour-Thomas 2006).

strongly_regular_graph_ty

StronglyRegularGraph : ∀ {V} [Fintype V] (G : SimpleGraph V) (k λ μ : Nat), Prop srg(n, k, λ, μ): k-regular, adjacent pairs have λ common neighbors, non-adjacent pairs have μ common neighbors.

sunflower_lemma_ty

SunflowerLemma : ∀ (p k : Nat) (F : Finset (Finset Nat)), |F| > (p-1)^k · k! → ∃ sunflower of size p in F Erdős-Ko-Rado sunflower lemma for set families.

szemeredi_regularity_ty

SzemerediRegularity : ∀ {V} [Fintype V] (G : SimpleGraph V) (ε : Real), ∃ partition, ε-regular and |partition| ≤ M(ε) Szemerédi regularity lemma: every graph has an ε-regular partition.

tree_decomposition_ty

TreeDecomposition : ∀ {V}, SimpleGraph V → Type A tree decomposition of G: a tree T with bags B(t) ⊆ V covering edges.

treewidth_duality_ty

TreewidthDuality : ∀ {V} [Fintype V] (G : SimpleGraph V) (k : Nat), Treewidth G ≤ k ↔ ¬ HasBranchDecompositionObstruction G k Treewidth duality via brambles/haven obstructions.

treewidth_ty

Treewidth : ∀ {V} [Fintype V], SimpleGraph V → Nat tw(G) = min over tree decompositions of (max bag size - 1).

tutte_polynomial_ty

TuttePolynomial : ∀ {V} [Fintype V], SimpleGraph V → (Real → Real → Real) T(G; x, y) = universal graph polynomial encoding many graph invariants.

type0

vertex_connectivity_ty

VertexConnectivity : ∀ {V} [Fintype V], SimpleGraph V → Nat κ(G) = minimum number of vertices whose removal disconnects G.

vertex_expansion_ty

VertexExpansion : ∀ {V}, SimpleGraph V → Real → Prop h-vertex expander: for all S with |S| ≤ |V|/2, |N(S)| ≥ h·|S|.

wagner_theorem_ty

WagnerThm : ∀ {V} (G : SimpleGraph V), IsPlanar G ↔ NoK5Minor G ∧ NoK33Minor G Wagner’s theorem: G is planar iff G has no K₅ or K₃,₃ minor.

walk_ty

Walk G u v = path from u to v in G (list of adjacent vertices)