Grace/Cumulus/FixedPoint/KuhnWallSimplex.g17

Open in Workbench Download source

Imports

KuhnExtend

Declarations

Source

1-- The far-wall face of a Kuhn simplex, restricted to the lower cube, is a2-- Kuhn simplex of one dimension less: its base is the restricted base and3-- its permutation is the rotated permutation restricted4-- 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.KuhnWallSimplex10import KuhnExtend1112def wallPerm (m u : Set) : Set := restrict(rotated(succ(m), u), m)1314-- A bijection of succ(m) fixing m restricts to a bijection of m.15theorem Bijective.restrict_fixed (m : Nat) (g : Set)16  requires bijective : BijectiveBetween(g, succ(m), succ(m))17  requires fixed : g(m) = m18  shows BijectiveBetween(restrict(g, m), m, m)19proof20  have injective := Bijective.injective with bijective21  have function := Injective.function with injective22  have mSubset := successor.subset at m23  have mIn := bootstrap.succ.self at m24  have closed : ∀ l ∈ m, g(l) ∈ m25    intros l hl26    have lIn := membership.into_successor with hl27    have valueIn := FunctionBetween.apply_closed with function, lIn28    have split := bootstrap.succ.membership.forward with valueIn29    cases split with below | same30    . exact below31    . exfalso32      rw ← fixed at same33      have equal := Injective.apply_cancel with injective, lIn, mIn, same34      rw equal at hl35      exact membership.irreflexive with hl36  have restricted := restrict.function with function, mSubset, closed37  constructor38  . apply Injective.of_cancel with restricted39    intros x hx y hy same40    have xValue := restrict.domain_apply with function, mSubset, hx41    have yValue := restrict.domain_apply with function, mSubset, hy42    rw [xValue, yValue] at same43    have xIn := membership.into_successor with hx44    have yIn := membership.into_successor with hy45    exact Injective.apply_cancel with injective, xIn, yIn, same46  . constructor47    . exact restricted48    . intros y hy49      obtain ⟨fn, law⟩ := Bijective.surjective with bijective50      have yIn := membership.into_successor with hy51      obtain ⟨l, hl, edge⟩ := law with yIn52      have value := FunctionBetween.apply_value with function, hl, edge53      have lBelow : l ∈ m54        have split := bootstrap.succ.membership.forward with hl55        cases split with below | same56        . exact below57        . exfalso58          rw [same, fixed] at value59          rw ← value at hy60          exact membership.irreflexive with hy61      witness l62      constructor63      . exact lBelow64      . have restrictedValue := restrict.domain_apply with function, mSubset, lBelow65        have edge2 := FunctionBetween.relates_apply with restricted, lBelow66        rwa [restrictedValue, value] at edge26768theorem wallPerm.bijective (m : Nat) (u : Set)69  requires updBijective : BijectiveBetween(u, succ(m), succ(m))70  requires first : u(0) = m71  shows BijectiveBetween(wallPerm(m, u), m, m)72proof73  have turned := rotated.bijective with updBijective74  have mIn := bootstrap.succ.self at m75  have top : succ(m) = succ(m) by rfl76  have fixed := rotated.wrap with updBijective, mIn, top77  rw first at fixed78  have same : wallPerm(m, u) = restrict(rotated(succ(m), u), m)79    unfold wallPerm80    rfl81  rw same82  exact Bijective.restrict_fixed with turned, fixed8384theorem wallPerm.value (m : Nat) (u l : Set)85  requires updBijective : BijectiveBetween(u, succ(m), succ(m))86  requires hl : l ∈ m87  shows wallPerm(m, u)(l) = u(succ(l))88proof89  have turned := rotated.bijective with updBijective90  have turnedFunction := Injective.function with (Bijective.injective with turned)91  have mSubset := successor.subset at m92  have lIn := membership.into_successor with hl93  have lNat := natural.member at m with hl94  have lLess := Less.of_membership with hl95  have sLess : succ(l) < succ(m) by arith96  have sIn := membership.of_Less with sLess97  have same : wallPerm(m, u) = restrict(rotated(succ(m), u), m)98    unfold wallPerm99    rfl100  rw same101  have value := restrict.domain_apply with turnedFunction, mSubset, hl102  rw value103  exact rotated.step with updBijective, lIn, sIn104105-- Below the far wall, the raised coordinates of the restricted simplex are106-- those of the original one step up.107theorem raised.wall_iff (m : Nat) (u k j : Set)108  requires updBijective : BijectiveBetween(u, succ(m), succ(m))109  requires first : u(0) = m110  requires hk : k ∈ succ(m)111  requires hj : j ∈ m112  shows j ∈ raised(m, wallPerm(m, u), k) ↔ j ∈ raised(succ(m), u, succ(k))113proof114  have kNat := natural.member at succ(m) with hk115  have kLess := Less.of_membership with hk116  have kInside := Ordinal.member_subset with (Ordinal.natural at succ(m)), hk117  have jIn := membership.into_successor with hj118  constructor119  . intro inside120    obtain ⟨inM, l, hl, shape⟩ := raised.membership.forward with inside121    have lIn := kInside with l, hl122    have lBelow : l ∈ m123      have lNat := natural.member at succ(m) with lIn124      have lLess := Less.of_membership with hl125      have less : l < m by arith126      exact membership.of_Less with less127    have value := wallPerm.value with updBijective, lBelow128    apply raised.membership.backward129    constructor130    . exact jIn131    . witness succ(l)132      constructor133      . have lNat := natural.member at m with lBelow134        have lLess := Less.of_membership with hl135        have less : succ(l) < succ(k) by arith136        exact membership.of_Less with less137      . rw [shape, value]138        rfl139  . intro inside140    obtain ⟨inSucc, i, hi, shape⟩ := raised.membership.forward with inside141    have iNat := natural.member at succ(k) with hi142    have iLess := Less.of_membership with hi143    have split := natural.zero_or_successor with iNat144    cases split with zero | successor145    . exfalso146      rw [zero, first] at shape147      rw shape at hj148      exact membership.irreflexive with hj149    . obtain ⟨l, lNat, iEq⟩ := successor150      rw iEq at iLess151      have lLess : l < k by arith152      have lIn := membership.of_Less with lLess153      have lBelow : l < m by arith154      have lInM := membership.of_Less with lBelow155      have value := wallPerm.value with updBijective, lInM156      apply raised.membership.backward157      constructor158      . exact hj159      . witness l160        constructor161        . exact lIn162        . rw [shape, iEq, value]163          rfl164165theorem kuhnVertex.wall (m : Nat) (b u k : Set)166  requires baseFunction : b : succ(m) → ℕ167  requires updBijective : BijectiveBetween(u, succ(m), succ(m))168  requires first : u(0) = m169  requires hk : k ∈ succ(m)170  shows restrict(kuhnVertex(succ(m), b, u)(succ(k)), m) = kuhnVertex(m, restrict(b, m), wallPerm(m, u))(k)171proof172  have mSubset := successor.subset at m173  have kNat := natural.member at succ(m) with hk174  have kLess := Less.of_membership with hk175  have sLess : succ(k) < succ(succ(m)) by arith176  have sIn := membership.of_Less with sLess177  have restrictedBase := restrict.domain_function with baseFunction, mSubset178  have vertexFunction := kuhnVertex.function_on at succ(m), b, u, succ(k) with baseFunction, sIn179  have leftFunction := restrict.domain_function with vertexFunction, mSubset180  have rightFunction := kuhnVertex.function_on at m, restrict(b, m), wallPerm(m, u), k with restrictedBase, hk181  apply FunctionBetween.ext with leftFunction, rightFunction182  intros j hj183  have leftValue := restrict.domain_apply with vertexFunction, mSubset, hj184  have jIn := membership.into_successor with hj185  have coordinate := kuhnVertex.coordinate at succ(m), b, u, succ(k), j with baseFunction, sIn, jIn186  have rightValue := kuhnVertex.coordinate at m, restrict(b, m), wallPerm(m, u), k, j with restrictedBase, hk, hj187  have baseValue := restrict.domain_apply with baseFunction, mSubset, hj188  have equivalent := raised.wall_iff with updBijective, first, hk, hj189  have same := indicator.congr with equivalent190  rw [leftValue, coordinate, rightValue, baseValue, same]191  rfl192193-- The far-wall face of a simplex, restricted, is the simplex one dimension194-- down with the restricted base and the rotated permutation restricted.195theorem kuhnSimplex.wall_face (m p : Nat) (b u : Set)196  requires baseFunction : b : succ(m) → ℕ197  requires bounds : ∀ j ∈ succ(m), b(j) < p198  requires updBijective : BijectiveBetween(u, succ(m), succ(m))199  requires first : u(0) = m200  shows functionImage(cubeRestrict(m, p), kuhnSimplex(succ(m), b, u) ∖ {kuhnVertex(succ(m), b, u)(0)}, functionSpace(m, succ(p))) =201    kuhnSimplex(m, restrict(b, m), wallPerm(m, u))202proof203  have updInjective := Bijective.injective with updBijective204  have mSubset := successor.subset at m205  have restrictedBase := restrict.domain_function with baseFunction, mSubset206  have zeroLess : 0 < succ(succ(m)) by arith207  have zeroIn := membership.of_Less with zeroLess208  ext y209  constructor210  . intro hy211    obtain ⟨yIn, x, hx, yShape⟩ := functionImage.membership.forward with hy212    have parts := difference.singleton_membership.forward with hx213    obtain ⟨inSpace, i, hi, xShape⟩ := kuhnSimplex.membership.forward with parts.left214    have xInCube : x ∈ functionSpace(succ(m), succ(p))215      rw xShape216      exact kuhnVertex.into_cube with baseFunction, bounds, hi217    have value := cubeRestrict.value with xInCube218    have iNat := natural.member at succ(succ(m)) with hi219    have iLess := Less.of_membership with hi220    have split := natural.zero_or_successor with iNat221    cases split with zero | successor222    . exfalso223      apply parts.right224      rw [xShape, zero]225      rfl226    . obtain ⟨k, kNat, iEq⟩ := successor227      rw iEq at iLess228      have kLess : k < succ(m) by arith229      have kIn := membership.of_Less with kLess230      have agree := kuhnVertex.wall with baseFunction, updBijective, first, kIn231      rw [yShape, value, xShape, iEq, agree]232      exact kuhnVertex.member with restrictedBase, kIn233  . intro hy234    obtain ⟨inSpace, k, hk, yShape⟩ := kuhnSimplex.membership.forward with hy235    have kNat := natural.member at succ(m) with hk236    have kLess := Less.of_membership with hk237    have sLess : succ(k) < succ(succ(m)) by arith238    have sIn := membership.of_Less with sLess239    have agree := kuhnVertex.wall with baseFunction, updBijective, first, hk240    have xInCube := kuhnVertex.into_cube at succ(m), p, b, u, succ(k) with baseFunction, bounds, sIn241    have value := cubeRestrict.value with xInCube242    have restrictedBounds : ∀ j ∈ m, restrict(b, m)(j) < p243      intros j hj244      have baseValue := restrict.domain_apply with baseFunction, mSubset, hj245      rw baseValue246      exact bounds with (membership.into_successor with hj)247    apply functionImage.membership.backward248    constructor249    . rw yShape250      exact kuhnVertex.into_cube with restrictedBase, restrictedBounds, hk251    . witness kuhnVertex(succ(m), b, u)(succ(k))252      constructor253      . apply difference.singleton_membership.backward254        constructor255        . exact kuhnVertex.member with baseFunction, sIn256        . intro equal257          have same := kuhnVertex.injective with baseFunction, updInjective, sIn, zeroIn, equal258          arith259      . rw [yShape, value, agree]260        rfl261