Grace/Cumulus/FixedPoint/KuhnInduction.g17

Open in Workbench Download source

Imports

KuhnWallCount

Declarations

Source

1-- Kuhn's lemma: a labelling of the grid points of a cube that respects its2-- walls has a completely labelled Kuhn simplex, so some cell carries, in3-- every coordinate, two points with different labels4-- 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.KuhnInduction10import KuhnWallCount1112theorem successor.zero_member (k : Set)13  requires hk : k ∈ succ(0)14  shows k = 015proof16  have split := bootstrap.succ.membership.forward with hk17  cases split with below | same18  . exfalso19    have kNat := natural.member at succ(0) with hk20    have less := Less.of_membership with below21    arith22  . exact same2324-- In dimension zero the only simplex is the single empty function.25theorem kuhnSimplices.zero_subset (p : Nat) (s : Set)26  requires hs : s ∈ kuhnSimplices(p, 0)27  shows s = {∅}28proof29  have parts := kuhnSimplices.membership.forward with hs30  have inCube := powerset.membership_iff.forward with parts.left31  have cubeEq : functionSpace(0, succ(p)) = {∅}32    rw nat.zero33    exact functionSpace.empty_domain34  rw cubeEq at inCube35  obtain ⟨base, baseFunction, bounds, upd, updBijective, shape⟩ := kuhnSimplices.shape with hs36  have zeroIn := bootstrap.succ.self at 037  have vertexIn : kuhnVertex(0, base, upd)(0) ∈ s38    rw shape39    exact kuhnVertex.member with baseFunction, zeroIn40  have vertexSingleton := inCube with vertexIn41  have vertexEq := singleton.membership.forward with vertexSingleton42  apply Subset.antisymmetric43  . exact inCube44  . intros x hx45    have xEq := singleton.membership.forward with hx46    rwa [xEq, ← vertexEq]4748theorem kuhnSimplices.zero_member (p : Nat)49  shows {∅} ∈ kuhnSimplices(p, 0)50proof51  have emptyFunction := FunctionBetween.empty at ℕ52  have baseFunction : ∅ : 0 → ℕ by rwa nat.zero53  have bounds : ∀ j ∈ 0, apply(∅, j) < p54    intros j hj55    exfalso56    have jNat := natural.member at 0 with hj57    have less := Less.of_membership with hj58    arith59  have updBijective := identity.bijective at 060  have member := kuhnSimplex.in_family with baseFunction, updBijective, bounds61  have same := kuhnSimplices.zero_subset with member62  rwa same at member6364theorem kuhnSimplices.zero (p : Nat)65  shows kuhnSimplices(p, 0) = {{∅}}66proof67  apply Subset.antisymmetric68  . intros s hs69    apply singleton.membership.backward70    exact kuhnSimplices.zero_subset with hs71  . intros s hs72    have same := singleton.membership.forward with hs73    rw same74    exact kuhnSimplices.zero_member7576theorem completeSimplices.zero (p : Nat) (lab : Set)77  shows completeSimplices(p, 0, lab) = kuhnSimplices(p, 0)78proof79  apply Subset.antisymmetric80  . intros s hs81    have parts := completeSimplices.membership.forward with hs82    exact parts.left83  . intros s hs84    apply completeSimplices.membership.backward85    constructor86    . exact hs87    . have same := kuhnSimplices.zero_subset with hs88      apply Subset.antisymmetric89      . intros k hk90        have parts := labelImage.membership.forward with hk91        exact parts.left92      . intros k hk93        have kEq := successor.zero_member with hk94        have emptyIn : ∅ ∈ s95          rw same96          apply singleton.membership.backward97          rfl98        have bound := reduced.bound at 0, lab, ∅99        have reducedEq := successor.zero_member with bound100        apply labelImage.membership.backward101        constructor102        . exact hk103        . witness ∅104          constructor105          . exact emptyIn106          . rw [kEq, reducedEq]107            rfl108109theorem kuhn.base (p : Nat) (lab : Set)110  shows Odd(cardinality(completeSimplices(p, 0, lab)))111proof112  have complete := completeSimplices.zero at p, lab113  have family := kuhnSimplices.zero at p114  have one := cardinality.singleton at {∅}115  rw [complete, family, one]116  have shape : 1 = succ(add(0, 0)) by compute117  rw shape118  exact Odd.double_successor119120-- Kuhn's combinatorial lemma: the number of completely labelled simplices121-- is odd, by induction on the dimension.122theorem kuhn.combinatorial (q n : Nat)123  shows ∀ lab, ∀ L, FunctionBetween(lab, functionSpace(n, succ(succ(q))), L) →124    (∀ x ∈ functionSpace(n, succ(succ(q))), ∀ j ∈ n, x(j) = 0 → lab(x)(j) = 0) →125    (∀ x ∈ functionSpace(n, succ(succ(q))), ∀ j ∈ n, x(j) = succ(q) → lab(x)(j) = 1) →126    Odd(cardinality(completeSimplices(succ(q), n, lab)))127proof128  induction n129  | zero =>130    intros lab L labFunction zeroWall fullWall131    exact kuhn.base at succ(q), lab132  | succ(m) using ih =>133    intros lab L labFunction zeroWall fullWall134    have boundaryEq := boundaryDoors.top_wall at m, succ(q), lab with zeroWall, fullWall135    have count := topWallFaces.count at m, q, lab, L with labFunction, fullWall136    have wallFunction := wallLabels.function at m, succ(q), lab, L with *137    have wallZero := wallLabels.zero_wall at m, succ(q), lab, L with labFunction, zeroWall138    have wallFull := wallLabels.full_wall at m, succ(q), lab, L with labFunction, fullWall139    have lower := ih with wallFunction, wallZero, wallFull140    have zeroLess : 0 < succ(m) by arith141    have positive := membership.of_Less with zeroLess142    apply kuhn.parity at succ(m), succ(q), lab with positive143    rw [boundaryEq, count]144    exact lower145146-- Kuhn's lemma: some cell of the grid carries, for every coordinate, two147-- points whose labels there differ.148theorem kuhn.lemma (q n : Nat) (lab L : Set)149  requires labFunction : lab : functionSpace(n, succ(succ(q))) → L150  requires zeroWall : ∀ x ∈ functionSpace(n, succ(succ(q))), ∀ j ∈ n, x(j) = 0 → lab(x)(j) = 0151  requires fullWall : ∀ x ∈ functionSpace(n, succ(succ(q))), ∀ j ∈ n, x(j) = succ(q) → lab(x)(j) = 1152  shows ∃ base ∈ functionSpace(n, ℕ), (∀ j ∈ n, base(j) < succ(q)) ∧153    ∀ i ∈ n, ∃ u ∈ functionSpace(n, succ(succ(q))), ∃ v ∈ functionSpace(n, succ(succ(q))),154      (∀ j ∈ n, base(j) ≤ u(j) ∧ u(j) ≤ base(j) + 1) ∧ (∀ j ∈ n, base(j) ≤ v(j) ∧ v(j) ≤ base(j) + 1) ∧155      lab(u)(i) = 0 ∧ lab(v)(i) ≠ 0156proof157  have all := kuhn.combinatorial at q, n158  have odd := all with labFunction, zeroWall, fullWall159  have inhabited : ∃ s, s ∈ completeSimplices(succ(q), n, lab)160    by_contra none161    have empty : completeSimplices(succ(q), n, lab) = ∅162      apply Subset.antisymmetric163      . intros s hs164        exfalso165        apply none166        witness s167        exact hs168      . intros s hs169        exfalso170        simpa using hs171    rw [empty, ← nat.zero] at odd172    have zero := cardinality.natural at 0173    rw zero at odd174    obtain ⟨k, kIn, shape⟩ := odd175    have kNat := nat.omega.backward with kIn176    have self := bootstrap.succ.self at add(k, k)177    rw [← shape, nat.zero] at self178    simpa using self179  obtain ⟨s, hs⟩ := inhabited180  obtain ⟨sIn, complete⟩ := completeSimplices.membership.forward with hs181  obtain ⟨base, baseFunction, bounds, upd, updBijective, sShape⟩ := kuhnSimplices.shape with sIn182  have sParts := kuhnSimplices.membership.forward with sIn183  have sCube := powerset.membership_iff.forward with sParts.left184  witness base185  constructor186  . exact functionSpace.mem_iff.backward with baseFunction187  . constructor188    . exact bounds189    . intros i hi190      have iNat := natural.member at n with hi191      have iLess := Less.of_membership with hi192      have iIn := membership.into_successor with hi193      have sLess : succ(i) < succ(n) by arith194      have succIn := membership.of_Less with sLess195      have upperIn : succ(i) ∈ labelImage(n, lab, s) by rwa complete196      have lowerIn : i ∈ labelImage(n, lab, s) by rwa complete197      obtain ⟨uBound, u, hu, uShape⟩ := labelImage.membership.forward with upperIn198      obtain ⟨vBound, v, hv, vShape⟩ := labelImage.membership.forward with lowerIn199      have uCube := sCube with u, hu200      have vCube := sCube with v, hv201      have uBetween : ∀ j ∈ n, base(j) ≤ u(j) ∧ u(j) ≤ base(j) + 1202        intros j hj203        rw sShape at hu204        obtain ⟨inSpace, k, hk, uVertex⟩ := kuhnSimplex.membership.forward with hu205        rw uVertex206        exact kuhnVertex.between with baseFunction, hk, hj207      have vBetween : ∀ j ∈ n, base(j) ≤ v(j) ∧ v(j) ≤ base(j) + 1208        intros j hj209        rw sShape at hv210        obtain ⟨inSpace, k, hk, vVertex⟩ := kuhnSimplex.membership.forward with hv211        rw vVertex212        exact kuhnVertex.between with baseFunction, hk, hj213      witness u214      constructor215      . exact uCube216      . witness v217        constructor218        . exact vCube219        . constructor220          . exact uBetween221          . constructor222            . exact vBetween223            . constructor224              . have inReduced : i ∈ reduced(n, lab, u)225                  rw ← uShape226                  exact bootstrap.succ.self227                exact reduced.below with inReduced228              . have stop := reduced.stop at n, lab, v229                rw ← vShape at stop230                cases stop with top | nonzero231                . exfalso232                  rw top at hi233                  exact membership.irreflexive with hi234                . exact nonzero235