Grace/Cumulus/FixedPoint/KuhnParity.g17

Open in Workbench Download source

Imports

KuhnDoors · Cardinal.Handshake

Declarations

Source

1-- The parity step of Kuhn's lemma: rooms are the simplices of the cube,2-- doors are their faces labelled 0, …, n − 1, and the handshake count3-- turns an odd number of doors on the boundary into an odd number of4-- completely labelled simplices5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.FixedPoint.KuhnParity11import KuhnDoors12import Cardinal.Handshake1314def kuhnDoors (n lab s : Set) : Set := doorsOf(reducedMap(n, lab, s), s, n)1516-- Faces of simplices of the cube whose labels are exactly 0, …, n − 1.17def labelledFaces (p n lab : Set) : Set :=18  { f ∈ 𝒫(functionSpace(n, succ(p))) |19    (∃ s ∈ kuhnSimplices(p, n), ∃ a ∈ s, f = s ∖ {a}) ∧ labelImage(n, lab, f) = n }2021def faceIncidence (p n lab : Set) : Set :=22  { q ∈ kuhnSimplices(p, n) × labelledFaces(p, n, lab) |23    ∃ s ∈ kuhnSimplices(p, n), ∃ a ∈ s, q = (s, s ∖ {a}) }2425theorem product.components (x y A B : Set)26  requires h : (x, y) ∈ A × B27  shows x ∈ A ∧ y ∈ B28proof29  obtain ⟨bound, a, ha, b, hb, equal⟩ := product.membership.forward with h30  obtain ⟨first, second⟩ := orderedPair.injective with equal31  rw [first, second]32  exact ⟨ha, hb⟩3334theorem faceIncidence.pair (p n lab s f : Set)35  shows (s, f) ∈ faceIncidence(p, n, lab) ↔36    s ∈ kuhnSimplices(p, n) ∧ f ∈ labelledFaces(p, n, lab) ∧ ∃ a ∈ s, f = s ∖ {a}37proof38  constructor39  . intro h40    obtain ⟨inProduct, t, ht, a, ha, equal⟩ := faceIncidence.membership.forward with h41    obtain ⟨sIn, fIn⟩ := product.components with inProduct42    obtain ⟨first, second⟩ := orderedPair.injective with equal43    constructor44    . exact sIn45    . constructor46      . exact fIn47      . witness a48        constructor49        . rw first50          exact ha51        . rw first52          exact second53  . intro h54    obtain ⟨sIn, fIn, a, ha, shape⟩ := h55    apply faceIncidence.membership.backward56    constructor57    . exact product.pair with sIn, fIn58    . witness s59      constructor60      . exact sIn61      . witness a62        constructor63        . exact ha64        . rw shape65          rfl6667-- The labels of a subset, read through the map on a larger set.68theorem labelImage.restrict (n : Nat) (lab S T : Set)69  requires subset : T ⊆ S70  shows functionImage(reducedMap(n, lab, S), T, succ(n)) = labelImage(n, lab, T)71proof72  ext k73  constructor74  . intro hk75    obtain ⟨kIn, x, hx, shape⟩ := functionImage.membership.forward with hk76    have xIn := subset with x, hx77    have value := reducedMap.value at n, lab, S, x with xIn78    apply labelImage.membership.backward79    constructor80    . exact kIn81    . witness x82      constructor83      . exact hx84      . rw [shape, value]85        rfl86  . intro hk87    obtain ⟨kIn, x, hx, shape⟩ := labelImage.membership.forward with hk88    have xIn := subset with x, hx89    have value := reducedMap.value at n, lab, S, x with xIn90    apply functionImage.membership.backward91    constructor92    . exact kIn93    . witness x94      constructor95      . exact hx96      . rw [shape, value]97        rfl9899theorem kuhnDoors.membership (n : Nat) (a lab s : Set)100  shows a ∈ kuhnDoors(n, lab, s) ↔ a ∈ s ∧ labelImage(n, lab, s ∖ {a}) = n101proof102  have same : kuhnDoors(n, lab, s) = doorsOf(reducedMap(n, lab, s), s, n)103    unfold kuhnDoors104    rfl105  have face := labelImage.restrict at n, lab, s, s ∖ {a} with (difference.subset_left at s, {a})106  rw [same, ← face]107  exact doorsOf.membership108109theorem kuhnSimplices.finite_member (n p : Nat) (s : Set)110  requires hs : s ∈ kuhnSimplices(p, n)111  shows Finite(s) ∧ cardinality(s) = succ(n)112proof113  obtain ⟨base, baseFunction, bounds, upd, updBijective, shape⟩ := kuhnSimplices.shape with hs114  have updInjective := Bijective.injective with updBijective115  rw shape116  constructor117  . exact kuhnSimplex.finite with baseFunction, updInjective118  . exact kuhnSimplex.cardinality with baseFunction, updInjective119120theorem kuhnDoors.count_complete (n p : Nat) (lab s : Set)121  requires hs : s ∈ kuhnSimplices(p, n)122  requires full : labelImage(n, lab, s) = succ(n)123  shows cardinality(kuhnDoors(n, lab, s)) = 1124proof125  obtain ⟨finite, size⟩ := kuhnSimplices.finite_member with hs126  have function := reducedMap.function at n, lab, s with *127  have selfSubset : s ⊆ s128    intros x hx129    exact hx130  have image := labelImage.restrict at n, lab, s, s with selfSubset131  rw full at image132  have same : kuhnDoors(n, lab, s) = doorsOf(reducedMap(n, lab, s), s, n)133    unfold kuhnDoors134    rfl135  rw same136  exact doorsOf.complete_count with function, finite, size, image137138theorem kuhnDoors.count_incomplete (n p : Nat) (lab s : Set)139  requires hs : s ∈ kuhnSimplices(p, n)140  requires partial : labelImage(n, lab, s) ≠ succ(n)141  shows cardinality(kuhnDoors(n, lab, s)) = 0 ∨ cardinality(kuhnDoors(n, lab, s)) = 2142proof143  obtain ⟨finite, size⟩ := kuhnSimplices.finite_member with hs144  have function := reducedMap.function at n, lab, s with *145  have selfSubset : s ⊆ s146    intros x hx147    exact hx148  have image := labelImage.restrict at n, lab, s, s with selfSubset149  rw ← image at partial150  have same : kuhnDoors(n, lab, s) = doorsOf(reducedMap(n, lab, s), s, n)151    unfold kuhnDoors152    rfl153  rw same154  exact doorsOf.incomplete with function, finite, size, partial155156-- Removing a vertex, as an injective map into the subsets of the simplex.157defgraph faceOpposite (s : Set) (a ∈ s) : 𝒫(s) := s ∖ {a}158proof159  exact powerset.membership_iff.backward with (difference.subset_left at s, {a})160161theorem faceOpposite.injective (s : Set)162  shows InjectiveBetween(faceOpposite(s), s, 𝒫(s))163proof164  have function := faceOpposite.function at s165  apply Injective.of_cancel with function166  intros x hx y hy same167  have xValue := faceOpposite.value with hx168  have yValue := faceOpposite.value with hy169  rw [xValue, yValue] at same170  by_contra different171  have inY : x ∈ s ∖ {y} := difference.singleton_membership.backward with ⟨hx, different⟩172  rw ← same at inY173  have parts := difference.singleton_membership.forward with inY174  apply parts.right175  rfl176177theorem fiber.doors (n p : Nat) (lab s : Set)178  requires hs : s ∈ kuhnSimplices(p, n)179  shows fiber(faceIncidence(p, n, lab), labelledFaces(p, n, lab), s) =180    functionImage(faceOpposite(s), kuhnDoors(n, lab, s), 𝒫(s))181proof182  have sParts := kuhnSimplices.membership.forward with hs183  have sSubset := powerset.membership_iff.forward with sParts.left184  ext f185  constructor186  . intro hf187    obtain ⟨fIn, incident⟩ := fiber.membership.forward with hf188    obtain ⟨sIn, fIn2, a, ha, shape⟩ := faceIncidence.pair.forward with incident189    have fParts := labelledFaces.membership.forward with fIn190    have labels := fParts.right.right191    have value := faceOpposite.value with ha192    apply functionImage.membership.backward193    constructor194    . rw shape195      exact powerset.membership_iff.backward with (difference.subset_left at s, {a})196    . witness a197      constructor198      . apply kuhnDoors.membership.backward199        constructor200        . exact ha201        . rw ← shape202          exact labels203      . rw [shape, value]204        rfl205  . intro hf206    obtain ⟨fIn, a, ha, shape⟩ := functionImage.membership.forward with hf207    obtain ⟨aIn, labels⟩ := kuhnDoors.membership.forward with ha208    have value := faceOpposite.value with aIn209    rw value at shape210    have fInFaces : f ∈ labelledFaces(p, n, lab)211      apply labelledFaces.membership.backward212      constructor213      . apply powerset.membership_iff.backward214        rw shape215        exact Subset.transitive with (difference.subset_left at s, {a}), sSubset216      . constructor217        . witness s218          constructor219          . exact hs220          . refine ⟨a, aIn, shape⟩221        . rw shape222          exact labels223    apply fiber.membership.backward224    constructor225    . exact fInFaces226    . exact faceIncidence.pair.backward with ⟨hs, fInFaces, a, aIn, shape⟩227228theorem fiber.doors_count (n p : Nat) (lab s : Set)229  requires hs : s ∈ kuhnSimplices(p, n)230  shows cardinality(fiber(faceIncidence(p, n, lab), labelledFaces(p, n, lab), s)) =231    cardinality(kuhnDoors(n, lab, s))232proof233  have same := fiber.doors at n, p, lab, s with hs234  rw same235  have injective := faceOpposite.injective at s236  have doorsSubset : kuhnDoors(n, lab, s) ⊆ s237    intros a ha238    have parts := kuhnDoors.membership.forward with ha239    exact parts.left240  obtain ⟨finite, size⟩ := kuhnSimplices.finite_member with hs241  have finiteDoors := Finite.subset with finite, doorsSubset242  exact cardinality.injective_image with injective, doorsSubset, finiteDoors243244theorem cofiber.through (n p : Nat) (lab f : Set)245  requires hf : f ∈ labelledFaces(p, n, lab)246  shows cofiber(faceIncidence(p, n, lab), kuhnSimplices(p, n), f) = simplicesThrough(p, n, f)247proof248  ext s249  constructor250  . intro hs251    obtain ⟨sIn, incident⟩ := cofiber.membership.forward with hs252    obtain ⟨sIn2, fIn, a, ha, shape⟩ := faceIncidence.pair.forward with incident253    apply simplicesThrough.membership.backward254    constructor255    . exact sIn256    . witness a257      constructor258      . exact ha259      . symm260        exact shape261  . intro hs262    obtain ⟨sIn, b, hb, shape⟩ := simplicesThrough.membership.forward with hs263    apply cofiber.membership.backward264    constructor265    . exact sIn266    . apply faceIncidence.pair.backward267      refine ⟨sIn, hf, b, hb, ?_⟩268      symm269      exact shape270271-- A labelled face meets one simplex when it lies on a wall and two otherwise.272theorem labelledFaces.through_wall (n p : Nat) (lab f : Set)273  requires positive : 0 ∈ n274  requires hf : f ∈ labelledFaces(p, n, lab)275  requires wall : ∃ j ∈ n, (∀ x ∈ f, x(j) = 0) ∨ (∀ x ∈ f, x(j) = p)276  shows cardinality(simplicesThrough(p, n, f)) = 1277proof278  obtain ⟨inCube, witnessed, labels⟩ := labelledFaces.membership.forward with hf279  obtain ⟨s, hs, a, ha, shape⟩ := witnessed280  obtain ⟨base, baseFunction, bounds, upd, updBijective, sShape⟩ := kuhnSimplices.shape with hs281  rw sShape at ha282  rw [sShape] at shape283  obtain ⟨j, hj, flat⟩ := wall284  rw under shape at flat285  rw shape286  exact simplicesThrough.wall_count with baseFunction, updBijective, bounds, positive, ha, hj, flat287288theorem labelledFaces.through_interior (n p : Nat) (lab f : Set)289  requires positive : 0 ∈ n290  requires hf : f ∈ labelledFaces(p, n, lab)291  requires interior : ¬(∃ j ∈ n, (∀ x ∈ f, x(j) = 0) ∨ (∀ x ∈ f, x(j) = p))292  shows cardinality(simplicesThrough(p, n, f)) = 2293proof294  obtain ⟨inCube, witnessed, labels⟩ := labelledFaces.membership.forward with hf295  obtain ⟨s, hs, a, ha, shape⟩ := witnessed296  obtain ⟨base, baseFunction, bounds, upd, updBijective, sShape⟩ := kuhnSimplices.shape with hs297  rw sShape at ha298  rw [sShape] at shape299  rw shape300  have lower : ∀ j ∈ n, ∃ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) ≠ 0301    intros j hj302    by_contra none303    apply interior304    witness j305    constructor306    . exact hj307    . left308      intros x hx309      by_contra nonzero310      apply none311      witness x312      constructor313      . rw ← shape314        exact hx315      . exact nonzero316  have upper : ∀ j ∈ n, ∃ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) ≠ p317    intros j hj318    by_contra none319    apply interior320    witness j321    constructor322    . exact hj323    . right324      intros x hx325      by_contra notFull326      apply none327      witness x328      constructor329      . rw ← shape330        exact hx331      . exact notFull332  exact simplicesThrough.interior_count with baseFunction, updBijective, bounds, positive, ha, lower, upper333334theorem boundaryDoors.wall (n p : Nat) (lab f : Set)335  requires positive : 0 ∈ n336  shows f ∈ boundaryDoors(faceIncidence(p, n, lab), kuhnSimplices(p, n), labelledFaces(p, n, lab)) ↔337    f ∈ labelledFaces(p, n, lab) ∧ (∃ j ∈ n, (∀ x ∈ f, x(j) = 0) ∨ (∀ x ∈ f, x(j) = p))338proof339  constructor340  . intro hf341    obtain ⟨fIn, one⟩ := boundaryDoors.membership.forward with hf342    constructor343    . exact fIn344    . by_contra interior345      have same := cofiber.through with fIn346      rw same at one347      have two := labelledFaces.through_interior with positive, fIn, interior348      rw two at one349      arith350  . intro h351    obtain ⟨fIn, wall⟩ := h352    apply boundaryDoors.membership.backward353    constructor354    . exact fIn355    . have same := cofiber.through with fIn356      rw same357      exact labelledFaces.through_wall with positive, fIn, wall358359theorem cube.finite (n p : Nat)360  shows Finite(functionSpace(n, succ(p)))361proof362  have pairs := Finite.product with (Finite.natural at n), (Finite.natural at succ(p))363  have inside := functionSpace.subset_powerset at n, succ(p)364  exact Finite.subset with (Finite.powerset with pairs), inside365366theorem labelledFaces.finite (n p : Nat) (lab : Set)367  shows Finite(labelledFaces(p, n, lab))368proof369  have inside : labelledFaces(p, n, lab) ⊆ 𝒫(functionSpace(n, succ(p)))370    intros f hf371    have parts := labelledFaces.membership.forward with hf372    exact parts.left373  exact Finite.subset with (Finite.powerset with (cube.finite at n, p)), inside374375-- The parity step: an odd number of labelled faces on the boundary forces an376-- odd number of completely labelled simplices.377theorem kuhn.parity (n p : Nat) (lab : Set)378  requires positive : 0 ∈ n379  requires boundary : Odd(cardinality(boundaryDoors(faceIncidence(p, n, lab), kuhnSimplices(p, n), labelledFaces(p, n, lab))))380  shows Odd(cardinality(completeSimplices(p, n, lab)))381proof382  have finiteR := kuhnSimplices.finite at n, p383  have finiteD := labelledFaces.finite at n, p, lab384  have inside : faceIncidence(p, n, lab) ⊆ kuhnSimplices(p, n) × labelledFaces(p, n, lab)385    intros q hq386    have parts := faceIncidence.membership.forward with hq387    exact parts.left388  have rooms : ∀ s ∈ kuhnSimplices(p, n),389      cardinality(fiber(faceIncidence(p, n, lab), labelledFaces(p, n, lab), s)) = 0 ∨390      cardinality(fiber(faceIncidence(p, n, lab), labelledFaces(p, n, lab), s)) = 1 ∨391      cardinality(fiber(faceIncidence(p, n, lab), labelledFaces(p, n, lab), s)) = 2392    intros s hs393    have count := fiber.doors_count at n, p, lab, s with hs394    rw count395    have alternatives : labelImage(n, lab, s) = succ(n) ∨ labelImage(n, lab, s) ≠ succ(n) by tauto396    cases alternatives with full | partial397    . right398      left399      exact kuhnDoors.count_complete with hs, full400    . have split := kuhnDoors.count_incomplete with hs, partial401      cases split with zero | two402      . left403        exact zero404      . right405        right406        exact two407  have doors : ∀ f ∈ labelledFaces(p, n, lab),408      cardinality(cofiber(faceIncidence(p, n, lab), kuhnSimplices(p, n), f)) = 1 ∨409      cardinality(cofiber(faceIncidence(p, n, lab), kuhnSimplices(p, n), f)) = 2410    intros f hf411    have same := cofiber.through with hf412    rw same413    have alternatives : (∃ j ∈ n, (∀ x ∈ f, x(j) = 0) ∨ (∀ x ∈ f, x(j) = p)) ∨414        ¬(∃ j ∈ n, (∀ x ∈ f, x(j) = 0) ∨ (∀ x ∈ f, x(j) = p))415      tauto416    cases alternatives with wall | interior417    . left418      exact labelledFaces.through_wall with positive, hf, wall419    . right420      exact labelledFaces.through_interior with positive, hf, interior421  have odd := handshake with finiteR, finiteD, inside, rooms, doors, boundary422  have same : completeRooms(faceIncidence(p, n, lab), kuhnSimplices(p, n), labelledFaces(p, n, lab)) = completeSimplices(p, n, lab)423    ext s424    constructor425    . intro hs426      obtain ⟨sIn, one⟩ := completeRooms.membership.forward with hs427      apply completeSimplices.membership.backward428      constructor429      . exact sIn430      . by_contra partial431        have count := fiber.doors_count at n, p, lab, s with sIn432        rw count at one433        have split := kuhnDoors.count_incomplete with sIn, partial434        cases split with zero | two435        . rw zero at one436          arith437        . rw two at one438          arith439    . intro hs440      obtain ⟨sIn, full⟩ := completeSimplices.membership.forward with hs441      apply completeRooms.membership.backward442      constructor443      . exact sIn444      . have count := fiber.doors_count at n, p, lab, s with sIn445        rw count446        exact kuhnDoors.count_complete with sIn, full447  rwa same at odd448