mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
allaun
254bbfcb9a
- ExtensionScaffold.Physics.NBody: migrate remaining Q16_16 calls to FixedPoint.Q16_16; simplify quantumErasureAffectsWhichPath proof; fix solveSheetSpeedup match handling. Builds with 1 known sorry at verlet_preserves_energy_approximate. - Semantics.CompleteInteractionGraph: complete directed graph / every-point- touches-every-point exploration module (builds with 1 sorry). - Semantics.GraphRank: graph rank exploration module (builds with 1 sorry). Build: 3315 jobs NBody, 3303 jobs GraphRank, 3297 jobs CompleteInteractionGraph, 0 errors
196 lines
10 KiB
Text
196 lines
10 KiB
Text
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
|