-- Counting the Kuhn simplices through a face: one when the face lies on a
-- wall of the cube, two otherwise
-- 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.KuhnThrough
import KuhnFamily

def simplicesThrough (p n f : Set) : Set :=
  { t ∈ kuhnSimplices(p, n) | ∃ b ∈ t, t ∖ {b} = f }

theorem kuhnSimplices.shape (t p n : Set)
  requires ht : t ∈ kuhnSimplices(p, n)
  shows ∃ base, FunctionBetween(base, n, ℕ) ∧ (∀ j ∈ n, base(j) < p) ∧
    ∃ upd, BijectiveBetween(upd, n, n) ∧ t = kuhnSimplex(n, base, upd)
proof
  have parts := kuhnSimplices.membership.forward with ht
  obtain ⟨base, baseIn, bounds, upd, bijective, shape⟩ := parts.right
  have baseFunction := functionSpace.mem_iff.forward with baseIn
  refine ⟨base, baseFunction, bounds, upd, bijective, shape⟩

-- A face on a wall of the cube belongs to one simplex only.
theorem simplicesThrough.wall (n p : Nat) (base upd a j : Set)
  requires baseFunction : base : n → ℕ
  requires updBijective : BijectiveBetween(upd, n, n)
  requires bounds : ∀ j ∈ n, base(j) < p
  requires positive : 0 ∈ n
  requires ha : a ∈ kuhnSimplex(n, base, upd)
  requires hj : j ∈ n
  requires wall : (∀ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) = 0) ∨
    (∀ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) = p)
  shows simplicesThrough(p, n, kuhnSimplex(n, base, upd) ∖ {a}) = {kuhnSimplex(n, base, upd)}
proof
  obtain ⟨inSpace, i, hi, shape⟩ := kuhnSimplex.membership.forward with ha
  ext t
  constructor
  . intro ht
    obtain ⟨inFamily, c, hc, same⟩ := simplicesThrough.membership.forward with ht
    obtain ⟨b2, f2, bounds2, u2, bij2, tShape⟩ := kuhnSimplices.shape with inFamily
    rw tShape at hc
    rw tShape at same
    apply singleton.membership.backward
    rw tShape
    cases wall with zero | full
    . have flat : ∀ x ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(i)}, x(j) = 0
        rwa under ← shape
      have top := kuhnSimplex.zero_face_top with baseFunction, updBijective, hi, hj, flat
      rw [shape, top] at same
      rw under top at flat
      exact kuhnSimplex.zero_face_unique with baseFunction, updBijective, f2, bij2, positive, hj, flat, hc, same
    . have flat : ∀ x ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(i)}, x(j) = p
        rwa under ← shape
      have below := bounds with hj
      have bottom := kuhnSimplex.full_face_bottom with baseFunction, updBijective, hi, hj, below, flat
      rw [shape, bottom] at same
      rw under bottom at flat
      have bound2 := bounds2 with hj
      exact kuhnSimplex.full_face_unique with baseFunction, updBijective, f2, bij2, positive, hj, bound2, flat, hc, same
  . intro ht
    have equal := singleton.membership.forward with ht
    rw under equal
    apply simplicesThrough.membership.backward
    constructor
    . exact kuhnSimplex.in_family with baseFunction, updBijective, bounds
    . witness a
      constructor
      . exact ha
      . rfl

theorem simplicesThrough.wall_count (n p : Nat) (base upd a j : Set)
  requires baseFunction : base : n → ℕ
  requires updBijective : BijectiveBetween(upd, n, n)
  requires bounds : ∀ j ∈ n, base(j) < p
  requires positive : 0 ∈ n
  requires ha : a ∈ kuhnSimplex(n, base, upd)
  requires hj : j ∈ n
  requires wall : (∀ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) = 0) ∨
    (∀ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) = p)
  shows cardinality(simplicesThrough(p, n, kuhnSimplex(n, base, upd) ∖ {a})) = 1
proof
  have same := simplicesThrough.wall with baseFunction, updBijective, bounds, positive, ha, hj, wall
  rw same
  exact cardinality.singleton

