Nim/lib/system/yrc_tarjan_proof.lean

/-
  Tarjan-based deadness computation — correctness proof
  =====================================================
  Self-contained, no Mathlib. Checked with Lean 4 (v4.32.0).

  Companion to yrc_proof.lean; models the NOVEL part of yrc.nim's
  collector: cycle detection via a single Tarjan SCC traversal plus one
  linear reverse scan over the condensation, replacing Bacon-style trial
  deletion (three traversals: markGray / scan / collectWhite).

  ## The algorithm (capture / computeDeadness in yrc.nim)

  `capture` runs an iterative Tarjan DFS from the candidate roots. Each
  visited cell is claimed (dense index in the header), its rc word is
  snapshotted, and every traversed slot contributes one edge record.
  SCCs are numbered 0, 1, 2, … in POP (completion) order. Tarjan's
  invariant: when an SCC is completed, every SCC it points to was
  completed earlier — so every condensation cross edge goes from a
  HIGHER SCC id to a LOWER one ("sinks first").

  `computeDeadness` then makes ONE pass s = nScc−1 … 0 (sources before
  sinks, since in-edges come from higher ids):

      ext(s) = sumRefs(s) − internal(s) − deadIn(s)
      if not forcedLive(s) and ext(s) == 0:
        s is DEAD;  for each cross edge s → t: deadIn(t) += 1
      else:
        s is LIVE;  for each cross edge s → t: forcedLive(t) := true

  where sumRefs(s) = Σ rc over members, internal(s) = # captured edges
  within s, and forcedLive is seeded from cells still registered in the
  roots buffer (inRootsFlag).

  ## What we prove

  Fix the SPEC of liveness on the condensation: an SCC is live iff it
  has an external reference, a roots-buffer seed, or a captured cross
  edge from a live SCC (`LiveScc`, an inductive definition).

  1. `scan_dead_iff_not_live` — any deadness assignment satisfying the
     scan's per-SCC equation (well-defined thanks to the sinks-first
     edge order) marks an SCC dead IFF it is not live. Soundness AND
     completeness in one theorem: the single reverse scan computes the
     garbage set EXACTLY on the captured snapshot.
  2. `impl_fixpoint_is_spec` — the implementation's ARITHMETIC form
     (ext = sumRefs − internal − deadIn with forcedLive propagation) is
     the same equation, given rc-exactness (sumRefs = external +
     internal + cross-in; established by merge + commit validation, see
     yrc_proof.lean §4).
  3. Cell-level bridge: `tarjan_sound` — cells of dead SCCs are
     unreachable in the snapshot; `tarjan_complete` — every captured
     garbage cell IS marked dead (this needs strong connectivity of the
     SCCs and exactness of the external counts; Bacon needs his second
     and third traversals for the same guarantee).
  4. `demotion_closure_sound` — validate-time demotion (an SCC dropped
     from the dead set because a mutator dirtied it) must PROPAGATE
     along captured cross edges: the freed set stays closed only if the
     demoted set is successor-closed within the dead set. A demoted SCC
     survives with its out-edges intact, so any still-dead target would
     be freed while a surviving cell points at it.

  ## What is assumed (and where it is discharged)

  • The sinks-first edge order (`horder`) — Tarjan's classical
    invariant; the DFS itself is not modeled.
  • rc-exactness (`hcount`) — discharged operationally by yrc_proof §4
    (merge + dirty check + rc-word recheck).
  • That `capture` records exactly the heap edges among captured cells
    and that SCC members are mutually reachable (`h_edge_resp`,
    `h_conn`, `h_cross_real`) — properties of the traversal + Tarjan.
-/

abbrev Obj := Nat

/-! ## §1 Descending induction

  The scan processes higher SCC ids first; every recursive dependency
  of `dead s` is on some `u > s`. This induction principle is the
  well-definedness of the whole scheme. -/

