Counting Hamilton circuits

Lax280166.CountingHamiltonCircuits · concepts/Lax280166/CountingHamiltonCircuits.lean · lax-280166

definition

Loading review…

Natural Language Statement

Definition

On a finite directed graph, #Directed Hamilton Circuit counts the directed Hamilton circuits, each given by its successor relation: a relation along the arcs that is a single cycle through every vertex. #Hamilton Circuit counts the undirected Hamilton circuits of the symmetric closure, each given by its set of edges, so that a circuit and its reverse count once.

Concept map

10 concepts; 25 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Tactic.FinCases
2	import Mathlib.Order.PiLex
3	import Mathlib.Data.Prod.Lex
4	import Mathlib.Data.Fintype.EquivFin
5	import Mathlib.ModelTheory.Order
6	import Mathlib.ModelTheory.Semantics
7	import Mathlib.ModelTheory.Complexity
8	import Mathlib.Logic.Equiv.Fin.Basic
9	import Mathlib.Data.Fintype.Lattice
10	import Mathlib.Data.Finite.Sigma
11	import Mathlib.Order.Lattice.Nat
12	import Mathlib.Data.Set.Card
13	import Mathlib.Data.Fintype.Pigeonhole
14	import Mathlib.Dynamics.FixedPoints.Basic
15	import Mathlib.ModelTheory.Syntax
16	import Mathlib.Algebra.Order.BigOperators.Group.Finset
17	import Mathlib.Data.Fintype.Card
18	import Mathlib.SetTheory.Cardinal.Finite
19	import Mathlib.Algebra.BigOperators.Finprod
20	import Mathlib.Data.Set.Finite.Lemmas
21	import Mathlib.Logic.Equiv.Prod
22	import Mathlib.Order.Fin.Basic
23	import Mathlib.Data.Fintype.Sort
24	import Mathlib.GroupTheory.Perm.Cycle.Basic
25	import Mathlib.GroupTheory.OrderOfElement
26	import Lax799700.Hamilton
27	import Lax904597.Machines
28	import Mathlib.SetTheory.Cardinal.Finite
29	import Lax366625.CountingProblems
30
31	/-!
32	---
33	title: Counting Hamilton circuits
34	type: definition
35	---
36	On a finite directed graph, #Directed Hamilton Circuit counts the directed
37	Hamilton circuits, each given by its successor relation: a relation along
38	the arcs that is a single cycle through every vertex. #Hamilton Circuit
39	counts the undirected Hamilton circuits of the symmetric closure, each given
40	by its set of edges, so that a circuit and its reverse count once.
41	-/
42
43	namespace Lax280166.CountingHamiltonCircuits
44
45	open Lax799700.Hamilton Lax904597.Machines
46
47	open FirstOrder
48
49	open Language Structure
50
51	section Circuit
52
53	variable {A : Type}
54
55	/-- `y` comes next after `x` on the circuit a linear order is a cut of: it is
56	the immediate successor of `x`, or `x` is the last element and `y` the
57	first. -/
58	def CycSucc (Le : A → A → Prop) (x y : A) : Prop :=
59	SuccOf Le x y ∨ ((∀ z, Le z x) ∧ ∀ z, Le y z)
60
61	/-- The relation `Nxt` is a Hamilton circuit of `R`: the cyclic successor
62	relation of a linear order of the universe, included in `R`. -/
63	def IsCircuit (R : A → A → Prop) (Nxt : A → A → Prop) : Prop :=
64	∃ Le : A → A → Prop, IsLinOrd Le ∧ (∀ x y, Nxt x y ↔ CycSucc Le x y) ∧
65	∀ x y, Nxt x y → R x y
66
67	end Circuit
68
69	section Problem
70
71	variable (A : Type) [digraph.Structure A]
72
73	/-- The relation `Nxt` is a Hamilton circuit of a finite digraph. -/
74	def DirCircuit (Nxt : A → A → Prop) : Prop :=
75	Finite A ∧ IsCircuit (fun x y : A => DGArc x y) Nxt
76
77	end Problem
78
79	open FirstOrder
80
81	open Language Structure
82
83	section UCircuit
84
85	variable {A : Type}
86
87	/-- The relation `E` is the edge set of a Hamilton circuit of `R`: the
88	symmetric closure of a circuit of `R`. -/
89	def IsUCircuit (R : A → A → Prop) (E : A → A → Prop) : Prop :=
90	∃ Nxt : A → A → Prop, IsCircuit R Nxt ∧ ∀ x y, E x y ↔ (Nxt x y ∨ Nxt y x)
91
92	end UCircuit
93
94	section Problem
95
96	variable (A : Type) [digraph.Structure A]
97
98	/-- The relation `E` is the edge set of a Hamilton circuit of a finite
99	graph. -/
100	def UCircuit (E : A → A → Prop) : Prop :=
101	Finite A ∧ IsUCircuit (fun x y : A => DGEdge x y) E
102
103	end Problem
104
105	open Lax366625.CountingProblems
106
107	/-- #Directed Hamilton Circuit, as a counting problem. -/
108	noncomputable def SharpDirHamCircuit : CountingProblem Lax799700.Hamilton.digraph :=
109	CountingProblem.ofFun fun A _ =>
110	Nat.card {Nxt : A → A → Prop // DirCircuit A Nxt}
111
112	/-- #Hamilton Circuit, as a counting problem. -/
113	noncomputable def SharpHamCircuit : CountingProblem Lax799700.Hamilton.digraph :=
114	CountingProblem.ofFun fun A _ =>
115	Nat.card {E : A → A → Prop // UCircuit A E}
116
117	end Lax280166.CountingHamiltonCircuits
118

Builds on

Used by

From Mathlib

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Counting Hamilton circuits

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments