Grace/Cumulus/FixedPoint/KuhnRotation.g17

Open in Workbench Download source

Imports

KuhnFaces · Nat.CyclicShift

Declarations

Source

1-- Kuhn simplices through the face opposite the bottom vertex: rotating the2-- permutation moves the bottom vertex to the top, and the two simplices3-- through such a face are the original one and its rotation4-- 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.KuhnRotation10import KuhnFaces11import Nat.CyclicShift1213def rotated (n upd : Set) : Set := compose(upd, rotation(n), n, n, n)1415theorem rotated.bijective (n : Nat) (upd : Set)16  requires updBijective : BijectiveBetween(upd, n, n)17  shows BijectiveBetween(rotated(n, upd), n, n)18proof19  have turn := rotation.bijective at n20  unfold rotated21  exact compose.bijective with turn, updBijective2223theorem rotated.value (n : Nat) (upd l : Set)24  requires updBijective : BijectiveBetween(upd, n, n)25  requires hl : l ∈ n26  shows rotated(n, upd)(l) = upd(rotation(n)(l))27proof28  have updFunction := Injective.function with (Bijective.injective with updBijective)29  have turn := rotation.function at n with *30  have same : rotated(n, upd)(l) = compose(upd, rotation(n), n, n, n)(l)31    unfold rotated32    rfl33  rw same34  exact compose.apply with turn, updFunction, hl3536theorem rotated.step (n : Nat) (upd l : Set)37  requires updBijective : BijectiveBetween(upd, n, n)38  requires hl : l ∈ n39  requires hs : succ(l) ∈ n40  shows rotated(n, upd)(l) = upd(succ(l))41proof42  have value := rotated.value with updBijective, hl43  have turn := rotation.step with hl, hs44  rw [value, turn]45  rfl4647theorem rotated.wrap (n : Nat) (upd l : Set)48  requires updBijective : BijectiveBetween(upd, n, n)49  requires hl : l ∈ n50  requires top : succ(l) = n51  shows rotated(n, upd)(l) = upd(0)52proof53  have value := rotated.value with updBijective, hl54  have turn := rotation.wrap with hl, top55  rw [value, turn]56  rfl5758-- The first k rotated coordinates are coordinates 1, …, k of the original.59theorem raised.rotated (n : Nat) (upd k : Set)60  requires updBijective : BijectiveBetween(upd, n, n)61  requires hk : k ∈ n62  shows raised(n, upd, succ(k)) = insert(upd(0), raised(n, rotated(n, upd), k))63proof64  have updFunction := Injective.function with (Bijective.injective with updBijective)65  have kNat := natural.member at n with hk66  have kLess := Less.of_membership with hk67  have kInside := Ordinal.member_subset with (Ordinal.natural at n), hk68  have zeroLess : 0 < n by arith69  have zeroIn := membership.of_Less with zeroLess70  ext y71  constructor72  . intro hy73    obtain ⟨inN, m, hm, shape⟩ := raised.membership.forward with hy74    have mNat := natural.member at succ(k) with hm75    have mLess := Less.of_membership with hm76    have split := natural.zero_or_successor with mNat77    apply insert.membership.backward78    cases split with zero | successor79    . left80      rw [shape, zero]81      rfl82    . right83      obtain ⟨l, lNat, mEq⟩ := successor84      rw mEq at mLess85      have lLess : l < k by arith86      have lIn := membership.of_Less with lLess87      have lInN := kInside with l, lIn88      have sLess : succ(l) < n by arith89      have sIn := membership.of_Less with sLess90      have value := rotated.step with updBijective, lInN, sIn91      apply raised.membership.backward92      constructor93      . exact inN94      . witness l95        constructor96        . exact lIn97        . rw [shape, mEq, value]98          rfl99  . intro hy100    have split := insert.membership.forward with hy101    cases split with same | below102    . apply raised.membership.backward103      constructor104      . rw same105        exact FunctionBetween.apply_closed with updFunction, zeroIn106      . witness 0107        constructor108        . have less : 0 < succ(k) by arith109          exact membership.of_Less with less110        . exact same111    . obtain ⟨inN, l, hl, shape⟩ := raised.membership.forward with below112      have lInN := kInside with l, hl113      have lNat := natural.member at n with lInN114      have lLess := Less.of_membership with hl115      have sLess : succ(l) < n by arith116      have sIn := membership.of_Less with sLess117      have value := rotated.step with updBijective, lInN, sIn118      apply raised.membership.backward119      constructor120      . exact inN121      . witness succ(l)122        constructor123        . have less : succ(l) < succ(k) by arith124          exact membership.of_Less with less125        . rw [shape, value]126          rfl127128theorem raised.rotated_fresh (n : Nat) (upd k : Set)129  requires updBijective : BijectiveBetween(upd, n, n)130  requires hk : k ∈ n131  shows ¬upd(0) ∈ raised(n, rotated(n, upd), k)132proof133  have updInjective := Bijective.injective with updBijective134  have kNat := natural.member at n with hk135  have kLess := Less.of_membership with hk136  have kInside := Ordinal.member_subset with (Ordinal.natural at n), hk137  have zeroLess : 0 < n by arith138  have zeroIn := membership.of_Less with zeroLess139  intro inside140  obtain ⟨inN, l, hl, shape⟩ := raised.membership.forward with inside141  have lInN := kInside with l, hl142  have lNat := natural.member at n with lInN143  have lLess := Less.of_membership with hl144  have sLess : succ(l) < n by arith145  have sIn := membership.of_Less with sLess146  have value := rotated.step with updBijective, lInN, sIn147  rw value at shape148  have same := Injective.apply_cancel with updInjective, zeroIn, sIn, shape149  arith150151theorem indicator.insert_fresh (a A j : Set)152  requires fresh : ¬a ∈ A153  shows indicator(insert(a, A), j) = indicator({a}, j) + indicator(A, j)154proof155  have alternatives : j = a ∨ j ≠ a by tauto156  cases alternatives with same | different157  . have inInsert : j ∈ insert(a, A)158      apply insert.membership.backward159      left160      exact same161    have absent : ¬j ∈ A by rwa same162    have one := indicator.member with inInsert163    have self : indicator({a}, j) = 1164      rw same165      exact indicator.singleton_self166    have zero := indicator.absent with absent167    rw [one, self, zero]168    arith169  . have equivalent : j ∈ insert(a, A) ↔ j ∈ A170      constructor171      . intro h172        have split := insert.membership.forward with h173        cases split with equal | inside174        . exfalso175          exact different with equal176        . exact inside177      . intro h178        apply insert.membership.backward179        right180        exact h181    have same := indicator.congr with equivalent182    have separated : a ≠ j183      intro equal184      apply different185      symm186      exact equal187    have zero := indicator.singleton_other with separated188    rw [same, zero]189    ring190191-- The rotated simplex, based at the second vertex, lists vertices 1, …, n192-- of the original followed by a new top.193theorem kuhnVertex.rotated (n : Nat) (base upd k : Set)194  requires baseFunction : base : n → ℕ195  requires updBijective : BijectiveBetween(upd, n, n)196  requires hk : k ∈ n197  shows kuhnVertex(n, kuhnVertex(n, base, upd)(succ(0)), rotated(n, upd))(k) = kuhnVertex(n, base, upd)(succ(k))198proof199  have updInjective := Bijective.injective with updBijective200  have kNat := natural.member at n with hk201  have kLess := Less.of_membership with hk202  have zeroLess : 0 < n by arith203  have positive := membership.of_Less with zeroLess204  have oneLess : succ(0) < succ(n) by arith205  have oneIn := membership.of_Less with oneLess206  have kInSucc := membership.into_successor with hk207  have sLess : succ(k) < succ(n) by arith208  have sIn := membership.of_Less with sLess209  have oneFunction := kuhnVertex.function_on at n, base, upd, succ(0) with baseFunction, oneIn210  have leftFunction := kuhnVertex.function_on at n, kuhnVertex(n, base, upd)(succ(0)), rotated(n, upd), k with oneFunction, kInSucc211  have rightFunction := kuhnVertex.function_on at n, base, upd, succ(k) with baseFunction, sIn212  apply FunctionBetween.ext with leftFunction, rightFunction213  intros j hj214  have leftValue := kuhnVertex.coordinate at n, kuhnVertex(n, base, upd)(succ(0)), rotated(n, upd), k, j with oneFunction, kInSucc, hj215  have oneValue := kuhnVertex.coordinate_succ with baseFunction, updInjective, positive, hj216  have zeroValue := kuhnVertex.zero_coordinate at n, base, upd, j with baseFunction, hj217  have rightValue := kuhnVertex.coordinate at n, base, upd, succ(k), j with baseFunction, sIn, hj218  have image := raised.rotated with updBijective, hk219  have fresh := raised.rotated_fresh with updBijective, hk220  have split := indicator.insert_fresh at upd(0), raised(n, rotated(n, upd), k), j with fresh221  have baseNatural := FunctionBetween.apply_closed with baseFunction, hj222  have baseNat := nat.omega.backward with baseNatural223  rw [leftValue, oneValue, zeroValue, rightValue, image, split]224  exact add.associative225226theorem kuhnSimplex.rotated_face (n : Nat) (base upd : Set)227  requires baseFunction : base : n → ℕ228  requires updBijective : BijectiveBetween(upd, n, n)229  requires positive : 0 ∈ n230  shows kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(0)} =231    kuhnSimplex(n, kuhnVertex(n, base, upd)(succ(0)), rotated(n, upd)) ∖232      {kuhnVertex(n, kuhnVertex(n, base, upd)(succ(0)), rotated(n, upd))(n)}233proof234  have updInjective := Bijective.injective with updBijective235  have rotatedInjective := Bijective.injective with (rotated.bijective with updBijective)236  have zeroLess := Less.of_membership with positive237  have oneLess : succ(0) < succ(n) by arith238  have oneIn := membership.of_Less with oneLess239  have oneFunction := kuhnVertex.function_on at n, base, upd, succ(0) with baseFunction, oneIn240  have zeroIn := membership.into_successor with positive241  have nIn := bootstrap.succ.self at n242  ext x243  constructor244  . intro hx245    have parts := difference.singleton_membership.forward with hx246    obtain ⟨inSpace, k, hk, shape⟩ := kuhnSimplex.membership.forward with parts.left247    have kNat := natural.member at succ(n) with hk248    have kLess := Less.of_membership with hk249    have split := natural.zero_or_successor with kNat250    cases split with zero | successor251    . exfalso252      apply parts.right253      rw [shape, zero]254      rfl255    . obtain ⟨m, mNat, kEq⟩ := successor256      rw kEq at kLess257      have mLess : m < n by arith258      have mIn := membership.of_Less with mLess259      have mInSucc := membership.into_successor with mIn260      have agree := kuhnVertex.rotated with baseFunction, updBijective, mIn261      apply difference.singleton_membership.backward262      constructor263      . rw [shape, kEq, ← agree]264        exact kuhnVertex.member with oneFunction, mInSucc265      . intro equal266        rw [shape, kEq, ← agree] at equal267        have same := kuhnVertex.injective with oneFunction, rotatedInjective, mInSucc, nIn, equal268        rw same at mIn269        exact membership.irreflexive with mIn270  . intro hx271    have parts := difference.singleton_membership.forward with hx272    obtain ⟨inSpace, m, hm, shape⟩ := kuhnSimplex.membership.forward with parts.left273    have mIn : m ∈ n274      have split := bootstrap.succ.membership.forward with hm275      cases split with below | same276      . exact below277      . exfalso278        apply parts.right279        rw [shape, same]280        rfl281    have mNat := natural.member at n with mIn282    have mLess := Less.of_membership with mIn283    have sLess : succ(m) < succ(n) by arith284    have sIn := membership.of_Less with sLess285    have agree := kuhnVertex.rotated with baseFunction, updBijective, mIn286    apply difference.singleton_membership.backward287    constructor288    . rw [shape, agree]289      exact kuhnVertex.member with baseFunction, sIn290    . intro equal291      rw [shape, agree] at equal292      have same := kuhnVertex.injective with baseFunction, updInjective, sIn, zeroIn, equal293      arith294295-- Away from the bottom vertex, coordinate upd(0) is constant on a simplex.296theorem kuhnSimplex.bottom_face_constant (n : Nat) (base upd x : Set)297  requires baseFunction : base : n → ℕ298  requires updBijective : BijectiveBetween(upd, n, n)299  requires positive : 0 ∈ n300  requires hx : x ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(0)}301  shows x(upd(0)) = kuhnVertex(n, base, upd)(succ(0))(upd(0))302proof303  have updFunction := Injective.function with (Bijective.injective with updBijective)304  have jIn := FunctionBetween.apply_closed with updFunction, positive305  have zeroLess := Less.of_membership with positive306  have oneLess : succ(0) < succ(n) by arith307  have oneIn := membership.of_Less with oneLess308  have parts := difference.singleton_membership.forward with hx309  obtain ⟨inSpace, k, hk, shape⟩ := kuhnSimplex.membership.forward with parts.left310  have kNat := natural.member at succ(n) with hk311  have zeroInK : 0 ∈ k312    have split := natural.zero_or_successor with kNat313    cases split with zero | successor314    . exfalso315      apply parts.right316      rw [shape, zero]317      rfl318    . obtain ⟨m, mNat, kEq⟩ := successor319      rw kEq320      have less : 0 < succ(m) by arith321      exact membership.of_Less with less322  have raisedK : upd(0) ∈ raised(n, upd, k)323    apply raised.membership.backward324    constructor325    . exact jIn326    . witness 0327      constructor328      . exact zeroInK329      . rfl330  have raisedOne : upd(0) ∈ raised(n, upd, succ(0))331    apply raised.membership.backward332    constructor333    . exact jIn334    . witness 0335      constructor336      . exact bootstrap.succ.self at 0337      . rfl338  have valueK := kuhnVertex.coordinate at n, base, upd, k, upd(0) with baseFunction, hk, jIn339  have valueOne := kuhnVertex.coordinate at n, base, upd, succ(0), upd(0) with baseFunction, oneIn, jIn340  have oneK := indicator.member with raisedK341  have oneOne := indicator.member with raisedOne342  rw [shape, valueK, valueOne, oneK, oneOne]343  rfl344345-- If every vertex but the k-th shares a coordinate value, the k-th vertex is346-- the bottom or the top.347theorem kuhnSimplex.constant_face_index (n : Nat) (base upd k j v : Set)348  requires baseFunction : base : n → ℕ349  requires updBijective : BijectiveBetween(upd, n, n)350  requires hk : k ∈ succ(n)351  requires hj : j ∈ n352  requires constant : ∀ m ∈ succ(n), m ≠ k → kuhnVertex(n, base, upd)(m)(j) = v353  shows k = 0 ∨ k = n354proof355  by_contra neither356  have notZero : 0 ≠ k357    intro same358    apply neither359    left360    symm361    exact same362  have notTop : n ≠ k363    intro same364    apply neither365    right366    symm367    exact same368  have zeroLess : 0 < succ(n) by arith369  have zeroIn := membership.of_Less with zeroLess370  have nIn := bootstrap.succ.self at n371  have atZero := constant with zeroIn, notZero372  have atTop := constant with nIn, notTop373  have zeroValue := kuhnVertex.zero_coordinate at n, base, upd, j with baseFunction, hj374  have topValue := kuhnVertex.top_coordinate with baseFunction, updBijective, hj375  rw zeroValue at atZero376  rw topValue at atTop377  have baseNatural := FunctionBetween.apply_closed with baseFunction, hj378  rw ← atZero at atTop379  arith380381-- Through the face opposite the bottom vertex there are exactly the original382-- simplex and its rotation.383theorem kuhnSimplex.bottom_face_neighbours (n : Nat) (base upd b2 u2 c : Set)384  requires baseFunction : base : n → ℕ385  requires updBijective : BijectiveBetween(upd, n, n)386  requires f2 : b2 : n → ℕ387  requires bij2 : BijectiveBetween(u2, n, n)388  requires positive : 0 ∈ n389  requires hc : c ∈ kuhnSimplex(n, b2, u2)390  requires same : kuhnSimplex(n, b2, u2) ∖ {c} = kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(0)}391  shows kuhnSimplex(n, b2, u2) = kuhnSimplex(n, base, upd) ∨392    kuhnSimplex(n, b2, u2) = kuhnSimplex(n, kuhnVertex(n, base, upd)(succ(0)), rotated(n, upd))393proof394  have updFunction := Injective.function with (Bijective.injective with updBijective)395  have injective2 := Bijective.injective with bij2396  have jIn := FunctionBetween.apply_closed with updFunction, positive397  have zeroLess := Less.of_membership with positive398  have oneLess : succ(0) < succ(n) by arith399  have oneIn := membership.of_Less with oneLess400  have oneFunction := kuhnVertex.function_on at n, base, upd, succ(0) with baseFunction, oneIn401  have rotatedBijective := rotated.bijective with updBijective402  obtain ⟨inSpace, k, hk, shape⟩ := kuhnSimplex.membership.forward with hc403  have constant : ∀ m ∈ succ(n), m ≠ k → kuhnVertex(n, b2, u2)(m)(upd(0)) = kuhnVertex(n, base, upd)(succ(0))(upd(0))404    intros m hm different405    have vertexMember := kuhnVertex.member at n, b2, u2, m with f2, hm406    have inFace : kuhnVertex(n, b2, u2)(m) ∈ kuhnSimplex(n, b2, u2) ∖ {c}407      apply difference.singleton_membership.backward408      constructor409      . exact vertexMember410      . intro equal411        rw shape at equal412        have index := kuhnVertex.injective with f2, injective2, hm, hk, equal413        exact different with index414    rw same at inFace415    exact kuhnSimplex.bottom_face_constant with baseFunction, updBijective, positive, inFace416  have index := kuhnSimplex.constant_face_index with f2, bij2, hk, jIn, constant417  cases index with zero | top418  . left419    rw [shape, zero] at same420    exact kuhnSimplex.eq_bottom with f2, bij2, baseFunction, updBijective, positive, same421  . right422    rw [shape, top] at same423    have face := kuhnSimplex.rotated_face with baseFunction, updBijective, positive424    rw face at same425    exact kuhnSimplex.eq_top with f2, bij2, oneFunction, rotatedBijective, positive, same426427theorem kuhnSimplex.rotated_ne (n : Nat) (base upd : Set)428  requires baseFunction : base : n → ℕ429  requires updBijective : BijectiveBetween(upd, n, n)430  requires positive : 0 ∈ n431  shows kuhnSimplex(n, kuhnVertex(n, base, upd)(succ(0)), rotated(n, upd)) ≠ kuhnSimplex(n, base, upd)432proof433  have updInjective := Bijective.injective with updBijective434  have rotatedInjective := Bijective.injective with (rotated.bijective with updBijective)435  have zeroLess := Less.of_membership with positive436  have oneLess : succ(0) < succ(n) by arith437  have oneIn := membership.of_Less with oneLess438  have oneFunction := kuhnVertex.function_on at n, base, upd, succ(0) with baseFunction, oneIn439  have nIn := bootstrap.succ.self at n440  intro equal441  have topMember := kuhnVertex.member at n, kuhnVertex(n, base, upd)(succ(0)), rotated(n, upd), n with oneFunction, nIn442  rw equal at topMember443  have bounds := kuhnSimplex.sum_bounds with baseFunction, updInjective, topMember444  have topSum := kuhnVertex.sum with oneFunction, rotatedInjective, nIn445  have oneSum := kuhnVertex.sum with baseFunction, updInjective, oneIn446  have upper := bounds.right447  rw [topSum, oneSum] at upper448  have baseWeights : ∀ j ∈ n, base(j) ∈ ℕ449    intros j hj450    exact FunctionBetween.apply_closed with baseFunction, hj451  have baseSum := natSum.natural with (Finite.natural at n), baseWeights452  arith453