theorem descending_induction {n : Nat} (P : Fin n → Prop)
    (step : ∀ s : Fin n, (∀ u : Fin n, s < u → P u) → P s) :
    ∀ s, P s := by
  have key : ∀ k, ∀ s : Fin n, n - s.val ≤ k → P s := by
    intro k
    induction k with
    | zero =>
      intro s hs
      have := s.isLt
      omega
    | succ k ih =>
      intro s _
      apply step
      intro u hu
      apply ih
      have h1 := u.isLt
      have h2 : s.val < u.val := hu
      omega
  intro s
  exact key n s (by omega)

/-! ## §2 The condensation and the liveness spec

  `edges` are the captured condensation cross edges (with multiplicity:
  one entry per traversed slot, exactly like cap.edges bucketed into
  crossTgt). `extRefs s` counts references into SCC `s` from OUTSIDE
  the capture: stack refs, uncaptured heap cells, other collections'
  partitions — everything in Σrc not explained by captured edges.
  `seed s` is the inRootsFlag forcedLive seeding. -/

section Condensation

variable {n : Nat}
variable (edges : List (Fin n × Fin n))
variable (extRefs : Fin n → Nat)
variable (seed : Fin n → Bool)

/-- The SPEC: an SCC is live iff something external anchors it —
    directly or through a chain of captured cross edges. -/
inductive LiveScc : Fin n → Prop where
  | ext (s : Fin n) : 0 < extRefs s → LiveScc s
  | root (s : Fin n) : seed s = true → LiveScc s
  | pred (u s : Fin n) : (u, s) ∈ edges → LiveScc u → LiveScc s

/-- The per-SCC equation the reverse scan establishes: dead iff no
    external refs, no seed, and ALL cross predecessors dead. (The
    sinks-first order makes this a valid definition: every predecessor
    has a higher id and is decided first — see `descending_induction`;
    without that order the "definition" would be circular.) -/
def ScanEq (dead : Fin n → Bool) : Prop :=
  ∀ s, dead s = true ↔
    (extRefs s = 0 ∧ seed s = false ∧
     ∀ e ∈ edges, e.2 = s → dead e.1 = true)

/-- Live SCCs are never marked dead (soundness direction). -/
theorem live_not_dead (dead : Fin n → Bool)
    (hfix : ScanEq edges extRefs seed dead) :
    ∀ s, LiveScc edges extRefs seed s → dead s ≠ true := by
  intro s hl
  induction hl with
  | ext s h =>
    intro hd
    have := ((hfix s).mp hd).1
    omega
  | root s h =>
    intro hd
    have := ((hfix s).mp hd).2.1
    rw [h] at this
    cases this
  | pred u s hmem _ ih =>
    intro hd
    exact ih (((hfix s).mp hd).2.2 (u, s) hmem rfl)

/-- Non-live SCCs are always marked dead (completeness direction) —
    by descending induction along the scan order. -/
theorem not_live_dead
    (horder : ∀ e ∈ edges, e.2 < e.1)
    (dead : Fin n → Bool)
    (hfix : ScanEq edges extRefs seed dead) :
    ∀ s, ¬ LiveScc edges extRefs seed s → dead s = true := by
  refine descending_induction
    (fun s => ¬ LiveScc edges extRefs seed s → dead s = true) ?_
  intro s ihs hnl
  rw [hfix]
  refine ⟨?_, ?_, ?_⟩
  · cases Nat.eq_zero_or_pos (extRefs s) with
    | inl h => exact h
    | inr h => exact absurd (LiveScc.ext s h) hnl
  · cases hsd : seed s with
    | false => rfl
    | true => exact absurd (LiveScc.root s hsd) hnl
  · intro e he hes
    have hlt : s < e.1 := by
      have := horder e he
      rw [hes] at this
      exact this
    apply ihs e.1 hlt
    intro hlu
    have hmem : (e.1, s) ∈ edges := by
      rw [← hes]
      simpa using he
    exact hnl (LiveScc.pred e.1 s hmem hlu)

