-- Stabilisation of the derived stages: a point removed at a stage is
-- witnessed by a basic open set, one basic set witnesses at most one
-- removal, so in a space with a countable base the stages stabilise below
-- the Hartogs bound of the base; the Cantor–Bendixson rank is the least
-- stable stage and the perfect kernel is the stage 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.Topology.CantorBendixson.Stabilise
import Iterate
import Cardinal
import Topology.Basis

-- A point removed at stage α is isolated in that stage, and a basic open
-- set around it meets the stage only in the point.
theorem derived.removed_witness (X T A B α x : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  requires closed : IsClosed(X, T, A)
  requires hAlpha : α ∈ Ordinal
  requires hx : x ∈ derived(X, T, A, α)
  requires away : ¬x ∈ derived(X, T, A, next(α))
  shows ∃ W ∈ B, W ∩ derived(X, T, A, α) = {x}
proof
  have closedStage := derived.closed with topology, closed, hAlpha
  have whole := closedStage.left
  rw derived.next at away
  have removed : x ∈ derived(X, T, A, α) ∖ derivedSet(X, T, derived(X, T, A, α))
    exact difference.membership.backward with ⟨hx, away⟩
  have isolated := derivedSet.removed_iff.forward with topology, whole, removed
  obtain ⟨hxStage, U, hU, hxU, trace⟩ := isolated
  obtain ⟨W, hW, hxW, below⟩ := Basis.refine with basis, hU, hxU
  witness W
  constructor
  . exact hW
  . apply Subset.antisymmetric
    . intros y hy
      have parts := intersection.membership.forward with hy
      have inU : y ∈ U ∩ derived(X, T, A, α)
        exact intersection.membership.backward with ⟨(below with
          y, parts.left), parts.right⟩
      rw trace at inU
      exact inU
    . intros y hy
      have same := singleton.membership.forward with hy
      rw same
      exact intersection.membership.backward with ⟨hxW, hx⟩

-- Conversely a basic set meeting stage α exactly in x removes x at α.
theorem derived.witness_removed (X T A B α x W : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  requires closed : IsClosed(X, T, A)
  requires hAlpha : α ∈ Ordinal
  requires hW : W ∈ B
  requires trace : W ∩ derived(X, T, A, α) = {x}
  shows x ∈ derived(X, T, A, α) ∧ ¬x ∈ derived(X, T, A, next(α))
proof
  have closedStage := derived.closed with topology, closed, hAlpha
  have whole := closedStage.left
  have self : x ∈ W ∩ derived(X, T, A, α)
    rw trace
    exact singleton.self at x
  have parts := intersection.membership.forward with self
  have openW := Basis.subset with basis, W, hW
  have isolated : IsolatedPoint(X, T, derived(X, T, A, α), x)
    exact ⟨parts.right, W, openW, parts.left, trace⟩
  have removed := derivedSet.removed_iff.backward with topology, whole, isolated
  have removedParts := difference.membership.forward with removed
  constructor
  . exact parts.right
  . rw derived.next
    exact removedParts.right

-- One basic set cannot witness a removal at two stages: a point removed
-- at the later stage δ lies in every stage up to next(γ), so it is the
-- point removed at γ, which is not in stage next(γ).
theorem derived.witness_below (X T A B γ δ x y W : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  requires closed : IsClosed(X, T, A)
  requires hGamma : γ ∈ Ordinal
  requires hDelta : δ ∈ Ordinal
  requires less : γ ∈ δ
  requires hW : W ∈ B
  requires first : W ∩ derived(X, T, A, γ) = {x}
  requires second : W ∩ derived(X, T, A, δ) = {y}
  shows ⊥
proof
  have removed := derived.witness_removed with
    topology, basis, closed, hGamma, hW, first
  have hNext := Ordinal.next with hGamma
  have nextBelow := Ordinal.member_iff_next_subset.forward with
    hGamma, hDelta, less
  have bound := Ordinal.subset_bound with hNext, hDelta, nextBelow
  have toNext := derived.decreasing with topology, closed, hNext, hDelta, bound
  have toGamma := derived.antitone with topology, closed, hGamma, hDelta, less
  have selfY : y ∈ W ∩ derived(X, T, A, δ)
    rw second
    exact singleton.self at y
  have partsY := intersection.membership.forward with selfY
  have yNext := toNext with y, partsY.right
  have yGamma := toGamma with y, partsY.right
  have yTrace : y ∈ W ∩ derived(X, T, A, γ)
    exact intersection.membership.backward with ⟨partsY.left, yGamma⟩
  rw first at yTrace
  have same := singleton.membership.forward with yTrace
  rw same at yNext
  exact removed.right with yNext

theorem derived.witness_injective (X T A B γ δ x y W : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  requires closed : IsClosed(X, T, A)
  requires hGamma : γ ∈ Ordinal
  requires hDelta : δ ∈ Ordinal
  requires hW : W ∈ B
  requires first : W ∩ derived(X, T, A, γ) = {x}
  requires second : W ∩ derived(X, T, A, δ) = {y}
  shows γ = δ ∧ x = y
proof
  have split := Ordinal.trichotomy with hGamma, δ, hDelta
  have same : γ = δ
    cases split with less | rest
    . exfalso
      exact derived.witness_below with
        topology, basis, closed, hGamma, hDelta, less, hW, first, second
    . cases rest with equal | greater
      . exact equal
      . exfalso
        exact derived.witness_below with
          topology, basis, closed, hDelta, hGamma, greater, hW, second, first
  constructor
  . exact same
  . rw same at first
    rw first at second
    have hx : x ∈ {y}
      rw ← second
      exact singleton.self at x
    exact singleton.membership.forward with hx

-- The drops of the stages indexed by D: a stage γ ∈ D is related to the
-- basic sets that witness a removal at γ.
def stageDrops (X T A B D : Set) : Set :=
  { p ∈ D × B | ∃ γ ∈ D, ∃ W ∈ B, p = (γ ↦ W) ∧
    (∃ x, W ∩ derived(X, T, A, γ) = {x}) }

theorem stageDrops.relates (X T A B D γ W : Set)
  shows relates(stageDrops(X, T, A, B, D), γ, W) ↔
    γ ∈ D ∧ W ∈ B ∧ (∃ x, W ∩ derived(X, T, A, γ) = {x})
proof
  constructor
  . intro edge
    unfold relates at edge
    have parts := stageDrops.membership.forward with edge
    obtain ⟨γ2, hγ2, W2, hW2, shape, witnessed⟩ := parts.right
    obtain ⟨rfl, rfl⟩ := orderedPair.injective with shape
    exact ⟨hγ2, hW2, witnessed⟩
  . intro h
    obtain ⟨hγ, hW, witnessed⟩ := h
    unfold relates
    apply stageDrops.membership.backward
    constructor
    . exact product.pair with hγ, hW
    . exact ⟨γ, hγ, W, hW, rfl, witnessed⟩

theorem stageDrops.separated (X T A B D : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  requires closed : IsClosed(X, T, A)
  requires ordinals : ∀ γ ∈ D, γ ∈ Ordinal
  shows ∀ γ ∈ D, ∀ δ ∈ D, ∀ W ∈ B,
    relates(stageDrops(X, T, A, B, D), γ, W) →
      relates(stageDrops(X, T, A, B, D), δ, W) → γ = δ
proof
  intros γ hγ δ hδ W hW first second
  obtain ⟨hγ2, hW2, x, traceX⟩ := stageDrops.relates.forward with first
  obtain ⟨hδ2, hW3, y, traceY⟩ := stageDrops.relates.forward with second
  have hGamma := ordinals with γ, hγ
  have hDelta := ordinals with δ, hδ
  have both := derived.witness_injective with
    topology, basis, closed, hGamma, hDelta, hW, traceX, traceY
  exact both.left

-- A stage that is not stable removes a point, witnessed by a basic set.
theorem stageDrops.offered (X T A B γ : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  requires closed : IsClosed(X, T, A)
  requires hGamma : γ ∈ Ordinal
  requires strict : derived(X, T, A, next(γ)) ≠ derived(X, T, A, γ)
  shows ∃ W ∈ B, ∃ x, W ∩ derived(X, T, A, γ) = {x}
proof
  have drop := derived.next_subset with topology, closed, hGamma
  have removed : ∃ x ∈ derived(X, T, A, γ),
      ¬x ∈ derived(X, T, A, next(γ))
    by_contra none
    apply strict
    apply Subset.antisymmetric with drop
    intros x hx
    by_contra outside
    apply none
    exact ⟨x, hx, outside⟩
  obtain ⟨x, hx, away⟩ := removed
  obtain ⟨W, hW, trace⟩ := derived.removed_witness with
    topology, basis, closed, hGamma, hx, away
  exact ⟨W, hW, x, trace⟩

-- Stabilisation: if every stage below the Hartogs bound of the base
-- dropped, the least-coded witnesses would inject the Hartogs bound into
-- the base.
theorem derived.stabilises (X T A B : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  requires closed : IsClosed(X, T, A)
  requires countable : Countable(B)
  shows ∃ γ ∈ hartogsBound(B),
    derived(X, T, A, next(γ)) = derived(X, T, A, γ)
proof
  obtain ⟨g, code⟩ := countable
  by_contra none
  have hBound := hartogsBound.ordinal at B
  have ordinals : ∀ γ ∈ hartogsBound(B), γ ∈ Ordinal
    intros γ hγ
    exact Ordinal.member with hBound, hγ
  have offered : ∀ γ ∈ hartogsBound(B), ∃ W ∈ B,
      relates(stageDrops(X, T, A, B, hartogsBound(B)), γ, W)
    intros γ hγ
    have hGamma := ordinals with γ, hγ
    have strict : derived(X, T, A, next(γ)) ≠ derived(X, T, A, γ)
      intro equal
      apply none
      exact ⟨γ, hγ, equal⟩
    obtain ⟨W, hW, x, trace⟩ := stageDrops.offered with
      topology, basis, closed, hGamma, strict
    witness W
    constructor
    . exact hW
    . apply stageDrops.relates.backward
      exact ⟨hγ, hW, x, trace⟩
  have separated := stageDrops.separated with topology, basis, closed, ordinals
  have injective := leastCoded.injective with code, offered, separated
  exact hartogsBound.no_injection with injective

-- Once two consecutive stages agree, every later stage is the same set.
theorem derived.stable_below (X T A γ ε : Set)
  requires topology : IsTopology(X, T)
  requires closed : IsClosed(X, T, A)
  requires hGamma : γ ∈ Ordinal
  requires hEpsilon : ε ∈ Ordinal
  requires stable : derived(X, T, A, next(γ)) = derived(X, T, A, γ)
  shows ∀ δ ∈ next(ε), γ ∈ next(δ) →
    derived(X, T, A, δ) = derived(X, T, A, γ)
proof
  have hNext := Ordinal.next with hEpsilon
  have transitive := Ordinal.transitive with hNext
  have unfolded := stable
  rw derived.next at unfolded
  induction δ over next(ε) ordered by membershipOn(next(ε)) certified by membershipOn.wellFounded at next(ε)
  intros current hCurrentIn ih hBound
  have hCurrent := Ordinal.member with hNext, hCurrentIn
  have bound := next.membership.forward with hBound
  cases bound with earlier | equal
  . have split := Ordinal.cases with hCurrent
    cases split with zero | rest
    . exfalso
      rw zero at earlier
      exact set.empty with earlier
    . cases rest with successor | limit
      . obtain ⟨β, hβ, equalNext⟩ := successor
        have hBeta := Ordinal.member with hCurrent, hβ
        have hBetaIn := transitive with current, hCurrentIn, β, hβ
        have rule := membershipOn.relates with hBetaIn, hCurrentIn
        have predecessor : β ∈ next(ε) ∧
            relates(membershipOn(next(ε)), β, current)
          exact ⟨hBetaIn, (rule.backward with hβ)⟩
        rw ← equalNext at earlier
        have same := ih with β, predecessor, earlier
        rw [← equalNext, derived.next, same]
        exact unfolded
      . have equation := derived.limit at X, T, A, current with limit
        apply Subset.antisymmetric
        . exact derived.antitone with
            topology, closed, hGamma, hCurrent, earlier
        . rw equation
          have stage := derived.stage_in_range at X, T, A with earlier
          have inhabited : Nonempty(Relation.range(derived.history(X, T, A, current)))
            exact ⟨derived(X, T, A, γ), stage⟩
          apply familyIntersection.greatest with inhabited
          intros S hS
          obtain ⟨β, hβ, shape⟩ := derived.history_range.forward with hS
          rw shape
          have hBeta := Ordinal.member with hCurrent, hβ
          have order := Ordinal.trichotomy with hBeta, γ, hGamma
          cases order with less | rest
          . exact derived.antitone with topology, closed, hBeta, hGamma, less
          . cases rest with sameStage | greater
            . rw sameStage
              exact Subset.reflexive
            . have hBetaIn := transitive with current, hCurrentIn, β, hβ
              have rule := membershipOn.relates with hBetaIn, hCurrentIn
              have predecessor : β ∈ next(ε) ∧
                  relates(membershipOn(next(ε)), β, current)
                exact ⟨hBetaIn, (rule.backward with hβ)⟩
              have boundBeta : γ ∈ next(β)
                apply next.membership.backward
                left
                exact greater
              have same := ih with β, predecessor, boundBeta
              rw same
              exact Subset.reflexive
  . rw equal
    rfl

theorem derived.stable_after (X T A γ δ : Set)
  requires topology : IsTopology(X, T)
  requires closed : IsClosed(X, T, A)
  requires hGamma : γ ∈ Ordinal
  requires hDelta : δ ∈ Ordinal
  requires stable : derived(X, T, A, next(γ)) = derived(X, T, A, γ)
  requires hBound : γ ∈ next(δ)
  shows derived(X, T, A, δ) = derived(X, T, A, γ)
proof
  have below := derived.stable_below at X, T, A, γ, δ with
    topology, closed, hGamma, hDelta, stable
  exact below with δ, (next.contains at δ), hBound

-- A point of A outside stage ρ is removed at some successor stage below
-- ρ: at the least stage it has left, which is neither zero nor a limit.

def leftStages (X T A ρ x : Set) : Set :=
  { α ∈ next(ρ) | ¬x ∈ derived(X, T, A, α) }

theorem derived.removed_stage (X T A ρ x : Set)
  requires topology : IsTopology(X, T)
  requires closed : IsClosed(X, T, A)
  requires hRho : ρ ∈ Ordinal
  requires hx : x ∈ A
  requires away : ¬x ∈ derived(X, T, A, ρ)
  shows ∃ β ∈ ρ,
    x ∈ derived(X, T, A, β) ∧ ¬x ∈ derived(X, T, A, next(β))
proof
  have hNext := Ordinal.next with hRho
  have transitive := Ordinal.transitive with hNext
  have ordinals : ∀ α ∈ leftStages(X, T, A, ρ, x), α ∈ Ordinal
    intros α hα
    have parts := leftStages.membership.forward with hα
    exact Ordinal.member with hNext, parts.left
  have member : ρ ∈ leftStages(X, T, A, ρ, x)
    exact leftStages.membership.backward with ⟨(next.contains at ρ), away⟩
  have inhabited : Nonempty(leftStages(X, T, A, ρ, x)) := ⟨ρ, member⟩
  have nonempty := Nonempty.ne_empty with inhabited
  obtain ⟨m, hm, least⟩ := Ordinal.least with ordinals, nonempty
  have parts := leftStages.membership.forward with hm
  have mIn := parts.left
  have mAway := parts.right
  have hM := Ordinal.member with hNext, mIn
  have split := Ordinal.cases with hM
  cases split with zero | rest
  . exfalso
    apply mAway
    rw [zero, ← nat.zero, derived.zero]
    exact hx
  . cases rest with successor | limit
    . obtain ⟨β, hβ, equalNext⟩ := successor
      have hBetaIn := transitive with m, mIn, β, hβ
      have hBetaRho : β ∈ ρ
        have order := next.membership.forward with hBetaIn
        cases order with less | same
        . exact less
        . exfalso
          rw same at equalNext
          rw ← equalNext at mIn
          exact membership.irreflexive with mIn
      have inBeta : x ∈ derived(X, T, A, β)
        by_contra outside
        have memberBeta : β ∈ leftStages(X, T, A, ρ, x)
          exact leftStages.membership.backward with ⟨hBetaIn, outside⟩
        have below := least with β, memberBeta
        exact Ordinal.not_member_of_subset with below, hβ
      refine ⟨β, hBetaRho, inBeta, ?_⟩
      rw equalNext
      exact mAway
    . exfalso
      have membership := derived.limit_membership at X, T, A, x, m with limit
      apply mAway
      apply membership.backward
      intros β hβ
      by_contra outside
      have hBetaIn := transitive with m, mIn, β, hβ
      have memberBeta : β ∈ leftStages(X, T, A, ρ, x)
        exact leftStages.membership.backward with ⟨hBetaIn, outside⟩
      have below := least with β, memberBeta
      exact Ordinal.not_member_of_subset with below, hβ

-- The Cantor–Bendixson rank: the least stable stage. The stable stages
-- are collected below the Hartogs bound of the topology, which contains
-- the Hartogs bound of every base; the rank is their intersection, the
-- least of them. The perfect kernel is the stage at the rank.

def stableStages (X T A : Set) : Set :=
  { γ ∈ hartogsBound(T) | derived(X, T, A, next(γ)) = derived(X, T, A, γ) }

def cantorBendixsonRank (X T A : Set) : Set := ⋂(stableStages(X, T, A))

def perfectKernel (X T A : Set) : Set :=
  derived(X, T, A, cantorBendixsonRank(X, T, A))

theorem stableStages.ordinal (X T A γ : Set)
  requires hγ : γ ∈ stableStages(X, T, A)
  shows γ ∈ Ordinal
proof
  have parts := stableStages.membership.forward with hγ
  exact Ordinal.member with (hartogsBound.ordinal at T), parts.left

theorem stableStages.nonempty (X T A B : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  requires closed : IsClosed(X, T, A)
  requires countable : Countable(B)
  shows stableStages(X, T, A) ≠ ∅
proof
  obtain ⟨γ, hγ, stable⟩ := derived.stabilises with
    topology, basis, closed, countable
  have inside := Basis.subset with basis
  have grows := hartogsBound.monotone with inside
  have inT := grows with γ, hγ
  have member : γ ∈ stableStages(X, T, A)
    exact stableStages.membership.backward with ⟨inT, stable⟩
  have inhabited : Nonempty(stableStages(X, T, A)) := ⟨γ, member⟩
  exact Nonempty.ne_empty with inhabited

theorem cantorBendixsonRank.stable (X T A B : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  requires closed : IsClosed(X, T, A)
  requires countable : Countable(B)
  shows cantorBendixsonRank(X, T, A) ∈ stableStages(X, T, A)
proof
  have nonempty := stableStages.nonempty with topology, basis, closed, countable
  have ordinals : ∀ γ ∈ stableStages(X, T, A), γ ∈ Ordinal
    intros γ hγ
    exact stableStages.ordinal with hγ
  have least := Ordinal.intersection_least with ordinals, nonempty
  unfold cantorBendixsonRank
  exact least.left

theorem cantorBendixsonRank.ordinal (X T A B : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  requires closed : IsClosed(X, T, A)
  requires countable : Countable(B)
  shows cantorBendixsonRank(X, T, A) ∈ Ordinal
proof
  have stable := cantorBendixsonRank.stable with
    topology, basis, closed, countable
  exact stableStages.ordinal with stable

theorem cantorBendixsonRank.fixed (X T A B : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  requires closed : IsClosed(X, T, A)
  requires countable : Countable(B)
  shows derived(X, T, A, next(cantorBendixsonRank(X, T, A))) =
    perfectKernel(X, T, A)
proof
  have same : perfectKernel(X, T, A) =
      derived(X, T, A, cantorBendixsonRank(X, T, A))
    unfold perfectKernel
    rfl
  have stable := cantorBendixsonRank.stable with
    topology, basis, closed, countable
  have parts := stableStages.membership.forward with stable
  rw same
  exact parts.right

theorem cantorBendixsonRank.in_hartogs (X T A B : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  requires closed : IsClosed(X, T, A)
  requires countable : Countable(B)
  shows cantorBendixsonRank(X, T, A) ∈ hartogsBound(T)
proof
  have stable := cantorBendixsonRank.stable with
    topology, basis, closed, countable
  have parts := stableStages.membership.forward with stable
  exact parts.left

-- The rank is the least stable ordinal: a stable ordinal below it would
-- be a stable stage below the intersection of the stable stages.
theorem cantorBendixsonRank.least (X T A B γ : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  requires closed : IsClosed(X, T, A)
  requires countable : Countable(B)
  requires hGamma : γ ∈ Ordinal
  requires stable : derived(X, T, A, next(γ)) = derived(X, T, A, γ)
  shows cantorBendixsonRank(X, T, A) ⊆ γ
proof
  have same : cantorBendixsonRank(X, T, A) = ⋂(stableStages(X, T, A))
    unfold cantorBendixsonRank
    rfl
  have hRank := cantorBendixsonRank.ordinal with
    topology, basis, closed, countable
  have inHartogs := cantorBendixsonRank.in_hartogs with
    topology, basis, closed, countable
  have order := Ordinal.subset_or_member with hRank, hGamma
  cases order with below | above
  . exact below
  . exfalso
    have inside := Ordinal.member_subset with
      (hartogsBound.ordinal at T), inHartogs
    have inT := inside with γ, above
    have member : γ ∈ stableStages(X, T, A)
      exact stableStages.membership.backward with ⟨inT, stable⟩
    have nonempty := stableStages.nonempty with
      topology, basis, closed, countable
    have ordinals : ∀ δ ∈ stableStages(X, T, A), δ ∈ Ordinal
      intros δ hδ
      exact stableStages.ordinal with hδ
    have least := Ordinal.intersection_least with ordinals, nonempty
    have rankBelow := least.right with γ, member
    have rankBelowGamma : cantorBendixsonRank(X, T, A) ⊆ γ
      rw same
      exact rankBelow
    exact Ordinal.not_member_of_subset with rankBelowGamma, above

-- Every stage from the rank on is the perfect kernel.
theorem perfectKernel.stage (X T A B δ : Set)
  requires topology : IsTopology(X, T)
  requires basis : Basis(X, T, B)
  requires closed : IsClosed(X, T, A)
  requires countable : Countable(B)
  requires hDelta : δ ∈ Ordinal
  requires hBound : cantorBendixsonRank(X, T, A) ∈ next(δ)
  shows derived(X, T, A, δ) = perfectKernel(X, T, A)
proof
  have same : perfectKernel(X, T, A) =
      derived(X, T, A, cantorBendixsonRank(X, T, A))
    unfold perfectKernel
    rfl
  have hRank := cantorBendixsonRank.ordinal with
    topology, basis, closed, countable
  have stable := cantorBendixsonRank.stable with
    topology, basis, closed, countable
  have parts := stableStages.membership.forward with stable
  rw same
  exact derived.stable_after with
    topology, closed, hRank, hDelta, parts.right, hBound