ENTER SOVEREIGN INTERIOR — BOB'S PLAYABLE WORM CHAIN
_{First-person Three.js + Rapier3D · inspect → collect → verify → unlock → seal}

Sov-Kernel-Monster is a local-first sovereign compute stack that:

1. Accepts quantum circuits or mathematical workloads
2. Compiles them through QATAAUM — a clean-room quantum compiler (33K+ lines Rust, 221 tests)
3. Executes through native Fortran, ARM64, WASM, or GPU targets where implemented
4. Checks designated mathematical and safety properties in Lean 4, Agda, and typed Haskell
5. Signs outputs with Ed25519 using your sovereign node key
6. Seals every execution receipt into a Blake3 hash-linked WORM chain

This is not a service. This is not a cloud platform. There is no remote server, no API key to a third party, no terms of service that can revoke your access.

The IBM quantum backend currently uses a deterministic mock (Phase 1). Real hardware routing is Phase 2. Everything else runs locally and is fully implemented.

This is not one executable. It is one architecture.

→ Enter Sovereign Interior — BOB's Game Walk the procedural chamber, recover its covenant evidence, verify the trust chain, unlock the terminal, and leave through the sealed door.

→ Interactive Trajectory Hub The trajectory renderer visualizes stochastic density-matrix paths over a Bures manifold, with playback controls and WORM-attested execution state.

→ BOB Meets BOB Two BOB agents — SnapKitty software and IBM hardware — shaking hands across the Bifrost FFI bridge. The handshake is real; the FFI is live.

→ Sovereign Convergence Art Real-time visualization of the Jordan Spectral Transformer converging. Watch entropy fall as ρ* approaches the BPS fixed point — what you are seeing is Bekenstein-Hawking black hole entropy converging live.

→ Sovereign Interior source — The complete dependency-free scaffold, game systems, procedural scene, and test suite.

USER INPUT (OpenQASM · Matrix · Agent Task)
          │
          ▼
┌─────────────────────────────────┐
│   QATAAUM QUANTUM COMPILER      │  33K+ Rust · 221 tests · 31 Lean theorems
│   Parse → IR → Route → Target   │
└────────────────┬────────────────┘
                 │
    ┌────────────┼─────────────┐
    ▼            ▼             ▼
Fortran      ARM64/SVE2     WASM/Browser
Bare-metal   LLVM target    wasm-pack
                 │
    ┌────────────┴─────────────┐
    ▼                          ▼
RTX/CUDA              Haskell/AToKio
GPU target            Agent simulation
                 │
    ┌────────────┴─────────────┐
    ▼                          ▼
IBM Quantum           (more targets)
MOCK BACKEND ⚠        Phase 2 planned
          │
          ▼
┌─────────────────────────────────┐
│   VERIFICATION BOUNDARY         │  65+ theorems · 0 sorry
│   Lean 4 + Agda + Haskell types │
└────────────────┬────────────────┘
                 ▼
┌─────────────────────────────────┐
│   CRYPTOGRAPHIC ATTESTATION     │  Blake3 → Ed25519 → SovKangarooShake
│   Hash → Sign → Seal            │
└────────────────┬────────────────┘
                 ▼
┌─────────────────────────────────┐
│   WORM RECEIPT CHAIN            │  Append-only · Hash-linked · Immutable
│   RECEIPT₀ → RECEIPT₁ → RECEIPTₙ│
└─────────────────────────────────┘

⚠️ IBM Quantum: The current implementation uses a deterministic mock backend for Phase 1 validation. Real IBM hardware routing is planned for Phase 2. The BUILD_VALIDATION.md explicitly documents this as "Phase 1 — Mock Quantum Backend."

Play Sovereign Interior or open the interactive research hub in any modern browser. No install required.

# Prerequisites: gfortran 12+, make
git clone https://github.com/SNAPKITTYWEST/sov-kernel-monster
cd sov-kernel-monster
make all
# Expected: native kernel binary, zero errors, zero warnings

# Prerequisites: Lean 4.14.0, Lake
cd lean
lake exe cache get    # downloads Mathlib cache (~2GB, one-time)
lake build
# Expected: ✔ Built SovMonster_Matrix_Closed, SovereignCalculusBridge,
#           MOCJordanRoundtrip, AdaptiveVerifiedRuntime, JordanMatrixProof
#           Build completed successfully.

# Prerequisites: Agda 2.6+
agda src/agda/Proofs/Safety.agda
# Expected: Type checks cleanly. safety-compose theorem verified.

