Add docs/RESEARCHER_EXPLANATION.md

docs/RESEARCHER_EXPLANATION.md

@@ -0,0 +1,161 @@
+# 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.