Asi transcendental-keyboard

Unified keyboard control surface for transcendental syntax proof environments (Stellogen, Proof General, Narya, Lean) with Gay.jl color feedback

install

source · Clone the upstream repo

git clone https://github.com/plurigrid/asi

Claude Code · Install into ~/.claude/skills/

T=$(mktemp -d) && git clone --depth=1 https://github.com/plurigrid/asi "$T" && mkdir -p ~/.claude/skills && cp -r "$T/skills/transcendental-keyboard" ~/.claude/skills/plurigrid-asi-transcendental-keyboard && rm -rf "$T"

manifest: skills/transcendental-keyboard/SKILL.md

source content

Transcendental Keyboard Control Surface

Trit: 0 (ERGODIC - coordination hub) GF(3) Conservation: Σ(proof-assistants) ≡ 0 (mod 3)

Overview

Unified Emacs keyboard control surface integrating:

Transcendental Syntax - Stellogen logic-agnostic programming
Proof General - Universal proof assistant interface
Narya - Higher-dimensional observational type theory
Lean - Interactive theorem prover
Gay.jl - Deterministic color feedback with GF(3) trits
Self-Operating Proofs - Automated tactic application

Architecture

┌─────────────────────────────────────────────────────────┐
│  User Keyboard Input                                    │
└────────────┬────────────────────────────────────────────┘
             │
             ▼
┌─────────────────────────────────────────────────────────┐
│  Transient Menu System (C-c t)                          │
│  ├─ Proof Menu (p)                                      │
│  ├─ Stellogen Menu (s)                                  │
│  ├─ Narya Menu (n)                                      │
│  └─ Color Menu (c)                                      │
└────────────┬────────────────────────────────────────────┘
             │
    ┌────────┼────────┬────────┐
    ▼        ▼        ▼        ▼
┌────────┐ ┌───────┐ ┌──────┐ ┌────────┐
│ Proof  │ │Stelle-│ │Narya │ │ Gay.jl │
│General │ │ gen   │ │Bridge│ │ Colors │
└───┬────┘ └───┬───┘ └──┬───┘ └───┬────┘
    │          │         │         │
    └──────────┴─────────┴─────────┘
                 │
                 ▼
         ┌──────────────────┐
         │  Mode-line Color │
         │  Visual Feedback │
         └──────────────────┘

Key Bindings

Main Control Panel

Key	Command	Description
`C-c t`	`transcendental`	Main control panel
`C-c t p`	`transcendental-proof-menu`	Proof navigation
`C-c t s`	`transcendental-stellogen-menu`	Stellogen control
`C-c t n`	`transcendental-narya-menu`	Narya templates
`C-c t c`	`transcendental-color-menu`	Color control

Proof Navigation (Direct)

Key	Command	Description
`C-c C-n`	`trans-kb-proof-forward`	Step forward
`C-c C-u`	`trans-kb-proof-backward`	Step backward
`C-c C-RET`	`trans-kb-proof-to-cursor`	Process to cursor
`C-c C-b`	`trans-kb-proof-whole-buffer`	Process entire buffer
`C-c C-a`	`trans-kb-auto-prove`	Attempt auto-proof

GF(3) Proof State Mapping

Proof States → GF(3) Trits → Mode-line Colors

unproved    → -1 (MINUS)   → RED     #FF0000
processing  → 0  (ERGODIC) → YELLOW  #FFFF00
proved      → +1 (PLUS)    → GREEN   #00FF00

Conservation Law

For any sequence of proof steps:

Σ (state_i mod 3) ≡ 0 (mod 3)

Example trajectory:

[proved unproved unproved proved proved proved]
  +1      -1       -1      +1     +1     +1

Sum: +1 - 1 - 1 + 1 + 1 + 1 = +2 ≡ -1 (mod 3)

Proof Assistant Integration

1. Stellogen (Transcendental Syntax)

' Create constellation
spec add =
  -add(z Y) +result(Y);
  -add(s(X) Y) +add(X s(Y)).

' Run with C-c t s r

Commands:

```
trans-kb-stellogen-run-file
```
- Execute .sg file
```
trans-kb-stellogen-constellation
```
- Insert template

2. Narya (Observational Bridge Types)

-- Bridge type template (C-c t n b)
def bridge (A : Type) (x y : A) : Type := x ≡ y

-- Transport template (C-c t n t)
def transport (A : Type) (P : A → Type) (x y : A) (p : x ≡ y) : P x → P y
  := λ px. subst P p px

Features:

