Grace/Cumulus/FixedPoint/KuhnThrough.g17

Open in Workbench Download source

Imports

KuhnFamily

Declarations

Source

1-- Counting the Kuhn simplices through a face: one when the face lies on a2-- wall of the cube, two otherwise3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.FixedPoint.KuhnThrough9import KuhnFamily1011def simplicesThrough (p n f : Set) : Set :=12  { t ∈ kuhnSimplices(p, n) | ∃ b ∈ t, t ∖ {b} = f }1314theorem kuhnSimplices.shape (t p n : Set)15  requires ht : t ∈ kuhnSimplices(p, n)16  shows ∃ base, FunctionBetween(base, n, ℕ) ∧ (∀ j ∈ n, base(j) < p) ∧17    ∃ upd, BijectiveBetween(upd, n, n) ∧ t = kuhnSimplex(n, base, upd)18proof19  have parts := kuhnSimplices.membership.forward with ht20  obtain ⟨base, baseIn, bounds, upd, bijective, shape⟩ := parts.right21  have baseFunction := functionSpace.mem_iff.forward with baseIn22  refine ⟨base, baseFunction, bounds, upd, bijective, shape⟩2324-- A face on a wall of the cube belongs to one simplex only.25theorem simplicesThrough.wall (n p : Nat) (base upd a j : Set)26  requires baseFunction : base : n → ℕ27  requires updBijective : BijectiveBetween(upd, n, n)28  requires bounds : ∀ j ∈ n, base(j) < p29  requires positive : 0 ∈ n30  requires ha : a ∈ kuhnSimplex(n, base, upd)31  requires hj : j ∈ n32  requires wall : (∀ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) = 0) ∨33    (∀ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) = p)34  shows simplicesThrough(p, n, kuhnSimplex(n, base, upd) ∖ {a}) = {kuhnSimplex(n, base, upd)}35proof36  obtain ⟨inSpace, i, hi, shape⟩ := kuhnSimplex.membership.forward with ha37  ext t38  constructor39  . intro ht40    obtain ⟨inFamily, c, hc, same⟩ := simplicesThrough.membership.forward with ht41    obtain ⟨b2, f2, bounds2, u2, bij2, tShape⟩ := kuhnSimplices.shape with inFamily42    rw tShape at hc43    rw tShape at same44    apply singleton.membership.backward45    rw tShape46    cases wall with zero | full47    . have flat : ∀ x ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(i)}, x(j) = 048        rwa under ← shape49      have top := kuhnSimplex.zero_face_top with baseFunction, updBijective, hi, hj, flat50      rw [shape, top] at same51      rw under top at flat52      exact kuhnSimplex.zero_face_unique with baseFunction, updBijective, f2, bij2, positive, hj, flat, hc, same53    . have flat : ∀ x ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(i)}, x(j) = p54        rwa under ← shape55      have below := bounds with hj56      have bottom := kuhnSimplex.full_face_bottom with baseFunction, updBijective, hi, hj, below, flat57      rw [shape, bottom] at same58      rw under bottom at flat59      have bound2 := bounds2 with hj60      exact kuhnSimplex.full_face_unique with baseFunction, updBijective, f2, bij2, positive, hj, bound2, flat, hc, same61  . intro ht62    have equal := singleton.membership.forward with ht63    rw under equal64    apply simplicesThrough.membership.backward65    constructor66    . exact kuhnSimplex.in_family with baseFunction, updBijective, bounds67    . witness a68      constructor69      . exact ha70      . rfl7172theorem simplicesThrough.wall_count (n p : Nat) (base upd a j : Set)73  requires baseFunction : base : n → ℕ74  requires updBijective : BijectiveBetween(upd, n, n)75  requires bounds : ∀ j ∈ n, base(j) < p76  requires positive : 0 ∈ n77  requires ha : a ∈ kuhnSimplex(n, base, upd)78  requires hj : j ∈ n79  requires wall : (∀ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) = 0) ∨80    (∀ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) = p)81  shows cardinality(simplicesThrough(p, n, kuhnSimplex(n, base, upd) ∖ {a})) = 182proof83  have same := simplicesThrough.wall with baseFunction, updBijective, bounds, positive, ha, hj, wall84  rw same85  exact cardinality.singleton8687-- The faces opposite the bottom vertex, the top vertex, and a middle vertex.88theorem simplicesThrough.bottom (n p : Nat) (base upd : Set)89  requires baseFunction : base : n → ℕ90  requires updBijective : BijectiveBetween(upd, n, n)91  requires bounds : ∀ j ∈ n, base(j) < p92  requires positive : 0 ∈ n93  requires upper : ∀ j ∈ n, ∃ x ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(0)}, x(j) ≠ p94  shows simplicesThrough(p, n, kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(0)}) =95    insert(kuhnSimplex(n, kuhnVertex(n, base, upd)(succ(0)), rotated(n, upd)), {kuhnSimplex(n, base, upd)})96proof97  have updFunction := Injective.function with (Bijective.injective with updBijective)98  have jIn := FunctionBetween.apply_closed with updFunction, positive99  have notFull := upper with jIn100  have zeroIn := membership.into_successor with positive101  have nIn := bootstrap.succ.self at n102  have zeroLess := Less.of_membership with positive103  have oneLess : succ(0) < succ(n) by arith104  have oneIn := membership.of_Less with oneLess105  have oneFunction := kuhnVertex.function_on at n, base, upd, succ(0) with baseFunction, oneIn106  ext t107  constructor108  . intro ht109    obtain ⟨inFamily, c, hc, same⟩ := simplicesThrough.membership.forward with ht110    obtain ⟨b2, f2, bounds2, u2, bij2, tShape⟩ := kuhnSimplices.shape with inFamily111    rw tShape at hc112    rw tShape at same113    have split := kuhnSimplex.bottom_face_neighbours with baseFunction, updBijective, f2, bij2, positive, hc, same114    apply insert.membership.backward115    rw tShape116    cases split with original | turned117    . right118      apply singleton.membership.backward119      exact original120    . left121      exact turned122  . intro ht123    have split := insert.membership.forward with ht124    apply simplicesThrough.membership.backward125    cases split with turned | original126    . rw under turned127      constructor128      . exact kuhnSimplex.rotated_in_family with baseFunction, updBijective, bounds, positive, notFull129      . witness kuhnVertex(n, kuhnVertex(n, base, upd)(succ(0)), rotated(n, upd))(n)130        constructor131        . exact kuhnVertex.member with oneFunction, nIn132        . symm133          exact kuhnSimplex.rotated_face with baseFunction, updBijective, positive134    . have equal := singleton.membership.forward with original135      rw under equal136      constructor137      . exact kuhnSimplex.in_family with baseFunction, updBijective, bounds138      . witness kuhnVertex(n, base, upd)(0)139        constructor140        . exact kuhnVertex.member with baseFunction, zeroIn141        . rfl142143theorem simplicesThrough.top (n p : Nat) (base upd m : Set)144  requires baseFunction : base : n → ℕ145  requires updBijective : BijectiveBetween(upd, n, n)146  requires bounds : ∀ j ∈ n, base(j) < p147  requires hm : m ∈ n148  requires top : succ(m) = n149  requires lower : ∀ j ∈ n, ∃ x ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(n)}, x(j) ≠ 0150  shows simplicesThrough(p, n, kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(n)}) =151    insert(kuhnSimplex(n, lowered(n, base, upd, m), unrotated(n, upd)), {kuhnSimplex(n, base, upd)})152proof153  have updFunction := Injective.function with (Bijective.injective with updBijective)154  have jIn := FunctionBetween.apply_closed with updFunction, hm155  have notZero := lower with jIn156  have rooted := kuhnSimplex.top_face_rooted with baseFunction, updBijective, hm, top, notZero157  have mNat := natural.member at n with hm158  have mLess := Less.of_membership with hm159  have zeroLess : 0 < n by arith160  have positive := membership.of_Less with zeroLess161  have zeroIn := membership.into_successor with positive162  have nIn := bootstrap.succ.self at n163  have lowFunction := lowered.function with baseFunction, rooted164  ext t165  constructor166  . intro ht167    obtain ⟨inFamily, c, hc, same⟩ := simplicesThrough.membership.forward with ht168    obtain ⟨b2, f2, bounds2, u2, bij2, tShape⟩ := kuhnSimplices.shape with inFamily169    rw tShape at hc170    rw tShape at same171    have split := kuhnSimplex.top_face_neighbours with baseFunction, updBijective, hm, top, rooted, f2, bij2, hc, same172    apply insert.membership.backward173    rw tShape174    cases split with original | shifted175    . right176      apply singleton.membership.backward177      exact original178    . left179      exact shifted180  . intro ht181    have split := insert.membership.forward with ht182    apply simplicesThrough.membership.backward183    cases split with shifted | original184    . rw under shifted185      constructor186      . exact kuhnSimplex.unrotated_in_family with baseFunction, updBijective, bounds, hm, top, rooted187      . witness kuhnVertex(n, lowered(n, base, upd, m), unrotated(n, upd))(0)188        constructor189        . exact kuhnVertex.member with lowFunction, zeroIn190        . symm191          exact kuhnSimplex.unrotated_face with baseFunction, updBijective, hm, top, rooted192    . have equal := singleton.membership.forward with original193      rw under equal194      constructor195      . exact kuhnSimplex.in_family with baseFunction, updBijective, bounds196      . witness kuhnVertex(n, base, upd)(n)197        constructor198        . exact kuhnVertex.member with baseFunction, nIn199        . rfl200201theorem kuhnSimplex.swapped_ne (n : Nat) (base upd a : Set)202  requires baseFunction : base : n → ℕ203  requires updBijective : BijectiveBetween(upd, n, n)204  requires ha : a ∈ n205  requires hb : succ(a) ∈ n206  shows kuhnSimplex(n, base, swapped(n, upd, a)) ≠ kuhnSimplex(n, base, upd)207proof208  have updInjective := Bijective.injective with updBijective209  have swapInjective := Bijective.injective with (swapped.bijective with updBijective, ha, hb)210  have bIn := membership.into_successor with hb211  have differs := kuhnVertex.swapped_differs with baseFunction, updBijective, ha, hb212  intro equal213  apply differs214  have vertexMember := kuhnVertex.member at n, base, swapped(n, upd, a), succ(a) with baseFunction, bIn215  rw equal at vertexMember216  have total := kuhnVertex.sum with baseFunction, swapInjective, bIn217  exact kuhnSimplex.vertex_of_sum with baseFunction, updInjective, vertexMember, bIn, total218219theorem simplicesThrough.middle (n p : Nat) (base upd a : Set)220  requires baseFunction : base : n → ℕ221  requires updBijective : BijectiveBetween(upd, n, n)222  requires bounds : ∀ j ∈ n, base(j) < p223  requires ha : a ∈ n224  requires hb : succ(a) ∈ n225  shows simplicesThrough(p, n, kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(succ(a))}) =226    insert(kuhnSimplex(n, base, swapped(n, upd, a)), {kuhnSimplex(n, base, upd)})227proof228  have swapBijective := swapped.bijective with updBijective, ha, hb229  have bIn := membership.into_successor with hb230  ext t231  constructor232  . intro ht233    obtain ⟨inFamily, c, hc, same⟩ := simplicesThrough.membership.forward with ht234    obtain ⟨b2, f2, bounds2, u2, bij2, tShape⟩ := kuhnSimplices.shape with inFamily235    rw tShape at hc236    rw tShape at same237    have split := kuhnSimplex.interior_neighbours with baseFunction, updBijective, f2, bij2, ha, hb, hc, same238    apply insert.membership.backward239    rw tShape240    cases split with original | exchanged241    . right242      apply singleton.membership.backward243      exact original244    . left245      exact exchanged246  . intro ht247    have split := insert.membership.forward with ht248    apply simplicesThrough.membership.backward249    cases split with exchanged | original250    . rw under exchanged251      constructor252      . exact kuhnSimplex.in_family with baseFunction, swapBijective, bounds253      . witness kuhnVertex(n, base, swapped(n, upd, a))(succ(a))254        constructor255        . exact kuhnVertex.member with baseFunction, bIn256        . symm257          exact kuhnSimplex.swapped_face with baseFunction, updBijective, ha, hb258    . have equal := singleton.membership.forward with original259      rw under equal260      constructor261      . exact kuhnSimplex.in_family with baseFunction, updBijective, bounds262      . witness kuhnVertex(n, base, upd)(succ(a))263        constructor264        . exact kuhnVertex.member with baseFunction, bIn265        . rfl266267-- A face off every wall belongs to exactly two simplices.268theorem simplicesThrough.interior (n p : Nat) (base upd a : Set)269  requires baseFunction : base : n → ℕ270  requires updBijective : BijectiveBetween(upd, n, n)271  requires bounds : ∀ j ∈ n, base(j) < p272  requires positive : 0 ∈ n273  requires ha : a ∈ kuhnSimplex(n, base, upd)274  requires lower : ∀ j ∈ n, ∃ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) ≠ 0275  requires upper : ∀ j ∈ n, ∃ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) ≠ p276  shows ∃ t, t ≠ kuhnSimplex(n, base, upd) ∧277    simplicesThrough(p, n, kuhnSimplex(n, base, upd) ∖ {a}) = insert(t, {kuhnSimplex(n, base, upd)})278proof279  have updFunction := Injective.function with (Bijective.injective with updBijective)280  obtain ⟨inSpace, i, hi, shape⟩ := kuhnSimplex.membership.forward with ha281  have iNat := natural.member at succ(n) with hi282  have iLess := Less.of_membership with hi283  rw under shape at lower284  rw under shape at upper285  rw under shape286  have split := natural.zero_or_successor with iNat287  cases split with zero | successor288  . rw under zero at upper289    rw under zero290    witness kuhnSimplex(n, kuhnVertex(n, base, upd)(succ(0)), rotated(n, upd))291    constructor292    . exact kuhnSimplex.rotated_ne with baseFunction, updBijective, positive293    . exact simplicesThrough.bottom with baseFunction, updBijective, bounds, positive, upper294  . obtain ⟨k, kNat, iEq⟩ := successor295    rw iEq at iLess296    have kLess : k < n by arith297    have kIn := membership.of_Less with kLess298    have alternatives : succ(k) = n ∨ succ(k) ≠ n by tauto299    cases alternatives with top | middle300    . rw under iEq at lower301      rw under top at lower302      rw under iEq303      rw under top304      have jIn := FunctionBetween.apply_closed with updFunction, kIn305      have notZero := lower with jIn306      have rooted := kuhnSimplex.top_face_rooted with baseFunction, updBijective, kIn, top, notZero307      witness kuhnSimplex(n, lowered(n, base, upd, k), unrotated(n, upd))308      constructor309      . exact kuhnSimplex.unrotated_ne with baseFunction, updBijective, kIn, top, rooted310      . exact simplicesThrough.top with baseFunction, updBijective, bounds, kIn, top, lower311    . have separated : n ≠ succ(k)312        intro equal313        apply middle314        symm315        exact equal316      have sLess := Less.successor_lower_of_ne with kLess, separated317      have sIn := membership.of_Less with sLess318      rw under iEq319      witness kuhnSimplex(n, base, swapped(n, upd, k))320      constructor321      . exact kuhnSimplex.swapped_ne with baseFunction, updBijective, kIn, sIn322      . exact simplicesThrough.middle with baseFunction, updBijective, bounds, kIn, sIn323324theorem simplicesThrough.interior_count (n p : Nat) (base upd a : Set)325  requires baseFunction : base : n → ℕ326  requires updBijective : BijectiveBetween(upd, n, n)327  requires bounds : ∀ j ∈ n, base(j) < p328  requires positive : 0 ∈ n329  requires ha : a ∈ kuhnSimplex(n, base, upd)330  requires lower : ∀ j ∈ n, ∃ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) ≠ 0331  requires upper : ∀ j ∈ n, ∃ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) ≠ p332  shows cardinality(simplicesThrough(p, n, kuhnSimplex(n, base, upd) ∖ {a})) = 2333proof334  obtain ⟨t, different, same⟩ := simplicesThrough.interior with baseFunction, updBijective, bounds, positive, ha, lower, upper335  rw same336  have fresh : ¬t ∈ {kuhnSimplex(n, base, upd)}337    intro inside338    have equal := singleton.membership.forward with inside339    exact different with equal340  have count := cardinality.insert with (Finite.singleton at kuhnSimplex(n, base, upd)), fresh341  have one := cardinality.singleton at kuhnSimplex(n, base, upd)342  rw [count, one]343  rfl344