-- The faces opposite the bottom vertex, the top vertex, and a middle vertex.
theorem simplicesThrough.bottom (n p : Nat) (base upd : Set)
  requires baseFunction : base : n → ℕ
  requires updBijective : BijectiveBetween(upd, n, n)
  requires bounds : ∀ j ∈ n, base(j) < p
  requires positive : 0 ∈ n
  requires upper : ∀ j ∈ n, ∃ x ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(0)}, x(j) ≠ p
  shows simplicesThrough(p, n, kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(0)}) =
    insert(kuhnSimplex(n, kuhnVertex(n, base, upd)(succ(0)), rotated(n, upd)), {kuhnSimplex(n, base, upd)})
proof
  have updFunction := Injective.function with (Bijective.injective with updBijective)
  have jIn := FunctionBetween.apply_closed with updFunction, positive
  have notFull := upper with jIn
  have zeroIn := membership.into_successor with positive
  have nIn := bootstrap.succ.self at n
  have zeroLess := Less.of_membership with positive
  have oneLess : succ(0) < succ(n) by arith
  have oneIn := membership.of_Less with oneLess
  have oneFunction := kuhnVertex.function_on at n, base, upd, succ(0) with baseFunction, oneIn
  ext t
  constructor
  . intro ht
    obtain ⟨inFamily, c, hc, same⟩ := simplicesThrough.membership.forward with ht
    obtain ⟨b2, f2, bounds2, u2, bij2, tShape⟩ := kuhnSimplices.shape with inFamily
    rw tShape at hc
    rw tShape at same
    have split := kuhnSimplex.bottom_face_neighbours with baseFunction, updBijective, f2, bij2, positive, hc, same
    apply insert.membership.backward
    rw tShape
    cases split with original | turned
    . right
      apply singleton.membership.backward
      exact original
    . left
      exact turned
  . intro ht
    have split := insert.membership.forward with ht
    apply simplicesThrough.membership.backward
    cases split with turned | original
    . rw under turned
      constructor
      . exact kuhnSimplex.rotated_in_family with baseFunction, updBijective, bounds, positive, notFull
      . witness kuhnVertex(n, kuhnVertex(n, base, upd)(succ(0)), rotated(n, upd))(n)
        constructor
        . exact kuhnVertex.member with oneFunction, nIn
        . symm
          exact kuhnSimplex.rotated_face with baseFunction, updBijective, positive
    . have equal := singleton.membership.forward with original
      rw under equal
      constructor
      . exact kuhnSimplex.in_family with baseFunction, updBijective, bounds
      . witness kuhnVertex(n, base, upd)(0)
        constructor
        . exact kuhnVertex.member with baseFunction, zeroIn
        . rfl

theorem simplicesThrough.top (n p : Nat) (base upd m : Set)
  requires baseFunction : base : n → ℕ
  requires updBijective : BijectiveBetween(upd, n, n)
  requires bounds : ∀ j ∈ n, base(j) < p
  requires hm : m ∈ n
  requires top : succ(m) = n
  requires lower : ∀ j ∈ n, ∃ x ∈ kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(n)}, x(j) ≠ 0
  shows simplicesThrough(p, n, kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(n)}) =
    insert(kuhnSimplex(n, lowered(n, base, upd, m), unrotated(n, upd)), {kuhnSimplex(n, base, upd)})
