Grace/Cumulus/FixedPoint/KuhnExtend.g17

Open in Workbench Download source

Imports

KuhnWallFace

Declarations

Source

1-- Points of the cube of one dimension lower, extended by the value p at the2-- last coordinate, and points on the far wall restricted back; labels and3-- reduced labels pass through both ways4-- 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.KuhnExtend10import KuhnWallFace1112def cubeExtend (m p y : Set) : Set := y ∪ constantFunction({m}, succ(p), p)1314theorem cubeExtend.disjoint (m : Set)15  shows Disjoint(m, {m})16proof17  apply Disjoint.iff.backward18  intros x hx inside19  have same := singleton.membership.forward with inside20  rw same at hx21  exact membership.irreflexive with hx2223theorem cubeExtend.function (m p : Nat) (y : Set)24  requires hy : y ∈ functionSpace(m, succ(p))25  shows cubeExtend(m, p, y) : succ(m) → succ(p)26proof27  have yFunction := functionSpace.mem_iff.forward with hy28  have pIn := bootstrap.succ.self at p29  have constant := constantFunction.function at {m}, succ(p), p with pIn30  have disjoint := cubeExtend.disjoint at m31  have union := FunctionBetween.union_disjoint with yFunction, constant, disjoint32  have asInsert := natural.successor_as_insert at m33  have unfolded : insert(m, m) = {m} ∪ m34    unfold insert35    rfl36  have domain : m ∪ {m} = succ(m)37    rw [asInsert, unfolded]38    exact union2.commutative39  have codomain := union2.idempotent at succ(p)40  rw [domain, codomain] at union41  have same : cubeExtend(m, p, y) = y ∪ constantFunction({m}, succ(p), p)42    unfold cubeExtend43    rfl44  rwa same4546theorem cubeExtend.apply_below (m p : Nat) (y j : Set)47  requires hy : y ∈ functionSpace(m, succ(p))48  requires hj : j ∈ m49  shows cubeExtend(m, p, y)(j) = y(j)50proof51  have yFunction := functionSpace.mem_iff.forward with hy52  have pIn := bootstrap.succ.self at p53  have constant := constantFunction.function at {m}, succ(p), p with pIn54  have disjoint := cubeExtend.disjoint at m55  have same : cubeExtend(m, p, y) = y ∪ constantFunction({m}, succ(p), p)56    unfold cubeExtend57    rfl58  rw same59  exact FunctionBetween.union_apply_left with yFunction, constant, disjoint, hj6061theorem cubeExtend.apply_top (m p : Nat) (y : Set)62  requires hy : y ∈ functionSpace(m, succ(p))63  shows cubeExtend(m, p, y)(m) = p64proof65  have yFunction := functionSpace.mem_iff.forward with hy66  have pIn := bootstrap.succ.self at p67  have constant := constantFunction.function at {m}, succ(p), p with pIn68  have disjoint := cubeExtend.disjoint at m69  have mIn : m ∈ {m}70    apply singleton.membership.backward71    rfl72  have same : cubeExtend(m, p, y) = y ∪ constantFunction({m}, succ(p), p)73    unfold cubeExtend74    rfl75  rw same76  have value := FunctionBetween.union_apply_right with yFunction, constant, disjoint, mIn77  rw value78  exact constantFunction.apply with mIn, pIn7980theorem cubeExtend.member (m p : Nat) (y : Set)81  requires hy : y ∈ functionSpace(m, succ(p))82  shows cubeExtend(m, p, y) ∈ functionSpace(succ(m), succ(p))83proof84  exact functionSpace.mem_iff.backward with (cubeExtend.function with hy)8586theorem successor.subset (m : Nat)87  shows m ⊆ succ(m)88proof89  intros l hl90  exact membership.into_successor with hl9192theorem cubeExtend.restrict (m p : Nat) (y : Set)93  requires hy : y ∈ functionSpace(m, succ(p))94  shows restrict(cubeExtend(m, p, y), m) = y95proof96  have yFunction := functionSpace.mem_iff.forward with hy97  have extended := cubeExtend.function with hy98  have mSubset := successor.subset at m99  have restricted := restrict.domain_function with extended, mSubset100  apply FunctionBetween.ext with restricted, yFunction101  intros j hj102  have value := restrict.domain_apply with extended, mSubset, hj103  rw value104  exact cubeExtend.apply_below with hy, hj105106theorem cubeRestrict.member (m p : Nat) (x : Set)107  requires hx : x ∈ functionSpace(succ(m), succ(p))108  shows restrict(x, m) ∈ functionSpace(m, succ(p))109proof110  have xFunction := functionSpace.mem_iff.forward with hx111  have mSubset := successor.subset at m112  exact functionSpace.mem_iff.backward with (restrict.domain_function with xFunction, mSubset)113114-- A point on the far wall is the extension of its restriction.115theorem cubeRestrict.extend (m p : Nat) (x : Set)116  requires hx : x ∈ functionSpace(succ(m), succ(p))117  requires top : x(m) = p118  shows cubeExtend(m, p, restrict(x, m)) = x119proof120  have xFunction := functionSpace.mem_iff.forward with hx121  have mSubset := successor.subset at m122  have restrictedIn := cubeRestrict.member with hx123  have extended := cubeExtend.function with restrictedIn124  apply FunctionBetween.ext with extended, xFunction125  intros j hj126  have split := bootstrap.succ.membership.forward with hj127  cases split with below | same128  . have value := cubeExtend.apply_below with restrictedIn, below129    rw value130    exact restrict.domain_apply with xFunction, mSubset, below131  . rw same132    have value := cubeExtend.apply_top with restrictedIn133    rw [value, top]134    rfl135136defgraph cubeRestrict (m p : Set) (x ∈ functionSpace(succ(m), succ(p))) : functionSpace(m, succ(p)) := restrict(x, m)137requires mNat : Nat(m)138requires pNat : Nat(p)139proof140  exact cubeRestrict.member with member141142-- The labelling of the lower cube induced by a labelling of the cube.143defgraph wallLabels (m p lab L : Set) (y ∈ functionSpace(m, succ(p))) : L := lab(cubeExtend(m, p, y))144requires mNat : Nat(m)145requires pNat : Nat(p)146requires labFunction : lab : functionSpace(succ(m), succ(p)) → L147proof148  have extendedIn := cubeExtend.member with member149  exact FunctionBetween.apply_closed with labFunction, extendedIn150151theorem wallLabels.zero_wall (m p : Nat) (lab L : Set)152  requires labFunction : lab : functionSpace(succ(m), succ(p)) → L153  requires zeroWall : ∀ x ∈ functionSpace(succ(m), succ(p)), ∀ j ∈ succ(m), x(j) = 0 → lab(x)(j) = 0154  shows ∀ y ∈ functionSpace(m, succ(p)), ∀ j ∈ m, y(j) = 0 → wallLabels(m, p, lab, L)(y)(j) = 0155proof156  intros y hy j hj zero157  have value := wallLabels.value at m, p, lab, L, y with *158  rw value159  have extendedIn := cubeExtend.member with hy160  have jIn := membership.into_successor with hj161  have below := cubeExtend.apply_below with hy, hj162  have forX := zeroWall with extendedIn163  apply forX with jIn164  rwa below165166theorem wallLabels.full_wall (m p : Nat) (lab L : Set)167  requires labFunction : lab : functionSpace(succ(m), succ(p)) → L168  requires fullWall : ∀ x ∈ functionSpace(succ(m), succ(p)), ∀ j ∈ succ(m), x(j) = p → lab(x)(j) = 1169  shows ∀ y ∈ functionSpace(m, succ(p)), ∀ j ∈ m, y(j) = p → wallLabels(m, p, lab, L)(y)(j) = 1170proof171  intros y hy j hj full172  have value := wallLabels.value at m, p, lab, L, y with *173  rw value174  have extendedIn := cubeExtend.member with hy175  have jIn := membership.into_successor with hj176  have below := cubeExtend.apply_below with hy, hj177  have forX := fullWall with extendedIn178  apply forX with jIn179  rwa below180181-- On the far wall the reduced label survives restriction.182theorem reduced.restrict (m p : Nat) (lab L x : Set)183  requires labFunction : lab : functionSpace(succ(m), succ(p)) → L184  requires fullWall : ∀ x ∈ functionSpace(succ(m), succ(p)), ∀ j ∈ succ(m), x(j) = p → lab(x)(j) = 1185  requires hx : x ∈ functionSpace(succ(m), succ(p))186  requires top : x(m) = p187  shows reduced(m, wallLabels(m, p, lab, L), restrict(x, m)) = reduced(succ(m), lab, x)188proof189  have yIn := cubeRestrict.member with hx190  have labelValue := wallLabels.value at m, p, lab, L, restrict(x, m) with *191  have back := cubeRestrict.extend with hx, top192  rw back at labelValue193  have mIn := bootstrap.succ.self at m194  have forX := fullWall with hx195  have labelOne := forX with mIn, top196  have nonzero : lab(x)(m) ≠ 0197    rw labelOne198    intro equal199    arith200  have bound := reduced.le_of_nonzero with mIn, nonzero201  have less : reduced(succ(m), lab, x) < succ(m) by arith202  have rIn := membership.of_Less with less203  apply reduced.unique204  . exact rIn205  . intros i hi206    have zero := reduced.below with hi207    rwa labelValue208  . have stop := reduced.stop at succ(m), lab, x209    cases stop with top2 | nonzero2210    . exfalso211      rw top2 at rIn212      exact membership.irreflexive with rIn213    . right214      rwa labelValue215216theorem labelImage.restrict_wall (m p : Nat) (lab L f : Set)217  requires labFunction : lab : functionSpace(succ(m), succ(p)) → L218  requires fullWall : ∀ x ∈ functionSpace(succ(m), succ(p)), ∀ j ∈ succ(m), x(j) = p → lab(x)(j) = 1219  requires inCube : f ⊆ functionSpace(succ(m), succ(p))220  requires top : ∀ x ∈ f, x(m) = p221  shows labelImage(m, wallLabels(m, p, lab, L), functionImage(cubeRestrict(m, p), f, functionSpace(m, succ(p)))) =222    labelImage(succ(m), lab, f)223proof224  ext k225  constructor226  . intro hk227    obtain ⟨kIn, y, hy, shape⟩ := labelImage.membership.forward with hk228    obtain ⟨yIn, x, hx, yShape⟩ := functionImage.membership.forward with hy229    have xIn := inCube with x, hx230    have value := cubeRestrict.value with xIn231    rw value at yShape232    have same := reduced.restrict with labFunction, fullWall, xIn, (top with hx)233    apply labelImage.membership.backward234    constructor235    . exact membership.into_successor with kIn236    . witness x237      constructor238      . exact hx239      . rw [shape, yShape, same]240        rfl241  . intro hk242    obtain ⟨kIn, x, hx, shape⟩ := labelImage.membership.forward with hk243    have xIn := inCube with x, hx244    have same := reduced.restrict with labFunction, fullWall, xIn, (top with hx)245    have value := cubeRestrict.value with xIn246    have restrictedIn := cubeRestrict.member with xIn247    have reducedBound := reduced.bound at m, wallLabels(m, p, lab, L), restrict(x, m)248    apply labelImage.membership.backward249    constructor250    . rw [shape, ← same]251      exact reducedBound252    . witness restrict(x, m)253      constructor254      . apply functionImage.membership.backward255        constructor256        . exact restrictedIn257        . witness x258          constructor259          . exact hx260          . rw value261            rfl262      . rw [shape, ← same]263        rfl264