/-- **Main condensation theorem**: the single reverse scan computes
    EXACTLY the non-live SCCs. One Tarjan DFS + one linear scan replace
    Bacon's three graph traversals, with no loss of precision on the
    snapshot. -/
theorem scan_dead_iff_not_live
    (horder : ∀ e ∈ edges, e.2 < e.1)
    (dead : Fin n → Bool)
    (hfix : ScanEq edges extRefs seed dead) :
    ∀ s, dead s = true ↔ ¬ LiveScc edges extRefs seed s := by
  intro s
  constructor
  · intro hd hl
    exact live_not_dead edges extRefs seed dead hfix s hl hd
  · exact not_live_dead edges extRefs seed horder dead hfix s

/-! ## §3 The implementation's arithmetic form

  computeDeadness does not test "all predecessors dead" directly; it
  maintains ext(s) = sumRefs(s) − internal(s) − deadIn(s) and a
  forcedLive flag pushed along cross edges of live SCCs. We show this
  is the same equation, given rc-exactness:

      sumRefs s = extRefs s + internal s + (# cross edges into s).

  ext(s) = 0 then says extRefs s = 0 AND every cross in-edge came from
  a dead predecessor; ¬forcedLive says no seed and no LIVE predecessor
  pushed the flag — together exactly `ScanEq`. -/

def inCount (s : Fin n) : Nat :=
  edges.countP (fun e => e.2 == s)

def deadInCount (dead : Fin n → Bool) (s : Fin n) : Nat :=
  edges.countP (fun e => e.2 == s && dead e.1)

/-- countP is monotone under pointwise implication. -/
theorem countP_le_of_imp {α : Type} (l : List α) (p q : α → Bool)
    (himp : ∀ x ∈ l, p x = true → q x = true) :
    l.countP p ≤ l.countP q := by
  induction l with
  | nil => simp
  | cons a l ih =>
    have iht := ih (fun x hx => himp x (List.mem_cons_of_mem a hx))
    by_cases hpa : p a = true
    · have hqa := himp a (by simp) hpa
      simp [hpa, hqa]
      omega
    · simp only [List.countP_cons]
      have : p a = false := by
        cases h : p a
        · rfl
        · exact absurd h hpa
      simp [this]
      omega

/-- If a stronger predicate matches as often as a weaker one, they
    agree on every element. -/
theorem countP_eq_forces_all {α : Type} (l : List α) (p q : α → Bool)
    (himp : ∀ x ∈ l, q x = true → p x = true)
    (heq : l.countP p = l.countP q) :
    ∀ x ∈ l, p x = true → q x = true := by
  induction l with
  | nil => intro x hx; cases hx
  | cons a l ih =>
    have himpt : ∀ x ∈ l, q x = true → p x = true :=
      fun x hx => himp x (List.mem_cons_of_mem a hx)
    have hmono := countP_le_of_imp l q p himpt
    intro x hx hpx
    simp only [List.countP_cons] at heq
    cases List.mem_cons.mp hx with
    | inl hxa =>
      subst hxa
      cases hqx : q x with
      | true => rfl
      | false =>
        exfalso
        simp [hpx, hqx] at heq
        omega
    | inr hxl =>
      have hqa_pa : (if q a = true then 1 else 0) ≤ (if p a = true then 1 else 0) := by
        by_cases hq : q a = true
        · simp [hq, himp a (by simp) hq]
        · simp [hq]
      have heqt : l.countP p = l.countP q := by
        by_cases hq : q a = true
        · simp [hq, himp a (by simp) hq] at heq
          omega
        · have hqf : q a = false := by
            cases h : q a
            · rfl
            · exact absurd h hq
          by_cases hp : p a = true
          · simp [hp, hqf] at heq
            omega
          · have hpf : p a = false := by
              cases h : p a
              · rfl
              · exact absurd h hp
            simp [hpf, hqf] at heq
            omega
      exact ih himpt heqt x hxl hpx

/-- If all cross predecessors of `s` are dead, deadIn equals the full
    in-count (and vice versa). -/
theorem deadIn_eq_inCount_iff (dead : Fin n → Bool) (s : Fin n) :
    deadInCount edges dead s = inCount edges s ↔
    (∀ e ∈ edges, e.2 = s → dead e.1 = true) := by
  constructor
  · intro heq e he hes
    have himp : ∀ x ∈ edges, (fun e => e.2 == s && dead e.1) x = true →
        (fun e => e.2 == s) x = true := by
      intro x _ hx
      simp only [Bool.and_eq_true] at hx
      exact hx.1
    have := countP_eq_forces_all edges
      (fun e => e.2 == s) (fun e => e.2 == s && dead e.1)
      himp heq.symm e he
    have hbeq : (e.2 == s) = true := by
      simp [hes]
    have := this hbeq
    simp only [Bool.and_eq_true] at this
    exact this.2
  · intro hall
    unfold deadInCount inCount
    apply List.countP_congr
    intro e he
    by_cases hes : e.2 = s
    · simp [hes, hall e he hes]
    · have : (e.2 == s) = false := by
        simp [hes]
      simp [this]

/-- The implementation's per-SCC decision, verbatim from
    computeDeadness: NOT forced (no seed, no live predecessor pushed
    the flag) and ext = sumRefs − internal − deadIn = 0 (stated
    subtraction-free). -/
def ImplEq (sumRefs internal : Fin n → Nat) (dead : Fin n → Bool) : Prop :=
  ∀ s, dead s = true ↔
    (¬ (seed s = true ∨ ∃ e ∈ edges, e.2 = s ∧ dead e.1 = false) ∧
     sumRefs s = internal s + deadInCount edges dead s)

/-- **The arithmetic is the spec**: under rc-exactness, the
    implementation's equation is `ScanEq`, so `scan_dead_iff_not_live`
    applies to computeDeadness as written. -/
theorem impl_fixpoint_is_spec
    (sumRefs internal : Fin n → Nat) (dead : Fin n → Bool)
    (hcount : ∀ s, sumRefs s = extRefs s + internal s + inCount edges s)
    (himpl : ImplEq edges seed sumRefs internal dead) :
    ScanEq edges extRefs seed dead := by
  intro s
  rw [himpl s]
  constructor
  · rintro ⟨hnf, harith⟩
    have hor := hnf
    rw [not_or] at hor
    obtain ⟨hseed, hnopred⟩ := hor
    have hseedf : seed s = false := by
      cases h : seed s
      · rfl
      · exact absurd h hseed
    have hall : ∀ e ∈ edges, e.2 = s → dead e.1 = true := by
      intro e he hes
      cases h : dead e.1 with
      | true => rfl
      | false => exact absurd ⟨e, he, hes, h⟩ hnopred
    have hdc := (deadIn_eq_inCount_iff edges dead s).mpr hall
    have hc := hcount s
    refine ⟨by omega, hseedf, hall⟩
  · rintro ⟨hext, hseedf, hall⟩
    have hdc := (deadIn_eq_inCount_iff edges dead s).mpr hall
    refine ⟨?_, ?_⟩
    · rw [not_or]
      refine ⟨by simp [hseedf], ?_⟩
      rintro ⟨e, he, hes, hdf⟩
      rw [hall e he hes] at hdf
      cases hdf
    · have hc := hcount s
      omega

end Condensation

/-! ## §4 Cell-level correctness

  Bridge from the condensation to the actual heap snapshot. `extRef`
  covers every reference source outside the capture: mutator stacks,
  the roots buffer, uncaptured heap cells' slots that the arithmetic
  cannot explain, and other collections' partitions (cross-collection
  edges — this is the SCC-side view of `cross_target_live` in
  yrc_proof.lean §5). -/

