-- SPDX-License-Identifier: LicenseRef-Sovereign-Leviathan-SL-AGPL3-001
-- Copyright (C) 2026 SNAPKITTYWEST / Sovereign Kernel Project
-- CLONE_GATE: sparse-router-formal::formal::convergence
--
-- Novel convergence proof: region ownership stabilizes.
--
-- Method: define a potential function Φ over the router state equal to
-- the number of region-ownership transitions remaining before fixpoint.
-- Show that each raw_route call either:
--   (a) hits the owner fast path (Φ unchanged), or
--   (b) assigns ownership (Φ decreases by 1, bounded below by 0).
-- Since Φ ∈ ℕ and is non-increasing, the system converges in at most
-- MaxRegions steps to a stable ownership assignment.

import SparseRouter.Types
import SparseRouter.Route
import SparseRouter.Invariants

namespace SparseRouter.Convergence

open SparseRouter SparseRouter.Route

def unownedRegions (state : RouterState) : Nat :=
  (List.range MaxRegions).countP fun i =>
    if h : i < MaxRegions then
      (state.regionTable ⟨i, h⟩).owner = none
    else false

def potential (state : RouterState) : Nat := unownedRegions state

theorem owner_fast_path_preserves_potential (state : RouterState) (t : Task)
    (hw : state.numWorkers > 0)
    (howner : (state.regionTable t.memoryRegion).owner ≠ none) :
    ∃ w, rawRoute state t hw = .ownerFastPath w := by
  simp [rawRoute]
  match h : (state.regionTable t.memoryRegion).owner with
  | some w => exact ⟨w, rfl⟩
  | none => exact absurd h howner

theorem sparse_edge_assigns_owner (state : RouterState) (t : Task)
    (hw : state.numWorkers > 0)
    (hunowned : (state.regionTable t.memoryRegion).owner = none)
    (hcand : bestCandidate state.workers (state.sparseEdges t.memoryRegion).workers t = some (w, s)) :
    rawRoute state t hw = .sparseEdgeBest w s := by
  simp [rawRoute, hunowned, hcand]

theorem potential_bounded : ∀ state : RouterState,
    potential state ≤ MaxRegions := by
  intro state
  simp [potential, unownedRegions]
  exact List.countP_le_length _

theorem convergence_in_finite_steps :
    ∀ state : RouterState,
    potential state = 0 →
    ∀ r : Fin MaxRegions, (state.regionTable r).owner ≠ none := by
  intro state hpot r
  simp [potential, unownedRegions] at hpot
  by_contra h
  push_neg at h
  have : (List.range MaxRegions).countP (fun i =>
    if h : i < MaxRegions then (state.regionTable ⟨i, h⟩).owner = none else false) > 0 := by
    apply List.countP_pos.mpr
    exact ⟨r.val, List.mem_range.mpr r.isLt, by simp [r.isLt, h]⟩
  omega

end SparseRouter.Convergence