Grace/Cumulus/Cardinal/Handshake.g17

Open in Workbench Download source

Imports

DoubleCounting · SumParity

Declarations

Source

1-- The handshake parity lemma for rooms and doors: with every room having2-- at most two doors and every door on one or two rooms, an odd number of3-- boundary doors forces an odd number of rooms with exactly one door4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Cardinal.Handshake10import DoubleCounting11import SumParity1213def cofiber (I R d : Set) : Set := { r ∈ R | (r, d) ∈ I }14def completeRooms (I R D : Set) : Set := { r ∈ R | cardinality(fiber(I, D, r)) = 1 }15def boundaryDoors (I R D : Set) : Set := { d ∈ D | cardinality(cofiber(I, R, d)) = 1 }1617-- The converse relation: its fibres are the cofibres, and it has the18-- same size.19theorem converse.subset (I R D : Set)20  shows converse(I, R, D) ⊆ D × R21proof22  intros p hp23  have parts := converse.membership.forward with hp24  exact parts.left2526theorem cofiber.converse (I R D d : Set)27  requires hd : d ∈ D28  shows fiber(converse(I, R, D), R, d) = cofiber(I, R, d)29proof30  ext r31  constructor32  . intro hr33    have parts := fiber.membership.forward with hr34    have converseParts := converse.membership.forward with parts.right35    obtain ⟨x, hx, y, hy, shape, related⟩ := converseParts.right36    have coordinates := orderedPair.injective with shape37    rw [coordinates.left, coordinates.right]38    exact cofiber.membership.backward with ⟨hx, related⟩39  . intro hr40    have parts := cofiber.membership.forward with hr41    have related : relates(I, r, d) := parts.right42    have member := converse.relates with parts.left, hd, related43    have inConverse : (d, r) ∈ converse(I, R, D) := member44    exact fiber.membership.backward with ⟨parts.left, inConverse⟩4546theorem converse.image (I R D : Set)47  requires inside : I ⊆ R × D48  shows functionImage(productSwap(R, D), I, D × R) = converse(I, R, D)49proof50  have function := Injective.function with (Bijective.injective with (productSwap.bijective at R, D))51  ext q52  constructor53  . intro hq54    simp [functionImage.membership] at hq55    obtain ⟨bound, p, hp, shape⟩ := hq56    obtain ⟨boundP, x, hx, y, hy, pairShape⟩ := product.membership.forward with (inside with p, hp)57    have swapped := productSwap.pair with hx, hy58    rw [pairShape, swapped] at shape59    rw pairShape at hp60    have related : relates(I, x, y) := hp61    have member := converse.relates with hx, hy, related62    rw shape63    exact member64  . intro hq65    have parts := converse.membership.forward with hq66    obtain ⟨x, hx, y, hy, shape, related⟩ := parts.right67    have inside2 : (x, y) ∈ R × D := product.pair with hx, hy68    have swapped := productSwap.pair with hx, hy69    rw [shape, ← swapped]70    have closed := FunctionBetween.apply_closed with function, inside271    simp [functionImage.membership]72    constructor73    . exact closed74    . witness (x, y)75      constructor76      . exact related77      . rfl7879theorem converse.cardinality (I R D : Set)80  requires finiteR : Finite(R)81  requires finiteD : Finite(D)82  requires inside : I ⊆ R × D83  shows cardinality(converse(I, R, D)) = cardinality(I)84proof85  have bijective := productSwap.bijective at R, D86  have injective := Bijective.injective with bijective87  have function := Injective.function with injective88  have finiteI := Finite.subset with (Finite.product with finiteR, finiteD), inside89  have closed : ∀ p ∈ I, productSwap(R, D)(p) ∈ D × R90    intros p hp91    exact FunctionBetween.apply_closed with function, (inside with p, hp)92  have restricted := restrict.function with function, inside, closed93  have restrictedInjective : InjectiveBetween(restrict(productSwap(R, D), I), I, converse(I, R, D))94    constructor95    . have image := converse.image with inside96      rw ← image97      apply restrict.function with function, inside98      intros p hp99      have value := FunctionBetween.apply_closed with function, (inside with p, hp)100      simp [functionImage.membership]101    . intros p hp q hq z hz hpz hqz102      have valueP := FunctionBetween.apply_value with restricted, hp, hpz103      have valueQ := FunctionBetween.apply_value with restricted, hq, hqz104      have stepP := restrict.apply with function, inside, closed, hp105      have stepQ := restrict.apply with function, inside, closed, hq106      rw stepP at valueP107      rw stepQ at valueQ108      have same : productSwap(R, D)(p) = productSwap(R, D)(q) by cc109      exact Injective.apply_cancel with injective, (inside with p, hp), (inside with q, hq), same110  have restrictedSurjective : SurjectiveBetween(restrict(productSwap(R, D), I), I, converse(I, R, D))111    constructor112    . exact restrictedInjective.left113    . intros q hq114      have image := converse.image with inside115      rw ← image at hq116      simp [functionImage.membership] at hq117      obtain ⟨bound, p, hp, shape⟩ := hq118      refine ⟨p, hp, ?_⟩119      have related := FunctionBetween.relates_apply with restrictedInjective.left, hp120      have step := restrict.apply with function, inside, closed, hp121      rwa [step, ← shape] at related122  have bijectiveRestricted : BijectiveBetween(restrict(productSwap(R, D), I), I, converse(I, R, D)) := ⟨restrictedInjective, restrictedSurjective⟩123  have same := cardinality.bijective with finiteI, bijectiveRestricted124  symm125  exact same126127-- The handshake lemma.128theorem handshake (I R D : Set)129  requires finiteR : Finite(R)130  requires finiteD : Finite(D)131  requires inside : I ⊆ R × D132  requires rooms : ∀ r ∈ R, cardinality(fiber(I, D, r)) = 0 ∨ cardinality(fiber(I, D, r)) = 1 ∨ cardinality(fiber(I, D, r)) = 2133  requires doors : ∀ d ∈ D, cardinality(cofiber(I, R, d)) = 1 ∨ cardinality(cofiber(I, R, d)) = 2134  requires boundary : Odd(cardinality(boundaryDoors(I, R, D)))135  shows Odd(cardinality(completeRooms(I, R, D)))136proof137  have sizeR : cardinality(R) = cardinality(R) by rfl138  have sizeD : cardinality(D) = cardinality(D) by rfl139  have correctR := cardinality.correct with finiteR140  have correctD := cardinality.correct with finiteD141  have natR := correctR.left142  have natD := correctD.left143  have rowCount := relation.count with finiteR, finiteD, sizeR, inside144  have converseInside := converse.subset at I, R, D145  have columnCount := relation.count with finiteD, finiteR, sizeD, converseInside146  have sameCount := converse.cardinality with finiteR, finiteD, inside147  have rowGraph := fiberSize.function at I, R, D with finiteD148  have columnGraph := fiberSize.function at converse(I, R, D), D, R with finiteR149  have rowWeights : ∀ r ∈ R, fiberSize(I, R, D)(r) = 0 ∨ fiberSize(I, R, D)(r) = 1 ∨ fiberSize(I, R, D)(r) = 2150    intros r hr151    have value := fiberSize.value at I, R, D, r with finiteD152    rw value153    exact rooms with r, hr154  have columnWeights : ∀ d ∈ D, fiberSize(converse(I, R, D), D, R)(d) = 0 ∨ fiberSize(converse(I, R, D), D, R)(d) = 1 ∨ fiberSize(converse(I, R, D), D, R)(d) = 2155    intros d hd156    have value := fiberSize.value at converse(I, R, D), D, R, d with finiteR157    have same := cofiber.converse at I, R, D, d with hd158    rw [value, same]159    have split := doors with d, hd160    cases split with one | two161    . right162      left163      exact one164    . right165      right166      exact two167  have rowParity := natSum.parity_of_size with finiteR, sizeR, rowWeights168  have columnParity := natSum.parity_of_size with finiteD, sizeD, columnWeights169  have rowOnes : ones(R, fiberSize(I, R, D)) = completeRooms(I, R, D)170    ext r171    constructor172    . intro hr173      have parts := ones.membership.forward with hr174      have inR := parts.left175      have value := fiberSize.value at I, R, D, r with finiteD, inR176      have weight := parts.right177      have one : cardinality(fiber(I, D, r)) = 1 by cc178      exact completeRooms.membership.backward with ⟨parts.left, one⟩179    . intro hr180      have parts := completeRooms.membership.forward with hr181      have inR := parts.left182      have value := fiberSize.value at I, R, D, r with finiteD, inR183      have count := parts.right184      have one : fiberSize(I, R, D)(r) = 1 by cc185      exact ones.membership.backward with ⟨parts.left, one⟩186  have columnOnes : ones(D, fiberSize(converse(I, R, D), D, R)) = boundaryDoors(I, R, D)187    ext d188    constructor189    . intro hd190      have parts := ones.membership.forward with hd191      have inD := parts.left192      have value := fiberSize.value at converse(I, R, D), D, R, d with finiteR, inD193      have same := cofiber.converse at I, R, D, d with parts.left194      have weight := parts.right195      have one : cardinality(cofiber(I, R, d)) = 1 by cc196      exact boundaryDoors.membership.backward with ⟨parts.left, one⟩197    . intro hd198      have parts := boundaryDoors.membership.forward with hd199      have inD := parts.left200      have value := fiberSize.value at converse(I, R, D), D, R, d with finiteR, inD201      have same := cofiber.converse at I, R, D, d with parts.left202      have count := parts.right203      have one : fiberSize(converse(I, R, D), D, R)(d) = 1 by cc204      exact ones.membership.backward with ⟨parts.left, one⟩205  rw rowOnes at rowParity206  rw columnOnes at columnParity207  rw ← rowCount at rowParity208  rw [← columnCount, sameCount] at columnParity209  have completeInside : completeRooms(I, R, D) ⊆ R210    intros r hr211    have parts := completeRooms.membership.forward with hr212    exact parts.left213  have finiteComplete := Finite.subset with finiteR, completeInside214  have correctComplete := cardinality.correct with finiteComplete215  have natComplete := correctComplete.left216  have notEvenBoundary := Odd.not_even with boundary217  have notEvenI : ¬Even(cardinality(I))218    intro evenI219    exact notEvenBoundary with (columnParity.forward with evenI)220  have notEvenComplete : ¬Even(cardinality(completeRooms(I, R, D)))221    intro evenComplete222    exact notEvenI with (rowParity.backward with evenComplete)223  have characterization := Odd.iff_not_even at cardinality(completeRooms(I, R, D))224  exact characterization.backward with notEvenComplete225