# Prerequisites: GHC 9.4+, Stack or Cabal
cd haskell
stack build              # or: cabal build
stack exec production-simulator
# Expected: 10 agents × 1000 steps
#           10,000 observations (WORM-sealed)
#           100 consensus rounds · 0 invariant violations
#           PRODUCTION RUN SUCCESSFUL [OK]

# Prerequisites: Rust, wasm-pack
make wasm
# Expected: wasm/pkg/ directory with .wasm binary (~44KB)

# Prerequisites: CMake, CUDA toolkit, NVIDIA GPU
cd rtx && mkdir build && cd build
cmake .. -DSOV_BUILD_CUDA=ON -DSOV_ZERO_LIBC=ON
cmake --build . --config Release

Every execution produces a receipt. Every receipt references the previous receipt's hash. The chain cannot be broken, reordered, or deleted.

What gets sealed: circuit compilations, density matrix evolution steps, measurement results, agent observations, consensus votes, game completion events, kernel executions.

What a receipt contains:

{
  "sequence": 42,
  "eventType": "MISSION_COMPLETED",
  "previousHash": "a3f9b2c1...",
  "payloadHash": "7c2ef445...",
  "stateHash":   "f1b83a92...",
  "currentHash": "2d9c7f01...",
  "timestamp":   1753361234
}

Verification: worm_grows and worm_history theorems in lean/SovMonster_Matrix_Closed.lean — machine-checked in Lean 4 — prove that appending never destroys history and the chain only grows.

• jordan_fixed_point_commutes — [U, ρ*] = 0 at matrix level over Matrix n n ℂ (PAR-011)
• omega_lt_phi_inv — Ω < φ⁻¹ using Real.exp_one_gt_d9
• dual_contraction_hierarchy — Ω < φ⁻¹ < 1, both layers contract
• moc_jordan_roundtrip — lossless encode/decode of Jordan states into MOC-108
• moc_encode_injective — encoding loses no information
• sovereign_bot_step_master — AToKio step is constitutionally valid, WORM-sealed, omega-bounded
• worm_grows / worm_history — WORM chain immutability
• softmax_sums_to_one / softmax_nonneg — Born rule on simplex
• fibonacci_channel_trace_preserving — tr(UρU†) = tr(ρ)
• safety-compose (Agda) — safe transitions compose to safe transitions
• 31 QATAAUM compiler theorems (see qataaum/verification/lean4/)

The following are not covered by the machine-checked proofs:

• Operating system behavior
• Compiler implementation correctness (gfortran, GHC, rustc)
• GPU driver and firmware
• FFI implementation behavior (behavior of C bindings, not their type signatures)
• IBM quantum hardware (mock backend in Phase 1)
• Browser runtime
• Physical hardware
• System clock
• External services
• Performance measurements (benchmark-environment specific)
• Every module in all 30 languages (formal verification covers the listed theorems only)

All performance numbers (P99 45ms, 1000 seals/sec) are from a single production simulator run on local hardware. They are not a continuous SLA measurement.

• IBM quantum interface uses a deterministic mock backend (Phase 1). Real hardware: Phase 2.
• RTX target requires NVIDIA GPU with CUDA toolkit.
• ARM64/SVE2 bare-metal requires flang-new-19 — not available in standard package managers.
• Formal verification covers the listed theorems. It does not cover every line of every module in all 30 languages.
• FFI boundaries — the type signatures of Fortran↔Haskell bridges are typed; the runtime behavior of C ABI implementations is tested but not formally proved.
• Performance numbers are benchmark-environment specific and not independently audited.
• Enterprise certification CERT-PHASE9-001 is a project-issued production-conformance certificate based on the published checks in this repository. It is not ISO, SOC 2, NIST, governmental, university, or independent third-party certification.
• Jacobian Conjecture — this repository contains formalized intermediate results, negative strategy certificates (three algebraic strategies proved impossible), and a proposed Jordan algebraic bypass (PAR-011, machine-checked). It does not contain a complete, independently-reviewed proof of the full conjecture.
• SLA targets — the published metrics (P99 45ms, 99.7% uptime) are from a single test run, not continuous production monitoring. The 99.7% achieved vs. 99.9% target is below target.

This system does not degrade silently. Every failure mode halts cleanly with a specific status:

The hlt #0 at address 0x0000DEAD0000 in src/start.S is not decoration. It is the fault handler — the machine writes to DEAD and stops. There is no recovery path. This is intentional.

