# Research Stack Project Map

**Purpose:** High-level pointer from concepts to canonical files.  
**Ground truth:** `0-Core-Formalism/lean/Semantics/` compiles with `lake build`.

---

## Core Formalism

| Concept | File | Notes |
|---------|------|-------|
| `bind` primitive, cost functions | `0-Core-Formalism/lean/Semantics/Semantics/Bind.lean` | Universal lawful translation |
| Q16_16 / Q0_16 fixed point | `0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean` | Hardware-native arithmetic, zero Float in compute path |
| Canonical state / PBACS | `0-Core-Formalism/lean/Semantics/Semantics/Canon.lean` | Constitution + prohibited-state predicates |
| AVM ISA + receipt emitter | `0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Emit.lean` | **Sole output boundary** for top-level receipt JSON |
| RRC alignment classifier | `0-Core-Formalism/lean/Semantics/Semantics/RRC/Emit.lean` | Feeds `AVMIsa.Emit`; no standalone top-level receipts |

## Recent Additions

| Concept | File | Notes |
|---------|------|-------|
| Coprime sieve observer / CRT reconstruction | `0-Core-Formalism/lean/Semantics/Semantics/SieveLemmas.lean` | `depth_token_coprime_intersect`; human ℓ=7 + dolphin ℓ=11 → coordinate 61 |
| RRC weak-axis ↔ atproto analogy | `0-Core-Formalism/lean/Semantics/Semantics/InteractionGraphSidon.lean` | Weak-axis projections + interaction-graph Sidon witness; toy identity/host/app axes |
| SDP certificate verification engine | `0-Core-Formalism/lean/Semantics/Semantics/SDPVerify.lean` | Sparse ℚ polynomial arithmetic; `verifyCertificate` + soundness theorem |
| Goormaghtigh SOS certificates | `0-Core-Formalism/lean/Semantics/Semantics/GoormaghtighCert.lean` | Certificate data for Goormaghtigh collision polynomial; pipeline validation certs included, full cert pending |
| Gremlin mathblob dependency loader | `scripts/load_dependency_graph.py` | Cross-layer dependency graph loader: 6 vertex types, 8 edge types, imports → theorems → receipts → shims → hardware probes |

## Infrastructure Shims

| Concept | File | Notes |
|---------|------|-------|
| Entropy candidate generator | `4-Infrastructure/shim/geometric_entropy_explorer.py` | Exploration-phase candidate generator |
| Candidate certification bridge | `4-Infrastructure/shim/candidate_certification_bridge.py` | Bridge to `Semantics.RRC.EntropyCandidates` |
| 250-equation corpus builder | `4-Infrastructure/shim/build_corpus250.py` | Regenerates `Semantics/RRC/Corpus250.lean` from `rrc_pist_predictions_250_v1.json` |

## Documentation Maps

| Map | File |
|-----|------|
| Math model catalog | `6-Documentation/docs/MATH_MODEL_MAP.md` |
| Domain-sorted math model catalog | `6-Documentation/docs/MATH_MODEL_MAP_BY_DOMAIN.md` |
| Lean port orchestration | `6-Documentation/docs/semantics/LEAN_PORT_ORCHESTRATION_MAP.md` |
| Sidon / FAMM operational map | `6-Documentation/famm/SIDON_FAMM_MAP.md` |
| Beginner's orientation | `6-Documentation/docs/BEGINNERS_MAP.md` |

## Build Gate

```bash
cd 0-Core-Formalism/lean/Semantics && lake build
```

The active Compiler surface was last verified at **3314 jobs, 0 errors**.