import Semantics.Spectrum

/-!
# GraphRank — Spectral-gap-gated ranking on social graphs

Maps the PageRank/HITS/Fiedler/PPR mathematical lineage onto the 8-bin
Sidon spectral space from `Semantics.Spectrum`.

The central claim: a "bad link" is any edge whose `piecewiseMerge` result
fails `verifySpectralGap`. This corresponds to classical failures as follows:

  PageRank  → the edge drains bin-0 (stationary) mass into non-dominant bins
  HITS      → adjacent bins fire; top singular vector becomes degenerate
  Fiedler   → bin-1 gap closes; community boundary disappears
  PPR       → seeded propagation dies at the bad-link boundary

All compute paths use Q16_16 fixed-point. No Float.
-/

namespace Semantics.GraphRank

open Semantics.Spectrum

-- ────────────────────────────────────────────────────────────────────────────
-- Types
-- ────────────────────────────────────────────────────────────────────────────

/-- A node in a social graph: index + spectral authority signature. -/
structure SocialNode where
  id  : Nat
  sig : SpectralSignature
deriving Repr, BEq

/-- An edge in a social graph: directed link with its own spectral weight. -/
structure SocialEdge where
  src : Nat
  dst : Nat
  sig : SpectralSignature  -- link's own spectral contribution
deriving Repr, BEq

/-- A directed social graph. -/
structure SocialGraph where
  nodes : List SocialNode
  edges : List SocialEdge
deriving Repr

-- ────────────────────────────────────────────────────────────────────────────
-- Graph operations
-- ────────────────────────────────────────────────────────────────────────────

def SocialGraph.lookupNode (g : SocialGraph) (id : Nat) : Option SocialNode :=
  g.nodes.find? (·.id == id)

def SocialGraph.outEdges (g : SocialGraph) (id : Nat) : List SocialEdge :=
  g.edges.filter (·.src == id)

def SocialGraph.inEdges (g : SocialGraph) (id : Nat) : List SocialEdge :=
  g.edges.filter (·.dst == id)

-- ────────────────────────────────────────────────────────────────────────────
-- Bad-link gate
-- ────────────────────────────────────────────────────────────────────────────

/-- Density ceiling: all 8 bins active = total spectral saturation. -/
def maxActiveBins : Nat := binCount  -- 8

/-- An edge is "bad" if merging source × link × destination signatures
    fails `verifySpectralGap` (adjacent bins simultaneously active)
    or exceeds `withinDensityBound` (too many concurrent activations).

    Eigenvalue sort correspondences:
      PageRank bad link    → bin-0 mass leaks into adjacent bands
      HITS bad link        → singular vectors become degenerate
      Fiedler bad link     → bin-1 gap closes, communities merge
      PPR bad link         → propagation path is cut (seed unreachable) -/
def badLink (g : SocialGraph) (e : SocialEdge) : Bool :=
  match g.lookupNode e.src, g.lookupNode e.dst with
  | some s, some d =>
      let merged := SpectralSignature.piecewiseMerge
                      (SpectralSignature.piecewiseMerge s.sig e.sig) d.sig
      !merged.verifySpectralGap || !merged.withinDensityBound maxActiveBins
  | _, _ => true  -- missing endpoint is conservatively bad

def SocialGraph.badLinkCount (g : SocialGraph) : Nat :=
  g.edges.countP (badLink g)

def SocialGraph.isClean (g : SocialGraph) : Bool :=
  g.edges.all (fun e => !badLink g e)

-- ────────────────────────────────────────────────────────────────────────────
-- Personalized PageRank propagation in spectral space
-- ────────────────────────────────────────────────────────────────────────────

/-- One PPR step: each node accumulates merged signatures from clean in-neighbors.
    Bad links are cut and do not contribute spectral mass. -/
def pprStep (g : SocialGraph) (scores : List (Nat × SpectralSignature))
    : List (Nat × SpectralSignature) :=
  scores.map fun (id, sig) =>
    let cleanIn := g.inEdges id |>.filter (fun e => !badLink g e)
    let merged  := cleanIn.foldl
      (fun acc e =>
        match scores.find? (fun s => s.1 == e.src) with
        | some (_, s) => SpectralSignature.piecewiseMerge acc s
        | none        => acc)
      sig
    (id, merged)

def initScores (g : SocialGraph) : List (Nat × SpectralSignature) :=
  g.nodes.map (fun n => (n.id, n.sig))

