docs/REPOSITORY_INVENTORY.md

# SnapKitty Repository Inventory

**Date:** 2026-09-03  
**Repository:** `SNAPKITTYWEST/sov-kernel-monster` (primary) + associated repos  
**Purpose:** Technical evidence map. Every claim points to a file and line.

---

## 1. Core Algorithm Inventory

### ALG-001: SUBLEQ Virtual Machine (Production-Ready)
| Field | Value |
|-------|-------|
| **Path** | `DEVFLOW-FINANCE/snapkitty-wasm/src/subleq_vm.rs` |
| **Language** | Rust / WASM |
| **Lines** | ~433 |
| **Status** | Working |
| **Tests** | 4 tests: memory r/w, subleq correctness, snapshot round-trip, trace recording |
| **Input** | i32 memory array (65,536-cell address space) |
| **Output** | Execution trace, final memory state |
| **Algorithm** | `mem[a] -= mem[b]; if result <= 0: jump to C` |
| **Arithmetic** | i32 wrapping subtract |
| **Deterministic** | Yes |
| **Evidence** | `execute_step()`, `run()`, `snapshot()`, `restore()` functions |
| **Novelty** | Established OISC (One-Instruction Set Computer) — no novelty claim |

### ALG-002: SUBLEQ Attention Head (Experimental)
| Field | Value |
|-------|-------|
| **Path** | `j-matrix-twin/subleq_attention.ijs` |
| **Language** | J (requires jconsole to run) |
| **Status** | Demonstrated (J runnable), ported to Python |
| **Input** | Float activation vector |
| **Output** | Integer address (Born-collapsed) |
| **Algorithm** | Floats → floor(256*\|x\|) → [A,B,C] triads → SUBLEQ → φ-weighted Born collapse |
| **Float elimination** | Partial: floats quantized to integers before SUBLEQ runs |
| **Matrix multiply eliminated** | Yes, within SUBLEQ phase |
| **Novelty** | SnapKitty combination — using SUBLEQ as attention routing is potentially novel; individual components established |
| **Benchmark vs. softmax** | Not yet benchmarked |

### ALG-003: Resonance ISA Virtual Machine
| Field | Value |
|-------|-------|
| **Path** | `snapkitty-resonance-isa/vm/src/lib.rs` |
| **Language** | Rust |
| **Lines** | ~160 |
| **Status** | Working, 3 tests |
| **Input** | ByteWord program (4-bit opcode + 8-bit operand) |
| **Output** | Step trace with τ (trust), ε (entropy), ρ (resonance) state |
| **8 opcodes** | LOAD, STORE, COMPARE, BRANCH, ENTER, FREEZE, SIGNAL, HALT |
| **Entropy gate** | `ENTROPY_THRESHOLD = 0.21` — execution blocked if ε ≥ 0.21 |
| **State** | All state is f64 (NOT integer — floats not eliminated) |
| **Novelty** | SnapKitty implementation of a custom ISA |

### ALG-004: ERE — Enochian Reconstruction Engine (JS)
| Field | Value |
|-------|-------|
| **Path** | `resonance-core/lib/math/ere.mjs` |
| **Language** | JavaScript ESM |
| **Lines** | 77 |
| **Status** | Fully working |
| **Input** | Array of claims/statements |
| **Output** | Score in [0,1] (fraction failed) |
| **5 passes** | Instantiation, fabrication markers, reversibility, mission alignment, undefined check |
| **Novelty** | SnapKitty implementation — an AI output quality filter, not formal logic |

### ALG-005: ERE — Prolog Knowledge Base
| Field | Value |
|-------|-------|
| **Path** | `ere.pl` |
| **Language** | SWI-Prolog |
| **Lines** | 236 |
| **Status** | Working knowledge base; `resolve_unknown` depends on external dynamic predicates |
| **Content** | 21 Enochian letters, 30 Aethyrs, 8 Hebrew roots, 7 Arabic roots, 8 Aramaic roots |
| **Solver** | `metatron_certify/4`, `call_49/2` — partially stubbed (external dependencies) |

### ALG-006: ICP-DAG — MUMPS Governance Engine
| Field | Value |
|-------|-------|
| **Path** | `ICP-DAG.m` |
| **Language** | MUMPS (GT.M or Caché compatible) |
| **Lines** | 258 |
| **Status** | Working — 10 integrity invariants, full lifecycle |
| **Input** | NODE/EDGE creation calls |
| **Output** | AUTHORIZED/BLOCKED verdict + audit log |
| **DAG nodes** | EVIDENCE, CLAIM, CONSTRAINT, PROOF, POLICY, DECISION, EXECUTION |
| **Test** | `TEST` entry executes BUILD → VERIFY → FINAL sequence |