structure CellGraph where
  edge : Obj → Obj → Prop
  extRef : Obj → Prop

/-- A cell is live iff an external reference anchors it through heap
    edges (the cell-level ground truth; `anchored` of yrc_proof.lean). -/
inductive CellLive (g : CellGraph) : Obj → Prop where
  | ext (x : Obj) : g.extRef x → CellLive g x
  | step (x y : Obj) : CellLive g x → g.edge x y → CellLive g y

/-- Paths through heap edges, used to move liveness around inside an
    SCC (Tarjan guarantees SCC members are mutually reachable). -/
inductive EdgePath (g : CellGraph) : Obj → Obj → Prop where
  | refl (x : Obj) : EdgePath g x x
  | step (x y z : Obj) : EdgePath g x y → g.edge y z → EdgePath g x z

theorem cellLive_along_path (g : CellGraph) (u v : Obj)
    (hl : CellLive g u) (hp : EdgePath g u v) : CellLive g v := by
  induction hp with
  | refl => exact hl
  | step _ _ _ hedge ih => exact CellLive.step _ _ ih hedge

section CellBridge

variable {n : Nat}
variable (g : CellGraph)
variable (edges : List (Fin n × Fin n))
variable (extRefs : Fin n → Nat)
variable (seed : Fin n → Bool)
variable (captured : Obj → Prop)
variable (scc : Obj → Fin n)

