docs/ARCHITECTURE.md

# SnapKitty Architecture

**Status:** Research project — inventory-driven design, September 2026.

---

## What Problem Are We Solving?

Existing AI systems produce outputs with no verifiable provenance. A model asserts a fact. There is no chain of custody from assertion back to evidence, proof, or authorization. Outputs are probabilistic, unauditable, and non-deterministic across runs.

SnapKitty asks: can an AI system be built where every output traces back through a formal graph of evidence → proof → decision, sealed with a cryptographic receipt?

A secondary question (under active investigation): can the conventional softmax attention mechanism be replaced with an integer-arithmetic routing mechanism that produces deterministic routing decisions and admits formal verification?

---

## What The Conventional Approach Does

```
Input
  ↓
Q/K/V projections (matrix multiply × 3)
  ↓
QKᵀ (matrix multiply, O(n²))
  ↓
Scale by 1/√d
  ↓
Softmax (exponentials, normalization)
  ↓
Attention weights × V (matrix multiply)
  ↓
Output
```

Characteristics: floating-point throughout, non-deterministic at scale, exponential operations, no formal specification of what the routing decision means.

---

## What SnapKitty Does Differently

### Layer 1: Governance DAG (IMPLEMENTED)

Every claim, proof, decision, and execution is a node in a formally specified directed acyclic graph.

```
EVIDENCE ──────────────────┐
                            ↓
            [CONSTRAINT checks]
                            ↓
CLAIM ──────→ PROOF ──────→ DECISION(authorized) ──→ EXECUTION ──→ AUDIT
                                    ↑
                            POLICY enforces
                            CONSTRAINT
```

**Implemented in two layers:**
- `ICP-DAG.m` (MUMPS): imperative runtime, stores nodes/edges in global arrays, enforces 10 integrity invariants
- `ICP-DAG.lp` (ASP): declarative constraint specification, 7 hard constraints. SAT = governance holds; UNSAT = HALT.

Nothing executes without passing this graph. This is not a convention — it is enforced by the ASP solver and the MUMPS gate check.

### Layer 2: SUBLEQ Attention (EXPERIMENTAL)

**Hypothesis:** Softmax attention's probability distribution over relationships can be replaced with integer-comparison-based deterministic routing using the SUBLEQ one-instruction machine.

```
Activation vector (floats)
  ↓
Quantize: floor(256 × |x|) → integers in [0, 255]
  ↓
Reshape into [A, B, C] SUBLEQ triads
  ↓
Load into 256-cell integer memory
  ↓
SUBLEQ: mem[B] -= mem[A]; if mem[B] ≤ 0: jump to C
         (run max 500 steps)
  ↓
Collect output addresses
  ↓
Born collapse: floor(256 mod Σ φ^(-i) · output_i) → scalar address
  ↓
Selected context / routing result
```

**What this eliminates:** matrix multiplication in the routing phase, softmax exponentials.
**What this does NOT eliminate:** float operations at the quantization step.
**What is not yet measured:** whether this produces equivalent attention-like routing quality on any benchmark.

**Evidence:** `j-matrix-twin/subleq_attention.ijs` (J language, runnable). Rust/WASM VM: `DEVFLOW-FINANCE/snapkitty-wasm/src/subleq_vm.rs` (production-ready, 4 tests).

### Layer 3: Entropy Governance (PROVED)

Every inference step is gated by a formally proved entropy bound.

**Theorem (proved in Lean 4, zero sorry):**
```
F ≥ 1 → T(F) ≤ 0.2218 → s = exp(d/T(F)) ≥ 90.75 → H < 0.20 nats
```

**Implementation:** `snapkitty_entropy.EntropyGovernor(LogitsProcessor)` — drop-in for any HuggingFace model.

### Layer 4: Formal Algebraic Foundation (PARTIAL)

**Jordan Fixed-Point Commutativity (proved):**
For the Jordan operator T(ρ) = φ⁻¹·U·ρ·U† + φ⁻²·ρ, any fixed point ρ* satisfies [U, ρ*] = 0.

