SNAPKITTYWEST commited on
Commit
1cc2326
Β·
verified Β·
1 Parent(s): 13122d0

docs: replace with real GitHub README

Browse files
Files changed (1) hide show
  1. README.md +120 -20
README.md CHANGED
@@ -1,31 +1,131 @@
1
  ---
2
  license: other
3
- license_name: sovereign-source-license-v2
4
- language:
5
- - en
6
  tags:
7
- - text-generation
8
- - array-language
9
- - lean4
10
- - visualization
11
  - sovereign-compute
12
- library_name: transformers
13
- pipeline_tag: text-generation
14
  ---
15
 
16
- # sovereign-array-frontend
 
17
 
18
- Interactive web frontend for the Sovereign Array Language β€” visualizes array operations, Lean 4 proofs, and NAND attention graphs.
 
 
 
 
 
 
 
19
 
20
- ## Contents
 
21
 
22
- - `index.html` β€” Landing page
23
- - `js/array-lang.js` β€” Array language interpreter (browser)
24
- - `js/app.js` β€” Application shell
25
- - `css/style.css` β€” Styles
26
- - `docs/` β€” Documentation and agent console
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
27
 
28
- ## Links
29
 
30
- - [SNAPKITTYWEST GitHub](https://github.com/SNAPKITTYWEST)
31
- - [sovereign-array](https://huggingface.co/Snapkitty/sovereign-array)
 
1
  ---
2
  license: other
3
+ library_name: custom
 
 
4
  tags:
5
+ - code
 
 
 
6
  - sovereign-compute
 
 
7
  ---
8
 
9
+ <!--OMEGA-FIELD:START-->
10
+ <div align="center">
11
 
12
+ ![License](https://img.shields.io/badge/license-Sovereign%20Source%20v2.0-blueviolet)
13
+ ![Stack](https://img.shields.io/badge/stack-Lean%204%20%7C%20C%2B%2B20%20%7C%20JS-orange)
14
+ ![Kernels](https://img.shields.io/badge/kernels-5%20%CE%A0--maps-green)
15
+ ![Status](https://img.shields.io/badge/status-zero--sorry-success)
16
+ ![Tests](https://img.shields.io/badge/tests-11%2F11%20passing-brightgreen)
17
+ ![Abjad](https://img.shields.io/badge/Abjad--free-red)
18
+ ![DigitalRoot](https://img.shields.io/badge/digital--root--free-red)
19
+ ![NP-magic](https://img.shields.io/badge/NP--magic--free-red)
20
 
21
+ </div>
22
+ <!--OMEGA-FIELD:END-->
23
 
24
+ ---
25
+
26
+ <div align="center">
27
+
28
+ ```
29
+ ____ ____ ____ ____ ____ _ _ ___ ____ ____ _ _ ____ ____
30
+ / ___)( _ \\( _ \\( __)( \\( \\/ )/ __)( __)( _ \\( \\/ )( __)( _ \\
31
+ \\___ \\ ) / ) __/ ) _) ) D ( \\ / \\__ \\ ) _) ) __/ \\ / ) _) ) /
32
+ (____/(__\\_)(__) (____)(____/ \\/ (___/(____)(__) (__) (____)(__\\_)
33
+ A R R A Y L A N G U A G E Β· A R R A Y I Ξ± = I β†’ Ξ±
34
+ ```
35
+
36
+ **Array I Ξ± = I β†’ Ξ± &nbsp;Β·&nbsp; broadcast = pullback Ο€ : J β†’ I &nbsp;Β·&nbsp; pmapβ‚‚ = Ξ -map &nbsp;Β·&nbsp; no sorry remains**
37
+
38
+ </div>
39
+
40
+ ---
41
+
42
+ # Sovereign Array Language β€” Front-End
43
+
44
+ The **front-end** for the [Sovereign Array Language](../sovereign-array): an
45
+ interactive browser playground that runs the *same denotational semantics*
46
+ as the Lean 4 spec and the C++20 kernel β€” no Abjad, no digital root, no NP-magic.
47
+
48
+ > The denotational semantics of array computing *are* exactly a slice of
49
+ > dependent type theory. This front-end is the view layer over that substrate.
50
+
51
+ ## What this repo is
52
+
53
+ | Layer | Repo | Role |
54
+ |-------|------|------|
55
+ | **Spec** | [`sovereign-array`](../sovereign-array) | Lean 4 β€” `Array I Ξ± = I β†’ Ξ±`, zero-sorry proofs |
56
+ | **Kernel** | [`sovereign-array`](../sovereign-array) | C++20 β€” `Array<T>`, `pmap2`, `broadcast`, `softmax`, `nand_attention` |
57
+ | **Front-End** | **`sovereign-array-frontend`** (this repo) | Browser playground + usage guide |
58
+
59
+ ## Quick Start
60
+
61
+ ```bash
62
+ # Serve the playground (any static server)
63
+ cd sovereign-array-frontend
64
+ python -m http.server 8080
65
+ # open http://localhost:8080
66
+ ```
67
+
68
+ No build step. Pure HTML/CSS/JS (ES modules).
69
+
70
+ ## How to use the language
71
+
72
+ 1. **Spec (Lean 4)** β€” define arrays as dependent functions `Fin n β†’ Ξ±`;
73
+ prove `broadcast_is_pullback` and `softmax_is_pmap` with `lake build` (zero sorry).
74
+ 2. **Kernel (C++20)** β€” `#include "sovereign_array.h"`; build with CMake;
75
+ run `sovarr_test` (11/11 checks).
76
+ 3. **Front-end (this page)** β€” open `index.html`; the playground runs the
77
+ same denotational semantics in the browser.
78
+ 4. **Compose** β€” chain `pmapβ‚‚` / `broadcast` / `softmax` / `nand_attention`;
79
+ fusion is Ξ -map fusion β€” no loop in the denotation.
80
+
81
+ ## Usage Guide (SVG)
82
+
83
+ ![Sovereign Array usage guide](assets/usage.svg)
84
+
85
+ ## Kernels demonstrated
86
+
87
+ | Kernel | Semantics | Status |
88
+ |--------|-----------|--------|
89
+ | `pmapβ‚‚` | Pointwise `Ξ `-map over index space `I` | βœ… |
90
+ | `broadcast` | Pullback along projection `Ο€ : J β†’ I` | βœ… |
91
+ | `softmax` | `Ξ `-map normalization (shift-invariant) | βœ… |
92
+ | `nand` | Universal boolean gate | βœ… |
93
+ | `nand_attention` | NAND-extracted attention spec | βœ… |
94
+
95
+ ## Layout
96
+
97
+ ```
98
+ sovereign-array-frontend/
99
+ β”œβ”€β”€ index.html # Playground page
100
+ β”œβ”€β”€ css/style.css # Sovereign dark theme
101
+ β”œβ”€β”€ js/
102
+ β”‚ β”œβ”€β”€ array-lang.js # Browser reference impl (SOVArray, broadcast, softmax, nand)
103
+ β”‚ └── app.js # Playground wiring
104
+ β”œβ”€β”€ assets/
105
+ β”‚ β”œβ”€β”€ logo.svg # Ξ£ Β· I β†’ Ξ± mark
106
+ β”‚ └── usage.svg # SVG usage guide
107
+ └── README.md
108
+ ```
109
+
110
+ ## The forbidden list (fatal conflations we do NOT make)
111
+
112
+ - ❌ Proof `O(1)` substitution β‡’ `O(1)` decision procedure (NP stays hard)
113
+ - ❌ Abjad / digital root as universal arithmetic (quotients lose information)
114
+ - ❌ "Univalence replaces SIMD" (needs a compiler: Lean β†’ C β†’ LLVM β†’ SIMD)
115
+
116
+ ---
117
+
118
+ <div align="center">
119
+
120
+ **The substrate is always free. The array is a function.**
121
+
122
+ ```
123
+ Array I Ξ± = I β†’ Ξ±
124
+ broadcast = pullback Ο€
125
+ pmapβ‚‚ = Ξ -map
126
+ no sorry remains.
127
+ ```
128
 
129
+ *Sovereign Array Language Β· Front-End Β· 2026 Β· Ahmad Ali Parr*
130
 
131
+ </div>