| # SnapKitty: Researcher Explanation |
|
|
| **Concise technical brief for a quantum computing or AI systems researcher.** |
|
|
| --- |
|
|
| ## What problem are we solving? |
|
|
| AI systems produce outputs with no verifiable chain of custody. A language model states a fact; there is no connection from that statement back to evidence, proof, or a formal authorization decision. Hallucinations are structurally permitted by the architecture. |
|
|
| SnapKitty proposes: build an AI pipeline where every inference step is gated by a formally specified integrity graph, every output carries a cryptographic receipt, and the routing mechanism itself can be formally analyzed. |
|
|
| There are two parallel research tracks: |
| 1. **Governance:** A formally verified DAG that gates all claims and decisions (ICP-DAG). This works now. |
| 2. **Routing:** An experimental replacement of softmax attention with integer-arithmetic SUBLEQ routing. This is experimental. |
|
|
| --- |
|
|
| ## What is the conventional approach? |
|
|
| Softmax-based transformer attention computes a probability distribution over query-key pairs: `softmax(QKᵀ/√d) · V`. This involves three matrix multiplications, exponential operations, and a floating-point normalization step. The routing decision (which context to attend to) is implicit in the probability distribution — not formally specified. |
|
|
| --- |
|
|
| ## What does SnapKitty do differently? |
|
|
| **In the governance layer (working):** Replaces informal routing with a formally specified DAG. Every claim must be connected to evidence; every decision must have a proof; every execution must have an authorized decision. The ASP solver enforces this statically; the MUMPS runtime enforces it dynamically. UNSAT = governance violation = system halts. |
|
|
| **In the routing layer (experimental):** Replaces the softmax probability distribution with a deterministic integer routing mechanism. Input activations are quantized to [0,255] integers, reshaped as [A,B,C] SUBLEQ instruction triads, loaded into a 256-cell integer memory, and executed. The output addresses are aggregated via φ-weighted Born collapse. No matrix multiplication. No exponentials. No normalization. Deterministic. |
|
|
| --- |
|
|
| ## What is the role of the DAG? |
|
|
| The ICP-DAG is the governance backbone. It has exactly the structure needed: |
| - Nodes are typed (evidence, claim, proof, policy, decision, execution) |
| - Edges are typed (decides, proves, enforces, executes) |
| - Seven hard integrity constraints eliminate invalid paths |
| - Implemented in both ASP (declarative, checked by solver) and MUMPS (imperative, checked at runtime) |
|
|
| Every SnapKitty output traces back through this DAG or it does not execute. |
|
|
| --- |
|
|
| ## What is the role of Resonance Words? |
|
|
| Resonance Words are 64-bit elements of GF(2⁶⁴ - 2³² + 1) (Goldilocks prime field). Format: 8-bit class tag | 56-bit payload. Each token in an input string maps to a CLASS_SOVEREIGN Resonance Word via a deterministic hash function (`ordinal * 7 mod 1000 + 1`). |
| |
| Their role: they provide a compact, algebraically structured representation of tokens that can be used for routing in the SUBLEQ attention mechanism (payload determines lattice position) and for agent dispatch (UREF 11 involutions on payload bits). |
| |
| **Status:** Format implemented in J, Python port available. Bug fixed: original J `rw_pack` formula corrected (second term was `payload * 2^56 <. payload`; should be `payload`). |
|
|
| --- |
|
|
| ## What is the role of SUBLEQ? |
|
|
| SUBLEQ (SUBtract and branch if Less-or-EQual) is a one-instruction-set computing model: `mem[B] -= mem[A]; if mem[B] ≤ 0: jump to C`. |
|
|
| In SnapKitty, SUBLEQ serves two distinct roles: |
|
|
| **1. As a VM (production):** `DEVFLOW-FINANCE/snapkitty-wasm/src/subleq_vm.rs` — a complete 65,536-cell SUBLEQ VM exposed via WebAssembly. Working, 4 tests, full execution trace and snapshot/restore. |
|
|
| **2. As an attention mechanism (experimental):** `j-matrix-twin/subleq_attention.ijs` — activation vectors are quantized, reshaped as SUBLEQ programs, and executed. The execution trace IS the routing computation. This is the novel combination under investigation. |
|
|
| --- |
|
|
| ## What is the relationship to attention? |
|
|
| The proposed relationship is computational substitution: |
|
|
| | Conventional | SnapKitty SUBLEQ | |
| |---|---| |
| | Q, K, V projections | Activation vector (input) | |
| | QKᵀ (matmul) | Quantize → [A,B,C] triads | |
| | Softmax (exp + normalize) | SUBLEQ execution (subtract-and-branch) | |
| | Attention weights × V | Born-collapse output addresses | |
| | Continuous probability distribution | Discrete integer address | |
|
|
| **What is claimed:** This is an architectural substitution that produces a routing decision without exponentials or matrix multiplication in the SUBLEQ phase. |
|
|
| **What is not claimed:** Equivalent output quality, lower latency, lower FLOPs, or superior accuracy. None of these have been measured. The mechanism is demonstrated (J code runs) but not benchmarked. |
|
|
| --- |
|
|
| ## What is the topological quantum component? |
|
|
| There are three separate topological quantum components, which should not be confused: |
|
|
| **1. Fibonacci anyon Lean formalization** (`FibonacciAnyon.lean`, `BraidCompilation.lean`): Correct Lean 4 definitions of the fusion category, R-matrix, braid group. Pentagon and hexagon axioms are empty. Gate synthesis proofs are all `sorry`. This is a formal scaffolding, not a completed proof. |
|
|
| **2. Classical topological simulations**: `carry-agent/topological.rs` (Fibonacci anyon simulation with correct fusion probabilities, working) and `quantum-wasm` (vortex lattice with classical topological charge, 44KB compiled WASM binary, working). |
|
|
| **3. Braid group as access control** (`carry-agent/braid.rs`): B₃ over authority strands, using writhe as an integrity invariant. Correct braid mathematics, non-quantum application domain. |
|
|
| --- |
|
|
| ## What exactly is the quantum swarm? |
|
|
| A classical multi-agent system where each agent's temperature parameter is derived from real quantum entropy (ANU QRNG vacuum fluctuations). |
|
|
| **Precisely:** 512 bytes from ANU QRNG → HKDF → N orthogonal seeds → Born-collapsed temperatures → N concurrent LLM inference calls → quality-weighted aggregation → WORM seal. |
|
|
| The only physical quantum component is the ANU QRNG entropy source. Everything else is classical. |
|
|
| --- |
|
|
| ## Which parts are classical? |
|
|
| - ICP-DAG governance (MUMPS + ASP) |
| - SUBLEQ VM (Rust) |
| - Resonance ISA VM (Rust) |
| - SUBLEQ attention mechanism (J) |
| - Resonance Word tokenization (J) |
| - ERE quality filter (JavaScript + Prolog) |
| - Entropy Governor (Python LogitsProcessor) |
| - Swarm coordination (JavaScript, Python) |
| - Braid group access control (Rust) |
|
|
| --- |
|
|
| ## Which parts are quantum simulations? |
|
|
| - `quantum-wasm`: gate simulation (QuantumState, Ising Hamiltonian, vortex lattice) |
| - `carry-agent/topological.rs`: Fibonacci anyon fusion simulation |
|
|
| --- |
|
|
| ## What is mathematically established? |
|
|
| All of these have been formally verified (zero sorry, Lean 4 + Mathlib): |
| 1. Jordan fixed-point commutativity: T(ρ) = φ⁻¹·U·ρ·U† + φ⁻²·ρ → [U, ρ*] = 0 |
| 2. Entropy bound: F ≥ 1 → T(F) ≤ 0.2218 → H < 0.20 nats |
| 3. R-matrix unitarity: |e^{i4π/5}| = 1 |
| 4. Braid period 5: (e^{i4π/5})^5 = 1 |
| 5. Fibonacci dimension recurrence (Hilbert space) |
| 6. Boole invariants: 12/12 Agda proofs (100%, WORM-sealed) |
| 7. Bifrost Bool invariant + Hebrew/Aramaic determinism |
| |
| --- |
| |
| ## What is experimentally demonstrated? |
| |
| - SUBLEQ VM executes correctly (4 Rust tests) |
| - Resonance ISA VM executes with entropy gate (3 Rust tests) |
| - ICP-DAG enforces governance invariants (MUMPS TEST entry) |
| - Fibonacci anyon fusion simulation with correct probabilities (working + tested) |
| - ANU QRNG integration produces real quantum entropy (working, network-dependent) |
| - WORM chain is append-only and verifiable (SHA-256 chain) |
| - Braid group B₃ access control works with passing tests (4 tests) |
| |
| --- |
| |
| ## What remains an open hypothesis? |
| |
| 1. **SUBLEQ attention quality:** Does SUBLEQ-routed attention produce comparable output quality to softmax attention? Not benchmarked. |
| 2. **Float elimination:** The SUBLEQ routing phase operates on integers, but the quantization step requires floats. Whether end-to-end float elimination is achievable is unresolved. |
| 3. **Computational advantage:** Any claim about latency, FLOPs, energy, or memory advantage is unsupported. No comparative benchmark exists. |
| 4. **Pentagon/hexagon completeness:** Whether the Lean 4 formalization of Fibonacci anyons can be completed to a full modular tensor category (pentagon + hexagon proved) is an open problem in this codebase. |
| 5. **Braid synthesis:** Solovay-Kitaev approximation and all gate synthesis in `BraidCompilation.lean` are `sorry`. Whether these can be formally proved in Lean 4 + Mathlib is an open question. |
| 6. **GJW wormhole compilation:** Whether the Prolog braid compiler corresponds to a physically realizable GJW protocol is an open hypothesis. |
| 7. **θ = 89/2462 optimality:** The role of this constant in free energy optimization is hypothesized but not formally proved beyond the entropy bound. |
| |