This means: if an agent's state converges under Jordan iteration, the converged state commutes with the unitary evolution operator. The agent cannot be driven out of its converged state by the same unitary that drove it there.

**Jacobian Conjecture formalization:** `sov-kernel-monster/jacobian-formal/JACOBIAN_BRIDGES_COMPLETE.lean` — 10 peer-review gap closures, self-declared zero-sorry.

**Grey-hat quantum defense:** `sov-kernel-monster/src/jordan_block.f90` — four invariants enforced in Fortran: side-channel resistance (∂U/∂t=0), fault injection impossibility (ρ*=ψψ†), coherence ([U,ρ*]=0), entropy bound (φ⁻²).

---

## The Canonical SnapKitty DAG

Derived from code (not imposed):

```
Node
├── id: string (unique identifier)
├── type: EVIDENCE | CLAIM | CONSTRAINT | PROOF | POLICY | DECISION | EXECUTION | AUDIT
├── state: UNKNOWN | OBSERVED | VERIFIED | PROVEN | AUTHORIZED | ACTIVE | PENDING | SEALED
└── payload: type-specific data

Edge
├── source: node id
├── destination: node id
└── relation: decides | executes | proves | enforces | proven-by | derived-from | supports
```

**Integrity invariants (enforced by both ASP and MUMPS):**
1. Every edge requires both endpoint nodes to exist
2. No self-edges
3. Unknown claims cannot reach decisions
4. Contradicted claims cannot reach decisions
5. Authorization requires proof
6. Execution requires authorized decision
7. Unknown and verified are mutually exclusive

---

## Is The DAG The Right Common Intermediate Representation?

**For governance:** YES. The ICP-DAG is the clearest, most implemented piece of the architecture. It already works.

**For SUBLEQ attention:** PARTIALLY. The SUBLEQ execution graph is NOT a DAG (it can branch backward). The dependency graph of how activation vectors produce routing results IS a DAG. The correct representation is:
- DAG for the dependency structure (which activations produced which routing decision)
- Directed graph (potentially cyclic) for the SUBLEQ execution trace itself

**For quantum structures:** NO — not all of them.
- Quantum circuit composition: DAG (always)
- Braid group operations: NOT a DAG — braids are reversible and can undo themselves
- Vortex lattice (quantum-wasm): undirected grid graph
- Quantum walk graph: undirected adjacency graph

**Correct distinction:**
```
Use DAG for:           dependency ordering, governance, provenance, execution ordering
Use directed graph for: SUBLEQ execution trace, state machines with loops
Use undirected graph for: coupling maps, vortex lattices, quantum walk substrates
Use braid for:          topological quantum evolution (σᵢ, σᵢ⁻¹ operations)
```

Forcing braids or quantum walks into the DAG abstraction would be technically incorrect.

---

## Repository Structure (Proposed)

Based on what actually exists:

