Archive research_stack_usage_graph.md

archive/2026-07-02/docs/research_stack_usage_graph.md

@@ -0,0 +1,92 @@
+# Research Stack Searchable Usage Map
+
+- **Entities:** 13296
+- **Edges:** 13913
+
+## Entity counts
+- `def`: 7784
+- `theorem`: 3175
+- `doc`: 1235
+- `module`: 849
+- `script`: 215
+- `mathlib`: 15
+- `service`: 8
+- `node`: 6
+- `database`: 4
+- `skill`: 3
+- `goal`: 2
+
+## Top modules by in-degree
+- `FixedPoint` — imported by 97 modules
+- `Bind` — imported by 18 modules
+- `Mathlib.Data.Nat.Basic` — imported by 16 modules
+- `Mathlib.Data.Real.Basic` — imported by 11 modules
+- `PhysicsScalarBridge` — imported by 10 modules
+- `ExtremeParameterTest` — imported by 9 modules
+- `Mathlib` — imported by 7 modules
+- `Mathlib.Tactic` — imported by 6 modules
+- `ManifoldNetworking` — imported by 6 modules
+- `Quaternion` — imported by 4 modules
+- `Mathlib.Data.Finset.Basic` — imported by 4 modules
+- `Mathlib.Data.Set.Basic` — imported by 4 modules
+- `Atoms` — imported by 4 modules
+- `PBACSSignal` — imported by 4 modules
+- `Mathlib.Data.Fin.Basic` — imported by 3 modules
+- `SSMS` — imported by 3 modules
+- `Mathlib.Data.List.Basic` — imported by 3 modules
+- `FAMM` — imported by 3 modules
+- `Mathlib.Data.Int.Basic` — imported by 3 modules
+- `Boundary` — imported by 3 modules
+
+## Top theorem-producing modules
+- `HamiltonianVerification` — theorems=324 defs=7 sorries=0 kind=quantum
+- `i` — theorems=107 defs=7 sorries=0 kind=algebra
+- `green_57` — theorems=69 defs=34 sorries=0 kind=algebra
+- `i` — theorems=68 defs=1 sorries=0 kind=number_theory
+- `SidonSets` — theorems=68 defs=17 sorries=0 kind=number_theory
+- `DeltaGCLCompression` — theorems=62 defs=37 sorries=0 kind=algebra
+- `FixedPoint` — theorems=62 defs=99 sorries=0 kind=fixedpoint
+- `HamiltonianFormal` — theorems=61 defs=25 sorries=0 kind=quantum
+- `E8Sidon` — theorems=60 defs=23 sorries=5 kind=number_theory
+- `tenenbaum` — theorems=54 defs=8 sorries=0 kind=number_theory
+- `bipartite_reconstruction` — theorems=52 defs=14 sorries=0 kind=algebra
+- `erdos_846` — theorems=47 defs=5 sorries=0 kind=number_theory
+- `erdos_152` — theorems=45 defs=7 sorries=0 kind=number_theory
+- `Q16InverseProof` — theorems=44 defs=10 sorries=0 kind=fixedpoint
+- `SpherionTwinPrime` — theorems=41 defs=28 sorries=0 kind=number_theory
+- `Tests` — theorems=39 defs=20 sorries=0 kind=algebra
+- `SpatialHashCodec` — theorems=36 defs=19 sorries=0 kind=rrc
+- `DomainDetector` — theorems=31 defs=7 sorries=0 kind=rrc
+- `graph_conjecture2` — theorems=30 defs=2 sorries=0 kind=algebra
+- `ii` — theorems=28 defs=3 sorries=0 kind=number_theory
+
+## Math-kind distribution
+- `fixedpoint`: 429
+- `algebra`: 132
+- `avm`: 51
+- `quantum`: 50
+- `braid`: 36
+- `routing`: 33
+- `geometry`: 33
+- `rrc`: 31
+- `number_theory`: 31
+- `general`: 15
+- `analysis`: 8
+
+## Neon-hosted services
+- **PostgreSQL on neon** —  arxiv-pg 
+- **Ollama on neon** — http://100.92.88.64:11434  DeepSeek-Prover,Goedel-Prover,Qwen,hermes3
+- **Vikunja on neon** — http://100.92.88.64:3456  
+- **Headroom proxy on neon** — http://100.92.88.64:8787  
+
+## Databases on neon
+- **arxiv** — arxiv_papers,arxiv_paper_codes8,citations 
+- **ene** —  ENE graph schema
+- **appflowy** —  
+- **vikunja** —  
+
+## How to use this graph
+- Load `research_stack_usage_graph.json` into any search/index tool.
+- Render the DOT with: `dot -Tsvg research_stack_usage_graph.dot -o graph.svg`
+- Query examples: find modules with `math_kind=braid` and `sorry_count>0`;
+  find scripts that touch `db:arxiv`; find docs referenced by a script.