### ALG-007: ICP-DAG — ASP Constraint Specification
| Field | Value |
|-------|-------|
| **Path** | `ICP-DAG.lp` |
| **Language** | Answer Set Programming (Clingo/DLV) |
| **Lines** | 37 |
| **Status** | Working constraint spec (requires external fact grounding) |
| **Content** | 7 hard integrity constraints: I1-I5, I9 plus `proven/1` derived predicate |

### ALG-008: Jordan Fixed-Point Commutativity (Proved)
| Field | Value |
|-------|-------|
| **Path** | `sov-kernel-monster/lean/JordanMatrixProof.lean` |
| **Language** | Lean 4 + Mathlib |
| **Status** | PROVED — zero sorry |
| **Theorem** | For T(ρ) = φ⁻¹·U·ρ·U† + φ⁻²·ρ, any fixed point ρ* satisfies [U, ρ*] = 0 |
| **Proof** | Algebraic: scalar cancellation + matrix multiplication, no analysis needed |
| **Connection** | SovMonster agent quantum state convergence; carries forward into BornRuleCollapse |

### ALG-009: Entropy Bound (Formally Proved)
| Field | Value |
|-------|-------|
| **Path** | `sovereign-entropy-theorem/lean/EntropyBound.lean` |
| **Language** | Lean 4 + Mathlib |
| **Status** | PROVED — zero sorry |
| **Theorem** | F ≥ 1 → T ≤ 0.2218 → s = exp(d/T) ≥ 90.75 → H < 0.20 nats |
| **Connection** | EntropyGovernor LogitsProcessor (harness already built and on HF) |

---

## 2. DAG Inventory

### DAG-001: ICP Governance DAG (PRIMARY)
| Field | Value |
|-------|-------|
| **Path** | `ICP-DAG.m` + `ICP-DAG.lp` |
| **Purpose** | Governance: nothing executes without passing the graph |
| **Node types** | EVIDENCE, CLAIM, CONSTRAINT, PROOF, POLICY, DECISION, EXECUTION |
| **Edge types** | decides, executes, proves, enforces, proven-by |
| **Is a DAG** | YES — explicitly enforced: no self-edges (I2), all edge endpoints must exist (I1) |
| **Traversal** | `AUTHORIZE` walks claim → decision → execution chain |
| **Status** | Working |
| **Classification** | CORE |

Node flow:
```
EVIDENCE → CLAIM → [CONSTRAINT checks] → PROOF → DECISION(authorized) → EXECUTION → AUDIT
```

### DAG-002: ICP-GOV Extension
| Field | Value |
|-------|-------|
| **Path** | `ICP-GOV.m` |
| **Purpose** | Extends DAG-001 with ACTOR, POLICY levels, PROVENANCE, REVOKE |
| **Status** | Working, has `TEST` entry |
| **Classification** | CORE (extension of DAG-001) |

### DAG-003: SUBLEQ Execution Graph (NOT a DAG)
| Field | Value |
|-------|-------|
| **Path** | `j-matrix-twin/subleq_attention.ijs`, `DEVFLOW-FINANCE/snapkitty-wasm/src/subleq_vm.rs` |
| **Purpose** | Execution trace of SUBLEQ instructions |
| **Is a DAG** | NO — SUBLEQ can loop (branch back to earlier instruction) |
| **Correct representation** | Directed graph (potentially cyclic control flow) |
| **Classification** | EXPERIMENTAL |

### DAG-004: Quantum Circuit DAG (Implicit)
| Field | Value |
|-------|-------|
| **Path** | `clay-institute-p-vs-np/HybridQuantumSAT/Quantum/GroverSearch.lean` |
| **Purpose** | Grover search composition: oracle → diffusion → iterate → measure |
| **Is a DAG** | YES — quantum circuit composition is always a DAG |
| **Implementation** | Function composition in Lean 4 (not an explicit graph structure) |
| **Classification** | EXPERIMENTAL |

### DAG-005: Agent Provenance Chain (WORM)
| Field | Value |
|-------|-------|
| **Path** | `bob-orchestrator/core/bob.mjs` |
| **Purpose** | Append-only event chain: each event hashes the previous |
| **Is a DAG** | YES — linear DAG (chain), extends to tree with branching events |
| **Quantum seeded** | YES — ANU QRNG seeds the genesis hash when available |
| **Classification** | CORE |

