From 5e0f8b72f1b4b62fd8ccfd17c2e27a1898960778 Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Mon, 22 Jun 2026 22:14:03 -0500
Subject: [PATCH] docs: SilverSight directory structure specification
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Formalizes:
- Naming conventions (PascalCase dirs, PascalCase.lean files)
- Repository root structure (formal/, python/, qubo/, tests/, docs/)
- Module naming (Schema, WireFormat, ProductSchema, etc.)
- Import conventions (cross-project from Semantics)
- Build targets (lake build SilverSight)
- File size limits (500 lines max per Lean module)
- What goes where (formal → formal/, shims → python/, etc.)
---
 .../lean/SilverSight/DIRECTORY_SPEC.md        | 140 ++++++++++++++++++
 1 file changed, 140 insertions(+)
 create mode 100644 0-Core-Formalism/lean/SilverSight/DIRECTORY_SPEC.md

diff --git a/0-Core-Formalism/lean/SilverSight/DIRECTORY_SPEC.md b/0-Core-Formalism/lean/SilverSight/DIRECTORY_SPEC.md
new file mode 100644
index 00000000..3cf7af7c
--- /dev/null
+++ b/0-Core-Formalism/lean/SilverSight/DIRECTORY_SPEC.md
@@ -0,0 +1,140 @@
+# SilverSight Directory Structure Specification
+
+## Naming Conventions
+
+| Item | Convention | Example |
+|------|-----------|---------|
+| Directory | `PascalCase` | `SilverSight/`, `CoreFormalism/` |
+| Lean file | `PascalCase.lean` | `Schema.lean`, `WireFormat.lean` |
+| Python file | `snake_case.py` | `chaos_game.py`, `q16_16_roundtrip.py` |
+| Config file | `lowercase.ext` | `lakefile.toml`, `lean-toolchain` |
+| Documentation | `UPPER_CASE.md` or `PascalCase.md` | `AGENTS.md`, `README.md` |
+
+## Repository Root
+
+```
+SilverSight/
+├── AGENTS.md                    ← operating contract
+├── README.md                    ← public-facing docs
+├── CITATION.cff                 ← citation metadata
+├── REBASE_RULES.md              ← migration rules
+├── PORTING_MAP.md               ← Research Stack → SilverSight mapping
+├── lakefile.toml                ← Lean build config
+├── lean-toolchain               ← Lean version pin
+├── lake-manifest.json           ← dependency lockfile
+├── pytest.ini                   ← Python test config
+├── requirements.txt             ← Python dependencies
+│
+├── formal/                      ← Lean 4 formal modules
+│   ├── SilverSight/             ← core SilverSight modules
+│   │   ├── Schema.lean
+│   │   ├── WireFormat.lean
+│   │   ├── ProductSchema.lean
+│   │   ├── ProductWireFormat.lean
+│   │   ├── Receipt.lean
+│   │   ├── Bind.lean
+│   │   ├── AVMIsa/              ← AVM ISA surface
+│   │   ├── RRC/                 ← Rainbow Raccoon Compiler
+│   │   └── PIST/                ← PIST classification
+│   │
+│   ├── CoreFormalism/           ← foundational theorems
+│   │   ├── FixedPoint.lean
+│   │   ├── SidonSets.lean
+│   │   └── ...
+│   │
+│   ├── PVGS_DQ_Bridge/          ← photon-varied Gaussian state bridge
+│   ├── UniversalEncoding/       ← 50-token math address space
+│   ├── BindingSite/             ← amino acid vocabulary
+│   └── RRCLib/                  ← RRC library modules
+│
+├── Core/                        ← core runtime modules
+│
+├── python/                      ← Python shims (I/O only)
+│   ├── chaos_game.py
+│   ├── sidon_addressing.py
+│   ├── spectral_profile.py
+│   └── q16_16_canonical.py
+│
+├── qubo/                        ← QUBO/QAOA optimization
+│   ├── finsler_metric.py
+│   ├── qubo_builder.py
+│   ├── qaoa_circuit.py
+│   └── classical_solver.py
+│
+├── tests/                       ← test suite
+│   ├── test_q16_roundtrip.py
+│   ├── test_schema.py
+│   └── test_bind.py
+│
+├── docs/                        ← documentation
+│   ├── architecture.md
+│   ├── glossary.md
+│   └── testing.md
+│
+├── experiments/                  ← experimental code (not production)
+│
+├── extraction/                   ← generated JSON artifacts
+│
+└── .github/workflows/           ← CI/CD
+    ├── lean-check.yml
+    ├── python-check.yml
+    └── q16-roundtrip.yml
+```
+
+## Module Naming (Lean)
+
+| Type | Pattern | Example |
+|------|---------|---------|
+| Schema class | `Schema` | `class Schema (α : Type)` |
+| Wire format | `WireFormat` | `structure WireFormat` |
+| Product type | `ProductSchema` | `instance : Schema (α × β)` |
+| Receipt | `Receipt` | `structure Receipt` |
+| Bind | `Bind` | `def bindReceipt` |
+| Theorem | `camelCase` | `byteSize_nonneg` |
+| Lemma | `camelCase` | `roundTrip_correct` |
+| Instance | `PascalCase` | `uint8Schema` |
+
+## Import Conventions
+
+```lean
+-- SilverSight modules import from Semantics cross-project
+import Semantics.FixedPoint
+import Semantics.Spectrum
+
+-- Internal SilverSight imports use relative paths
+import SilverSight.Schema
+import SilverSight.WireFormat
+```
+
+## Build Targets
+
+```bash
+# Full SilverSight build
+lake build SilverSight
+
+# Narrow target
+lake build SilverSight.Schema
+
+# Compiler surface (blessed API)
+lake build Compiler
+```
+
+## File Size Limits
+
+| File | Max Lines | Notes |
+|------|-----------|-------|
+| Lean module | 500 | One namespace per file |
+| Python shim | 300 | Pure I/O only |
+| Documentation | No limit | But prefer modular docs |
+
+## What Goes Where
+
+| Content | Location | Why |
+|---------|----------|-----|
+| Lean formal modules | `formal/SilverSight/` | Core formalization |
+| Python shims | `python/` | I/O only, no logic |
+| QUBO/QAOA | `qubo/` | Optimization domain |
+| Tests | `tests/` | Verification |
+| Docs | `docs/` | Human-readable |
+| Experiments | `experiments/` | Not production |
+| Generated JSON | `extraction/` | Artifacts |