```
snapkitty/
├── core/
│   ├── icp_dag.m             # ICP governance DAG (MUMPS) — CORE, WORKING
│   ├── icp_dag.lp            # ICP ASP constraints — CORE, WORKING
│   └── icp_gov.m             # Governance extension — CORE, WORKING
├── subleq/
│   ├── vm.rs                 # SUBLEQ VM (Rust/WASM) — PRODUCTION
│   ├── attention.ijs         # SUBLEQ attention (J) — EXPERIMENTAL
│   └── python_port.py        # Python port for visualization
├── resonance/
│   ├── vm/                   # Resonance ISA VM (Rust, 8 opcodes) — WORKING
│   ├── assembler/            # .rasm → bytecode — WORKING
│   ├── word.ijs              # Resonance Word GF(p) format (J) — WORKING (bug fixed)
│   └── abjad/                # Abjad tokenizer — WORKING
├── algebra/
│   ├── JordanMatrixProof.lean    # PROVED (0 sorry)
│   ├── EntropyBound.lean         # PROVED (0 sorry)
│   ├── jordan_block.f90          # Fortran grey-hat layer
│   └── jacobian_bridges.lean     # Jacobian Conjecture formalization
├── quantum/
│   ├── formal/
│   │   ├── FibonacciAnyon.lean   # Fusion category (partial proof)
│   │   ├── BraidCompilation.lean # Braid → gate synthesis (skeleton, sorry)
│   │   └── LogicalQubits.lean    # Anyon encoding structures
│   ├── simulation/
│   │   ├── quantum_wasm.rs       # WASM simulation (vortex lattice) — WORKING
│   │   └── topological.rs        # Fibonacci anyon sim — WORKING
│   └── entropy/
│       └── quantum.mjs           # ANU QRNG integration — WORKING
├── swarm/
│   ├── quantum-swarm.mjs         # PRIMARY swarm engine — WORKING
│   ├── swarm_coordinator.mjs     # 5-agent named roles — WORKING
│   └── sovereign_crew/           # Python CrewAI with entropy gate — WORKING
├── visualization/
│   ├── app.py                    # Gradio algorithmic art Space
│   ├── subleq_engine.py          # Python SUBLEQ port
│   └── resonance_word.py         # Python Resonance Word port
├── formal/
│   ├── lean/                     # All Lean 4 proofs
│   ├── agda/                     # Agda invariants
│   └── prolog/                   # ERE.pl, GJW traversability
├── benchmarks/                   # EMPTY — needs building
├── tests/
│   ├── subleq_vm/                # 4 Rust tests (working)
│   ├── resonance_isa/            # 3 Rust tests (working)
│   └── braid/                    # 4 Rust tests (working)
└── docs/
    ├── REPOSITORY_INVENTORY.md
    ├── ARCHITECTURE.md
    ├── DAG.md
    ├── QUANTUM_SWARM.md
    └── RESEARCHER_EXPLANATION.md
```

---

## Algorithm Implementation Status

| Algorithm | File | Working | Tested | Benchmarked |
|-----------|------|:-------:|:------:|:-----------:|
| SUBLEQ VM | `subleq_vm.rs` | ✓ | ✓ | ✗ |
| SUBLEQ Attention | `subleq_attention.ijs` | ✓ | ✗ | ✗ |
| Resonance ISA VM | `vm/src/lib.rs` | ✓ | ✓ | ✗ |
| ICP Governance DAG | `ICP-DAG.m` | ✓ | ✓ | ✗ |
| Entropy Governor | `governor.py` | ✓ | ✗ | ✗ |
| Jordan proof | `JordanMatrixProof.lean` | ✓ (proved) | ✓ | N/A |
| Entropy bound | `EntropyBound.lean` | ✓ (proved) | ✓ | N/A |
| Fibonacci anyon sim | `topological.rs` | ✓ | ✓ | ✗ |
| Quantum WASM | `quantum_wasm.rs` | ✓ (binary) | ✗ | ✗ |
| ANU QRNG | `quantum.mjs` | ✓ | ✗ | ✗ |
| Braid gate synthesis | `BraidCompilation.lean` | ✗ (sorry) | ✗ | N/A |
| Grover search | `GroverSearch.lean` | partial | ✗ | N/A |

---

## What Is The Main Open-Source Product?

**Product name:** `snapkitty-dag` — The SnapKitty Integrity DAG

**One-sentence definition:** A formally specified directed acyclic graph that gates every claim, proof, decision, and execution in an AI pipeline, enforced simultaneously by Answer Set Programming constraints and an imperative MUMPS runtime, with cryptographic WORM sealing at every node.

**Why this over the other candidates:**
- SUBLEQ attention is experimental and unbenched — cannot be a product yet
- The Jordan proof is a building block, not a standalone product
- The ICP-DAG is complete, working, tested, and directly usable by anyone building an auditable AI pipeline
- It is the only component that enforces constraints on ALL the other components

The SUBLEQ attention and quantum swarm work are the **research tracks** that feed into a future version of this product.