### DAG-006: Quantum Circuit Hardware Topology (NOT topological QC)
| Field | Value |
|-------|-------|
| **Path** | `sov-kernel-monster/rust/phase2-quantum-backend/src/topology.rs` |
| **Purpose** | Hardware qubit coupling map — BFS, shortest path, articulation points |
| **Is a DAG** | NO — undirected coupling graph |
| **Classification** | SUPPORTING |

---

## 3. Quantum Research Inventory

### Q-001: Fibonacci Anyon Lean Formalization (Core Math)
| Field | Value |
|-------|-------|
| **Path** | `FibonacciAnyon.lean` (root) |
| **Type** | Pure math/proof in Lean 4 |
| **What's proved** | R-matrix unitary (\|R\|=1), Fibonacci dimension recurrence |
| **What's axiomatic** | pentagon_axiom, hexagon_axiom, topological_protection — all stated as `axiom … True` |
| **Status** | Partial proof — combinatorial facts proved, structural axioms empty |

### Q-002: Braid Compilation Lean Formalization
| Field | Value |
|-------|-------|
| **Path** | `BraidCompilation.lean` (root) |
| **Type** | Pure math spec in Lean 4 |
| **What's proved** | R-move eigenvalue \|e^{i4π/5}\|=1, braid period 5 |
| **What's sorry** | All gate synthesis, Yang-Baxter, Solovay-Kitaev, universality |
| **Status** | Complete skeleton — 15+ sorry terms |

### Q-003: Logical Qubits Lean Formalization
| Field | Value |
|-------|-------|
| **Path** | `LogicalQubits.lean` (root) |
| **Type** | Pure math in Lean 4 |
| **Content** | 3-anyon, 4-anyon, 2n-anyon encoding structures; Hilbert space dimension |
| **Status** | Structural definitions only |

### Q-004: Grover Search Lean Formalization
| Field | Value |
|-------|-------|
| **Path** | `clay-institute-p-vs-np/HybridQuantumSAT/Quantum/GroverSearch.lean` |
| **Type** | Pure math formalization |
| **What's proved** | Structure of phase oracle, diffusion operator, grover iteration (mathematically) |
| **Amplitude bound** | Stated, not fully discharged analytically |
| **Status** | Prototype — `quantum_search` stub returns `{ success := false }` |

### Q-005: Quantum WASM Simulation (WORKING)
| Field | Value |
|-------|-------|
| **Path** | `quantum-wasm/pkg/quantum_wasm_bg.wasm` (44KB compiled binary) |
| **Type** | Classical simulation of quantum systems |
| **What it simulates** | Quantum state (complex amplitudes), Ising Hamiltonian Trotter evolution, VortexLattice with topological charge, winding numbers |
| **Type of quantum** | Classical simulation — NOT physical quantum hardware |
| **Status** | Working compiled binary with TypeScript bindings |

### Q-006: Fibonacci Anyon Classical Simulation (WORKING)
| Field | Value |
|-------|-------|
| **Path** | `carry-agent/quantum/topological.rs` (location inferred from agent report) |
| **Type** | Classical simulation |
| **Fusion probabilities** | τ⊗τ→1 with prob 1/φ², τ⊗τ→τ with prob 1−1/φ² (physically correct) |
| **Braid operations** | B₃ generators via anyon swap |
| **Disclaimer** | Explicit: "does not claim physical fault tolerance" |
| **Status** | Working with tests |

### Q-007: Braid Group B₃ as Access Control (WORKING)
| Field | Value |
|-------|-------|
| **Path** | `carry-agent/braid.rs` |
| **Type** | Classical computation using braid group mathematics |
| **What it is** | B₃ over three authority strands (Curry, Crystal, C3) |
| **Writhe invariant** | Used as integrity check (topologically correct terminology) |
| **Tests** | 4 passing: canonical_pipeline_proves, entropy_gate_blocks, inverse_cancellation, authority_transfer |
| **Status** | Working |

### Q-008: ANU QRNG Quantum Entropy (WORKING)
| Field | Value |
|-------|-------|
| **Path** | `bob-orchestrator/core/quantum.mjs` + `bob-orchestrator/core/bob.mjs` |
| **Type** | Real quantum hardware entropy (ANU quantum vacuum fluctuations) |
| **What's quantum** | The entropy SOURCE — QRNG samples from Australian National University API |
| **What's classical** | Everything else — the WORM chain uses quantum entropy as SEED |
| **Status** | Working (requires network access to ANU API) |

