Grace/Cumulus/FixedPoint/KuhnDoors.g17

Open in Workbench Download source

Imports

KuhnLabel · Cardinal.Pigeonhole

Declarations

Source

1-- Doors of a labelled simplex: the faces whose labels are exactly2-- 0, …, n − 1.  A completely labelled simplex has one door; any other3-- simplex has none or two4-- 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.FixedPoint.KuhnDoors10import KuhnLabel11import Cardinal.Pigeonhole1213-- The vertices whose opposite face carries exactly the labels below n.14def doorsOf (ℓ s n : Set) : Set := { a ∈ s | functionImage(ℓ, s ∖ {a}, succ(n)) = n }1516theorem Injective.of_cancel (f A B : Set)17  requires function : f : A → B18  requires cancel : ∀ x ∈ A, ∀ y ∈ A, f(x) = f(y) → x = y19  shows InjectiveBetween(f, A, B)20proof21  constructor22  . exact function23  . intros x hx y hy z hz hxz hyz24    have xValue := FunctionBetween.apply_value with function, hx, hxz25    have yValue := FunctionBetween.apply_value with function, hy, hyz26    have same : f(x) = f(y)27      rw [xValue, yValue]28      rfl29    have first := cancel with hx30    exact first with hy, same3132-- A completely labelled simplex: the vertex labelled n is its only door.33theorem doorsOf.complete (ℓ s : Set) (n : Nat)34  requires function : ℓ : s → succ(n)35  requires finite : Finite(s)36  requires size : cardinality(s) = succ(n)37  requires full : functionImage(ℓ, s, succ(n)) = succ(n)38  shows ∃ a ∈ s, ℓ(a) = n ∧ doorsOf(ℓ, s, n) = {a}39proof40  have nIn := bootstrap.succ.self at n41  have selfSubset : s ⊆ s42    intros x hx43    exact hx44  have imageCount : cardinality(functionImage(ℓ, s, succ(n))) = cardinality(s)45    rw [full, size]46    exact cardinality.natural47  have inImage : n ∈ functionImage(ℓ, s, succ(n)) by rwa full48  obtain ⟨inSucc, a, ha, shape⟩ := functionImage.membership.forward with inImage49  witness a50  constructor51  . exact ha52  . constructor53    . symm54      exact shape55    . ext b56      constructor57      . intro hb58        obtain ⟨bIn, door⟩ := doorsOf.membership.forward with hb59        apply singleton.membership.backward60        by_contra different61        have aRest : a ∈ s ∖ {b}62          apply difference.singleton_membership.backward63          constructor64          . exact ha65          . intro equal66            apply different67            symm68            exact equal69        have nInFace : n ∈ functionImage(ℓ, s ∖ {b}, succ(n))70          apply functionImage.membership.backward71          constructor72          . exact nIn73          . refine ⟨a, aRest, shape⟩74        rw door at nInFace75        exact membership.irreflexive with nInFace76      . intro hb77        have equal := singleton.membership.forward with hb78        rw equal79        apply doorsOf.membership.backward80        constructor81        . exact ha82        . apply Subset.antisymmetric83          . intros k hk84            obtain ⟨kIn, x, hx, kShape⟩ := functionImage.membership.forward with hk85            obtain ⟨xIn, xDifferent⟩ := difference.singleton_membership.forward with hx86            have notTop : k ≠ n87              intro same88              apply xDifferent89              have values : ℓ(x) = ℓ(a) by rwa [← kShape, same]90              exact cardinality.injective_of_image with function, selfSubset, finite, imageCount, xIn, ha, values91            have split := bootstrap.succ.membership.forward with kIn92            cases split with below | same93            . exact below94            . exfalso95              exact notTop with same96          . intros k hk97            have kInSucc := membership.into_successor with hk98            have kInImage : k ∈ functionImage(ℓ, s, succ(n)) by rwa full99            obtain ⟨kIn, x, hx, kShape⟩ := functionImage.membership.forward with kInImage100            apply functionImage.membership.backward101            constructor102            . exact kIn103            . witness x104              constructor105              . apply difference.singleton_membership.backward106                constructor107                . exact hx108                . intro xa109                  rw [xa, ← shape] at kShape110                  rw kShape at hk111                  exact membership.irreflexive with hk112              . exact kShape113114theorem doorsOf.complete_count (ℓ s : Set) (n : Nat)115  requires function : ℓ : s → succ(n)116  requires finite : Finite(s)117  requires size : cardinality(s) = succ(n)118  requires full : functionImage(ℓ, s, succ(n)) = succ(n)119  shows cardinality(doorsOf(ℓ, s, n)) = 1120proof121  obtain ⟨a, ha, label, doors⟩ := doorsOf.complete with function, finite, size, full122  rw doors123  exact cardinality.singleton124125-- No door when some label below n is missing altogether.126theorem doorsOf.empty_of_missing (ℓ s : Set) (n : Nat)127  requires missing : ¬n ⊆ functionImage(ℓ, s, succ(n))128  shows doorsOf(ℓ, s, n) = ∅129proof130  apply Subset.antisymmetric131  . intros x hx132    obtain ⟨xIn, door⟩ := doorsOf.membership.forward with hx133    exfalso134    apply missing135    have mono := functionImage.monotone at ℓ, s, succ(n), s ∖ {x}, s with (difference.subset_left at s, {x})136    rwa door at mono137  . intros x hx138    exfalso139    simpa using hx140141theorem doorsOf.image_of_covered (ℓ s : Set) (n : Nat)142  requires covered : n ⊆ functionImage(ℓ, s, succ(n))143  requires partial : functionImage(ℓ, s, succ(n)) ≠ succ(n)144  shows functionImage(ℓ, s, succ(n)) = n145proof146  have imageSubset := functionImage.subset at ℓ, s, succ(n)147  apply Subset.antisymmetric148  . intros k hk149    have kInSucc := imageSubset with k, hk150    have split := bootstrap.succ.membership.forward with kInSucc151    cases split with below | same152    . exact below153    . exfalso154      apply partial155      apply Subset.antisymmetric156      . exact imageSubset157      . intros j hj158        have split2 := bootstrap.succ.membership.forward with hj159        cases split2 with jBelow | jSame160        . exact covered with j, jBelow161        . rw jSame162          rwa same at hk163  . exact covered164165-- Labels onto n from succ(n) vertices must collide.166theorem doorsOf.collision (ℓ s : Set) (n : Nat)167  requires function : ℓ : s → succ(n)168  requires finite : Finite(s)169  requires size : cardinality(s) = succ(n)170  requires imageEq : functionImage(ℓ, s, succ(n)) = n171  shows ∃ a ∈ s, ∃ b ∈ s, a ≠ b ∧ ℓ(a) = ℓ(b)172proof173  by_contra none174  have cancel : ∀ x ∈ s, ∀ y ∈ s, ℓ(x) = ℓ(y) → x = y175    intros x hx y hy same176    by_contra different177    apply none178    witness x179    constructor180    . exact hx181    . witness y182      constructor183      . exact hy184      . exact ⟨different, same⟩185  have injective := Injective.of_cancel with function, cancel186  have selfSubset : s ⊆ s187    intros x hx188    exact hx189  have count := cardinality.injective_image with injective, selfSubset, finite190  rw [imageEq, size] at count191  have natural := cardinality.natural at n192  rw natural at count193  arith194195-- With a collision ℓ(a) = ℓ(b) and image n, the face opposite a is complete.196theorem doorsOf.face_full (ℓ s a b : Set) (n : Nat)197  requires function : ℓ : s → succ(n)198  requires imageEq : functionImage(ℓ, s, succ(n)) = n199  requires ha : a ∈ s200  requires hb : b ∈ s201  requires different : a ≠ b202  requires same : ℓ(a) = ℓ(b)203  shows functionImage(ℓ, s ∖ {a}, succ(n)) = n204proof205  have restSubset := difference.subset_left at s, {a}206  have bRest : b ∈ s ∖ {a}207    apply difference.singleton_membership.backward208    constructor209    . exact hb210    . intro equal211      apply different212      symm213      exact equal214  apply Subset.antisymmetric215  . have mono := functionImage.monotone at ℓ, s, succ(n), s ∖ {a}, s with restSubset216    rwa imageEq at mono217  . intros k hk218    have kInImage : k ∈ functionImage(ℓ, s, succ(n)) by rwa imageEq219    obtain ⟨kIn, x, hx, kShape⟩ := functionImage.membership.forward with kInImage220    apply functionImage.membership.backward221    constructor222    . exact kIn223    . have alternatives : x = a ∨ x ≠ a224        tauto225      cases alternatives with xa | xna226      . witness b227        constructor228        . exact bRest229        . rw [kShape, xa, same]230          rfl231      . refine ⟨x, (difference.singleton_membership.backward with ⟨hx, xna⟩), kShape⟩232233theorem doorsOf.of_collision (ℓ s a b : Set) (n : Nat)234  requires function : ℓ : s → succ(n)235  requires finite : Finite(s)236  requires size : cardinality(s) = succ(n)237  requires imageEq : functionImage(ℓ, s, succ(n)) = n238  requires ha : a ∈ s239  requires hb : b ∈ s240  requires different : a ≠ b241  requires same : ℓ(a) = ℓ(b)242  shows doorsOf(ℓ, s, n) = insert(a, {b})243proof244  have restSubset := difference.subset_left at s, {a}245  have restFinite := Finite.subset with finite, restSubset246  have restNat := cardinality.nat with restFinite247  have removed := cardinality.remove with finite, ha248  rw size at removed249  have restCount : cardinality(s ∖ {a}) = n250    have forward : cardinality(s ∖ {a}) ≤ n by arith251    have backward : n ≤ cardinality(s ∖ {a}) by arith252    exact LessEqual.antisymmetric with forward, backward253  have bRest : b ∈ s ∖ {a}254    apply difference.singleton_membership.backward255    constructor256    . exact hb257    . intro equal258      apply different259      symm260      exact equal261  have reversed : b ≠ a262    intro equal263    apply different264    symm265    exact equal266  have sameReversed : ℓ(b) = ℓ(a)267    symm268    exact same269  have faceA := doorsOf.face_full with function, imageEq, ha, hb, different, same270  have faceB := doorsOf.face_full with function, imageEq, hb, ha, reversed, sameReversed271  have faceCount : cardinality(functionImage(ℓ, s ∖ {a}, succ(n))) = cardinality(s ∖ {a})272    rw [faceA, restCount]273    exact cardinality.natural274  ext x275  constructor276  . intro hx277    obtain ⟨xIn, door⟩ := doorsOf.membership.forward with hx278    apply insert.membership.backward279    by_contra neither280    have notA : x ≠ a281      intro equal282      apply neither283      left284      exact equal285    have notB : x ≠ b286      intro equal287      apply neither288      right289      exact singleton.membership.backward with equal290    have xRest : x ∈ s ∖ {a} := difference.singleton_membership.backward with ⟨xIn, notA⟩291    have valueIn : ℓ(x) ∈ functionImage(ℓ, s ∖ {x}, succ(n))292      rw door293      have inImage : ℓ(x) ∈ functionImage(ℓ, s, succ(n))294        apply functionImage.membership.backward295        constructor296        . exact FunctionBetween.apply_closed with function, xIn297        . witness x298          constructor299          . exact xIn300          . rfl301      rwa imageEq at inImage302    obtain ⟨vIn, y, hy, yShape⟩ := functionImage.membership.forward with valueIn303    obtain ⟨yIn, yDifferent⟩ := difference.singleton_membership.forward with hy304    have alternatives : y = a ∨ y ≠ a by tauto305    cases alternatives with ya | yna306    . have values : ℓ(x) = ℓ(b)307        rw [yShape, ya, same]308        rfl309      have equal := cardinality.injective_of_image with function, restSubset, restFinite, faceCount, xRest, bRest, values310      exact notB with equal311    . have yRest : y ∈ s ∖ {a} := difference.singleton_membership.backward with ⟨yIn, yna⟩312      have equal := cardinality.injective_of_image with function, restSubset, restFinite, faceCount, xRest, yRest, yShape313      apply yDifferent314      symm315      exact equal316  . intro hx317    have split := insert.membership.forward with hx318    apply doorsOf.membership.backward319    cases split with xa | xb320    . rw xa321      exact ⟨ha, faceA⟩322    . have equal := singleton.membership.forward with xb323      rw equal324      exact ⟨hb, faceB⟩325326theorem doorsOf.incomplete (ℓ s : Set) (n : Nat)327  requires function : ℓ : s → succ(n)328  requires finite : Finite(s)329  requires size : cardinality(s) = succ(n)330  requires partial : functionImage(ℓ, s, succ(n)) ≠ succ(n)331  shows cardinality(doorsOf(ℓ, s, n)) = 0 ∨ cardinality(doorsOf(ℓ, s, n)) = 2332proof333  have alternatives : n ⊆ functionImage(ℓ, s, succ(n)) ∨ ¬n ⊆ functionImage(ℓ, s, succ(n)) by tauto334  cases alternatives with covered | missing335  . right336    have imageEq := doorsOf.image_of_covered with covered, partial337    obtain ⟨a, ha, b, hb, different, same⟩ := doorsOf.collision with function, finite, size, imageEq338    have doors := doorsOf.of_collision with function, finite, size, imageEq, ha, hb, different, same339    rw doors340    have fresh : ¬a ∈ {b}341      intro inside342      exact different with (singleton.membership.forward with inside)343    have count := cardinality.insert with (Finite.singleton at b), fresh344    have one := cardinality.singleton at b345    rw [count, one]346    rfl347  . left348    have doors := doorsOf.empty_of_missing with missing349    rw [doors, ← nat.zero]350    exact cardinality.natural351