Observational equality (no interval type)
Higher-dimensional type theory
Bridge types computed from structure

3. Proof General (Coq/Lean/Agda)

Standard Proof General commands enhanced with:

Color state feedback
Auto-save on successful steps
GF(3) conservation tracking

Gay.jl Color Integration

Deterministic Color Generation

;; Set seed (matches Gay.jl)
(setq trans-kb-gay-seed 1069)

;; Get next color in sequence
(trans-kb-next-color)
;; => (:L 52.3 :C 78.1 :H 215.7 :hex "#2D4FE8" :index 1)

;; Update mode-line based on proof state
(trans-kb-update-mode-line-color)

Color Menu (C-c t c)

Command	Description
`n`	Next color in sequence
`s`	Set Gay.jl seed
`t`	Toggle mode-line coloring
`r`	Reset color index
`c`	Show current color info

Self-Operating Proof Automation

Auto-Prove Tactics

(setq trans-kb-auto-tactics
  '("reflexivity"      ; Identity proofs
    "apply assumption" ; Use hypotheses
    "intro"            ; Introduce variables
    "split"            ; Conjunction
    "left"             ; Disjunction left
    "right"            ; Disjunction right
    "exact rfl"))      ; Definitional equality

Usage

(* Unsolved goal *)
Theorem auto_example : forall x, x = x.
Proof.
  C-c C-a  (* Auto-prove attempts tactics *)
  (* ✅ Auto-proved with: reflexivity *)
Qed.

Mode-Line Visual Feedback

┌─────────────────────────────────────────────────────────┐
│  [RED]     U:--- proof.v  All L1   𝕋𝕊   (Coq)         │ ← Unproved
└─────────────────────────────────────────────────────────┘

┌─────────────────────────────────────────────────────────┐
│  [YELLOW]  U:**- proof.v  All L3   𝕋𝕊   (Coq)         │ ← Processing
└─────────────────────────────────────────────────────────┘

┌─────────────────────────────────────────────────────────┐
│  [GREEN]   U:--- proof.v  All L10  𝕋𝕊   (Coq)         │ ← Proved
└─────────────────────────────────────────────────────────┘

Lighter: 𝕋𝕊 = Transcendental Syntax

Installation

Via straight.el

(use-package transcendental-keyboard
  :straight (transcendental-keyboard
             :type git
             :host github
             :repo "plurigrid/asi"
             :files ("skills/transcendental-keyboard/*.el"))
  :config
  (setq trans-kb-gay-seed 1069)
  (setq trans-kb-color-mode t)
  (add-hook 'coq-mode-hook #'transcendental-keyboard-mode)
  (add-hook 'lean-mode-hook #'transcendental-keyboard-mode))

Manual

# Clone ASI repo
git clone https://github.com/plurigrid/asi ~/asi

# Add to init.el
(add-to-list 'load-path "~/asi/skills/transcendental-keyboard")
(require 'transcendental-keyboard)

Dependencies

# Proof General
git clone https://github.com/ProofGeneral/PG ~/.emacs.d/proof-general

# Narya
git clone https://github.com/mikeshulman/narya ~/narya
cd ~/narya && dune build

# Stellogen
git clone https://github.com/engboris/stellogen ~/stellogen
cd ~/stellogen && dune build

# Gay.jl (for Emacs integration)
git clone https://github.com/bmorphism/Gay.jl ~/Gay.jl
ln -s ~/i/gay.el ~/.emacs.d/gay.el

Example Workflow

1. Narya Higher-Dimensional Proof

-- File: bridge_example.ny

-- Define natural numbers
def Nat : Type := data [
  | zero : Nat
  | suc : Nat → Nat
]

-- Addition
def add : Nat → Nat → Nat := [
  | zero, n => n
  | suc m, n => suc (add m n)
]

-- Bridge between two addition orders
def add_comm (m n : Nat) : add m n ≡ add n m := {
  -- C-c C-a to auto-prove
  -- Mode-line: RED → YELLOW → GREEN
}

Keyboard sequence:

```
C-c t
```
→ Main menu
```
p
```
→ Proof menu
```
n
```
→ Step forward (mode-line: RED → YELLOW → GREEN)
```
C-c C-a
```
→ Auto-prove attempt

2. Stellogen Constellation

# File: nat_add.sg

spec nat =
  -i(z) ok;
  -i(s(X)) +i(X).

spec add =
  -add(z Y) +result(Y);
  -add(s(X) Y) +add(X s(Y)).

show process #input(s(s(z))). #add. &kill. end