Loopy graphs
class graph (n : ℕ) :
(edges : set ... )
(vertices : set ...)
(can_exist_loops : ...)
(can_exist_many_edges_between_eq_vertices : ...)
def subgraph (F S : graph) :=
S.vertices ⊆ F.vertices ∧ S.edges ⊆ F.edges
/-- every vertex has 4 incident edges -/
def 4_regular (F : graph) :=
∀ v, card(v.e) = 4
/-
O - O
| \ |
O - O
perform an edge cut on the graph
O - O
|
O O
-/
def edge_cut : set edges :=
-- the graph becomes disconnected when these are removed
-- splits into two graphs or more
variable (m : 4_regular n)
def split (m : 4_regular n) (v : vertex in m) : graph n-1 := sorry
-- remove the vertex and pair the incident edges
/-- split -/
def transition at a vertex v :=
a partition of the four half-edges incident on v into two pairs.
split
\ /
.
/ \
\ / \ / ----- \ /
\ / | |
/ \ / \ ----- / \
𝒯(F) denotes the set of all transitions in F.
def natural (n : ℕ) (f : 4_regular n → 4_regular n) [invol f] := f(n-1) ∘ (split v₁) = (split v₂) ∘ f(n)
A 4-regular graph with one vertex has four distinct circuits.
A circuit in a graph is a sequence v1, h1, h1’, v2, h2, …, hk, hk’ = h0’, v_{k+1} = v1. For each i ∈ {1,…,k}, hi and h’i are half-edges of a single edge and h’_{i-1} and hi are both indicent on vi.
The half-edges that appear in a circuit must be pairwise distinct, but vertices may be repeated.
Two circuits are considered to be the same if they differ only by a combination of cyclic permutations.
“Theorem 2: if an operation of 4_regular graphs preserves interlacement graphs, then also preserves transition matroids.”
“Implies there are two fundamental types of interlacement-preserving operations, associated with edge cuts of size two or four.”
variables (F₁ F₂ : 4_regular n) [e₁ = {h₁,h'₁}] [e₁ ∈ F₁.edges] [e₂ = {h₂,h'₂}] [e₂ ∈ F₂.edges]
/-
connected sum and separation
/ - \ / - \ / --- \
. | | . <--> . .
\ - / \ - / \ --- /
-/
def connected_sum F₁ F₂ e₁ e₂ : graph :=
replace e₁ and e₂ in F₁ ∪ F₂ with new edges {h₁,h₂} and {h'₁,h'₂}.
def separation (graph F) (edges e1 = {h₁, h₁'} e2 = {h₂, h₂'}) [edge_cut F {e1,e2}] : graph :=
replace e₁ and e₂ with new edges {h₁, h₂} and {h₁', h₂'}
s.t. resulting graph F' satisfies c(F') = c(F) + 1
balanced mutation /-------------\ /-----\ /----\ | | | \/ | |/-----------\| |/-----/\----\| . . <--> . . |\-----------/| |\-----\/----/| | | | /\ | \-------------/ \-----/ \----/
def balanced_mutation (graph F) [subgraph F F₁] [subgraph F F₂] [nonempty F₁] [nonempty F₂]
[V(F) = V(F₁) ∪ V(F₂)] [V(F₁) ∩ V(F₂) = ∅] [four edges connect F₁ to F₂] : graph :=
take these four edges and make two new edges that each connect F₁ to F₂.
/-- what is interlacement and why do these operations preserve it?
def interlace_eq (F) (F') :=
related through a sequence of connected sums, separations and balanced_mutations
lemma natural_iff_interlace_eq_after_map (t : Sₙ → Sₙ) [involution t] :
natural t ↔ (interlace_eq F F' → interlace_eq (t F) (t F')) := sorry
def trivial (t : Sₙ → Sₙ) [involution t] :=
∀ F, interlace_eq F (t F)
/-- prove there exists a natural involution t --/
theoerm exists : ∃ t, natural t := sorry
/-- or prove it cannot exist -/
theorem does_not_exist : ¬ ∃ t, natural t := sorry
- so much room for animations
def circuit_partition (F) (P) := sorry
notation `|`P`|` := number of circuits included in P
- “Let F be a 4-regular graph with c(F) connected components and n vertices.
| Then there is a rank n matroid M(F) defined on vertex triple 𝒯(F) who rank function extends a well-known formula: for each circuit partition P of F, the rank τ(P) in Mτ(F) is given by r(τ(P)) = n + c(F) - | P | .” |
lemma circuit_nullity {n c : ℕ} (F : 4_regular n) [connected_components F = c] :
∃ vertex triple 𝒯(F),
∃ rank n matroid Mτ(F) 𝒯,
∀ (P) [circuit_partition F P],
r(τ(P)) = n + c(F) - |P| := sorry
"We call Mτ(F) the transition matroid of F.
def transition_matroid {F : 4-regular n} (C : Euler_system F) :=
a_binary_matroid_on vertex triple 𝒯(F) represented by the matrix M(C)
Rewrite formula as |P| - c(F) = n - r(τ(P)):
the number of 'extra' circuits in P equals the nullity of τ(P)."
def Euler_circ (F : 4_regular n) (C : circuit F) :=
-- includes every half edge of F
theorem thm6 (F F' : 4_regular n) :
isomorphic (Mτ F) (Mτ F') ↔
(∃ s : sequence of connected_sums, separations and balanced mutations, F' = s F) := sorry
theorem thm8 (F F' : 4_regular n) :
(∃ s : sequence of connected_sums, separations and balanced mutations, F' = s F)
↔ ∀ weight functions on vertex triple 𝒯(F),
∃ weight functions on vertex triple 𝒯(F'),
Tutte polynomials Mτ(F) = Tutte polynomials Mτ(F') := sorry
example : conn F {h1,h1'} {h2,h2'} = conn F {h1',h1} {h2,h2'} := sorry
example : conn F {h1,h1'} {h2,h2'} = conn F {h1,h1'} {h2',h2} := sorry