allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
Research-Stack/6-Documentation/PROJECT_MAP.md
allaun 14cde6d09c docs: refresh READMEs, AGENTS.md, and project maps for recent Lean surface 
- 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
2026-06-20 20:34:09 -05:00

3.1 KiB
Raw Blame History

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

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

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