# Architecture

## Overview

Research-Stack v2 is organized into 6 layers, each with a single responsibility:

```
Layer 6: Infrastructure    <- CI/CD, docs, repo hygiene (this stage)
Layer 5: Integrate         <- Language bridges (C, Python, Lean FFI)
Layer 4: Optimize          <- QUBO/QAOA, Finsler annealing
Layer 3: Search            <- Chaos game, basin finding, equation candidates
Layer 2: Codec             <- Hachimoji encoding, Q16_16, Sidon addressing
Layer 1: Core              <- Chentsov theorem, statistical manifolds
```

## Layer Details

### Layer 1: Core (CoreFormalism/)

- **ChentsovTheorem.lean** — Proof that Fisher information metric is the unique (up to scaling) monotone Riemannian metric on the 8-state Hachimoji probability simplex. 883 lines, 0 sorry.
- **StatisticalManifold.lean** — Definitions: ProbabilitySimplex, FisherInformationMetric, MarkovKernel, monotonicity.
- **Q16_16.lean** — Canonical fixed-point type with round-half-up semantics. Proven equivalent across Lean, C, and Python.

**Status**: PROVEN. No axioms beyond standard Lean/mathlib.

### Layer 2: Codec (Codec/)

- **hachimoji_codec.py** — Deterministic codec: UTF-8 string -> Hachimoji DNA sequence. No ML. No randomness. Pure function.
- **q16_roundtrip.py** — Cross-language roundtrip test: Lean <-> C <-> Python.
- **sidon_address.py** — Sidon set generation for collision-free memory addressing.

**Key invariant**: `decode(encode(s)) == s` for all valid UTF-8 strings `s`.

### Layer 3: Search (Search/)

- **chaos_game.py** — Iterated function system for basin boundary sampling.
- **basin_finder.py** — Classifies orbits into basins of attraction.
- **equation_candidates.py** — Generates equation candidates from basin representatives.

**Status**: PROTOTYPE. Chaos game converges; basin classification heuristic.

### Layer 4: Optimize (Optimize/)

- **finsler_qubo.py** — Finsler-anisotropic QUBO formulation.
- **qaoa_pipeline.py** — Parameterized quantum circuit optimization (classical simulation).
- **annealer.py** — Simulated annealing with Finsler metric temperature schedule.

**Status**: IN DEVELOPMENT. QUBO formulation solid; QAOA classical simulation slow.

### Layer 5: Integrate (CBridge/, PythonBridge/)

- **CBridge/** — C shared library with Q16_16 operations, compiled to `.so`.
- **PythonBridge/** — Python ctypes bindings to C library. `ctypes.CDLL("./libq16.so")`.
- **FFI/** — Lean FFI stubs (future work: direct Lean <-> C calls).

**Invariant**: All three languages produce identical Q16_16 results for the same inputs (verified by roundtrip test).

### Layer 6: Infrastructure (.github/, docs, repo hygiene)

- **4 CI workflows** — lean-check, python-check, q16-roundtrip, doc-sync.
- **pre-commit hooks** — Same checks as CI, run locally before every commit.
- **.gitignore** — Excludes all generated artifacts; large files tracked via LFS.

## Data Flow

```
Input equation string
    |
    v
[Codec] Hachimoji encode -> DNA sequence
    |
    v
[Search] Chaos game -> basin representative
    |
    v
[Optimize] QUBO/QAOA -> optimal parameters
    |
    v
[Core] Chentsov metric -> classification score
    |
    v
Output: classified equation with provenance
```

## Cross-Language Contracts

### Q16_16 Fixed-Point

| Language | File | Semantics |
|----------|------|-----------|
| Lean | CoreFormalism/Q16_16.lean | Round-half-up, saturating |
| C | CBridge/libq16.c | Round-half-up, saturating |
| Python | PythonBridge/q16_binding.py | Round-half-up, saturating |

**Verification**: `Tests/q16_roundtrip_test.py` checks all triples (x, y) in [-1, 1] x [-1, 1] with step 1/256.

### Build Commands

```bash
# Lean
lake build

# C
make -f CBridge/Makefile

# Python
pytest Tests/ -v
```

## Repository Layout

```
/
├── CoreFormalism/       <- Layer 1: Lean proofs
├── Codec/              <- Layer 2: Encoding/decoding
├── Search/             <- Layer 3: Chaos game, basins
├── Optimize/           <- Layer 4: QUBO, QAOA
├── CBridge/            <- Layer 5: C library
├── PythonBridge/       <- Layer 5: Python bindings
├── FFI/                <- Layer 5: Lean FFI (stub)
├── Tests/              <- Cross-layer tests
├── .github/
│   ├── workflows/      <- 4 CI workflows
│   └── scripts/        <- doc-sync check
├── .gitignore
├── .pre-commit-config.yaml
├── README.md
└── ARCHITECTURE.md
```