/-- Any live captured cell sits in a live SCC.
    Premises are properties of `capture`:
    * `h_edge_resp` — every heap edge between captured cells was
      recorded (same SCC → internal; different → cross edge);
    * `h_closed` — an edge from an UNCAPTURED cell is unexplained by
      the captured arithmetic, so it lands in extRefs;
    * `h_ext` — direct external refs (stacks, roots buffer, foreign
      partitions) are counted in extRefs. -/
theorem captured_live_scc
    (h_edge_resp : ∀ u v, captured u → captured v → g.edge u v →
        scc u = scc v ∨ (scc u, scc v) ∈ edges)
    (h_closed : ∀ u v, captured v → g.edge u v → ¬ captured u →
        0 < extRefs (scc v))
    (h_ext : ∀ v, captured v → g.extRef v → 0 < extRefs (scc v)) :
    ∀ x, CellLive g x → captured x →
      LiveScc edges extRefs seed (scc x) := by
  intro x hl
  induction hl with
  | ext x h =>
    intro hc
    exact LiveScc.ext _ (h_ext x hc h)
  | step u v hu hedge ih =>
    intro hcv
    by_cases hcu : captured u
    · cases h_edge_resp u v hcu hcv hedge with
      | inl heq => rw [← heq]; exact ih hcu
      | inr hmem => exact LiveScc.pred _ _ hmem (ih hcu)
    · exact LiveScc.ext _ (h_closed u v hcv hedge hcu)

/-- **Soundness**: every cell of a dead SCC is unanchored in the
    snapshot — freeing it is justified by yrc_proof.lean §1
    (`yrc_safety`) + §3 (stability through the commit window). -/
theorem tarjan_sound
    (dead : Fin n → Bool)
    (hfix : ScanEq edges extRefs seed dead)
    (h_edge_resp : ∀ u v, captured u → captured v → g.edge u v →
        scc u = scc v ∨ (scc u, scc v) ∈ edges)
    (h_closed : ∀ u v, captured v → g.edge u v → ¬ captured u →
        0 < extRefs (scc v))
    (h_ext : ∀ v, captured v → g.extRef v → 0 < extRefs (scc v)) :
    ∀ x, captured x → dead (scc x) = true → ¬ CellLive g x := by
  intro x hc hd hl
  exact live_not_dead edges extRefs seed dead hfix (scc x)
    (captured_live_scc g edges extRefs seed captured scc
      h_edge_resp h_closed h_ext x hl hc) hd

