Grace/Cumulus/FixedPoint/KuhnFaces.g17

Imports

Declarations

kuhnSimplex.zero_face_top theorem derivation
kuhnSimplex.full_face_bottom theorem derivation
kuhnSimplex.zero_face_unique theorem derivation
kuhnSimplex.full_face_unique theorem derivation
Source

1-- Faces of Kuhn simplices on the boundary of the cube: a face lying on a2-- coordinate hyperplane x_j = 0 misses the top vertex, one lying on x_j = p3-- misses the bottom vertex, and in either case the simplex through the4-- face is unique5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.FixedPoint.KuhnFaces11import KuhnNeighbour1213theorem kuhnSimplex.zero_face_top (n : Nat) (base upd i j : Set)14  requires baseFunction : base : n → ℕ15  requires updBijective : BijectiveBetween(upd, n, n)16  requires hi : i ∈ succ(n)17  requires hj : j ∈ n18  requires flat : ∀ x ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(i)}, x(j) = 019  shows i = n20proof21  have updInjective := Bijective.injective with updBijective22  have nIn := bootstrap.succ.self at n23  by_contra different24  have topMember := kuhnVertex.member at n, base, upd, n with baseFunction, nIn25  have topDifferent : kuhnVertex(n, base, upd)(n) ≠ kuhnVertex(n, base, upd)(i)26    intro equal27    have same := kuhnVertex.injective with baseFunction, updInjective, nIn, hi, equal28    apply different29    symm30    exact same31  have inFace : kuhnVertex(n, base, upd)(n) ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(i)}32    exact difference.singleton_membership.backward with ⟨topMember, topDifferent⟩33  have zero := flat with kuhnVertex(n, base, upd)(n), inFace34  have value := kuhnVertex.top_coordinate with baseFunction, updBijective, hj35  rw value at zero36  have baseValue := FunctionBetween.apply_closed with baseFunction, hj37  have baseNat := nat.omega.backward with baseValue38  arith3940theorem kuhnSimplex.full_face_bottom (n p : Nat) (base upd i j : Set)41  requires baseFunction : base : n → ℕ42  requires updBijective : BijectiveBetween(upd, n, n)43  requires hi : i ∈ succ(n)44  requires hj : j ∈ n45  requires bound : base(j) < p46  requires flat : ∀ x ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(i)}, x(j) = p47  shows i = 048proof49  have updInjective := Bijective.injective with updBijective50  have zeroNat : Nat(0) by typecheck51  have positive : 0 < succ(n) by arith52  have zeroIn := membership.of_Less with positive53  by_contra different54  have bottomMember := kuhnVertex.member at n, base, upd, 0 with baseFunction, zeroIn55  have bottomDifferent : kuhnVertex(n, base, upd)(0) ≠ kuhnVertex(n, base, upd)(i)56    intro equal57    have same := kuhnVertex.injective with baseFunction, updInjective, zeroIn, hi, equal58    apply different59    symm60    exact same61  have inFace : kuhnVertex(n, base, upd)(0) ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(i)}62    exact difference.singleton_membership.backward with ⟨bottomMember, bottomDifferent⟩63  have full := flat with kuhnVertex(n, base, upd)(0), inFace64  have value := kuhnVertex.zero_coordinate at n, base, upd, j with baseFunction, hj65  rw value at full66  have baseValue := FunctionBetween.apply_closed with baseFunction, hj67  have baseNat := nat.omega.backward with baseValue68  arith6970-- Through a face on x_j = 0 or on x_j = p there is exactly one simplex.71theorem kuhnSimplex.zero_face_unique (n : Nat) (b u b2 u2 c j : Set)72  requires f1 : b : n → ℕ73  requires bij1 : BijectiveBetween(u, n, n)74  requires f2 : b2 : n → ℕ75  requires bij2 : BijectiveBetween(u2, n, n)76  requires positive : 0 ∈ n77  requires hj : j ∈ n78  requires flat : ∀ x ∈ kuhnSimplex(n, b, u) ∖ {kuhnVertex(n, b, u)(n)}, x(j) = 079  requires hc : c ∈ kuhnSimplex(n, b2, u2)80  requires same : kuhnSimplex(n, b2, u2) ∖ {c} = kuhnSimplex(n, b, u) ∖ {kuhnVertex(n, b, u)(n)}81  shows kuhnSimplex(n, b2, u2) = kuhnSimplex(n, b, u)82proof83  obtain ⟨inSpace, k, hk, shape⟩ := kuhnSimplex.membership.forward with hc84  have flat2 : ∀ x ∈ kuhnSimplex(n, b2, u2) ∖ {kuhnVertex(n, b2, u2)(k)}, x(j) = 085    rw under ← shape86    rwa under same87  have top := kuhnSimplex.zero_face_top with f2, bij2, hk, hj, flat288  rw [shape, top] at same89  exact kuhnSimplex.eq_top with f2, bij2, f1, bij1, positive, same9091theorem kuhnSimplex.full_face_unique (n p : Nat) (b u b2 u2 c j : Set)92  requires f1 : b : n → ℕ93  requires bij1 : BijectiveBetween(u, n, n)94  requires f2 : b2 : n → ℕ95  requires bij2 : BijectiveBetween(u2, n, n)96  requires positive : 0 ∈ n97  requires hj : j ∈ n98  requires bound2 : b2(j) < p99  requires flat : ∀ x ∈ kuhnSimplex(n, b, u) ∖ {kuhnVertex(n, b, u)(0)}, x(j) = p100  requires hc : c ∈ kuhnSimplex(n, b2, u2)101  requires same : kuhnSimplex(n, b2, u2) ∖ {c} = kuhnSimplex(n, b, u) ∖ {kuhnVertex(n, b, u)(0)}102  shows kuhnSimplex(n, b2, u2) = kuhnSimplex(n, b, u)103proof104  obtain ⟨inSpace, k, hk, shape⟩ := kuhnSimplex.membership.forward with hc105  have flat2 : ∀ x ∈ kuhnSimplex(n, b2, u2) ∖ {kuhnVertex(n, b2, u2)(k)}, x(j) = p106    rw under ← shape107    rwa under same108  have bottom := kuhnSimplex.full_face_bottom with f2, bij2, hk, hj, bound2, flat2109  rw [shape, bottom] at same110  exact kuhnSimplex.eq_bottom with f2, bij2, f1, bij1, positive, same111