docs: add Research Stack porting candidates shortlist

Generate a ranked shortlist of high-value Research Stack modules to port, scored by theorem count, in-degree (foundational), definitions, and sorry penalty. Filtered to SilverSight-relevant math kinds. - docs/research_stack_porting_candidates.md — top 50 + by-kind breakdown + zero-sorry foundation modules + script/database links - docs/generate_porting_candidates.py — regeneration from usage graph JSON Build: 2978 jobs, 0 errors (lake build)
2026-07-31 01:25:21 +00:00 · 2026-06-21 06:42:53 -05:00 · 2026-06-21 06:42:53 -05:00 · 974b4768ad
commit 974b4768ad
parent 3b15d252f7
4 changed files with 321 additions and 1 deletions
--- a/PORTING_MAP.md
+++ b/PORTING_MAP.md
@ -4,7 +4,8 @@
 **Target:** SilverSight (`https://github.com/allaunthefox/SilverSight`)  
 **Goal:** Move only what is proven, active, and compatible with the library-method architecture.

-**Searchable inventory:** `docs/research_stack_usage_graph.json` / `.md` / `.dot` — a point graph of all 849 Semantics modules, 3,175 theorems, 7,784 defs, 215 scripts, 1,235 docs, services, databases, nodes, skills, and goals.
+**Searchable inventory:** `docs/research_stack_usage_graph.json` / `.md` / `.dot` — a point graph of all 849 Semantics modules, 3,175 theorems, 7,784 defs, 215 scripts, 1,235 docs, services, databases, nodes, skills, and goals.  
+**Porting shortlist:** `docs/research_stack_porting_candidates.md` — ranked by theorem count, in-degree, definitions, and sorry count.

 ---

--- a/README.md
+++ b/README.md
@ -26,6 +26,8 @@ databases, nodes, skills, and goals. Use them to discover what is worth porting.
 - `docs/research_stack_usage_graph.md` — human-readable summary
 - `docs/research_stack_usage_graph.dot` — visual graph (render with Graphviz)
 - `docs/generate_research_stack_usage_map.py` — regeneration script
+- `docs/research_stack_porting_candidates.md` — ranked porting shortlist
+- `docs/generate_porting_candidates.py` — candidates regeneration script

 ## Key Papers