/-- Every cell of a live SCC is genuinely live. Needs the converse
    premises: external counts are EXACT (no phantom refs — deferred
    decs inflate rc, so in the running system this holds only after
    the merge; overcounts delay collection by a round, they never
    cause a wrong free), cross edges are real edges, and SCC members
    are mutually reachable (Tarjan). -/
theorem live_scc_cells_live
    (h_ext_exact : ∀ s : Fin n, 0 < extRefs s →
        ∃ v, captured v ∧ scc v = s ∧ g.extRef v)
    (h_seed_exact : ∀ s : Fin n, seed s = true →
        ∃ v, captured v ∧ scc v = s ∧ g.extRef v)
    (h_cross_real : ∀ (u s : Fin n), (u, s) ∈ edges →
        ∃ cu cv, captured cu ∧ captured cv ∧ scc cu = u ∧ scc cv = s ∧
          g.edge cu cv)
    (h_conn : ∀ u v, captured u → captured v → scc u = scc v →
        EdgePath g u v) :
    ∀ s, LiveScc edges extRefs seed s →
      ∀ x, captured x → scc x = s → CellLive g x := by
  intro s hl
  induction hl with
  | ext s h =>
    intro x hc hs
    obtain ⟨v, hcv, hsv, hev⟩ := h_ext_exact s h
    exact cellLive_along_path g v x (CellLive.ext v hev)
      (h_conn v x hcv hc (by rw [hsv, hs]))
  | root s h =>
    intro x hc hs
    obtain ⟨v, hcv, hsv, hev⟩ := h_seed_exact s h
    exact cellLive_along_path g v x (CellLive.ext v hev)
      (h_conn v x hcv hc (by rw [hsv, hs]))
  | pred u s hmem _ ih =>
    intro x hc hs
    obtain ⟨cu, cv, hccu, hccv, hscu, hscv, he⟩ := h_cross_real u s hmem
    have hculive : CellLive g cu := ih cu hccu hscu
    exact cellLive_along_path g cv x (CellLive.step cu cv hculive he)
      (h_conn cv x hccv hc (by rw [hscv, hs]))

/-- **Completeness**: every captured garbage cell is marked dead — the
    scan collects ALL cycles reachable from the candidate set in one
    round (on the snapshot; concurrent inflation only defers). -/
theorem tarjan_complete
    (horder : ∀ e ∈ edges, e.2 < e.1)
    (dead : Fin n → Bool)
    (hfix : ScanEq edges extRefs seed dead)
    (h_ext_exact : ∀ s : Fin n, 0 < extRefs s →
        ∃ v, captured v ∧ scc v = s ∧ g.extRef v)
    (h_seed_exact : ∀ s : Fin n, seed s = true →
        ∃ v, captured v ∧ scc v = s ∧ g.extRef v)
    (h_cross_real : ∀ (u s : Fin n), (u, s) ∈ edges →
        ∃ cu cv, captured cu ∧ captured cv ∧ scc cu = u ∧ scc cv = s ∧
          g.edge cu cv)
    (h_conn : ∀ u v, captured u → captured v → scc u = scc v →
        EdgePath g u v) :
    ∀ x, captured x → ¬ CellLive g x → dead (scc x) = true := by
  intro x hc hnl
  apply not_live_dead edges extRefs seed horder dead hfix
  intro hl
  exact hnl (live_scc_cells_live g edges extRefs seed captured scc
    h_ext_exact h_seed_exact h_cross_real h_conn (scc x) hl x hc rfl)

end CellBridge

