# 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 |