-- With labels respecting the walls of the cube, a labelled face on any wall
-- lies on the far wall of the last coordinate, so the boundary doors of the
-- parity count are exactly the labelled faces there
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.FixedPoint.KuhnWallFace
import KuhnParity

def topWallFaces (p m lab : Set) : Set :=
  { f ∈ labelledFaces(p, succ(m), lab) | ∀ x ∈ f, x(m) = p }

-- A labelled face on any wall lies on the far wall of the last coordinate.
theorem labelledFaces.wall_top (m p : Nat) (lab f : Set)
  requires zeroWall : ∀ x ∈ functionSpace(succ(m), succ(p)), ∀ j ∈ succ(m), x(j) = 0 → lab(x)(j) = 0
  requires fullWall : ∀ x ∈ functionSpace(succ(m), succ(p)), ∀ j ∈ succ(m), x(j) = p → lab(x)(j) = 1
  requires hf : f ∈ labelledFaces(p, succ(m), lab)
  requires wall : ∃ j ∈ succ(m), (∀ x ∈ f, x(j) = 0) ∨ (∀ x ∈ f, x(j) = p)
  shows ∀ x ∈ f, x(m) = p
proof
  have parts := labelledFaces.membership.forward with hf
  have inCube := powerset.membership_iff.forward with parts.left
  have labels := parts.right.right
  obtain ⟨j, hj, flat⟩ := wall
  have jNat := natural.member at succ(m) with hj
  cases flat with zero | full
  . exfalso
    have jInImage : j ∈ labelImage(succ(m), lab, f) by rwa labels
    obtain ⟨jIn, x, hx, shape⟩ := labelImage.membership.forward with jInImage
    have xInCube := inCube with x, hx
    have forX := zeroWall with xInCube
    have labelZero := forX with hj, (zero with hx)
    have different := reduced.ne_of_zero with hj, labelZero
    apply different
    symm
    exact shape
  . intros x hx
    have alternatives : j = m ∨ j ≠ m by tauto
    cases alternatives with same | different
    . rw ← same
      exact full with hx
    . exfalso
      have jBelow : j ∈ m
        have split := bootstrap.succ.membership.forward with hj
        cases split with below | top
        . exact below
        . exfalso
          exact different with top
      have jLess := Less.of_membership with jBelow
      have mInImage : m ∈ labelImage(succ(m), lab, f)
        rw labels
        exact bootstrap.succ.self
      obtain ⟨mIn, y, hy, yShape⟩ := labelImage.membership.forward with mInImage
      have yInCube := inCube with y, hy
      have forY := fullWall with yInCube
      have labelOne := forY with hj, (full with hy)
      have nonzero : lab(y)(j) ≠ 0
        rw labelOne
        intro equal
        arith
      have bound := reduced.le_of_nonzero with hj, nonzero
      rw ← yShape at bound
      arith

theorem boundaryDoors.top_wall (m p : Nat) (lab : Set)
  requires zeroWall : ∀ x ∈ functionSpace(succ(m), succ(p)), ∀ j ∈ succ(m), x(j) = 0 → lab(x)(j) = 0
  requires fullWall : ∀ x ∈ functionSpace(succ(m), succ(p)), ∀ j ∈ succ(m), x(j) = p → lab(x)(j) = 1
  shows boundaryDoors(faceIncidence(p, succ(m), lab), kuhnSimplices(p, succ(m)), labelledFaces(p, succ(m), lab)) =
    topWallFaces(p, m, lab)
proof
  have zeroLess : 0 < succ(m) by arith
  have positive := membership.of_Less with zeroLess
  ext f
  have walls := boundaryDoors.wall at succ(m), p, lab, f with positive
  constructor
  . intro hf
    obtain ⟨fIn, wall⟩ := walls.forward with hf
    apply topWallFaces.membership.backward
    constructor
    . exact fIn
    . exact labelledFaces.wall_top with zeroWall, fullWall, fIn, wall
  . intro hf
    obtain ⟨fIn, top⟩ := topWallFaces.membership.forward with hf
    apply walls.backward
    constructor
    . exact fIn
    . witness m
      constructor
      . exact bootstrap.succ.self at m
      . right
        exact top