Grace/Cumulus/FixedPoint/KuhnLabel.g17

Imports

Declarations

labelStops def
reduced def
labelStops.nonempty theorem derivation
labelStops.naturals theorem derivation
reduced.stops theorem derivation
reduced.bound theorem derivation
reduced.natural theorem derivation
reduced.stop theorem derivation
reduced.least theorem derivation
reduced.below theorem derivation
reduced.unique theorem derivation
reduced.ne_of_zero theorem derivation
reduced.le_of_nonzero theorem derivation
reducedMap defgraph
labelImage def
labelImage.membership theorem derivation
completeSimplices def
Source

1-- The reduced labelling of a point of the cube: the first coordinate whose2-- label is one, or the dimension when every label is zero3-- 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.KuhnLabel9import KuhnThrough1011-- The indices where a labelling stops: the dimension itself and every12-- coordinate whose label is not zero.13def labelStops (n lab x : Set) : Set := { k ∈ succ(n) | k = n ∨ lab(x)(k) ≠ 0 }1415def reduced (n lab x : Set) : Set := leastNatural(labelStops(n, lab, x))1617theorem labelStops.nonempty (n : Nat) (lab x : Set)18  shows Nonempty(labelStops(n, lab, x))19proof20  witness n21  apply labelStops.membership.backward22  constructor23  . exact bootstrap.succ.self at n24  . left25    rfl2627theorem labelStops.naturals (n : Nat) (lab x : Set)28  shows labelStops(n, lab, x) ⊆ ℕ29proof30  intros k hk31  have parts := labelStops.membership.forward with hk32  have kNat := natural.member at succ(n) with parts.left33  exact nat.omega.forward with kNat3435theorem reduced.stops (n : Nat) (lab x : Set)36  shows reduced(n, lab, x) ∈ labelStops(n, lab, x)37proof38  have inhabited := labelStops.nonempty at n, lab, x39  have naturals := labelStops.naturals at n, lab, x40  have same : reduced(n, lab, x) = leastNatural(labelStops(n, lab, x))41    unfold reduced42    rfl43  rw same44  exact leastNatural.member with inhabited, naturals4546theorem reduced.bound (n : Nat) (lab x : Set)47  shows reduced(n, lab, x) ∈ succ(n)48proof49  have stops := reduced.stops at n, lab, x50  have parts := labelStops.membership.forward with stops51  exact parts.left5253theorem reduced.natural (n : Nat) (lab x : Set)54  shows Nat(reduced(n, lab, x))55proof56  have bound := reduced.bound at n, lab, x57  exact natural.member at succ(n) with bound5859theorem reduced.stop (n : Nat) (lab x : Set)60  shows reduced(n, lab, x) = n ∨ lab(x)(reduced(n, lab, x)) ≠ 061proof62  have stops := reduced.stops at n, lab, x63  have parts := labelStops.membership.forward with stops64  exact parts.right6566theorem reduced.least (n : Nat) (lab x k : Set)67  requires hk : k ∈ labelStops(n, lab, x)68  shows reduced(n, lab, x) ≤ k69proof70  have inhabited := labelStops.nonempty at n, lab, x71  have naturals := labelStops.naturals at n, lab, x72  have parts := labelStops.membership.forward with hk73  have kNat := natural.member at succ(n) with parts.left74  have same : reduced(n, lab, x) = leastNatural(labelStops(n, lab, x))75    unfold reduced76    rfl77  rw same78  exact leastNatural.least with inhabited, naturals, hk7980-- Below the reduced label every label is zero.81theorem reduced.below (n : Nat) (lab x i : Set)82  requires hi : i ∈ reduced(n, lab, x)83  shows lab(x)(i) = 084proof85  have reducedNat := reduced.natural at n, lab, x86  have iNat := natural.member at reduced(n, lab, x) with hi87  have iLess := Less.of_membership with hi88  have bound := reduced.bound at n, lab, x89  have reducedLess := Less.of_membership with bound90  by_contra nonzero91  have less : i < succ(n) by arith92  have iIn := membership.of_Less with less93  have stop : i ∈ labelStops(n, lab, x)94    apply labelStops.membership.backward95    constructor96    . exact iIn97    . right98      exact nonzero99  have least := reduced.least with stop100  arith101102theorem reduced.unique (n : Nat) (lab x r : Set)103  requires hr : r ∈ succ(n)104  requires zeros : ∀ i ∈ r, lab(x)(i) = 0105  requires stop : r = n ∨ lab(x)(r) ≠ 0106  shows reduced(n, lab, x) = r107proof108  have rNat := natural.member at succ(n) with hr109  have rLess := Less.of_membership with hr110  have inStops : r ∈ labelStops(n, lab, x) := labelStops.membership.backward with ⟨hr, stop⟩111  have least := reduced.least with inStops112  by_contra different113  have strict : reduced(n, lab, x) < r114    by_contra notLess115    have reverse := LessEqual.of_not_Less with notLess116    apply different117    exact LessEqual.antisymmetric with least, reverse118  have inside := membership.of_Less with strict119  have zero := zeros with inside120  have reducedStop := reduced.stop at n, lab, x121  cases reducedStop with top | nonzero122  . rw top at strict123    arith124  . exact nonzero with zero125126theorem reduced.ne_of_zero (n : Nat) (lab x j : Set)127  requires hj : j ∈ n128  requires zero : lab(x)(j) = 0129  shows reduced(n, lab, x) ≠ j130proof131  intro equal132  have stop := reduced.stop at n, lab, x133  rw equal at stop134  cases stop with top | nonzero135  . rw top at hj136    exact membership.irreflexive with hj137  . exact nonzero with zero138139theorem reduced.le_of_nonzero (n : Nat) (lab x j : Set)140  requires hj : j ∈ n141  requires nonzero : lab(x)(j) ≠ 0142  shows reduced(n, lab, x) ≤ j143proof144  have inStops : j ∈ labelStops(n, lab, x)145    apply labelStops.membership.backward146    constructor147    . exact membership.into_successor with hj148    . right149      exact nonzero150  exact reduced.least with inStops151152-- The reduced labelling as a function on a set of points.153defgraph reducedMap (n lab S : Set) (x ∈ S) : succ(n) := reduced(n, lab, x)154requires nNat : Nat(n)155proof156  exact reduced.bound157158def labelImage (n lab S : Set) : Set := functionImage(reducedMap(n, lab, S), S, succ(n))159160theorem labelImage.membership (n : Nat) (k lab S : Set)161  shows k ∈ labelImage(n, lab, S) ↔ k ∈ succ(n) ∧ ∃ x ∈ S, k = reduced(n, lab, x)162proof163  have same : labelImage(n, lab, S) = functionImage(reducedMap(n, lab, S), S, succ(n))164    unfold labelImage165    rfl166  rw same167  constructor168  . intro hk169    obtain ⟨inSucc, x, hx, shape⟩ := functionImage.membership.forward with hk170    have value := reducedMap.value at n, lab, S, x with *171    constructor172    . exact inSucc173    . witness x174      constructor175      . exact hx176      . rw [shape, value]177        rfl178  . intro hk179    obtain ⟨inSucc, x, hx, shape⟩ := hk180    have value := reducedMap.value at n, lab, S, x with *181    apply functionImage.membership.backward182    constructor183    . exact inSucc184    . witness x185      constructor186      . exact hx187      . rw [shape, value]188        rfl189190-- The simplices all of whose vertices carry different reduced labels.191def completeSimplices (p n lab : Set) : Set :=192  { s ∈ kuhnSimplices(p, n) | labelImage(n, lab, s) = succ(n) }193