Grace/Cumulus/Combinatorics/RamseyChain.g17

Open in Workbench Download source

Imports

RamseyPigeonhole · Set.Choice

Declarations

Source

1-- The Ramsey chain: from an infinite set S and a colouring of its2-- (n + 1)-subsets, a descending sequence of infinite stages Sᵢ ⊆ S with3-- distinguished points aᵢ ∈ Sᵢ ∖ Sᵢ₊₁, where every n-subset T of Sᵢ₊₁4-- gives insert(aᵢ, T) one colour cᵢ. Each stage is chosen among the5-- homogeneous subsets that the Ramsey property for n provides.6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Combinatorics.RamseyChain12import RamseyPigeonhole13import Set.Choice1415-- Every colouring of the n-subsets of an infinite set with colours in K has16-- an infinite homogeneous subset.17predicate RamseyProperty (n K : Set) :=18  ∀ S, ∀ C, Infinite(S) → FunctionBetween(C, subsetsOfSize(S, n), K) →19    ∃ H, H ⊆ S ∧ Infinite(H) ∧20      ∃ c ∈ K, ∀ U ∈ subsetsOfSize(H, n), C(U) = c2122-- The colouring of the n-subsets of Y obtained from a colouring C of the23-- (n + 1)-subsets of S by adjoining a point a of S outside Y.24defgraph inducedColouring (C S Y a K : Set, n : Nat) (T ∈ subsetsOfSize(Y, n)) : K :=25  C(insert(a, T))26requires colouring : C : subsetsOfSize(S, n + 1) → K27requires subset : Y ⊆ S28requires ha : a ∈ S29requires fresh : ¬a ∈ Y30proof31  have memberS := subsetsOfSize.member_of_subset with subset, member32  have tSubset := subsetsOfSize.subset with member33  have freshT : ¬a ∈ T34    intro inT35    exact fresh with (tSubset with a, inT)36  have inserted := subsetsOfSize.insert_member with memberS, ha, freshT37  exact FunctionBetween.apply_closed with colouring, inserted3839-- The infinite subsets of Y on whose n-subsets D is constant.40def homogeneousSubsets (D K Y : Set, n : Nat) : Set :=41  { Z ∈ 𝒫(Y) | Infinite(Z) ∧42      ∃ c ∈ K, ∀ U ∈ subsetsOfSize(Z, n), D(U) = c }4344-- A chosen infinite subset of Y homogeneous for the induced colouring.45def homogeneousChoice (C S Y a K : Set, n : Nat) : Set :=46  choose(homogeneousSubsets(inducedColouring(C, S, Y, a, K, n), K, Y, n))4748theorem homogeneousChoice.value (C S Y a K : Set, n : Nat)49  shows homogeneousChoice(C, S, Y, a, K, n) =50    choose(homogeneousSubsets(inducedColouring(C, S, Y, a, K, n), K, Y, n))51proof52  simp [homogeneousChoice]5354theorem homogeneousChoice.properties (C S Y a K : Set, n : Nat)55  requires ramsey : RamseyProperty(n, K)56  requires colouring : C : subsetsOfSize(S, n + 1) → K57  requires subset : Y ⊆ S58  requires ha : a ∈ S59  requires fresh : ¬a ∈ Y60  requires infinite : Infinite(Y)61  shows homogeneousChoice(C, S, Y, a, K, n) ⊆ Y ∧62    Infinite(homogeneousChoice(C, S, Y, a, K, n)) ∧63    ∃ c ∈ K,64      ∀ T ∈ subsetsOfSize(homogeneousChoice(C, S, Y, a, K, n), n),65        C(insert(a, T)) = c66proof67  have induced := inducedColouring.function at C, S, Y, a, K, n with68    colouring, subset, ha, fresh69  obtain ⟨H, hH, hInfinite, c, hc, homogeneous⟩ :=70    ramsey with Y, inducedColouring(C, S, Y, a, K, n), infinite, induced71  have candidate : H ∈ homogeneousSubsets(inducedColouring(C, S, Y, a, K, n), K, Y, n)72    have power := powerset.membership_iff.backward with hH73    apply homogeneousSubsets.membership.backward74    exact ⟨power, hInfinite, c, hc, homogeneous⟩75  have inhabited : Nonempty(homogeneousSubsets(inducedColouring(C, S, Y, a, K, n), K, Y, n)) :=76    ⟨H, candidate⟩77  have selected := choose.member with inhabited78  rw ← homogeneousChoice.value at selected79  obtain ⟨power, chosenInfinite, d, hd, chosenHomogeneous⟩ :=80    homogeneousSubsets.membership.forward with selected81  have chosenSubset := powerset.membership_iff.forward with power82  refine ⟨chosenSubset, chosenInfinite, d, hd, ?_⟩83  intros T hT84  have memberY := subsetsOfSize.member_of_subset with chosenSubset, hT85  have value := inducedColouring.value at C, S, Y, a, K, n, T with86    colouring, subset, ha, fresh, memberY87  rw ← value88  exact chosenHomogeneous with T, hT8990-- One step of the chain: remove the chosen point of X and pass to a91-- homogeneous infinite subset of what remains.92def ramseyStep (C S K X : Set, n : Nat) : Set :=93  homogeneousChoice(C, S, X ∖ {choose(X)}, choose(X), K, n)9495theorem ramseyStep.value (C S K X : Set, n : Nat)96  shows ramseyStep(C, S, K, X, n) =97    homogeneousChoice(C, S, X ∖ {choose(X)}, choose(X), K, n)98proof99  simp [ramseyStep]100101theorem ramseyStep.properties (C S K X : Set, n : Nat)102  requires ramsey : RamseyProperty(n, K)103  requires colouring : C : subsetsOfSize(S, n + 1) → K104  requires subset : X ⊆ S105  requires infinite : Infinite(X)106  shows ramseyStep(C, S, K, X, n) ⊆ X ∖ {choose(X)} ∧107    Infinite(ramseyStep(C, S, K, X, n)) ∧108    ∃ c ∈ K, ∀ T ∈ subsetsOfSize(ramseyStep(C, S, K, X, n), n),109      C(insert(choose(X), T)) = c110proof111  have chosen := choose.member with (Infinite.nonempty with infinite)112  have inS := subset with choose(X), chosen113  have restSubset : X ∖ {choose(X)} ⊆ S :=114    Subset.transitive with (difference.subset_left at X, {choose(X)}), subset115  have restInfinite := Infinite.remove at X, choose(X) with infinite116  have fresh : ¬choose(X) ∈ X ∖ {choose(X)} by117    simp [difference.membership, singleton.membership]118  have parts := homogeneousChoice.properties with119    ramsey, colouring, restSubset, inS, fresh, restInfinite120  simpa [ramseyStep.value] using parts121122-- The stages and their points.123124def ramseyStage (C S K : Set, n : Nat, i : Nat) → Set125  | C, S, K, n, zero => S126  | C, S, K, n, succ(k) => ramseyStep(C, S, K, ramseyStage(C, S, K, n, k), n)127128theorem ramseyStage.zero (C S K : Set, n : Nat)129  shows ramseyStage(C, S, K, n, 0) = S130proof131  simp [ramseyStage]132133theorem ramseyStage.succ (C S K : Set, n : Nat, k : Nat)134  shows ramseyStage(C, S, K, n, k + 1) =135    ramseyStep(C, S, K, ramseyStage(C, S, K, n, k), n)136proof137  have one : k + 1 = succ(k) := add.right_one with *138  rw one139  simp [ramseyStage]140141def ramseyPoint (C S K : Set, n : Nat, i : Nat) : Set :=142  choose(ramseyStage(C, S, K, n, i))143144theorem ramseyPoint.value (C S K : Set, n : Nat, i : Nat)145  shows ramseyPoint(C, S, K, n, i) = choose(ramseyStage(C, S, K, n, i))146proof147  simp [ramseyPoint]148149section RamseyChain150variable (C S K : Set) (n : Nat)151hypothesis ramsey : RamseyProperty(n, K)152hypothesis colouring : FunctionBetween(C, subsetsOfSize(S, n + 1), K)153hypothesis infinite : Infinite(S)154155theorem ramseyStage.invariant (i : Nat)156  shows ramseyStage(C, S, K, n, i) ⊆ S ∧157    Infinite(ramseyStage(C, S, K, n, i))158proof159  induction i160  | zero =>161    rw ramseyStage.zero162    exact ⟨Subset.reflexive at S, infinite⟩163  | k + 1 using ih =>164    rw ramseyStage.succ165    obtain ⟨subsetK, infiniteK⟩ := ih166    obtain ⟨next, nextInfinite, _⟩ := ramseyStep.properties at167      C, S, K, ramseyStage(C, S, K, n, k), n with168      ramsey, colouring, subsetK, infiniteK169    have rest := difference.subset_left at170      ramseyStage(C, S, K, n, k), {choose(ramseyStage(C, S, K, n, k))}171    have nextSubset : ramseyStep(C, S, K, ramseyStage(C, S, K, n, k), n) ⊆ S :=172      Subset.transitive with (Subset.transitive with next, rest), subsetK173    exact ⟨nextSubset, nextInfinite⟩174175theorem ramseyStage.subset (i : Nat)176  shows ramseyStage(C, S, K, n, i) ⊆ S177proof178  have parts := ramseyStage.invariant at C, S, K, n, i with *179  exact parts.left180181theorem ramseyStage.infinite (i : Nat)182  shows Infinite(ramseyStage(C, S, K, n, i))183proof184  have parts := ramseyStage.invariant at C, S, K, n, i with *185  exact parts.right186187theorem ramseyPoint.member (i : Nat)188  shows ramseyPoint(C, S, K, n, i) ∈ ramseyStage(C, S, K, n, i)189proof190  have stageInfinite := ramseyStage.infinite at C, S, K, n, i with *191  rw ramseyPoint.value192  exact choose.member with (Infinite.nonempty with stageInfinite)193194theorem ramseyPoint.in_set (i : Nat)195  shows ramseyPoint(C, S, K, n, i) ∈ S196proof197  have stageSubset := ramseyStage.subset at C, S, K, n, i with *198  have member := ramseyPoint.member at C, S, K, n, i with *199  exact stageSubset with ramseyPoint(C, S, K, n, i), member200201theorem ramseyStage.step (i : Nat)202  shows ramseyStage(C, S, K, n, i + 1) ⊆203      ramseyStage(C, S, K, n, i) ∖ {ramseyPoint(C, S, K, n, i)} ∧204    ∃ c ∈ K, ∀ T ∈ subsetsOfSize(ramseyStage(C, S, K, n, i + 1), n),205      C(insert(ramseyPoint(C, S, K, n, i), T)) = c206proof207  have stageSubset := ramseyStage.subset at C, S, K, n, i with *208  have stageInfinite := ramseyStage.infinite at C, S, K, n, i with *209  obtain ⟨next, _, c, hc, homogeneous⟩ := ramseyStep.properties at210    C, S, K, ramseyStage(C, S, K, n, i), n with211    ramsey, colouring, stageSubset, stageInfinite212  constructor213  . rw [ramseyStage.succ, ramseyPoint.value]214    exact next215  . refine ⟨c, hc, ?_⟩216    intros T hT217    rw ramseyStage.succ at hT218    rw ramseyPoint.value219    exact homogeneous with T, hT220221theorem ramseyStage.succ_subset (i : Nat)222  shows ramseyStage(C, S, K, n, i + 1) ⊆223    ramseyStage(C, S, K, n, i) ∖ {ramseyPoint(C, S, K, n, i)}224proof225  have parts := ramseyStage.step at C, S, K, n, i with *226  exact parts.left227228theorem ramseyStage.succ_homogeneous (i : Nat)229  shows ∃ c ∈ K, ∀ T ∈ subsetsOfSize(ramseyStage(C, S, K, n, i + 1), n),230    C(insert(ramseyPoint(C, S, K, n, i), T)) = c231proof232  have parts := ramseyStage.step at C, S, K, n, i with *233  exact parts.right234235theorem ramseyStage.antitone (i d : Nat)236  shows ramseyStage(C, S, K, n, i + d) ⊆ ramseyStage(C, S, K, n, i)237proof238  induction d239  | zero =>240    have same : i + 0 = i by ring241    rw same242    exact Subset.reflexive at ramseyStage(C, S, K, n, i)243  | k + 1 using ih =>244    have shape : i + (k + 1) = (i + k) + 1 by ring245    rw shape246    have step := ramseyStage.succ_subset at C, S, K, n, i + k with247      ramsey, colouring, infinite248    have rest := difference.subset_left at249      ramseyStage(C, S, K, n, i + k), {ramseyPoint(C, S, K, n, i + k)}250    exact Subset.transitive with (Subset.transitive with step, rest), ih251252theorem ramseyStage.monotone (i j : Nat)253  requires le : i ≤ j254  shows ramseyStage(C, S, K, n, j) ⊆ ramseyStage(C, S, K, n, i)255proof256  obtain ⟨d, dNat, shape⟩ := le257  rw ← shape258  exact ramseyStage.antitone at C, S, K, n, i, d with *259260-- Later points lie in every earlier successor stage, so the points are261-- pairwise distinct.262theorem ramseyPoint.later_member (i j : Nat)263  requires below : i < j264  shows ramseyPoint(C, S, K, n, j) ∈ ramseyStage(C, S, K, n, i + 1)265proof266  have le := Less.gap.forward with below267  have nested := ramseyStage.monotone at C, S, K, n, i + 1, j with *268  have member := ramseyPoint.member at C, S, K, n, j with *269  exact nested with ramseyPoint(C, S, K, n, j), member270271theorem ramseyPoint.distinct (i j : Nat)272  requires below : i < j273  shows ramseyPoint(C, S, K, n, i) ≠ ramseyPoint(C, S, K, n, j)274proof275  intro same276  have later := ramseyPoint.later_member at C, S, K, n, i, j with *277  have excluded := ramseyStage.succ_subset at C, S, K, n, i with *278  have inRest := excluded with ramseyPoint(C, S, K, n, j), later279  have parts := difference.singleton_membership.forward with inRest280  apply parts.right281  symm282  exact same283284theorem ramseyPoint.injective_on (i j : Nat)285  requires same : ramseyPoint(C, S, K, n, i) = ramseyPoint(C, S, K, n, j)286  shows i = j287proof288  have alternatives := Less.trichotomy at i, j with *289  rcases alternatives with below | equal | above290  . exfalso291    have distinct := ramseyPoint.distinct at C, S, K, n, i, j with *292    exact distinct with same293  . exact equal294  . exfalso295    have distinct := ramseyPoint.distinct at C, S, K, n, j, i with *296    apply distinct297    symm298    exact same299300end RamseyChain301302-- The colour of stage i: the colour that every n-subset T of Sᵢ₊₁303-- gives to insert(aᵢ, T).304def ramseyColours (C S K : Set, n : Nat, i : Nat) : Set :=305  { c ∈ K | ∀ T ∈ subsetsOfSize(ramseyStage(C, S, K, n, i + 1), n),306      C(insert(ramseyPoint(C, S, K, n, i), T)) = c }307308def ramseyColour (C S K : Set, n : Nat, i : Nat) : Set :=309  choose(ramseyColours(C, S, K, n, i))310311section RamseyColour312variable (C S K : Set) (n : Nat)313hypothesis ramsey : RamseyProperty(n, K)314hypothesis colouring : FunctionBetween(C, subsetsOfSize(S, n + 1), K)315hypothesis infinite : Infinite(S)316317theorem ramseyColour.properties (i : Nat)318  shows ramseyColour(C, S, K, n, i) ∈ K ∧319    ∀ T ∈ subsetsOfSize(ramseyStage(C, S, K, n, i + 1), n),320      C(insert(ramseyPoint(C, S, K, n, i), T)) = ramseyColour(C, S, K, n, i)321proof322  obtain ⟨c, hc, law⟩ :=323    ramseyStage.succ_homogeneous at C, S, K, n, i with *324  have candidate : c ∈ ramseyColours(C, S, K, n, i) :=325    ramseyColours.membership.backward with ⟨hc, law⟩326  have inhabited : Nonempty(ramseyColours(C, S, K, n, i)) := ⟨c, candidate⟩327  have selected : ramseyColour(C, S, K, n, i) ∈ ramseyColours(C, S, K, n, i)328    unfold ramseyColour329    exact choose.member with inhabited330  exact ramseyColours.membership.forward with selected331332theorem ramseyColour.member (i : Nat)333  shows ramseyColour(C, S, K, n, i) ∈ K334proof335  have parts := ramseyColour.properties at C, S, K, n, i with *336  exact parts.left337338theorem ramseyColour.law (T : Set) (i : Nat)339  requires hT : T ∈ subsetsOfSize(ramseyStage(C, S, K, n, i + 1), n)340  shows C(insert(ramseyPoint(C, S, K, n, i), T)) = ramseyColour(C, S, K, n, i)341proof342  have parts := ramseyColour.properties at C, S, K, n, i with *343  exact parts.right with T, hT344345end RamseyColour346