Grace/Cumulus/GraphTheory/CountingInvariant.g17

Open in Workbench Download source

Imports

Counting · Cardinal.Enumeration

Declarations

Source

1-- Vertex labels and enumeration choices do not change graph counts.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.GraphTheory.CountingInvariant8import Counting9import Cardinal.Enumeration1011namespace GraphCount1213theorem degree.reindex (V E f g x : Set, n m : Nat)14  requires enumerationF : BijectiveBetween(f, n, V)15  requires enumerationG : BijectiveBetween(g, m, V)16  shows GraphCount.degree(E, f, x, n) = GraphCount.degree(E, g, x, m)17proof18  have valuesF := Bijective.values with enumerationF19  have valuesG := Bijective.values with enumerationG20  have left := GraphCount.degree.neighbors at V, E, f, x, n with valuesF21  have right := GraphCount.degree.neighbors at V, E, g, x, m with valuesG22  rw [left, right]23  exact countMembers.reindex with enumerationF, enumerationG2425-- Cross sums allow two independent enumerations of the two endpoints.26def crossSum (E f g : Set, n m : Nat) → Set27  | E, f, g, n, zero => 028  | E, f, g, n, succ(k) => add(crossSum(E, f, g, n, k), GraphCount.degree(E, f, g[k], n))29  descends m3031theorem crossSum.natural (E f g : Set, n m : Nat)32  shows Nat(crossSum(E, f, g, n, m))33proof34  induction m35  | zero =>36    rw crossSum37    typecheck38  | succ(k) using ih =>39    rw crossSum40    have value := GraphCount.degree.natural at E, f, g[k], n with assumption41    typecheck4243theorem crossSum.diagonal (E f : Set, n m : Nat)44  shows crossSum(E, f, f, n, m) = GraphCount.degreeSum(E, f, n, m)45proof46  induction m47  | zero =>48    simp [crossSum, GraphCount.degreeSum]49  | succ(k) using ih =>50    rw [crossSum, GraphCount.degreeSum, ih]51    rfl5253theorem crossSum.empty_left (E f g : Set, m : Nat)54  shows crossSum(E, f, g, 0, m) = 055proof56  induction m57  | zero =>58    rw crossSum59    rfl60  | succ(k) using ih =>61    rw [crossSum, GraphCount.degree, ih]62    simp [add]6364theorem crossSum.extend_left (V E f g : Set, n m : Nat)65  requires graph : SimpleGraph(V, E)66  shows crossSum(E, f, g, succ(n), m) =67    add(crossSum(E, f, g, n, m), GraphCount.degree(E, g, f[n], m))68proof69  induction m70  | zero =>71    simp [crossSum, GraphCount.degree, add]72  | succ(k) using ih =>73    rw [crossSum, crossSum, GraphCount.degree, GraphCount.degree, ih]74    have symmetric := GraphCount.indicator.symmetric at V, E, g[k], f[n] with graph75    rw symmetric76    have a := crossSum.natural at E, f, g, n, k with *77    have b := GraphCount.degree.natural at E, g, f[n], k with assumption78    have c := GraphCount.degree.natural at E, f, g[k], n with assumption79    have d := indicator.natural at E, (f[n], g[k])80    exact add.four_shuffle with a, b, c, d8182theorem crossSum.transpose (V E f g : Set, m n : Nat)83  requires graph : SimpleGraph(V, E)84  shows crossSum(E, f, g, n, m) = crossSum(E, g, f, m, n)85proof86  induction n87  | zero =>88    rw [crossSum.empty_left, crossSum]89    rfl90  | succ(k) using ih =>91    have extended := crossSum.extend_left at V, E, f, g, k, m with *92    rw [extended, crossSum, ih]93    rfl9495theorem crossSum.reindex_neighbors (V E f g h : Set, n m k : Nat)96  requires enumerationF : BijectiveBetween(f, n, V)97  requires enumerationG : BijectiveBetween(g, m, V)98  shows crossSum(E, f, h, n, k) = crossSum(E, g, h, m, k)99proof100  induction k101  | zero =>102    simp [crossSum]103  | succ(j) using ih =>104    rw [crossSum, crossSum, ih]105    have equal := GraphCount.degree.reindex at V, E, f, g, h[j], n, m with *106    rw equal107    rfl108109theorem degreeSum.reindex (V E f g : Set, n m : Nat)110  requires graph : SimpleGraph(V, E)111  requires enumerationF : BijectiveBetween(f, n, V)112  requires enumerationG : BijectiveBetween(g, m, V)113  shows GraphCount.degreeSum(E, f, n, n) = GraphCount.degreeSum(E, g, m, m)114proof115  have diagonalF := crossSum.diagonal at E, f, n, n with *116  have diagonalG := crossSum.diagonal at E, g, m, m with *117  have first := crossSum.reindex_neighbors at V, E, f, g, f, n, m, n with118    *{3}, enumerationF, enumerationG119  have transpose := crossSum.transpose at V, E, g, f, n, m with *120  have second := crossSum.reindex_neighbors at V, E, f, g, g, n, m, m with121    *{3}, enumerationF, enumerationG122  rwa [← diagonalF, first, transpose, second]123124theorem edgeCount.reindex (V E f g : Set, n m : Nat)125  requires graph : SimpleGraph(V, E)126  requires enumerationF : BijectiveBetween(f, n, V)127  requires enumerationG : BijectiveBetween(g, m, V)128  shows GraphCount.edgeCount(E, f, n) = GraphCount.edgeCount(E, g, m)129proof130  have totals := degreeSum.reindex with graph, enumerationF, enumerationG131  have left := GraphCount.handshaking at V, E, f, n with graph132  have right := GraphCount.handshaking at V, E, g, m with graph133  rw [left, right] at totals134  have positive : 2 ≠ 0135    intro zero136    have reversed : 0 = 2 by cc137    exact Naturals.disjoint.zero.succ at 1 with reversed138  exact mul.left_cancel_positive with positive, totals139140end GraphCount141