MultigraphStarter

Edge identities, parallel bridges, loops, and the Euler-trail obstruction

Open in Workbench View on GitHub

1-- Edge identities, parallel bridges, loops, and the Euler-trail obstruction.2-- Part of the Grace17 proof assistant for mathematics based on set theory.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module User.MultigraphStarter8import Grace.Cumulus.GraphTheory910-- Two distinct bridges with the same endpoints contribute two to the degree.11theorem parallel_bridges_count_twice (leftEnd rightEnd edges x y : Set)12  requires distinct : edges[0] ≠ edges[1]13  requires endpoints : x ≠ y14  requires left0 : leftEnd(edges[0]) = x15  requires left1 : leftEnd(edges[1]) = x16  requires right0 : rightEnd(edges[0]) = y17  requires right1 : rightEnd(edges[1]) = y18  shows Multigraph.incidences(leftEnd, rightEnd, edges, x, 2) = 219proof20  have xMember := singleton.self at x21  have xCount := indicator.member with xMember22  have yMissing : ¬(y ∈ {x})23    intro member24    have equal := singleton.membership.forward with member25    cc26  have yCount := indicator.absent with yMissing27  simp [Multigraph.incidences]2829-- A loop has two incident ends even though it has just one edge identity.30theorem a_loop_counts_twice (leftEnd rightEnd edges x : Set)31  requires left : leftEnd(edges[0]) = x32  requires right : rightEnd(edges[0]) = x33  shows Multigraph.incidences(leftEnd, rightEnd, edges, x, 1) = 234proof35  have member := singleton.self at x36  have value := indicator.member with member37  simp [Multigraph.incidences]3839theorem closed_walk_degrees_are_even (V E leftEnd rightEnd edges vertices x : Set, n : Nat)40  requires walk : Multigraph.Walk(V, E, leftEnd, rightEnd, edges, vertices, n)41  requires closed : vertices[n] = vertices[0]42  shows Even(Multigraph.incidences(leftEnd, rightEnd, edges, x, n))43proof44  exact Multigraph.Walk.closed_even at V, E, leftEnd, rightEnd, edges, vertices, x, n with *4546-- The obstruction uses a fixed enumeration, independently of the alleged trail.47theorem three_noneven_degrees_preclude_an_euler_trail (V E leftEnd rightEnd edges vertices enumeration a b c : Set, n m : Nat)48  requires enumeration : BijectiveBetween(enumeration, m, E)49  requires ab : a ≠ b50  requires ac : a ≠ c51  requires bc : b ≠ c52  requires degreeA : ¬Even(Multigraph.incidences(leftEnd, rightEnd, enumeration, a, m))53  requires degreeB : ¬Even(Multigraph.incidences(leftEnd, rightEnd, enumeration, b, m))54  requires degreeC : ¬Even(Multigraph.incidences(leftEnd, rightEnd, enumeration, c, m))55  shows ¬Multigraph.EulerTrail(V, E, leftEnd, rightEnd, edges, vertices, n)56proof57  exact Multigraph.EulerTrail.three_noneven_obstruction at V, E, leftEnd, rightEnd,58    edges, vertices, enumeration, a, b, c, n, m with *59