--- a/docs/generate_porting_candidates.py
+++ b/docs/generate_porting_candidates.py
@ -0,0 +1,97 @@
+#!/usr/bin/env python3
+"""Generate a high-value porting candidates report from the Research Stack usage graph."""
+import json
+from collections import Counter
+from pathlib import Path
+
+ROOT = Path("/tmp/SilverSight/docs")
+graph = json.loads((ROOT / "research_stack_usage_graph.json").read_text())
+
+ents = {e["id"]: e for e in graph["entities"]}
+
+# Build in-degree and dependency depth
+indeg = Counter()
+outdeg = Counter()
+for e in graph["edges"]:
+    if e["kind"] == "imports":
+        indeg[e["dst"]] += 1
+        outdeg[e["src"]] += 1
+
+modules = [e for e in graph["entities"] if e["kind"] == "module"]
+
+# Scoring: high theorem count, low sorries, imported by many, kind matches SilverSight priorities
+def score(m):
+    th = m.get("theorem_count", 0)
+    so = m.get("sorry_count", 0)
+    im = indeg.get(m["id"], 0)
+    de = m.get("def_count", 0)
+    # penalize sorries heavily, reward theorems and in-degree
+    return th * 2 + de + im * 3 - so * 10
+
+# Priority kinds for SilverSight
+priority_kinds = {"fixedpoint", "number_theory", "braid", "rrc", "avm", "geometry", "algebra"}
+
+candidates = sorted(
+    [m for m in modules if m.get("math_kind") in priority_kinds and m.get("sorry_count", 0) <= 5],
+    key=score,
+    reverse=True,
+)
+
+md = ["# Research Stack → SilverSight Porting Candidates", ""]
+md.append("Generated from `research_stack_usage_graph.json`. Scores reward theorem count,")
+md.append("in-degree (foundational), and definitions; penalize sorries. Filtered to")
+md.append("SilverSight-relevant math kinds with ≤5 sorries.")
+md.append("")
+
+md.append(f"## Top 50 candidates")
+md.append("")
+md.append("| Module | Kind | Theorems | Defs | Sorries | In-degree | Score |")
+md.append("|--------|------|----------|------|---------|-----------|-------|")
+for m in candidates[:50]:
+    md.append(
+        f"| `{m['name']}` | {m.get('math_kind','?')} | "
+        f"{m.get('theorem_count',0)} | {m.get('def_count',0)} | {m.get('sorry_count',0)} | "
+        f"{indeg.get(m['id'],0)} | {score(m)} |"
+    )
+md.append("")
+
+md.append("## Candidates by math kind")
+md.append("")
+for kind in priority_kinds:
+    kind_mods = [m for m in candidates if m.get("math_kind") == kind][:15]
+    if not kind_mods:
+        continue
+    md.append(f"### {kind}")
+    for m in kind_mods:
+        md.append(
+            f"- `{m['name']}` — th={m.get('theorem_count',0)} def={m.get('def_count',0)} "
+            f"sorry={m.get('sorry_count',0)} in={indeg.get(m['id'],0)}"
+        )
+    md.append("")
+
+md.append("## Zero-sorry foundation modules")
+md.append("")
+md.append("Modules with 0 sorries that are imported by at least 3 other modules:")
+md.append("")
+for m in sorted(
+    [m for m in modules if m.get("sorry_count", 0) == 0 and indeg.get(m["id"], 0) >= 3],
+    key=lambda x: -indeg.get(x["id"], 0),
+)[:30]:
+    md.append(
+        f"- `{m['name']}` ({m.get('math_kind','?')}) — imported by {indeg.get(m['id'],0)}, "
+        f"th={m.get('theorem_count',0)}"
+    )
+md.append("")
+
+md.append("## Most referenced concepts by script")
+md.append("")
+script_edges = [e for e in graph["edges"] if e["kind"] == "touches_database"]
+for db_edge in sorted(script_edges, key=lambda x: ents.get(x["src"], {}).get("name", ""))[:20]:
+    src = ents.get(db_edge["src"], {})
+    dst = ents.get(db_edge["dst"], {})
+    md.append(f"- `{src.get('name','?')}` → `{dst.get('name','?')}`")
+md.append("")
+
+(ROOT / "research_stack_porting_candidates.md").write_text("\n".join(md), encoding="utf-8")
+print(f"Wrote {ROOT / 'research_stack_porting_candidates.md'}")
+print(f"Total candidates: {len(candidates)}")
--- a/docs/research_stack_porting_candidates.md
+++ b/docs/research_stack_porting_candidates.md
@ -0,0 +1,220 @@
+# Research Stack → SilverSight Porting Candidates
+
+Generated from `research_stack_usage_graph.json`. Scores reward theorem count,
+in-degree (foundational), and definitions; penalize sorries. Filtered to
+SilverSight-relevant math kinds with ≤5 sorries.
+
+## Top 50 candidates
+
+| Module | Kind | Theorems | Defs | Sorries | In-degree | Score |
+|--------|------|----------|------|---------|-----------|-------|
+| `FixedPoint` | fixedpoint | 62 | 99 | 0 | 97 | 514 |
+| `EntropyMeasures` | fixedpoint | 4 | 456 | 0 | 0 | 464 |
+| `i` | algebra | 107 | 7 | 0 | 0 | 221 |
+| `green_57` | algebra | 69 | 34 | 0 | 0 | 172 |
+| `DeltaGCLCompression` | algebra | 62 | 37 | 0 | 0 | 161 |
+| `SidonSets` | number_theory | 68 | 17 | 0 | 0 | 153 |
+| `PistSimulation` | fixedpoint | 16 | 111 | 0 | 0 | 143 |
+| `i` | number_theory | 68 | 1 | 0 | 0 | 137 |
+| `bipartite_reconstruction` | algebra | 52 | 14 | 0 | 0 | 118 |
+| `tenenbaum` | number_theory | 54 | 8 | 0 | 0 | 116 |
+| `Law15_Field` | fixedpoint | 27 | 58 | 0 | 0 | 112 |
+| `SpherionTwinPrime` | number_theory | 41 | 28 | 0 | 0 | 110 |
+| `NBody` | fixedpoint | 13 | 83 | 0 | 0 | 109 |
+| `HachimojiPipeline` | fixedpoint | 0 | 105 | 0 | 0 | 105 |
+| `SSMS` | fixedpoint | 14 | 67 | 0 | 3 | 104 |
+| `erdos_846` | number_theory | 47 | 5 | 0 | 0 | 99 |
+| `Q16InverseProof` | fixedpoint | 44 | 10 | 0 | 0 | 98 |
+| `Tests` | algebra | 39 | 20 | 0 | 0 | 98 |
+| `erdos_152` | number_theory | 45 | 7 | 0 | 0 | 97 |
+| `E8Sidon` | number_theory | 60 | 23 | 5 | 0 | 93 |
+| `SpatialHashCodec` | rrc | 36 | 19 | 0 | 0 | 91 |
+| `ExtendedManifoldEncoding` | rrc | 23 | 42 | 0 | 0 | 88 |
+| `MassNumberPreSlots` | algebra | 0 | 82 | 0 | 0 | 82 |
+| `F01_Q16_16_FixedPoint` | fixedpoint | 27 | 19 | 0 | 0 | 73 |
+| `UniversalBridge` | fixedpoint | 26 | 20 | 0 | 0 | 72 |
+| `UnifiedConvictionFlow` | algebra | 17 | 38 | 0 | 0 | 72 |
+| `EntropyPhaseEngine` | fixedpoint | 10 | 51 | 0 | 0 | 71 |
+| `PhysicsScalarBridge` | fixedpoint | 0 | 41 | 0 | 10 | 71 |
+| `FoldedPointManifold` | avm | 21 | 28 | 0 | 0 | 70 |
+| `BurgersPDE` | fixedpoint | 20 | 29 | 0 | 0 | 69 |
+| `DomainDetector` | rrc | 31 | 7 | 0 | 0 | 69 |
+| `PreRegisteredPredictions` | algebra | 21 | 26 | 0 | 0 | 68 |
+| `AdjugateMatrix` | fixedpoint | 20 | 27 | 0 | 0 | 67 |
+| `SDPVerify` | algebra | 23 | 30 | 1 | 0 | 66 |
+| `ExtremeParameterTest` | algebra | 0 | 39 | 0 | 9 | 66 |
+| `TransportTheory` | fixedpoint | 26 | 14 | 0 | 0 | 66 |
+| `RustOISCDecompressor` | avm | 14 | 36 | 0 | 0 | 64 |
+| `DynamicCanal` | fixedpoint | 8 | 44 | 0 | 1 | 63 |
+| `graph_conjecture2` | algebra | 30 | 2 | 0 | 0 | 62 |
+| `HumanNeuralCompression` | fixedpoint | 15 | 32 | 0 | 0 | 62 |
+| `ii` | number_theory | 26 | 9 | 0 | 0 | 61 |
+| `ii` | number_theory | 28 | 3 | 0 | 0 | 59 |
+| `BraidSpherionBridge` | fixedpoint | 25 | 9 | 0 | 0 | 59 |
+| `ParameterSensitivity` | avm | 16 | 27 | 0 | 0 | 59 |
+| `HutterPrizeFlow` | algebra | 14 | 30 | 0 | 0 | 58 |
+| `Bind` | algebra | 6 | 21 | 3 | 18 | 57 |
+| `Classify` | algebra | 12 | 32 | 0 | 0 | 56 |
+| `CayleyFibergraph` | rrc | 24 | 8 | 0 | 0 | 56 |
+| `BaselineComparison` | braid | 15 | 24 | 0 | 0 | 54 |
+| `BraidEigensolid` | braid | 16 | 19 | 0 | 1 | 54 |
+
+## Candidates by math kind
+
+### braid
+- `BaselineComparison` — th=15 def=24 sorry=0 in=0
+- `BraidEigensolid` — th=16 def=19 sorry=0 in=1
+- `ThresholdVector` — th=15 def=17 sorry=0 in=0
+- `BraidDiatCodec` — th=13 def=19 sorry=0 in=0
+- `MOIMBenchmark` — th=5 def=33 sorry=0 in=0
+- `BraidSerial` — th=8 def=26 sorry=0 in=0
+- `EntropyCollapseDetector` — th=6 def=28 sorry=0 in=0
+- `TopologicalBraidAdapter` — th=8 def=23 sorry=0 in=0
+- `CalibratedKernel` — th=1 def=32 sorry=0 in=0
+- `DimensionalConsistency` — th=7 def=18 sorry=0 in=0
+- `Toolkit` — th=9 def=14 sorry=0 in=0
+- `ASICTopology` — th=5 def=21 sorry=0 in=0
+- `LogogramRotationLoop` — th=9 def=13 sorry=0 in=0
+- `BraidedField` — th=4 def=20 sorry=0 in=0
+- `MereotopologicalSheafHypergraph` — th=6 def=15 sorry=0 in=0
+
+### rrc
+- `SpatialHashCodec` — th=36 def=19 sorry=0 in=0
+- `ExtendedManifoldEncoding` — th=23 def=42 sorry=0 in=0
+- `DomainDetector` — th=31 def=7 sorry=0 in=0
+- `CayleyFibergraph` — th=24 def=8 sorry=0 in=0
+- `Prohibited` — th=10 def=30 sorry=0 in=0
+- `TreeDIATKruskal` — th=16 def=13 sorry=0 in=0
+- `PIST` — th=11 def=21 sorry=0 in=0
+- `ErdosHarness` — th=5 def=29 sorry=0 in=1
+- `ManifoldBoundaryAtlas` — th=9 def=15 sorry=0 in=0
+- `BraidTreeDIATPIST` — th=9 def=11 sorry=0 in=0
+- `Witness` — th=10 def=5 sorry=0 in=1
+- `GeometricCompressionWorkspace` — th=3 def=20 sorry=0 in=0
+- `Emit` — th=0 def=26 sorry=0 in=0
+- `RRCLogogramProjection` — th=7 def=8 sorry=0 in=1
+- `Verification` — th=5 def=13 sorry=0 in=0
+
+### geometry
+- `ManifoldNetworking` — th=8 def=14 sorry=0 in=6
+- `TriangleManifold` — th=10 def=20 sorry=0 in=0
+- `BlitterPolymorphism` — th=5 def=26 sorry=0 in=0
+- `PathEpigeneticManifold` — th=7 def=21 sorry=0 in=0
+- `S3CProjectedGeodesicResolution` — th=10 def=15 sorry=0 in=0
+- `S3C` — th=11 def=9 sorry=0 in=0
+- `TopologicalStateMachine` — th=7 def=15 sorry=0 in=0
+- `BraidField` — th=0 def=23 sorry=0 in=1
+- `ManifoldBlit` — th=4 def=17 sorry=0 in=0
+- `InformationConservation` — th=8 def=5 sorry=0 in=0
+- `PhiShellEncoding` — th=4 def=10 sorry=0 in=0
+- `UniversalCoupling` — th=1 def=13 sorry=0 in=1
+- `GoldenSpiralNavigation` — th=1 def=14 sorry=0 in=0
+- `NS_MD` — th=0 def=16 sorry=0 in=0
+- `CollectiveManifoldInterface` — th=3 def=9 sorry=0 in=0
+
+### algebra
+- `i` — th=107 def=7 sorry=0 in=0
+- `green_57` — th=69 def=34 sorry=0 in=0
+- `DeltaGCLCompression` — th=62 def=37 sorry=0 in=0
+- `bipartite_reconstruction` — th=52 def=14 sorry=0 in=0
+- `Tests` — th=39 def=20 sorry=0 in=0
+- `MassNumberPreSlots` — th=0 def=82 sorry=0 in=0
+- `UnifiedConvictionFlow` — th=17 def=38 sorry=0 in=0
+- `PreRegisteredPredictions` — th=21 def=26 sorry=0 in=0
+- `SDPVerify` — th=23 def=30 sorry=1 in=0
+- `ExtremeParameterTest` — th=0 def=39 sorry=0 in=9
+- `graph_conjecture2` — th=30 def=2 sorry=0 in=0
+- `HutterPrizeFlow` — th=14 def=30 sorry=0 in=0
+- `Bind` — th=6 def=21 sorry=3 in=18
+- `Classify` — th=12 def=32 sorry=0 in=0
+- `EpistemicHonesty` — th=16 def=20 sorry=0 in=0
+
+### avm
+- `FoldedPointManifold` — th=21 def=28 sorry=0 in=0
+- `RustOISCDecompressor` — th=14 def=36 sorry=0 in=0
+- `ParameterSensitivity` — th=16 def=27 sorry=0 in=0
+- `CandidateDictionary` — th=14 def=20 sorry=0 in=0
+- `FractionScan` — th=17 def=14 sorry=0 in=0
+- `Omindirection` — th=12 def=21 sorry=0 in=1
+- `GCCL` — th=12 def=18 sorry=0 in=1
+- `ExperimentTracker` — th=11 def=11 sorry=0 in=0
+- `ContinuedFractionCompression` — th=10 def=12 sorry=0 in=0
+- `MinimalBitcoinL3` — th=13 def=6 sorry=0 in=0
+- `BernoulliOccupancyShockbow` — th=6 def=18 sorry=0 in=0
+- `LogogramSubstitution` — th=8 def=14 sorry=0 in=0
+- `LadderLUT` — th=8 def=13 sorry=0 in=0
+- `AntiBraidStorm` — th=9 def=7 sorry=0 in=0
+- `Surface` — th=10 def=4 sorry=0 in=0
+
+### number_theory
+- `SidonSets` — th=68 def=17 sorry=0 in=0
+- `i` — th=68 def=1 sorry=0 in=0
+- `tenenbaum` — th=54 def=8 sorry=0 in=0
+- `SpherionTwinPrime` — th=41 def=28 sorry=0 in=0
+- `erdos_846` — th=47 def=5 sorry=0 in=0
+- `erdos_152` — th=45 def=7 sorry=0 in=0
+- `E8Sidon` — th=60 def=23 sorry=5 in=0
+- `ii` — th=26 def=9 sorry=0 in=0
+- `ii` — th=28 def=3 sorry=0 in=0
+- `ImaginarySemanticTime` — th=19 def=16 sorry=0 in=0
+- `SidonAVM` — th=3 def=24 sorry=0 in=0
+- `GoormaghtighEnumeration` — th=13 def=1 sorry=0 in=0
+- `PrimeGearCache` — th=7 def=13 sorry=0 in=0
+- `AntiDiophantine` — th=10 def=6 sorry=0 in=0
+- `GoldenRatioSeparation` — th=8 def=8 sorry=0 in=0
+
+### fixedpoint
+- `FixedPoint` — th=62 def=99 sorry=0 in=97
+- `EntropyMeasures` — th=4 def=456 sorry=0 in=0
+- `PistSimulation` — th=16 def=111 sorry=0 in=0
+- `Law15_Field` — th=27 def=58 sorry=0 in=0
+- `NBody` — th=13 def=83 sorry=0 in=0
+- `HachimojiPipeline` — th=0 def=105 sorry=0 in=0
+- `SSMS` — th=14 def=67 sorry=0 in=3
+- `Q16InverseProof` — th=44 def=10 sorry=0 in=0
+- `F01_Q16_16_FixedPoint` — th=27 def=19 sorry=0 in=0
+- `UniversalBridge` — th=26 def=20 sorry=0 in=0
+- `EntropyPhaseEngine` — th=10 def=51 sorry=0 in=0
+- `PhysicsScalarBridge` — th=0 def=41 sorry=0 in=10
+- `BurgersPDE` — th=20 def=29 sorry=0 in=0
+- `AdjugateMatrix` — th=20 def=27 sorry=0 in=0
+- `TransportTheory` — th=26 def=14 sorry=0 in=0
+
+## Zero-sorry foundation modules
+
+Modules with 0 sorries that are imported by at least 3 other modules:
+
+- `FixedPoint` (fixedpoint) — imported by 97, th=62
+- `PhysicsScalarBridge` (fixedpoint) — imported by 10, th=0
+- `ExtremeParameterTest` (algebra) — imported by 9, th=0
+- `ManifoldNetworking` (geometry) — imported by 6, th=8
+- `Atoms` (fixedpoint) — imported by 4, th=0
+- `PBACSSignal` (fixedpoint) — imported by 4, th=0
+- `Quaternion` (fixedpoint) — imported by 4, th=1
+- `FAMM` (fixedpoint) — imported by 3, th=0
+- `Boundary` (quantum) — imported by 3, th=0
+- `SSMS` (fixedpoint) — imported by 3, th=14
+- `Core` (algebra) — imported by 3, th=0
+
+## Most referenced concepts by script
+
+- `alphaproof_loop.py` → `ene`
+- `arxiv_crossref_stream.py` → `arxiv`
+- `arxiv_crossref_stream.py` → `ene`
+- `arxiv_oaipmh_harvest.py` → `arxiv`
+- `bao_peak_shift.py` → `ene`
+- `batch_embed_artifacts.py` → `ene`
+- `beaver_mask_freshness_negative_controls.py` → `ene`
+- `benchmark_finsler_qaoa.py` → `ene`
+- `benchmark_finsler_qap.py` → `ene`
+- `braid_diat_codec.py` → `ene`
+- `braid_mutation_optimizer.py` → `ene`
+- `braid_search.py` → `ene`
+- `braid_vcn_encoder.py` → `ene`
+- `build_corpus250.py` → `arxiv`
+- `build_corpus250.py` → `ene`
+- `build_math_symbols_db.py` → `ene`
+- `build_pist_matrices_250.py` → `ene`
+- `burgers_0d_braid_exact.py` → `ene`
+- `burgers_2d_simplification.py` → `ene`
+- `burgers_cfl_sweep.py` → `ene`