proof
  have updFunction := Injective.function with (Bijective.injective with updBijective)
  have jIn := FunctionBetween.apply_closed with updFunction, hm
  have notZero := lower with jIn
  have rooted := kuhnSimplex.top_face_rooted with baseFunction, updBijective, hm, top, notZero
  have mNat := natural.member at n with hm
  have mLess := Less.of_membership with hm
  have zeroLess : 0 < n by arith
  have positive := membership.of_Less with zeroLess
  have zeroIn := membership.into_successor with positive
  have nIn := bootstrap.succ.self at n
  have lowFunction := lowered.function with baseFunction, rooted
  ext t
  constructor
  . intro ht
    obtain ⟨inFamily, c, hc, same⟩ := simplicesThrough.membership.forward with ht
    obtain ⟨b2, f2, bounds2, u2, bij2, tShape⟩ := kuhnSimplices.shape with inFamily
    rw tShape at hc
    rw tShape at same
    have split := kuhnSimplex.top_face_neighbours with baseFunction, updBijective, hm, top, rooted, f2, bij2, hc, same
    apply insert.membership.backward
    rw tShape
    cases split with original | shifted
    . right
      apply singleton.membership.backward
      exact original
    . left
      exact shifted
  . intro ht
    have split := insert.membership.forward with ht
    apply simplicesThrough.membership.backward
    cases split with shifted | original
    . rw under shifted
      constructor
      . exact kuhnSimplex.unrotated_in_family with baseFunction, updBijective, bounds, hm, top, rooted
      . witness kuhnVertex(n, lowered(n, base, upd, m), unrotated(n, upd))(0)
        constructor
        . exact kuhnVertex.member with lowFunction, zeroIn
        . symm
          exact kuhnSimplex.unrotated_face with baseFunction, updBijective, hm, top, rooted
    . have equal := singleton.membership.forward with original
      rw under equal
      constructor
      . exact kuhnSimplex.in_family with baseFunction, updBijective, bounds
      . witness kuhnVertex(n, base, upd)(n)
        constructor
        . exact kuhnVertex.member with baseFunction, nIn
        . rfl

theorem kuhnSimplex.swapped_ne (n : Nat) (base upd a : Set)
  requires baseFunction : base : n → ℕ
  requires updBijective : BijectiveBetween(upd, n, n)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  shows kuhnSimplex(n, base, swapped(n, upd, a)) ≠ kuhnSimplex(n, base, upd)
proof
  have updInjective := Bijective.injective with updBijective
  have swapInjective := Bijective.injective with (swapped.bijective with updBijective, ha, hb)
  have bIn := membership.into_successor with hb
  have differs := kuhnVertex.swapped_differs with baseFunction, updBijective, ha, hb
  intro equal
  apply differs
  have vertexMember := kuhnVertex.member at n, base, swapped(n, upd, a), succ(a) with baseFunction, bIn
  rw equal at vertexMember
  have total := kuhnVertex.sum with baseFunction, swapInjective, bIn
  exact kuhnSimplex.vertex_of_sum with baseFunction, updInjective, vertexMember, bIn, total

theorem simplicesThrough.middle (n p : Nat) (base upd a : Set)
  requires baseFunction : base : n → ℕ
  requires updBijective : BijectiveBetween(upd, n, n)
  requires bounds : ∀ j ∈ n, base(j) < p
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  shows simplicesThrough(p, n, kuhnSimplex(n, base, upd) ∖ {kuhnVertex(n, base, upd)(succ(a))}) =
    insert(kuhnSimplex(n, base, swapped(n, upd, a)), {kuhnSimplex(n, base, upd)})
proof
  have swapBijective := swapped.bijective with updBijective, ha, hb
  have bIn := membership.into_successor with hb
  ext t
  constructor
  . intro ht
    obtain ⟨inFamily, c, hc, same⟩ := simplicesThrough.membership.forward with ht
    obtain ⟨b2, f2, bounds2, u2, bij2, tShape⟩ := kuhnSimplices.shape with inFamily
    rw tShape at hc
    rw tShape at same
    have split := kuhnSimplex.interior_neighbours with baseFunction, updBijective, f2, bij2, ha, hb, hc, same
    apply insert.membership.backward
    rw tShape
    cases split with original | exchanged
    . right
      apply singleton.membership.backward
      exact original
    . left
      exact exchanged
  . intro ht
    have split := insert.membership.forward with ht
    apply simplicesThrough.membership.backward
    cases split with exchanged | original
    . rw under exchanged
      constructor
      . exact kuhnSimplex.in_family with baseFunction, swapBijective, bounds
      . witness kuhnVertex(n, base, swapped(n, upd, a))(succ(a))
        constructor
        . exact kuhnVertex.member with baseFunction, bIn
        . symm
          exact kuhnSimplex.swapped_face with baseFunction, updBijective, ha, hb
    . have equal := singleton.membership.forward with original
      rw under equal
      constructor
      . exact kuhnSimplex.in_family with baseFunction, updBijective, bounds
      . witness kuhnVertex(n, base, upd)(succ(a))
        constructor
        . exact kuhnVertex.member with baseFunction, bIn
        . rfl

