Grace/Cumulus/FixedPoint/KuhnTopFace.g17

Open in Workbench Download source

Imports

KuhnRotation

Declarations

Source

1-- Kuhn simplices through the face opposite the top vertex: lowering the base2-- at the last raised coordinate and shifting the permutation the other way3-- gives the second simplex through such a face4-- 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.KuhnTopFace10import KuhnRotation1112-- The inverse cyclic shift sends 0 to n − 1 and l + 1 to l.13def unrotation (n : Set) : Set := converse(rotation(n), n, n)1415theorem unrotation.bijective (n : Nat)16  shows BijectiveBetween(unrotation(n), n, n)17proof18  have turn := rotation.bijective at n19  unfold unrotation20  exact converse.bijective with turn2122theorem unrotation.step (n : Nat) (l : Set)23  requires hl : l ∈ n24  requires hs : succ(l) ∈ n25  shows unrotation(n)(succ(l)) = l26proof27  have turn := rotation.step with hl, hs28  have bijective := rotation.bijective at n29  have same : unrotation(n)(succ(l)) = converse(rotation(n), n, n)(succ(l))30    unfold unrotation31    rfl32  rw [same, ← turn]33  exact Bijective.inverse_apply with bijective, hl3435theorem unrotation.wrap (n : Nat) (m : Set)36  requires hm : m ∈ n37  requires top : succ(m) = n38  shows unrotation(n)(0) = m39proof40  have turn := rotation.wrap with hm, top41  have bijective := rotation.bijective at n42  have same : unrotation(n)(0) = converse(rotation(n), n, n)(0)43    unfold unrotation44    rfl45  rw [same, ← turn]46  exact Bijective.inverse_apply with bijective, hm4748def unrotated (n upd : Set) : Set := compose(upd, unrotation(n), n, n, n)4950theorem unrotated.bijective (n : Nat) (upd : Set)51  requires updBijective : BijectiveBetween(upd, n, n)52  shows BijectiveBetween(unrotated(n, upd), n, n)53proof54  have turn := unrotation.bijective at n55  unfold unrotated56  exact compose.bijective with turn, updBijective5758theorem unrotated.value (n : Nat) (upd l : Set)59  requires updBijective : BijectiveBetween(upd, n, n)60  requires hl : l ∈ n61  shows unrotated(n, upd)(l) = upd(unrotation(n)(l))62proof63  have updFunction := Injective.function with (Bijective.injective with updBijective)64  have turn := Injective.function with (Bijective.injective with (unrotation.bijective at n))65  have same : unrotated(n, upd)(l) = compose(upd, unrotation(n), n, n, n)(l)66    unfold unrotated67    rfl68  rw same69  exact compose.apply with turn, updFunction, hl7071theorem unrotated.step (n : Nat) (upd l : Set)72  requires updBijective : BijectiveBetween(upd, n, n)73  requires hl : l ∈ n74  requires hs : succ(l) ∈ n75  shows unrotated(n, upd)(succ(l)) = upd(l)76proof77  have value := unrotated.value with updBijective, hs78  have turn := unrotation.step with hl, hs79  rw [value, turn]80  rfl8182theorem unrotated.wrap (n : Nat) (upd m : Set)83  requires updBijective : BijectiveBetween(upd, n, n)84  requires hm : m ∈ n85  requires top : succ(m) = n86  shows unrotated(n, upd)(0) = upd(m)87proof88  have mNat := natural.member at n with hm89  have mLess := Less.of_membership with hm90  have zeroLess : 0 < n by arith91  have zeroIn := membership.of_Less with zeroLess92  have value := unrotated.value with updBijective, zeroIn93  have turn := unrotation.wrap with hm, top94  rw [value, turn]95  rfl9697-- The first k + 1 shifted coordinates are upd(n − 1) and the first k of the98-- original.99theorem raised.unrotated (n : Nat) (upd m k : Set)100  requires updBijective : BijectiveBetween(upd, n, n)101  requires hm : m ∈ n102  requires top : succ(m) = n103  requires hk : k ∈ n104  shows raised(n, unrotated(n, upd), succ(k)) = insert(upd(m), raised(n, upd, k))105proof106  have updFunction := Injective.function with (Bijective.injective with updBijective)107  have kNat := natural.member at n with hk108  have kLess := Less.of_membership with hk109  have kInside := Ordinal.member_subset with (Ordinal.natural at n), hk110  ext y111  constructor112  . intro hy113    obtain ⟨inN, l, hl, shape⟩ := raised.membership.forward with hy114    have lNat := natural.member at succ(k) with hl115    have lLess := Less.of_membership with hl116    have split := natural.zero_or_successor with lNat117    apply insert.membership.backward118    cases split with zero | successor119    . left120      have value := unrotated.wrap with updBijective, hm, top121      rw [shape, zero, value]122      rfl123    . right124      obtain ⟨l2, l2Nat, lEq⟩ := successor125      rw lEq at lLess126      have l2Less : l2 < k by arith127      have l2In := membership.of_Less with l2Less128      have l2InN := kInside with l2, l2In129      have sLess : succ(l2) < n by arith130      have sIn := membership.of_Less with sLess131      have value := unrotated.step with updBijective, l2InN, sIn132      apply raised.membership.backward133      constructor134      . exact inN135      . witness l2136        constructor137        . exact l2In138        . rw [shape, lEq, value]139          rfl140  . intro hy141    have split := insert.membership.forward with hy142    cases split with same | below143    . have value := unrotated.wrap with updBijective, hm, top144      apply raised.membership.backward145      constructor146      . rw same147        exact FunctionBetween.apply_closed with updFunction, hm148      . witness 0149        constructor150        . have less : 0 < succ(k) by arith151          exact membership.of_Less with less152        . rw [same, value]153          rfl154    . obtain ⟨inN, l, hl, shape⟩ := raised.membership.forward with below155      have lInN := kInside with l, hl156      have lNat := natural.member at n with lInN157      have lLess := Less.of_membership with hl158      have sLess : succ(l) < n by arith159      have sIn := membership.of_Less with sLess160      have value := unrotated.step with updBijective, lInN, sIn161      apply raised.membership.backward162      constructor163      . exact inN164      . witness succ(l)165        constructor166        . have less : succ(l) < succ(k) by arith167          exact membership.of_Less with less168        . rw [shape, value]169          rfl170171theorem raised.unrotated_fresh (n : Nat) (upd m k : Set)172  requires updBijective : BijectiveBetween(upd, n, n)173  requires hm : m ∈ n174  requires top : succ(m) = n175  requires hk : k ∈ n176  shows ¬upd(m) ∈ raised(n, upd, k)177proof178  have updInjective := Bijective.injective with updBijective179  have mNat := natural.member at n with hm180  have kNat := natural.member at n with hk181  have kLess := Less.of_membership with hk182  have kInside := Ordinal.member_subset with (Ordinal.natural at n), hk183  intro inside184  obtain ⟨inN, l, hl, shape⟩ := raised.membership.forward with inside185  have lInN := kInside with l, hl186  have lNat := natural.member at n with lInN187  have lLess := Less.of_membership with hl188  have same := Injective.apply_cancel with updInjective, hm, lInN, shape189  rw ← top at kLess190  arith191192-- The base lowered by one at coordinate upd(m): the unique function with193-- lowered(j) + [j = upd(m)] = base(j).194defunique loweredValue (n base upd m j : Set) (y ∈ ℕ) := y + indicator({upd(m)}, j) = base(j)195requires baseFunction : base : n → ℕ196requires rooted : 0 < base(upd(m))197requires hj : j ∈ n198proof199  have baseIn := FunctionBetween.apply_closed with baseFunction, hj200  have baseNat := nat.omega.backward with baseIn201  have alternatives : j = upd(m) ∨ j ≠ upd(m) by tauto202  cases alternatives with same | different203  . have positive : 0 < base(j)204      rwa same205    have shape := natural.zero_or_successor with baseNat206    cases shape with zero | successor207    . exfalso208      rw zero at positive209      arith210    . obtain ⟨k, kNat, eq⟩ := successor211      have kIn := nat.omega.forward with kNat212      refine ⟨k, kIn, ?_⟩213      have one : indicator({upd(m)}, j) = 1214        rw same215        exact indicator.singleton_self216      rw [one, eq]217      exact add.right_one218  . have separated : upd(m) ≠ j219      intro equal220      apply different221      symm222      exact equal223    have zero := indicator.singleton_other with separated224    refine ⟨base(j), baseIn, ?_⟩225    rw zero226    exact add.right_unit227uniqueness228  intros u hu first v hv second229  have uNat := nat.omega.backward with hu230  have vNat := nat.omega.backward with hv231  have same : u + indicator({upd(m)}, j) = v + indicator({upd(m)}, j)232    rw [first, second]233    rfl234  exact add.right_cancel with same235236defgraph lowered (n base upd m : Set) (j ∈ n) : ℕ := loweredValue(n, base, upd, m, j)237requires baseFunction : base : n → ℕ238requires rooted : 0 < base(upd(m))239proof240  have selected := loweredValue.selected at n, base, upd, m, j with *241  exact selected.left242243theorem lowered.restores (n : Nat) (base upd m j : Set)244  requires baseFunction : base : n → ℕ245  requires rooted : 0 < base(upd(m))246  requires hj : j ∈ n247  shows lowered(n, base, upd, m)(j) + indicator({upd(m)}, j) = base(j)248proof249  have value := lowered.value at n, base, upd, m, j with *250  have selected := loweredValue.selected at n, base, upd, m, j with *251  rw value252  exact selected.right253254-- The lowered simplex lists a new bottom followed by vertices 0, …, n − 1 of255-- the original.256theorem kuhnVertex.unrotated (n : Nat) (base upd m k : Set)257  requires baseFunction : base : n → ℕ258  requires updBijective : BijectiveBetween(upd, n, n)259  requires hm : m ∈ n260  requires top : succ(m) = n261  requires rooted : 0 < base(upd(m))262  requires hk : k ∈ n263  shows kuhnVertex(n, lowered(n, base, upd, m), unrotated(n, upd))(succ(k)) = kuhnVertex(n, base, upd)(k)264proof265  have lowFunction := lowered.function with baseFunction, rooted266  have kNat := natural.member at n with hk267  have kLess := Less.of_membership with hk268  have kInSucc := membership.into_successor with hk269  have sLess : succ(k) < succ(n) by arith270  have sIn := membership.of_Less with sLess271  have leftFunction := kuhnVertex.function_on at n, lowered(n, base, upd, m), unrotated(n, upd), succ(k) with lowFunction, sIn272  have rightFunction := kuhnVertex.function_on at n, base, upd, k with baseFunction, kInSucc273  apply FunctionBetween.ext with leftFunction, rightFunction274  intros j hj275  have leftValue := kuhnVertex.coordinate at n, lowered(n, base, upd, m), unrotated(n, upd), succ(k), j with lowFunction, sIn, hj276  have rightValue := kuhnVertex.coordinate at n, base, upd, k, j with baseFunction, kInSucc, hj277  have image := raised.unrotated with updBijective, hm, top, hk278  have fresh := raised.unrotated_fresh with updBijective, hm, top, hk279  have split := indicator.insert_fresh at upd(m), raised(n, upd, k), j with fresh280  have restores := lowered.restores with baseFunction, rooted, hj281  have lowNat := nat.omega.backward with (FunctionBetween.apply_closed with lowFunction, hj)282  rw [leftValue, rightValue, image, split, ← restores]283  exact add.associative_reverse284285theorem kuhnSimplex.unrotated_face (n : Nat) (base upd m : Set)286  requires baseFunction : base : n → ℕ287  requires updBijective : BijectiveBetween(upd, n, n)288  requires hm : m ∈ n289  requires top : succ(m) = n290  requires rooted : 0 < base(upd(m))291  shows kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(n)} =292    kuhnSimplex(n, lowered(n, base, upd, m), unrotated(n, upd)) ∖293      {kuhnVertex(n, lowered(n, base, upd, m), unrotated(n, upd))(0)}294proof295  have updInjective := Bijective.injective with updBijective296  have lowFunction := lowered.function with baseFunction, rooted297  have unrotatedInjective := Bijective.injective with (unrotated.bijective with updBijective)298  have zeroLess : 0 < succ(n) by arith299  have zeroIn := membership.of_Less with zeroLess300  have nIn := bootstrap.succ.self at n301  ext x302  constructor303  . intro hx304    have parts := difference.singleton_membership.forward with hx305    obtain ⟨inSpace, k, hk, shape⟩ := kuhnSimplex.membership.forward with parts.left306    have kIn : k ∈ n307      have split := bootstrap.succ.membership.forward with hk308      cases split with below | same309      . exact below310      . exfalso311        apply parts.right312        rw [shape, same]313        rfl314    have kNat := natural.member at n with kIn315    have kLess := Less.of_membership with kIn316    have sLess : succ(k) < succ(n) by arith317    have sIn := membership.of_Less with sLess318    have agree := kuhnVertex.unrotated with baseFunction, updBijective, hm, top, rooted, kIn319    apply difference.singleton_membership.backward320    constructor321    . rw [shape, ← agree]322      exact kuhnVertex.member with lowFunction, sIn323    . intro equal324      rw [shape, ← agree] at equal325      have same := kuhnVertex.injective with lowFunction, unrotatedInjective, sIn, zeroIn, equal326      arith327  . intro hx328    have parts := difference.singleton_membership.forward with hx329    obtain ⟨inSpace, l, hl, shape⟩ := kuhnSimplex.membership.forward with parts.left330    have lNat := natural.member at succ(n) with hl331    have lLess := Less.of_membership with hl332    have split := natural.zero_or_successor with lNat333    cases split with zero | successor334    . exfalso335      apply parts.right336      rw [shape, zero]337      rfl338    . obtain ⟨k, kNat, lEq⟩ := successor339      rw lEq at lLess340      have kLess : k < n by arith341      have kIn := membership.of_Less with kLess342      have kInSucc := membership.into_successor with kIn343      have agree := kuhnVertex.unrotated with baseFunction, updBijective, hm, top, rooted, kIn344      apply difference.singleton_membership.backward345      constructor346      . rw [shape, lEq, agree]347        exact kuhnVertex.member with baseFunction, kInSucc348      . intro equal349        rw [shape, lEq, agree] at equal350        have same := kuhnVertex.injective with baseFunction, updInjective, kInSucc, nIn, equal351        rw same at kIn352        exact membership.irreflexive with kIn353354-- Away from the top vertex, coordinate upd(n − 1) is constant on a simplex.355theorem kuhnSimplex.top_face_constant (n : Nat) (base upd m x : Set)356  requires baseFunction : base : n → ℕ357  requires updBijective : BijectiveBetween(upd, n, n)358  requires hm : m ∈ n359  requires top : succ(m) = n360  requires hx : x ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(n)}361  shows x(upd(m)) = base(upd(m))362proof363  have updFunction := Injective.function with (Bijective.injective with updBijective)364  have jIn := FunctionBetween.apply_closed with updFunction, hm365  have parts := difference.singleton_membership.forward with hx366  obtain ⟨inSpace, k, hk, shape⟩ := kuhnSimplex.membership.forward with parts.left367  have kIn : k ∈ n368    have split := bootstrap.succ.membership.forward with hk369    cases split with below | same370    . exact below371    . exfalso372      apply parts.right373      rw [shape, same]374      rfl375  have fresh := raised.unrotated_fresh with updBijective, hm, top, kIn376  have zero := indicator.absent with fresh377  have value := kuhnVertex.coordinate at n, base, upd, k, upd(m) with baseFunction, hk, jIn378  have baseNat := nat.omega.backward with (FunctionBetween.apply_closed with baseFunction, jIn)379  rw [shape, value, zero]380  exact add.right_unit381382-- A top face off the wall x_{upd(n − 1)} = 0 has a positive base coordinate383-- there, so the lowered base exists.384theorem kuhnSimplex.top_face_rooted (n : Nat) (base upd m : Set)385  requires baseFunction : base : n → ℕ386  requires updBijective : BijectiveBetween(upd, n, n)387  requires hm : m ∈ n388  requires top : succ(m) = n389  requires notZero : ∃ x ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(n)}, x(upd(m)) ≠ 0390  shows 0 < base(upd(m))391proof392  have updFunction := Injective.function with (Bijective.injective with updBijective)393  have jIn := FunctionBetween.apply_closed with updFunction, hm394  have baseNat := nat.omega.backward with (FunctionBetween.apply_closed with baseFunction, jIn)395  obtain ⟨x, hx, apart⟩ := notZero396  have constant := kuhnSimplex.top_face_constant with baseFunction, updBijective, hm, top, hx397  rw constant at apart398  have shape := natural.zero_or_successor with baseNat399  cases shape with zero | successor400  . exfalso401    exact apart with zero402  . obtain ⟨k, kNat, eq⟩ := successor403    rw eq404    arith405406-- Through the face opposite the top vertex there are exactly the original407-- simplex and its lowering.408theorem kuhnSimplex.top_face_neighbours (n : Nat) (base upd m b2 u2 c : Set)409  requires baseFunction : base : n → ℕ410  requires updBijective : BijectiveBetween(upd, n, n)411  requires hm : m ∈ n412  requires top : succ(m) = n413  requires rooted : 0 < base(upd(m))414  requires f2 : b2 : n → ℕ415  requires bij2 : BijectiveBetween(u2, n, n)416  requires hc : c ∈ kuhnSimplex(n, b2, u2)417  requires same : kuhnSimplex(n, b2, u2) ∖ {c} = kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(n)}418  shows kuhnSimplex(n, b2, u2) = kuhnSimplex(n, base, upd) ∨419    kuhnSimplex(n, b2, u2) = kuhnSimplex(n, lowered(n, base, upd, m), unrotated(n, upd))420proof421  have updFunction := Injective.function with (Bijective.injective with updBijective)422  have injective2 := Bijective.injective with bij2423  have jIn := FunctionBetween.apply_closed with updFunction, hm424  have mNat := natural.member at n with hm425  have mLess := Less.of_membership with hm426  have zeroLess : 0 < n by arith427  have positive := membership.of_Less with zeroLess428  have lowFunction := lowered.function with baseFunction, rooted429  have unrotatedBijective := unrotated.bijective with updBijective430  obtain ⟨inSpace, k, hk, shape⟩ := kuhnSimplex.membership.forward with hc431  have constant : ∀ l ∈ succ(n), l ≠ k → kuhnVertex(n, b2, u2)(l)(upd(m)) = base(upd(m))432    intros l hl different433    have vertexMember := kuhnVertex.member at n, b2, u2, l with f2, hl434    have inFace : kuhnVertex(n, b2, u2)(l) ∈ kuhnSimplex(n, b2, u2) ∖ {c}435      apply difference.singleton_membership.backward436      constructor437      . exact vertexMember438      . intro equal439        rw shape at equal440        have index := kuhnVertex.injective with f2, injective2, hl, hk, equal441        exact different with index442    rw same at inFace443    exact kuhnSimplex.top_face_constant with baseFunction, updBijective, hm, top, inFace444  have index := kuhnSimplex.constant_face_index with f2, bij2, hk, jIn, constant445  cases index with zero | topIndex446  . right447    rw [shape, zero] at same448    have face := kuhnSimplex.unrotated_face with baseFunction, updBijective, hm, top, rooted449    rw face at same450    exact kuhnSimplex.eq_bottom with f2, bij2, lowFunction, unrotatedBijective, positive, same451  . left452    rw [shape, topIndex] at same453    exact kuhnSimplex.eq_top with f2, bij2, baseFunction, updBijective, positive, same454455theorem kuhnSimplex.unrotated_ne (n : Nat) (base upd m : Set)456  requires baseFunction : base : n → ℕ457  requires updBijective : BijectiveBetween(upd, n, n)458  requires hm : m ∈ n459  requires top : succ(m) = n460  requires rooted : 0 < base(upd(m))461  shows kuhnSimplex(n, lowered(n, base, upd, m), unrotated(n, upd)) ≠ kuhnSimplex(n, base, upd)462proof463  have updInjective := Bijective.injective with updBijective464  have lowFunction := lowered.function with baseFunction, rooted465  have unrotatedInjective := Bijective.injective with (unrotated.bijective with updBijective)466  have mNat := natural.member at n with hm467  have mLess := Less.of_membership with hm468  have zeroLess : 0 < n by arith469  have positive := membership.of_Less with zeroLess470  have zeroIn := membership.into_successor with positive471  have oneLess : succ(0) < succ(n) by arith472  have oneIn := membership.of_Less with oneLess473  intro equal474  have bottomMember := kuhnVertex.member at n, lowered(n, base, upd, m), unrotated(n, upd), 0 with lowFunction, zeroIn475  rw equal at bottomMember476  have bounds := kuhnSimplex.sum_bounds with baseFunction, updInjective, bottomMember477  have bottomSum := kuhnVertex.sum with lowFunction, unrotatedInjective, zeroIn478  have oneSum := kuhnVertex.sum with lowFunction, unrotatedInjective, oneIn479  have agree := kuhnVertex.unrotated with baseFunction, updBijective, hm, top, rooted, positive480  have zeroSum := kuhnVertex.sum with baseFunction, updInjective, zeroIn481  rw [agree, zeroSum] at oneSum482  have lower := bounds.left483  rw bottomSum at lower484  have baseWeights : ∀ j ∈ n, base(j) ∈ ℕ485    intros j hj486    exact FunctionBetween.apply_closed with baseFunction, hj487  have baseSum := natSum.natural with (Finite.natural at n), baseWeights488  have lowWeights : ∀ j ∈ n, lowered(n, base, upd, m)(j) ∈ ℕ489    intros j hj490    exact FunctionBetween.apply_closed with lowFunction, hj491  have lowSum := natSum.natural with (Finite.natural at n), lowWeights492  arith493