docs: add proper model card

README.md

@@ -1,123 +1,31 @@
-<!--OMEGA-FIELD:START-->
-<div align="center">
-
-![License](https://img.shields.io/badge/license-Sovereign%20Source%20v2.0-blueviolet)
-![Stack](https://img.shields.io/badge/stack-Lean%204%20%7C%20C%2B%2B20%20%7C%20JS-orange)
-![Kernels](https://img.shields.io/badge/kernels-5%20%CE%A0--maps-green)
-![Status](https://img.shields.io/badge/status-zero--sorry-success)
-![Tests](https://img.shields.io/badge/tests-11%2F11%20passing-brightgreen)
-![Abjad](https://img.shields.io/badge/Abjad--free-red)
-![DigitalRoot](https://img.shields.io/badge/digital--root--free-red)
-![NP-magic](https://img.shields.io/badge/NP--magic--free-red)
-
-</div>
-<!--OMEGA-FIELD:END-->
-
----
-
-<div align="center">
-
-```
-  ____  ____  ____  ____  ____  _  _  ___  ____  ____  _  _  ____  ____
- / ___)(  _ \\(  _ \\(  __)(    \\( \\/ )/ __)(  __)(  _ \\( \\/ )(  __)(  _ \\
- \\___ \\ )   / ) __/  ) _)  ) D ( \\  / \\__ \\ ) _)  ) __/ \\  /  ) _)  )   /
- (____/(__\\_)(__)   (____)(____/  \\/  (___/(____)(__)   (__)  (____)(__\\_)
-        A R R A Y   L A N G U A G E   ·   A R R A Y   I  α  =  I  →  α
-```
-
-**Array I α = I → α &nbsp;·&nbsp; broadcast = pullback π : J → I &nbsp;·&nbsp; pmap₂ = Π-map &nbsp;·&nbsp; no sorry remains**
-
-</div>
-
----
-
-# Sovereign Array Language — Front-End
-
-The **front-end** for the [Sovereign Array Language](../sovereign-array): an
-interactive browser playground that runs the *same denotational semantics*
-as the Lean 4 spec and the C++20 kernel — no Abjad, no digital root, no NP-magic.
-
-> The denotational semantics of array computing *are* exactly a slice of
-> dependent type theory. This front-end is the view layer over that substrate.
-
-## What this repo is
-
-| Layer | Repo | Role |
-|-------|------|------|
-| **Spec** | [`sovereign-array`](../sovereign-array) | Lean 4 — `Array I α = I → α`, zero-sorry proofs |
-| **Kernel** | [`sovereign-array`](../sovereign-array) | C++20 — `Array<T>`, `pmap2`, `broadcast`, `softmax`, `nand_attention` |
-| **Front-End** | **`sovereign-array-frontend`** (this repo) | Browser playground + usage guide |
-
-## Quick Start
-
-```bash
-# Serve the playground (any static server)
-cd sovereign-array-frontend
-python -m http.server 8080
-# open http://localhost:8080
-```
-
-No build step. Pure HTML/CSS/JS (ES modules).
-
-## How to use the language
-
-1. **Spec (Lean 4)** — define arrays as dependent functions `Fin n → α`;
-   prove `broadcast_is_pullback` and `softmax_is_pmap` with `lake build` (zero sorry).
-2. **Kernel (C++20)** — `#include "sovereign_array.h"`; build with CMake;
-   run `sovarr_test` (11/11 checks).
-3. **Front-end (this page)** — open `index.html`; the playground runs the
-   same denotational semantics in the browser.
-4. **Compose** — chain `pmap₂` / `broadcast` / `softmax` / `nand_attention`;
-   fusion is Π-map fusion — no loop in the denotation.
-
-## Usage Guide (SVG)
-
-![Sovereign Array usage guide](assets/usage.svg)
-
-## Kernels demonstrated
-
-| Kernel | Semantics | Status |
-|--------|-----------|--------|
-| `pmap₂` | Pointwise `Π`-map over index space `I` | ✅ |
-| `broadcast` | Pullback along projection `π : J → I` | ✅ |
-| `softmax` | `Π`-map normalization (shift-invariant) | ✅ |
-| `nand` | Universal boolean gate | ✅ |
-| `nand_attention` | NAND-extracted attention spec | ✅ |
-
-## Layout
-
-```
-sovereign-array-frontend/
-├── index.html          # Playground page
-├── css/style.css       # Sovereign dark theme
-├── js/
-│   ├── array-lang.js   # Browser reference impl (SOVArray, broadcast, softmax, nand)
-│   └── app.js          # Playground wiring
-├── assets/
-│   ├── logo.svg        # Σ · I → α mark
-│   └── usage.svg       # SVG usage guide
-└── README.md
-```
-
-## The forbidden list (fatal conflations we do NOT make)
-
-- ❌ Proof `O(1)` substitution ⇒ `O(1)` decision procedure (NP stays hard)
-- ❌ Abjad / digital root as universal arithmetic (quotients lose information)
-- ❌ "Univalence replaces SIMD" (needs a compiler: Lean → C → LLVM → SIMD)
-
----
-
-<div align="center">
-
-**The substrate is always free. The array is a function.**
-
-```
-Array I α = I → α
-broadcast  = pullback π
-pmap₂      = Π-map
-no sorry remains.
-```
-
-*Sovereign Array Language · Front-End · 2026 · Ahmad Ali Parr*
-
-</div>
+---
+license: other
+license_name: sovereign-source-license-v2
+language:
+- en
+tags:
+- text-generation
+- array-language
+- lean4
+- visualization
+- sovereign-compute
+library_name: transformers
+pipeline_tag: text-generation
+---
+
+# sovereign-array-frontend
+
+Interactive web frontend for the Sovereign Array Language — visualizes array operations, Lean 4 proofs, and NAND attention graphs.
+
+## Contents
+
+- `index.html` — Landing page
+- `js/array-lang.js` — Array language interpreter (browser)
+- `js/app.js` — Application shell
+- `css/style.css` — Styles
+- `docs/` — Documentation and agent console
+
+## Links
+
+- [SNAPKITTYWEST GitHub](https://github.com/SNAPKITTYWEST)
+- [sovereign-array](https://huggingface.co/Snapkitty/sovereign-array)