/-- Run PPR for k steps. k-bounded so termination is trivial. -/
def pprRun (g : SocialGraph) (k : Nat) : List (Nat × SpectralSignature) :=
  (List.range k).foldl (fun acc _ => pprStep g acc) (initScores g)

-- ────────────────────────────────────────────────────────────────────────────
-- Rank modes — eigenvalue sort correspondence
-- ────────────────────────────────────────────────────────────────────────────

/-- Each classical ranking algorithm favors a specific spectral bin range.
    This type makes the correspondence explicit and machine-checkable. -/
inductive RankMode
  | pagerank                   -- bin 0: stationary distribution (DC)
  | hitsAuthority              -- bins 0+1: top singular vector
  | fiedler                    -- bin 1: community boundary eigenvector
  | personalizedPR (seed : Fin 8)  -- whichever bin the seed activates
  | cheirank                   -- inverted bin 0: givers rank above receivers
  deriving Repr, BEq

/-- Project a signature onto a rank mode's preferred bin(s).
    Sorting nodes by `modeScore` recovers the classical eigenvalue sort
    for that method, grounded in the 8-bin Sidon basis. -/
def modeScore (mode : RankMode) (sig : SpectralSignature) : Q16_16 :=
  let b := sig.bins
  match mode with
  | .pagerank          => b.getD 0 Q16_16.zero
  | .hitsAuthority     => Q16_16.add (b.getD 0 Q16_16.zero) (b.getD 1 Q16_16.zero)
  | .fiedler           => b.getD 1 Q16_16.zero
  | .personalizedPR n  => b.getD n.val Q16_16.zero
  | .cheirank          => Q16_16.sub Q16_16.one (b.getD 0 Q16_16.zero)

-- ────────────────────────────────────────────────────────────────────────────
-- Spectral ranking
-- ────────────────────────────────────────────────────────────────────────────

/-- Spectral overlap with a seed = the PPR dot-product score.
    Higher overlap = more semantically aligned with the seed community. -/
def spectralScore (sig seed : SpectralSignature) : Q16_16 :=
  SpectralSignature.spectralOverlap sig seed

private def insertDesc (x : Nat × Q16_16)
    : List (Nat × Q16_16) → List (Nat × Q16_16)
  | []     => [x]
  | h :: t => if Q16_16.lt h.2 x.2 then x :: h :: t
              else h :: insertDesc x t

private def sortDesc : List (Nat × Q16_16) → List (Nat × Q16_16)
  | []     => []
  | h :: t => insertDesc h (sortDesc t)

/-- Rank all nodes by spectral overlap with a seed after k PPR steps.
    Returns (node_id, score) sorted descending — this is the "eigenvalue sort"
    expressed in the 8-bin Sidon basis. -/
def rankNodes (g : SocialGraph) (k : Nat) (seed : SpectralSignature)
    : List (Nat × Q16_16) :=
  sortDesc (pprRun g k |>.map (fun (id, sig) => (id, spectralScore sig seed)))

-- ────────────────────────────────────────────────────────────────────────────
-- Invariants and receipts
-- ────────────────────────────────────────────────────────────────────────────

/-- The bad-link gate is a decidable Bool computation. -/
theorem badLink_decidable (g : SocialGraph) (e : SocialEdge) :
    badLink g e = true ∨ badLink g e = false := by
  cases badLink g e <;> simp

/-- The clean-graph predicate is a decidable Bool computation. -/
theorem isClean_decidable (g : SocialGraph) :
    g.isClean = true ∨ g.isClean = false := by
  cases g.isClean <;> simp

/-- Empty signature has no active bins. -/
theorem activeBins_empty :
    SpectralSignature.activeBins SpectralSignature.empty = [] := by
  native_decide

/-- Key open theorem: merging two gap-valid signatures with zero resonance
    degeneracy (no bin active in both) preserves the spectral gap.
    Interpretation: a clean edge cannot corrupt a clean node. -/
theorem cleanMerge_preservesGap (s e : SpectralSignature)
    (hs  : s.verifySpectralGap = true)
    (he  : e.verifySpectralGap = true)
    (hne : s.resonanceDegeneracy e = 0) :
    (SpectralSignature.piecewiseMerge s e).verifySpectralGap = true := by
  sorry  -- induction over 8-bin list; decidable by 2^8 case split

end Semantics.GraphRank