KonigsbergStarter

The seven-bridge theorem through Cumulus's public graph entrypoint

Open in Workbench View on GitHub

1-- The seven-bridge theorem through Cumulus's public graph entrypoint.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.KonigsbergStarter8import Grace.Cumulus.GraphTheory910theorem the_seven_bridges11  shows ¬(∃ n ∈ ℕ, ∃ edges, ∃ vertices,12    Multigraph.EulerTrail(4, 7, Konigsberg.bridgeLeft, Konigsberg.bridgeRight, edges, vertices, n))13proof14  exact Konigsberg.no_euler_trail_exists1516theorem the_city_is_a_multigraph17  shows Multigraph.Graph(4, 7, Konigsberg.bridgeLeft, Konigsberg.bridgeRight)18proof19  exact Konigsberg.graph2021theorem the_four_degrees22  shows Multigraph.incidences(Konigsberg.bridgeLeft, Konigsberg.bridgeRight, identity(7), 0, 7) = 3 ∧23    Multigraph.incidences(Konigsberg.bridgeLeft, Konigsberg.bridgeRight, identity(7), 1, 7) = 3 ∧24    Multigraph.incidences(Konigsberg.bridgeLeft, Konigsberg.bridgeRight, identity(7), 2, 7) = 5 ∧25    Multigraph.incidences(Konigsberg.bridgeLeft, Konigsberg.bridgeRight, identity(7), 3, 7) = 326proof27  refine ⟨Konigsberg.degree_land1, Konigsberg.degree_land2,28    Konigsberg.degree_island1, Konigsberg.degree_island2⟩29