plurigrid ProofGeneral + Narya Skill
"Observational type theory: where equality is what you can observe, not what you can prove."
Overview
This skill combines:
- Proof General (543⭐): The universal Emacs interface for proof assistants
- Narya (225⭐): Higher-dimensional type theory proof assistant
Proof General Basics
;; 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 Bindings
| 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 |
Proof State Visualization
┌─────────────────────────────────────────────────────────────┐
│ ████████████████████░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░ │
│ ▲ Locked (proven) ▲ Processing ▲ Unprocessed │
│ │
│ GF(3) Trit Mapping: │
│ Locked → +1 (LIVE) → Red #FF0000 │
│ Processing → 0 (VERIFY) → Green #00FF00 │
│ Unprocessed → -1 (BACKFILL) → Blue #0000FF │
└─────────────────────────────────────────────────────────────┘
Narya: Higher-Dimensional Type Theory
Narya is a proof assistant for higher observational type theory (HOTT).
Key Features
- Observational Equality: Bridge types computed inductively from type structure
- Higher Dimensions: Support for 2-cells, 3-cells, etc.
- No Interval Type: Unlike cubical type theory, no explicit interval
Narya Syntax
-- 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
Observational Bridge Types (gay.el integration)
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)))
Hierarchical Agent Structure: 3×3×3 = 27
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)
Bruhat-Tits Tree Navigation
;; 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))))
Möbius Inversion for Trajectory Analysis
;; 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)
Bumpus Laxity Measures
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))))
Version Control Operations
| 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 |
Xenomodern Stance
The ironic detachment here is recognizing that:
- Proof assistants are version control systems for mathematical truth
- Type theory is a programming language for proofs
- Observational equality is more practical than definitional equality
- Higher dimensions emerge naturally from conflict resolution
Commands
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