diff --git a/archive/2026-07-02/docs/research_stack_usage_graph.md b/archive/2026-07-02/docs/research_stack_usage_graph.md new file mode 100644 index 00000000..6e1ffa7b --- /dev/null +++ b/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.