Note on Haskell build tool: Stack and Cabal are both supported. The haskell/ directory contains both stack.yaml and liquidlean-theorem3.cabal. Use Stack for the simulator; use Cabal for the theorem library.

APL (financial array engine), Prolog (quantum monad / watchtower), COBOL (structured records), PL/I (sovereign governance), INTERCAL (COMEFROM tripwire), Janet, Julia, Zig, OCaml, Odin, Racket, Smalltalk, R, Go (NATS subjects) — each exists for a specific role. None are decorative. The APL array engine replaces Python/NumPy for all array operations: ⌽ (one symbol) processes an entire financial dataset simultaneously. That is not language tourism. That is the right tool for the job.

These items address the review feedback directly:

"Formally verified end-to-end" means: the mathematical core (Jordan operator, WORM chain immutability, AToKio invariants, MOC-Jordan encoding) is machine-checked. It does not mean every line of every file in 30 languages is covered by a proof. The verification boundary section above lists exactly what is proved.

"Zero dependencies" refers to the bare-metal Fortran kernel specifically — no libc, no C runtime, no external libraries in the src/ execution path. The broader stack (QATAAUM, Haskell runtime) uses standard ecosystem dependencies.

"Zero libc" refers to src/sov_monster_kernel.f90 and the start.S entry point. The RTX and WASM targets use their respective platform runtimes.

Uptime 99.7% vs target 99.9% — this is from a single production simulator run, not continuous production monitoring. The 99.7% figure reflects 997/1000 steps completing without error in that run. It is below the stated 99.9% target.

Enterprise certification CERT-PHASE9-001 — project-issued. The checks are real, the evidence is in this repository, and any party can independently rerun them using the commands in this README. It is not issued by an independent third party.

BOB MEETS BOB

Two BOBs. Two Realms. One Bridge. Infinite Possibilities. Built on IBM credits. In IBM's IDE. With IBM's model. The handshake before the revolution.

Every quantum computing platform today runs on someone else's cloud. IBM Qiskit routes through IBM hardware. Google Cirq requires Google infrastructure. Amazon Braket bills by the shot. Your quantum programs, your algorithms, your results — all pass through a corporation that can revoke access, inspect your work, or shut down the service.

The AI stack has the same problem. Every LLM inference call goes to OpenAI, Anthropic, or Google. They decide what you can ask. They see every prompt. Your intellectual work passes through their servers, subject to their terms, logged in their databases.

This repository is the answer to both problems at once.

A complete, sovereign quantum computing and AI platform — compiler, execution engine, AI inference runtime, formal verification layer, multi-agent spacetime simulator, and cryptographic attestation system — that runs on YOUR hardware, answers to YOUR keys, and proves its own correctness mathematically.

Three systems fused into one:

QATAAUM — A clean-room quantum circuit compiler. OpenQASM 2.0/3.0 input. 9 intermediate representations. SABRE qubit routing. Pulse schedule output. 33,000+ lines of Rust. 221 passing tests. 31 Lean 4 theorems, zero sorry.

Sov-Kernel-Monster — A Fortran 2018 bare-metal quantum math kernel. Evolves density matrices via the Jordan Spectral Transformer. Runs on ARM64 SVE2 or RTX 4090. Zero libc. Zero C runtime. Every output Blake3+Ed25519 signed and sealed to an append-only WORM chain.

AToKio Spacetime Simulator — A formally verified multi-agent simulation runtime. Ahmad_bot agents operate in a physics manifold (Quantum / Gravity / Relativity / Wormhole frames). 7 Agda invariants enforced on every monadic bind. WORM-sealed per observation. Byzantine fault-tolerant consensus every 10 steps. Enterprise Level 3 certified.

Certificate ID: CERT-PHASE9-001 Level: Level3_Production_Hardened Issued: 2026-07-24 Issuing authority: SnapKitty Collective / Bel Esprit D'Accord Irrevocable Trust · EIN 42-697643

The mathematical foundation connecting two formal systems:

Proved in Lean 4.14.0 + Mathlib, zero sorry (lean/SovereignCalculusBridge.lean):

Ω < φ⁻¹ < 1

The domain wall is the harder constraint. Any transition satisfying Ω-admissibility is automatically φ⁻¹-stable. A system satisfying both constants is doubly stable at two independent layers.

Master theorem sovereign_bot_step_master:

Every AToKio step is a constitutionally valid SDCTransition with omega_weight = φ⁻¹, sealed by a 64-char SovKangarooShake hash, within a SovereignDomain partitioned by the frame detection function. Proved simultaneously:

• omega_weight = φ⁻¹
• Ω < omega_weight < 1
• step counter advances by exactly 1
• worm_hash.length = 64

MOC-Jordan roundtrip (lean/MOCJordanRoundtrip.lean, zero sorry):

decode ∘ encode = id on Matrix (Fin 10) (Fin 10) α embedded in Fin 108. Encoding is injective — no information lost. Key: 10×10 = 100 entries fit in 108 slots (8 zero-padding). Proved by omega.

Total: 65+ theorems. Zero sorry. All machine-checked.

Key theorems:

• jordan_fixed_point_commutes — [U, ρ*] = 0 at matrix level over Matrix n n ℂ
• omega_lt_phi_inv — Ω < φ⁻¹ using Real.exp_one_gt_d9 (2.7182818283 < e)
• moc_jordan_roundtrip — lossless encode/decode of Jordan states into MOC-108
• sovereign_bot_step_master — all four bridge gaps closed simultaneously
• safety-compose (Agda) — safe transitions compose to safe transitions

SovKangarooShake (haskell/SovKangarooShake.hs)

input
  ↓  KangarooTwelve (12-round Keccak fast absorb)
  ↓  domain separator "SOVKERNELv1\x1F"
  ↓  SHAKE256 (extendable sponge, 256-bit security)
  ↓
32 bytes → hex encode → 64 chars

Enforced by type: ProvenanceSeal.h_length : worm_hash.length = 64 You cannot construct a ProvenanceSeal with a non-64-char hash. The Lean type system is the gate.

haskell/AToKio.hs — Work-stealing scheduler with invariant precondition gates

haskell/AToKioMonad.hs — 7 invariants enforced on every >>=