/-! ## §5 Validate-time demotion must propagate

  validateDead demotes a dead SCC when a mutator dirtied it (queue
  entry or changed rc word). A demoted SCC becomes a survivor: its
  slots are NOT nil'd at commit, so its captured out-edges remain in
  the heap. If a cross target of a demoted SCC stayed in the dead set,
  the commit would free a cell that a surviving cell still points to —
  deadIn had explained that edge away under the assumption that the
  predecessor dies too.

  Minimal instance of the hazard: two SCCs, one edge 1 → 0, both
  computed dead (ext = 0 for both; SCC 0's only reference comes from
  SCC 1, subtracted as deadIn). Demote SCC 1 alone, and the freed set
  {0} has a live in-edge from the surviving SCC 1.

  The theorem below states the repair: if the demoted set `K` is
  successor-closed within the dead set (demoting s also demotes every
  dead t with a captured edge s → t, transitively — one countdown pass
  suffices because edges go from higher to lower ids), then the freed
  set F = dead ∖ K is predecessor-closed: every captured edge into F
  comes from F. Combined with extRefs = 0 and no seed (ScanEq) this
  makes F closed in the sense of yrc_proof.lean §3, so freeing F is
  covered by `commit_free_safe` there. -/

theorem demotion_closure_sound {n : Nat}
    (edges : List (Fin n × Fin n))
    (extRefs : Fin n → Nat) (seed : Fin n → Bool)
    (dead : Fin n → Bool)
    (hfix : ScanEq edges extRefs seed dead)
    (K : Fin n → Prop)                       -- the demoted SCCs
    (hK_closed : ∀ e ∈ edges, K e.1 → dead e.2 = true → K e.2) :
    -- every captured edge into the freed set comes from the freed set
    ∀ e ∈ edges, (dead e.2 = true ∧ ¬ K e.2) →
      (dead e.1 = true ∧ ¬ K e.1) := by
  intro e he ⟨hd2, hk2⟩
  have hd1 : dead e.1 = true :=
    ((hfix e.2).mp hd2).2.2 e he rfl
  refine ⟨hd1, ?_⟩
  intro hk1
  exact hk2 (hK_closed e he hk1 hd2)

/-- Without successor-closure the guarantee genuinely fails: in the
    two-SCC instance above, demoting only SCC 1 leaves the freed set
    {0} with an in-edge from a survivor. (Concrete witness, checked by
    `decide`-style evaluation.) -/
example :
    let edges : List (Fin 2 × Fin 2) := [(1, 0)]
    let dead : Fin 2 → Bool := fun _ => true
    let K : Fin 2 → Prop := fun s => s = 1     -- demote only SCC 1
    -- ScanEq holds for `dead` (both SCCs legitimately computed dead) …
    ScanEq edges (fun _ => 0) (fun _ => false) dead ∧
    -- … yet the freed set {0} has an in-edge from surviving SCC 1:
    ((1, 0) ∈ edges ∧ dead 0 = true ∧ ¬ K 0 ∧ K 1) := by
  refine ⟨?_, ?_⟩
  · intro s
    simp
  · refine ⟨by simp, rfl, by simp, rfl⟩

/-! ## Summary (all QED, no sorry)

  * `descending_induction` — the sinks-first SCC numbering makes the
    reverse scan a well-founded definition.
  * `scan_dead_iff_not_live` — the scan marks an SCC dead iff it is
    not externally anchored: exact garbage identification in ONE
    linear pass over the condensation.
  * `impl_fixpoint_is_spec` — the implementation's arithmetic
    (ext = sumRefs − internal − deadIn, forcedLive propagation) is
    that same equation under rc-exactness.
  * `tarjan_sound` / `tarjan_complete` — at the cell level: dead cells
    are unanchored (frees are safe) and unanchored captured cells are
    freed (nothing is missed on the snapshot).
  * `demotion_closure_sound` + counterexample — demotion is sound iff
    it propagates along captured cross edges to still-dead targets;
    a lone demotion can leave the freed set with a surviving
    predecessor.

  Not modeled: the Tarjan DFS itself (its two classical invariants —
  SCC partition and sinks-first emission — enter as premises), the
  iterative traceStack encoding, crossPend (cross-collection edges are
  folded into `extRefs`, justified by yrc_proof.lean §5), and the
  temporal validity of rc-exactness (yrc_proof.lean §4).
-/