-- A face off every wall belongs to exactly two simplices.
theorem simplicesThrough.interior (n p : Nat) (base upd a : Set)
  requires baseFunction : base : n → ℕ
  requires updBijective : BijectiveBetween(upd, n, n)
  requires bounds : ∀ j ∈ n, base(j) < p
  requires positive : 0 ∈ n
  requires ha : a ∈ kuhnSimplex(n, base, upd)
  requires lower : ∀ j ∈ n, ∃ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) ≠ 0
  requires upper : ∀ j ∈ n, ∃ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) ≠ p
  shows ∃ t, t ≠ kuhnSimplex(n, base, upd) ∧
    simplicesThrough(p, n, kuhnSimplex(n, base, upd) ∖ {a}) = insert(t, {kuhnSimplex(n, base, upd)})
proof
  have updFunction := Injective.function with (Bijective.injective with updBijective)
  obtain ⟨inSpace, i, hi, shape⟩ := kuhnSimplex.membership.forward with ha
  have iNat := natural.member at succ(n) with hi
  have iLess := Less.of_membership with hi
  rw under shape at lower
  rw under shape at upper
  rw under shape
  have split := natural.zero_or_successor with iNat
  cases split with zero | successor
  . rw under zero at upper
    rw under zero
    witness kuhnSimplex(n, kuhnVertex(n, base, upd)(succ(0)), rotated(n, upd))
    constructor
    . exact kuhnSimplex.rotated_ne with baseFunction, updBijective, positive
    . exact simplicesThrough.bottom with baseFunction, updBijective, bounds, positive, upper
  . obtain ⟨k, kNat, iEq⟩ := successor
    rw iEq at iLess
    have kLess : k < n by arith
    have kIn := membership.of_Less with kLess
    have alternatives : succ(k) = n ∨ succ(k) ≠ n by tauto
    cases alternatives with top | middle
    . rw under iEq at lower
      rw under top at lower
      rw under iEq
      rw under top
      have jIn := FunctionBetween.apply_closed with updFunction, kIn
      have notZero := lower with jIn
      have rooted := kuhnSimplex.top_face_rooted with baseFunction, updBijective, kIn, top, notZero
      witness kuhnSimplex(n, lowered(n, base, upd, k), unrotated(n, upd))
      constructor
      . exact kuhnSimplex.unrotated_ne with baseFunction, updBijective, kIn, top, rooted
      . exact simplicesThrough.top with baseFunction, updBijective, bounds, kIn, top, lower
    . have separated : n ≠ succ(k)
        intro equal
        apply middle
        symm
        exact equal
      have sLess := Less.successor_lower_of_ne with kLess, separated
      have sIn := membership.of_Less with sLess
      rw under iEq
      witness kuhnSimplex(n, base, swapped(n, upd, k))
      constructor
      . exact kuhnSimplex.swapped_ne with baseFunction, updBijective, kIn, sIn
      . exact simplicesThrough.middle with baseFunction, updBijective, bounds, kIn, sIn

theorem simplicesThrough.interior_count (n p : Nat) (base upd a : Set)
  requires baseFunction : base : n → ℕ
  requires updBijective : BijectiveBetween(upd, n, n)
  requires bounds : ∀ j ∈ n, base(j) < p
  requires positive : 0 ∈ n
  requires ha : a ∈ kuhnSimplex(n, base, upd)
  requires lower : ∀ j ∈ n, ∃ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) ≠ 0
  requires upper : ∀ j ∈ n, ∃ x ∈ kuhnSimplex(n, base, upd) ∖ {a}, x(j) ≠ p
  shows cardinality(simplicesThrough(p, n, kuhnSimplex(n, base, upd) ∖ {a})) = 2
proof
  obtain ⟨t, different, same⟩ := simplicesThrough.interior with baseFunction, updBijective, bounds, positive, ha, lower, upper
  rw same
  have fresh : ¬t ∈ {kuhnSimplex(n, base, upd)}
    intro inside
    have equal := singleton.membership.forward with inside
    exact different with equal
  have count := cardinality.insert with (Finite.singleton at kuhnSimplex(n, base, upd)), fresh
  have one := cardinality.singleton at kuhnSimplex(n, base, upd)
  rw [count, one]
  rfl