### Q-009: Born Rule Collapse Formalization
| Field | Value |
|-------|-------|
| **Path** | `sov-kernel-monster/lean/BornRuleCollapse.lean` |
| **Type** | Lean 4 spec |
| **Content** | Formal specification of Born rule collapse on ANU QRNG samples |
| **Reference implementation** | `backend/bob/quantum.mjs` (JavaScript) |
| **Status** | Specification only (Lean proofs not shown in visible content) |

---

## 4. Product Readiness Matrix

| Component | Exists | Works | Tested | Benchmarked | Documented | Core Candidate |
|-----------|:------:|:-----:|:------:|:-----------:|:----------:|:--------------:|
| ICP-DAG MUMPS | ✓ | ✓ | ✓(TEST entry) | ✗ | ✓ | ✓ |
| ICP-DAG ASP | ✓ | ✓ | ✗(no runner) | ✗ | ✓ | ✓ |
| SUBLEQ VM (Rust/WASM) | ✓ | ✓ | ✓(4 tests) | ✗ | ✓ | ✓ |
| SUBLEQ Attention (J) | ✓ | ✓ | ✗ | ✗ | partial | Candidate |
| Resonance ISA VM | ✓ | ✓ | ✓(3 tests) | ✗ | partial | ✓ |
| ERE.mjs | ✓ | ✓ | ✗ | ✗ | partial | ✓ |
| ERE.pl | ✓ | partial | ✗ | ✗ | ✓ | Candidate |
| Jordan Proof | ✓ | ✓ | ✓(Lean) | N/A | ✓ | ✓ |
| Entropy Bound Proof | ✓ | ✓ | ✓(Lean) | N/A | ✓ | ✓ |
| EntropyGovernor (harness) | ✓ | ✓ | ✗ | ✗ | ✓ | ✓ |
| Fibonacci Anyon Lean | ✓ | partial | ✓(partial) | N/A | ✓ | Supporting |
| Braid Compilation Lean | ✓ | ✗(all sorry) | ✗ | N/A | ✓ | Experimental |
| Quantum WASM | ✓ | ✓ | ✗ | ✗ | partial | Candidate |
| Fibonacci Anyon Sim (Rust) | ✓ | ✓ | ✓ | ✗ | partial | Supporting |
| ANU QRNG integration | ✓ | ✓ | ✗ | ✗ | ✓ | Supporting |
| WORM chain | ✓ | ✓ | ✓ | ✗ | ✓ | ✓ |

---

## 5. Experimental / Unfinished Systems

| System | Issue |
|--------|-------|
| BraidCompilation.lean | All gate synthesis has `sorry` — structure correct, proofs absent |
| HybridQuantumSAT | `quantum_search` is a stub returning failure; axioms are empty placeholders |
| SovMonster Lean | 26 sorry terms across 11 files, concentrated in matrix closed-form proofs |
| ERE.pl | `resolve_unknown` depends on external `prev_letter`/`next_letter` predicates not in file |
| ConstraintPass (src/lib.rs?) | Agent reported stubs, but inspection shows different code — needs re-verification |

---

## 6. Missing Components

Before the architecture can be considered complete:

1. **SUBLEQ attention benchmark** — compare latency, FLOPs, output quality vs. softmax attention on real tasks
2. **BraidCompilation sorry discharge** — Solovay-Kitaev + Yang-Baxter need actual proofs
3. **SovMonster matrix closed-form** — 7 sorry terms in `SovMonster_Matrix_Closed.lean`
4. **ERE.pl external predicate definitions** — `prev_letter`, `next_letter`, `call_48`
5. **SUBLEQ ↔ ICP-DAG bridge** — the SUBLEQ VM and ICP-DAG exist separately; no integration layer
6. **Quantum swarm topology definition** — precise mathematical statement of what a swarm element IS

---

## Repository Statistics

| Metric | Value |
|--------|-------|
| Primary working directory | `C:\Users\jessi\Desktop\bobs control repo` |
| Languages identified | Rust, Lean 4, MUMPS, J, Prolog, JavaScript/ESM, Python, NASM, Q#, Agda, Idris, F#, Ada, Haskell |
| Identified algorithms | 9 (ALG-001 to ALG-009) |
| Identified DAGs | 6 (DAG-001 to DAG-006), of which 3 are actual DAGs |
| Quantum components | 9 (Q-001 to Q-009) |
| Physical quantum components | 1 (Q-008: ANU QRNG as entropy source) |
| Classical quantum simulations | 3 (Q-005, Q-006, Q-007) |
| Pure math/proof | 4 (Q-001, Q-002, Q-003, Q-004) |
| Proved (0 sorry) | 2 (Jordan fixed-point, Entropy bound) |
| Working compiled artifacts | 2 (quantum-wasm .wasm binary, SUBLEQ VM) |