mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
allaun
14cde6d09c
- Update README.md and 0-Core-Formalism/README.md with build baseline (3314 jobs, 0 errors) and new modules (SDPVerify, GoormaghtighCert, Hachimoji, SieveLemmas, InteractionGraphSidon, GeneticBraidBridge) - Update AGENTS.md and 0-Core-Formalism/lean/Semantics/AGENTS.md blessed surface tables and build baselines - Add 6-Documentation/PROJECT_MAP.md and update existing project maps (MATH_MODEL_MAP*, LEAN_PORT_ORCHESTRATION_MAP, SIDON_FAMM_MAP, BEGINNERS_MAP) with new components and Gremlin mathblob graph loader
52 lines
3.1 KiB
Markdown
52 lines
3.1 KiB
Markdown
# 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**.
|