SilverSight Porting Map
Source: Research-Stack (/home/allaun/Research Stack)
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.
Porting shortlist: docs/research_stack_porting_candidates.md — ranked by theorem count, in-degree, definitions, and sorry count.
1. Current SilverSight State
SilverSight already has a clean skeleton built around the 5-layer conceptual map:
Core/
SilverSightCore.lean ← 200-line invariant core
formal/
CoreFormalism/ ← Chentsov, Hachimoji, Q16_16
PVGS_DQ_Bridge/ ← 7 sections + master bridge
UniversalEncoding/ ← 50-token math address space
BindingSite/ ← amino-acid / protein binding sketches
python/
chaos_game.py
sidon_address.py
spectral_profile.py
q16_canonical.py
qubo/
finsler_metric.py
qubo_builder.py
qaoa_circuit.py
classical_solver.py
tests/
q16_roundtrip_test.py
docs/
ARCHITECTURE.md
LIBRARY_MANIFEST.md
RRC_PLACEMENT.md
REBASE_RULES.md ← seed ruleset from Research-Stack
2. Research-Stack Source Inventory
The source tree is large (~9,600 objects, ~1,300 Lean files). Most of it is exploratory or extracted to other repos. The durable, proven subset lives in:
| Area |
What matters |
0-Core-Formalism/lean/Semantics/Semantics/ |
Proven Lean modules: FixedPoint, SidonSets, SieveLemmas, InteractionGraphSidon, BraidEigensolid, BraidSpherionBridge, AVMIsa.*, RRC.Emit/Corpus250, TransportQUBOBridge, ChentsovBridge. |
4-Infrastructure/shim/ |
Python shims: qaoa_adapter.py, qubo_highs.py, benchmark_finsler_qap.py, chaos_game_16d.py, sidon_generation_kernel.py, geometric_entropy_explorer.py, candidate_certification_bridge.py, stack_solidification_audit.py. |
6-Documentation/docs/ |
AGENTS.md strict rules, architecture specs, distilled notes, specs (DP-RRC, Virtio-Net compute, etc.). |
5-Applications/text-to-cad/ |
CAD/URDF harness and skills. |
scripts/qc-flag/ |
Lean QC flagger protocol. |
.devin/skills/lean-proof/SKILL.md |
Mandatory proof-quality skill. |
.github/skills/contextstream-workflow/SKILL.md |
Persistent memory workflow. |
.github/skills/research-stack-workflow/SKILL.md |
Token-efficient proof workflow. |
.cursorrules, .devin/, .claude/, .roo/, .kilo/, .windsurf/ |
Editor/agent hook configs that enforce ContextStream-first rules. |
3. Porting Matrix
Legend
| Status |
Meaning |
| ✅ PORTED |
Already exists in SilverSight in compatible form. |
| 🟡 PORT |
Proven/active in Research-Stack; should move to SilverSight as-is or with minimal renaming. |
| 🟠 ADAPT |
Concept survives, but implementation must be refactored for the library-method architecture. |
| 🔴 DROP |
Quarantined, hairy, extracted to other repos, or superseded by SilverSight design. |
Core Layer
| Research-Stack |
SilverSight Target |
Status |
Notes |
Semantics.FixedPoint.lean |
formal/CoreFormalism/FixedPoint.lean |
✅ PORTED |
Full FixedPoint module with Q0_16/Q16_16 inverse trig, clamping, and determinism theorems. Replaced the thin Q16_16_Spec.lean. |
Semantics.Q16InverseProof.lean |
formal/CoreFormalism/FixedPoint.lean |
✅ PORTED |
Absorbed into FixedPoint.lean; inverse-proof machinery for bounded KKT systems and no-Float Q16_16 boundaries. |
Semantics.SidonSets.lean |
formal/CoreFormalism/SidonSets.lean |
✅ PORTED |
Builds (lake build CoreFormalism.SidonSets). Core Sidon definitions, extremal bounds, and Singer construction. Chaos-game appendix dropped. |
Semantics.InteractionGraphSidon.lean |
formal/CoreFormalism/InteractionGraphSidon.lean |
✅ PORTED |
Typed interaction graphs, bounded Sidon witness, RRC weak-axis CRT reconstruction. No Float. |
Semantics.SieveLemmas.lean |
formal/CoreFormalism/SieveLemmas.lean |
✅ PORTED |
Coprime-sieve observers, CRT reconstruction, executable human/dolphin witness. No Float. |
Semantics.ChentsovBridge.lean |
formal/CoreFormalism/ChentsovFinite.lean |
✅ PORTED |
Already present; keep the finite n=8 proof as the core theorem. |
Semantics.TransportQUBOBridge.lean |
QUBOLib/ or MetricLib/ |
🟡 PORT |
Finsler → QUBO bridge; 0 sorries, 2 axioms with TODO(lean-port). Clean fit. |
LexLib / MathLib Layer
| Research-Stack |
SilverSight Target |
Status |
Notes |
UniversalMathEncoding.lean |
formal/UniversalEncoding/UniversalMathEncoding.lean |
✅ PORTED |
Already exists. Needs LaTeX parser (expressionToReceipt) completed. |
ChiralitySpace.lean |
formal/UniversalEncoding/ChiralitySpace.lean |
✅ PORTED |
Already exists. |
math_symbols.py, build_math_symbols_db.py |
python/ |
🟡 PORT |
Token vocabulary builder for the 50-token address space. |
equation_shape_parser.py |
python/ |
🟡 PORT |
Parses equation strings into structural features. |
SearchLib Layer
| Research-Stack |
SilverSight Target |
Status |
Notes |
python/chaos_game_16d.py |
python/chaos_game.py |
🟠 ADAPT |
16D chaos game engine. Port logic but strip Research-Stack hair (VCN refs, etc.). |
python/sidon_generation_kernel.py |
python/sidon_address.py |
🟠 ADAPT |
Sidon label generation. Merge into existing sidon_address.py. |
python/geometric_entropy_explorer.py |
python/spectral_profile.py |
🟠 ADAPT |
Entropy-exploration candidate generator. Use as basis for SearchLib basin exploration. |
python/candidate_certification_bridge.py |
python/ |
🟠 ADAPT |
Generates Candidates.lean from entropy exploration. Refactor to produce SilverSight receipts. |
Semantics.BraidEigensolid.lean |
formal/CoreFormalism/BraidEigensolid.lean |
✅ PORTED |
Namespace SilverSight.BraidEigensolid. Builds: lake build CoreFormalism.BraidEigensolid (2986 jobs, 0 errors). Minor proof adaptations for Q16_16.toInt/coercion and PhaseVec.add zero-fast-path. |
Semantics.BraidSpherionBridge.lean |
formal/CoreFormalism/BraidSpherionBridge.lean |
✅ PORTED |
Namespace SilverSight.BraidSpherionBridge. Dependency chain (Tactics, Q16_16Numerics, DynamicCanal, Bind, BraidBracket, BraidStrand, BraidCross, BraidField) added to lakefile.lean roots. Builds: lake build CoreFormalism.BraidSpherionBridge (2989 jobs, 0 errors). |
Semantics.AntiBraidStorm.lean |
SearchLib/ |
🟡 PORT |
Adversarial verification for receipt aliasing. |
Semantics.BaselineComparison.lean |
SearchLib/ |
🟡 PORT |
Comparative baseline fixtures for eigensolid/meta-solid packing-bound claims. |
StructureLib Layer
| Research-Stack |
SilverSight Target |
Status |
Notes |
formal/UniversalEncoding/ChiralitySpace.lean |
StructureLib/ |
✅ PORTED |
Already present. |
formal/BindingSite/*.lean |
StructureLib/ or Library/BindingSite/ |
🟠 ADAPT |
Move from standalone directory into a library that imports only Core. |
MetricLib Layer
| Research-Stack |
SilverSight Target |
Status |
Notes |
4-Infrastructure/shim/qaoa_adapter.py |
qubo/finsler_metric.py / qubo/qubo_builder.py |
🟠 ADAPT |
2,421-line QUBO ↔ Ising ↔ Pauli bridge. Split into MetricLib + QUBOLib pieces. |
4-Infrastructure/shim/benchmark_finsler_qap.py |
qubo/test_optimize.py |
🟠 ADAPT |
Finsler-Randers QAP benchmark. Use as validation suite. |
4-Infrastructure/shim/benchmark_finsler_qaoa.py |
qubo/test_optimize.py |
🟠 ADAPT |
Finsler-QAOA benchmark. Use as validation suite. |
Semantics.TransportTheory / Semantics.ChentsovBridge |
MetricLib/ |
🟡 PORT |
Finsler metric + Chentsov theorem formalisms. |
QUBOLib Layer
| Research-Stack |
SilverSight Target |
Status |
Notes |
4-Infrastructure/shim/qaoa_adapter.py |
qubo/qaoa_circuit.py / qubo/qubo_builder.py |
🟠 ADAPT |
Split: QUBO builder stays in QUBOLib; Finsler metric moves to MetricLib. |
4-Infrastructure/shim/qubo_highs.py |
qubo/classical_solver.py |
🟠 ADAPT |
HiGHS MIP bridge and TSP assignment relaxation. Merge into classical_solver.py. |
4-Infrastructure/shim/pist_matrix_builder.py |
python/ |
🟡 PORT |
250-equation PIST matrix builder; produces deterministic 8×8 strand adjacency. |
4-Infrastructure/shim/build_corpus250.py |
python/ |
🟠 ADAPT |
Generates RRC corpus rows. Refactor to emit SilverSight LexLib inputs. |
PVGSLib Layer
| Research-Stack |
SilverSight Target |
Status |
Notes |
formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean + sections |
formal/PVGS_DQ_Bridge/ |
✅ PORTED |
Already present. Still has sorrys to close. |
Semantics.EffectiveBoundDQ.lean |
PVGSLib/ |
🟡 PORT |
DualQuaternion effective bounds; dependency for bridge. |
Semantics.DualQuaternion.lean (if exists) |
PVGSLib/ |
🟡 PORT |
Required by EffectiveBoundDQ. |
EventLib Layer
| Research-Stack |
SilverSight Target |
Status |
Notes |
SilverSightCore.lean TIC axiom |
Core/SilverSightCore.lean |
✅ PORTED |
Already present conceptually. |
python/chaos_game.py iteration counter |
python/chaos_game.py |
🟠 ADAPT |
Make TIC derivation explicit: each chaos-game step emits an event receipt. |
4-Infrastructure/shim/run_trace_v2_canary.py |
EventLib/ |
🔴 DROP |
Trace-canary runner tied to Research-Stack ENE schema. Reimplement against SilverSight core. |
AuditLib Layer
| Research-Stack |
SilverSight Target |
Status |
Notes |
5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py |
AuditLib/ |
🟠 ADAPT |
Receipt verification + SHA256 answer check. Refactor to verify SilverSight receipts. |
4-Infrastructure/shim/pvgs_receipt_hash.py |
formal/PVGS_DQ_Bridge/ / AuditLib/ |
✅ PORTED |
Already present in SilverSight. |
shared-data/data/stack_solidification/ receipts |
AuditLib/ |
🔴 DROP |
Research-Stack runtime receipts; archive only. Regenerate in SilverSight. |
RRCLib Layer
| Research-Stack |
SilverSight Target |
Status |
Notes |
Semantics.RRC.Emit.lean |
RRCLib/ |
🟡 PORT |
Alignment classifier; emits RRC verdicts. |
Semantics.RRC.Corpus250.lean |
RRCLib/ |
🟡 PORT |
250-equation raw-feature corpus. |
Semantics.AVMIsa.Emit.lean |
RRCLib/ |
🟡 PORT |
Sole output boundary for top-level receipt JSON. |
Semantics.AVMIsa.Run.lean |
Core/SilverSightCore.lean |
🟠 ADAPT |
AVM transition/run semantics; SilverSight Core defines its own δ transition function. |
Semantics.RRC.ReceiptDensity.lean |
RRCLib/ |
🟡 PORT |
Receipt density scoring. |
Semantics.RRCLogogramProjection.lean |
RRCLib/ |
🟡 PORT |
Logogram receipt types + admission gates. |
4-Infrastructure/shim/validate_rrc_predictions.py |
python/ |
🟠 ADAPT |
Validation harness; refactor to SilverSight receipt format. |
Infrastructure Layer
| Research-Stack |
SilverSight Target |
Status |
Notes |
AGENTS.md hierarchy |
docs/ + root AGENTS.md |
🟡 PORT |
Bring root + core subtree AGENTS.md rules. Drop stale project-state blocks. |
REBASE_RULES.md |
root REBASE_RULES.md |
✅ PORTED |
Already pushed. |
.github/workflows/lean-check.yml |
.github/workflows/ |
🟠 ADAPT |
Adapt CI to SilverSight lake build paths. |
.github/workflows/python-check.yml |
.github/workflows/ |
🟠 ADAPT |
Adapt Python test paths. |
.github/workflows/q16-roundtrip.yml |
.github/workflows/ |
✅ PORTED |
Already present. |
.devin/skills/lean-proof/SKILL.md |
.devin/skills/ |
🟡 PORT |
Mandatory for all Lean work. |
.github/skills/contextstream-workflow/SKILL.md |
.github/skills/ |
🟡 PORT |
Persistent memory workflow. |
.github/skills/research-stack-workflow/SKILL.md |
.github/skills/ |
🟠 ADAPT |
Rename to silversight-workflow; update paths. |
.cursorrules, .devin/config.json, .claude/settings.json |
root / .devin/ |
🟡 PORT |
Editor hook configs enforcing ContextStream-first rules. |
scripts/qc-flag/ |
scripts/qc-flag/ |
🟡 PORT |
7-check Lean QC protocol. |
4. Gaps
Things SilverSight's architecture calls for but Research-Stack does not cleanly provide:
| Gap |
Where it belongs |
What to build |
SilverSightCore.lean completeness |
Core/ |
Finish HachimojiState, Receipt, Instruction, δ, TIC axiom, loop invariant. Current file is a sketch. |
| LexLib / MathLib |
Library/LexLib.lean |
No complete LaTeX/ASCII tokenizer exists in Research-Stack. Build from equation_shape_parser.py + math_symbols.py. |
| EventLib |
Library/EventLib.lean |
TIC counter is conceptual only. Implement event receipts from chaos-game steps. |
| RRCLib |
Library/RRCLib/ |
RRC is in PVGS_DQ_Bridge_fixed.lean §4. Extract into standalone library per docs/RRC_PLACEMENT.md. |
| Orchestrator |
Orchestrator/SilverSight.lean |
No equivalent in Research-Stack. Build new composition layer. |
| CBridge / PythonBridge |
CBridge/, PythonBridge/ |
Mentioned in docs/ARCHITECTURE.md but not present. Build Q16_16 C lib + ctypes bindings. |
| Doc-sync CI |
.github/workflows/doc-sync.yml |
Exists but needs to verify porting map + architecture docs stay consistent. |
5. Conflicts
| Conflict |
Resolution |
Research-Stack Q16_16.lean / FixedPoint.lean vs SilverSight Q16_16_Spec.lean |
✅ PORTED — Q16_16_Spec.lean deleted; formal/CoreFormalism/FixedPoint.lean is now the canonical source of truth. |
Research-Stack qaoa_adapter.py (2,421 lines) vs SilverSight split qubo/*.py |
Split adapter: Finsler/QUBO builder → MetricLib/QUBOLib; circuit generation → QUBOLib; bitstring bridge → PVGSLib. |
Research-Stack AGENTS.md references many dead paths |
Port rules, not state. Update path references to SilverSight equivalents. |
SilverSight ARCHITECTURE.md uses 6 layers; conceptual map uses 5 |
Reconcile: 5-layer conceptual map is authoritative; 6-layer doc is an older draft. Update ARCHITECTURE.md to match 5-layer model + library method. |
6. Recommended Porting Order
- Core first — ✅ Replace
Q16_16_Spec.lean with full FixedPoint.lean. Lock down SilverSightCore.lean. SilverSightCore.lean now builds with no sorries and no Float.
- SearchLib — Port
SidonSets.lean, SieveLemmas.lean, InteractionGraphSidon.lean.
- RRCLib — Extract RRC gates from
PVGS_DQ_Bridge_fixed.lean §4 into standalone library.
- QUBOLib + MetricLib — Split
qaoa_adapter.py and qubo_highs.py cleanly.
- LexLib — Build tokenizer from
math_symbols.py + equation_shape_parser.py.
- AuditLib + EventLib — Implement receipt validation and TIC counting.
- Orchestrator — Compose all libraries through Core.
- Skills + editor configs — Port agent rules last, once directory structure is stable.
7. Drop List
Do not port these Research-Stack artifacts:
legacy/ and ExtensionScaffold/ modules with pre-existing errors.- Quarantined
PIST.HybridTSMPISTTorus.
- VCN/LUPINE infrastructure (extracted to
distributed-compute-fabric).
- Kubernetes/k3s manifests, Ray actors, Garage/restic storage scripts (extracted to
distributed-compute-fabric).
- Stale assignment boards (
windsurf/ASSIGNMENTS.md) and old sorry audits (windsurf/SORRY_AUDIT.md).
- Runtime DBs, consolidation manifests, and generated receipts under
shared-data/ and .headroom/.
.agents/plugins/marketplace.json and dormant substack-connector.- Biological/genetics extensions unless the BindingSite direction is pursued.
This map is a living document. Update it as components are ported or reclassified.
CFF-to-Module Mapping
Cross-reference between CITATION.cff reference notes and SilverSight modules.
Entries marked 🟡 are planned or partially ported; ✅ means a corresponding
SilverSight file currently exists on disk.
| CFF reference |
Research-Stack module(s) |
SilverSight target |
Exists? |
| Giani, Win, Conti (2025) — Photon-Varied Gaussian States |
Semantics.PVGS_DQ_Bridge |
formal/PVGS_DQ_Bridge/ |
✅ |
| Chabaud, Mehraban (2022) — Stellar representation |
Semantics.PVGS_DQ_Bridge |
formal/PVGS_DQ_Bridge/ |
✅ |
| Pizzimenti et al. (2024) — Wigner negativity |
Semantics.BindingSite, Semantics.PVGS_DQ_Bridge |
formal/BindingSite/, formal/PVGS_DQ_Bridge/ |
✅ |
| Wassner et al. (2025) — Single quadrature noise tomography |
Semantics.PVGS_DQ_Bridge |
formal/PVGS_DQ_Bridge/ |
✅ |
| Saucedo (2019) — Pascal's Triangle / Sidon constructions |
Semantics.SidonSets |
formal/CoreFormalism/SidonSets.lean |
✅ (CoreFormalism.SidonSets builds; chaos-game appendix dropped) |
| Farr, Groot (2009) — Close packing density |
Semantics.BraidEigensolid, Semantics.BraidSpherionBridge, Semantics.BaselineComparison |
formal/CoreFormalism/BraidEigensolid.lean, formal/CoreFormalism/BraidSpherionBridge.lean |
✅ (BaselineComparison not yet ported) |
| Fasolo, Sollich (2004) — Fractionation effects |
Semantics.BraidEigensolid (meta-solid concept) |
formal/CoreFormalism/BraidEigensolid.lean |
✅ |
| Baranau, Tallarek (2014) — Random-close packing limits |
Semantics.BraidEigensolid |
formal/CoreFormalism/BraidEigensolid.lean |
✅ |
| Kofke, Bolhuis (1999) — Freezing of polydisperse hard spheres |
Semantics.BraidEigensolid, Semantics.BaselineComparison |
formal/CoreFormalism/BraidEigensolid.lean |
✅ (BaselineComparison not yet ported) |
| Arrizabalaga, Tracy, Manchester (2026) — Differentiable IPM |
Semantics.FixedPoint, Semantics.Q16InverseProof |
formal/CoreFormalism/FixedPoint.lean (absorbed) |
✅ |
| Yang et al. (2026) — STARS recurrent dynamics |
Semantics.AVMIsa.*, Semantics.Run |
Core/SilverSightCore.lean (AVM transition function) |
✅ |
Unresolved references
Semantics.MetaSolid is cited in CITATION.cff as a Research-Stack module, but
no Semantics.MetaSolid.lean file exists in Research-Stack. It is treated here as
the meta-solid concept documented in the ContextStream node
e967f515-3af9-46c9-9fc8-e5c766a6c4fc and bound to Semantics.BraidEigensolid.Semantics.BaselineComparison and the meta-solid concept (Semantics.MetaSolid)
are cited in CITATION.cff but have no corresponding SilverSight module on disk
yet. They are tracked as 🟡 PORT targets in the SearchLib layer above.- The original
CITATION.cff cited formal/BraidEigensolid.lean and
formal/BraidSpherionBridge.lean at the repository root; those files now live at
formal/CoreFormalism/BraidEigensolid.lean and
formal/CoreFormalism/BraidSpherionBridge.lean.
allaun
4490dc28a7