From asi
Guides Emacs setup, key bindings, and usage of Proof General with Narya for higher-dimensional observational type theory proofs and version control via bridge types.
npx claudepluginhub plurigrid/asi --plugin asiThis skill uses the workspace's default tool permissions.
> *"Observational type theory: where equality is what you can observe, not what you can prove."*
Guides use of Narya Hatchery proof assistant for higher-dimensional observational type theory with Id/Bridge types, parametricity, normalization-by-evaluation, typed holes, and ProofGeneral integration.
Assists with Lean 4 theorem proving: editing .lean files, debugging builds (type mismatches, sorries, axioms, lake errors), searching mathlib lemmas, formalizing mathematics, and learning concepts via commands like /lean4:prove and /lean4:formalize.
Orchestrates collaborative theorem proving in Lean using lc CLI for state management and parallel agents. Employs skeleton verification, math cards, and architecture planning for complex goals.
Share bugs, ideas, or general feedback.
"Observational type theory: where equality is what you can observe, not what you can prove."
"universal topos construction for social cognition and democratization of mathematical approach to problem-solving to all" — Plurigrid: the story thus far
Active Inference via String Diagrams: Narya's observational bridge types connect to the Active Inference in String Diagrams framework where perception and action form bidirectional loops. The bridge types implement:
Narya Reference (from hatchery-papers):
This skill combines:
;; Install via straight.el or package.el
(use-package proof-general
:mode ("\\.v\\'" . coq-mode)
:config
(setq proof-splash-enable nil
proof-three-window-mode-policy 'hybrid))
| Key | Action | Description |
|---|---|---|
C-c C-n | proof-assert-next-command-interactive | Step forward |
C-c C-u | proof-undo-last-successful-command | Step backward |
C-c C-RET | proof-goto-point | Process to cursor |
C-c C-b | proof-process-buffer | Process entire buffer |
C-c C-. | proof-goto-end-of-locked | Jump to locked region end |
┌─────────────────────────────────────────────────────────────┐
│ ████████████████████░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░ │
│ ▲ Locked (proven) ▲ Processing ▲ Unprocessed │
│ │
│ GF(3) Trit Mapping: │
│ Locked → +1 (LIVE) → Red #FF0000 │
│ Processing → 0 (VERIFY) → Green #00FF00 │
│ Unprocessed → -1 (BACKFILL) → Blue #0000FF │
└─────────────────────────────────────────────────────────────┘
Narya is a proof assistant for higher observational type theory (HOTT).
-- Define a type
def Nat : Type := data [
| zero : Nat
| suc : Nat → Nat
]
-- Bridge type between values
def bridge (A : Type) (x y : A) : Type := x ≡ y
-- Transport along bridge
def transport (A : Type) (P : A → Type) (x y : A) (p : x ≡ y) : P x → P y
:= λ px. subst P p px
From narya_observational_bridge.el:
(cl-defstruct (obs-bridge (:constructor obs-bridge-create))
"An observational bridge type connecting two versions."
source ; Source object
target ; Target object
bridge ; The diff/relation between them
dimension ; 0 = value, 1 = diff, 2 = conflict resolution
tap-state ; TAP state: -1 BACKFILL, 0 VERIFY, +1 LIVE
color ; Gay.jl color
fingerprint) ; Content hash
;; Create diff as bridge type
(defun obs-bridge-diff (source target seed)
"Create an observational bridge (diff) from SOURCE to TARGET."
(let* ((source-hash (sxhash source))
(target-hash (sxhash target))
(bridge-hash (logxor source-hash target-hash))
(index (mod bridge-hash 1000))
(color (gay/color-at seed index)))
(obs-bridge-create
:source source
:target target
:bridge (list :from source-hash :to target-hash)
:dimension 1
:color color)))
Level 0: Root (VERIFY)
│
├── Level 1: BACKFILL (-1) ─── L2: [-1, 0, +1] ─── L3: 3×3 = 9 agents
├── Level 1: VERIFY (0) ─── L2: [-1, 0, +1] ─── L3: 3×3 = 9 agents
└── Level 1: LIVE (+1) ─── L2: [-1, 0, +1] ─── L3: 3×3 = 9 agents
Total: 1 + 3 + 9 + 27 = 40 agents (or 27 leaves)
;; Navigate the Z_3 gamut poset
(defun bt-node-child (node branch)
"Return child of NODE at BRANCH (0, 1, or 2)."
(bt-node (append (bt-node-path node) (list branch))))
(defun bt-node-distance (node1 node2)
"Return tree distance between NODE1 and NODE2."
(let* ((lca (bt-node-lca-depth node1 node2))
(d1 (bt-node-depth node1))
(d2 (bt-node-depth node2)))
(+ (- d1 lca) (- d2 lca))))
;; Map TAP trajectory to multiplicative structure
;; -1 → 2, 0 → 3, +1 → 5 (first three primes)
(defun moebius/trajectory-to-multiplicative (trajectory)
(let ((result 1))
(dolist (t trajectory)
(setq result (* result
(pcase t
(-1 2)
(0 3)
(+1 5)))))
result))
;; μ(n) ≠ 0 ⟹ square-free trajectory (no redundancy)
For coherence between proof states:
(defun bumpus/compute-laxity (agent1 agent2)
"Laxity = 0 means strict functor (perfect coherence).
Laxity = 1 means maximally lax."
(let* ((d (bt-node-distance (narya-agent-bt-node agent1)
(narya-agent-bt-node agent2)))
(mu1 (narya-agent-moebius-mu agent1))
(mu2 (narya-agent-moebius-mu agent2))
(mu-diff (abs (- mu1 mu2))))
(min 1.0 (/ (+ d (* 0.5 mu-diff)) 10.0))))
| Operation | Description | Dimension |
|---|---|---|
fork | Create 3 branches (balanced ternary) | 0 → 1 |
continue | Choose branch (-1, 0, +1) | 1 → 1 |
merge | Resolve conflict (2D cubical) | 1 → 2 |
The ironic detachment here is recognizing that:
just narya-demo # Run Narya bridge demonstration
just proofgeneral-setup # Configure Proof General
just spawn-hierarchy # Create 27-agent hierarchy
just measure-laxity # Compute Bumpus laxity metrics
This skill connects to the K-Dense-AI/claude-scientific-skills ecosystem:
cryptography: 1 citations in bib.duckdbThis skill maps to Cat# = Comod(P) as a bicomodule in the equipment structure:
Trit: 0 (ERGODIC)
Home: Prof
Poly Op: ⊗
Kan Role: Adj
Color: #26D826
The skill participates in triads satisfying:
(-1) + (0) + (+1) ≡ 0 (mod 3)
This ensures compositional coherence in the Cat# equipment structure.