haskell/AToKioLinear.hs — {-# LANGUAGE LinearTypes #-} resource safety at compile time

The 7 invariants from BotAgentLoop.agda:

1. step ≡ k              step counter matches expected index
2. errorStatus ≡ 0       no errors
3. stateValid ≡ true     internal state consistent
4. messageCount ≡ step   messages track steps exactly
5. apiKeyUsage ≤ 1000    bounded API calls
6. protocolSteps ≤ msgs  protocol bounded by messages
7. messageCount ≤ 10000  max queue size

Invariant violation → atomic halt. No silent degradation.

haskell/AhmadBotAgent.hs — Ahmad_bot operates inside the physics manifold.

Frame detection by position magnitude:

Goal state machine: ExploreFrame → DeepInspect → BridgeFrames → HaltAtBoundary

At the Horizon, the bot recognizes the limit — it does not crash. 5-bot swarm. Consensus every 10 steps. All 7 invariants. WORM-sealed per observation.

Three certified strategy failures documented in haskell/LiquidLean/Jacobian/NegativeResult.hs:

Two independent paths to the conjecture:

Path A (Osgood-Picard 1899): det JF=1 → étale → proper → finite cover → degree 1. Requires entire function theory not yet in Mathlib.

Path B (Parr 2026 — PAR-011, machine-checked): det JF=1 → polynomial Hamiltonian → Jordan T(ρ) = φ⁻¹·UρU† + φ⁻²·ρ → [U,ρ*]=0 (zero sorry) → ρ* ∈ polynomial commutant → F⁻¹ polynomial. No entire function theory needed.

The Phase 8 certificate exports: phase8_certificate.json · jacobian_proof_dag.tikz · TheoremB1.lean · StrategyFailures.lean · JordanBridge.lean

haskell/LiquidLean/AdaptiveVerifiedRuntime.hs

K₀ running
  → profiler detects hot path / performance regression
  → MLIR rewriter generates K₁ candidate
  → Lean verifier: K₁ ⊨ all invariants?
  → speedup(K₁) ≥ 1.05×?
  → both pass: atomic STM hot-swap K₀→K₁ + WORM receipt
  → either fails: rollback (also re-verified)
  → MetaLearner weights strategies → exponential decay 0.9
  → loop forever

IR ladder: Fortran → Cmm → MLIR_Quantum → MLIR_Pulse → MLIR_LLVM → LLVM → Native

No kernel is ever deployed without a passing Lean proof.

Physics modules:

Production run results:

10 agents × 1,000 steps
10,000 observations (WORM-sealed)
100 consensus rounds
0 invariant violations
Deterministic (seed = 42)
CERT-PHASE9-001: Level3_Production_Hardened

# Quantum engine (gfortran)
make all

# Full LLVM pipeline → ARM64 SVE2 bare metal (flang-new-19)
make monster

# WASM bridge → browser
make wasm

# RTX 4090 zero-libc inference
cd rtx && mkdir build && cd build
cmake .. -DSOV_BUILD_CUDA=ON -DSOV_ZERO_LIBC=ON
cmake --build . --config Release

# Lean formal verification
cd lean && lake exe cache get && lake build

# Haskell spacetime simulator
cd haskell && stack build && stack exec production-simulator

# Run compliance audit
stack exec compliance-audit -- PHASE9

# Full sovereign pipeline with node key
SOV_SK=path/to/node_sk.bin ./build_monster.sh

sov-kernel-monster/
├── bobs game/              Playable Sovereign Interior (Three.js + Rapier3D)
├── src/                    Fortran 2018 quantum kernel (22 modules)
├── lean/
│   ├── SovMonster_Matrix_Closed.lean   Jordan commutativity (12 theorems, 0 sorry)
│   ├── SovereignCalculusBridge.lean    Ω↔φ⁻¹ bridge (8 theorems, 0 sorry)
│   ├── MOCJordanRoundtrip.lean         MOC-108 ↔ Jordan 10×10 (2 theorems, 0 sorry)
│   ├── AdaptiveVerifiedRuntime.lean    AVR proof obligations
│   └── JordanMatrixProof.lean          Jordan block proofs
├── haskell/
│   ├── AToKio.hs                  Bounded scheduler (7 Agda invariants)
│   ├── AToKioMonad.hs             Invariant-checking monad
│   ├── AToKioLinear.hs            Linear types resource safety
│   ├── AhmadBotAgent.hs           Ahmad_bot as SpacetimeAgent
│   ├── SovKangarooShake.hs        K12∘SHAKE256 sovereign hash
│   ├── SpacetimeAgent.hs          Frame detection + decision policy
│   ├── ManifoldGeometry.hs        Metric tensors, regions
│   ├── GravityModule.hs           Newtonian gravity
│   ├── RelativityModule.hs        Time dilation, Schwarzschild
│   ├── QuantumModule.hs           Superposition, decoherence
│   ├── WormholeModule.hs          Topology shortcuts
│   ├── SimulationStep.hs          Unified physics step
│   ├── AgentGoals.hs              Adaptive goal system
│   ├── AgentMemory.hs             WORM observation history
│   ├── ConsensusTypes.hs          Voting types
│   ├── ConsensusVoting.hs         Byzantine fault-tolerant consensus
│   ├── ProductionSimulator.hs     10 agents × 1,000 steps
│   ├── ComplianceFramework.hs     Level 3 enterprise certification
│   ├── AuditTrailExporter.hs      WORM chain integrity + CSV
│   └── LiquidLean/
│       ├── AdaptiveVerifiedRuntime.hs  Self-modifying kernels
│       └── Jacobian/NegativeResult.hs  Phase 8 certificate
├── src/agda/               Agda capability algebra + safety proofs
├── qataaum/                Quantum compiler (33K+ Rust, 221 tests, 31 Lean theorems)
├── rtx/                    RTX 4090 zero-libc inference engine
├── mlir/                   MLIR polyhedral fusion pipeline
├── sovereign-pli/          PL/I + COBOL + INTERCAL governance
└── trust/                  Sovereignty deeds + WORM workflow

One person. Ahmad Ali Parr. AI-assisted. 3 months. 110+ repos.

The architecture was conceived as a unit. Ω and φ⁻¹ are not arbitrary constants — they encode the same stability requirement at two different layers. The frame detection function in the spacetime simulator formalizes the same cognitive pattern Ahmad uses when approaching mathematical problems. The WORM receipt in the 3D game uses the same cryptographic structure as the quantum kernel's execution log. The Jacobian negative result certificate exports Lean stubs, TikZ, and JSON — formal documentation of mathematical progress, WORM-anchored.

This is not a collection of projects. It is one system.

Prior art: PAR-001 through PAR-016 under SSL v3.0 Part IX. LinkedIn publication July 1, 2026. Zenodo DOIs: see project Zenodo papers.

Sovereign Source License v3.0 — SnapKitty Collective / Bel Esprit D'Accord Trust · EIN 42-697643

Functional Source License 1.1 — Change Date: 2030-07-22. Change License: Apache-2.0.