Grace/Cumulus/FixedPoint/KuhnWallFace.g17

Open in Workbench Download source

Imports

KuhnParity

Declarations

Source

1-- With labels respecting the walls of the cube, a labelled face on any wall2-- lies on the far wall of the last coordinate, so the boundary doors of the3-- parity count are exactly the labelled faces there4-- 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.KuhnWallFace10import KuhnParity1112def topWallFaces (p m lab : Set) : Set :=13  { f ∈ labelledFaces(p, succ(m), lab) | ∀ x ∈ f, x(m) = p }1415-- A labelled face on any wall lies on the far wall of the last coordinate.16theorem labelledFaces.wall_top (m p : Nat) (lab f : Set)17  requires zeroWall : ∀ x ∈ functionSpace(succ(m), succ(p)), ∀ j ∈ succ(m), x(j) = 0 → lab(x)(j) = 018  requires fullWall : ∀ x ∈ functionSpace(succ(m), succ(p)), ∀ j ∈ succ(m), x(j) = p → lab(x)(j) = 119  requires hf : f ∈ labelledFaces(p, succ(m), lab)20  requires wall : ∃ j ∈ succ(m), (∀ x ∈ f, x(j) = 0) ∨ (∀ x ∈ f, x(j) = p)21  shows ∀ x ∈ f, x(m) = p22proof23  have parts := labelledFaces.membership.forward with hf24  have inCube := powerset.membership_iff.forward with parts.left25  have labels := parts.right.right26  obtain ⟨j, hj, flat⟩ := wall27  have jNat := natural.member at succ(m) with hj28  cases flat with zero | full29  . exfalso30    have jInImage : j ∈ labelImage(succ(m), lab, f) by rwa labels31    obtain ⟨jIn, x, hx, shape⟩ := labelImage.membership.forward with jInImage32    have xInCube := inCube with x, hx33    have forX := zeroWall with xInCube34    have labelZero := forX with hj, (zero with hx)35    have different := reduced.ne_of_zero with hj, labelZero36    apply different37    symm38    exact shape39  . intros x hx40    have alternatives : j = m ∨ j ≠ m by tauto41    cases alternatives with same | different42    . rw ← same43      exact full with hx44    . exfalso45      have jBelow : j ∈ m46        have split := bootstrap.succ.membership.forward with hj47        cases split with below | top48        . exact below49        . exfalso50          exact different with top51      have jLess := Less.of_membership with jBelow52      have mInImage : m ∈ labelImage(succ(m), lab, f)53        rw labels54        exact bootstrap.succ.self55      obtain ⟨mIn, y, hy, yShape⟩ := labelImage.membership.forward with mInImage56      have yInCube := inCube with y, hy57      have forY := fullWall with yInCube58      have labelOne := forY with hj, (full with hy)59      have nonzero : lab(y)(j) ≠ 060        rw labelOne61        intro equal62        arith63      have bound := reduced.le_of_nonzero with hj, nonzero64      rw ← yShape at bound65      arith6667theorem boundaryDoors.top_wall (m p : Nat) (lab : Set)68  requires zeroWall : ∀ x ∈ functionSpace(succ(m), succ(p)), ∀ j ∈ succ(m), x(j) = 0 → lab(x)(j) = 069  requires fullWall : ∀ x ∈ functionSpace(succ(m), succ(p)), ∀ j ∈ succ(m), x(j) = p → lab(x)(j) = 170  shows boundaryDoors(faceIncidence(p, succ(m), lab), kuhnSimplices(p, succ(m)), labelledFaces(p, succ(m), lab)) =71    topWallFaces(p, m, lab)72proof73  have zeroLess : 0 < succ(m) by arith74  have positive := membership.of_Less with zeroLess75  ext f76  have walls := boundaryDoors.wall at succ(m), p, lab, f with positive77  constructor78  . intro hf79    obtain ⟨fIn, wall⟩ := walls.forward with hf80    apply topWallFaces.membership.backward81    constructor82    . exact fIn83    . exact labelledFaces.wall_top with zeroWall, fullWall, fIn, wall84  . intro hf85    obtain ⟨fIn, top⟩ := topWallFaces.membership.forward with hf86    apply walls.backward87    constructor88    . exact fIn89    . witness m90      constructor91      . exact bootstrap.succ.self at m92      . right93        exact top94