Ordered Locale Skill Skill

Ordered Locale Skill

Trit: +1 (PLUS/GENERATOR) GF(3): Σ(-1,0,+1) = 0 (conserved)

Overview

Point-free topology with direction. MCP servers indexed by creation-time color via SplitMix64. Every decision trifurcates into MINUS/ERGODIC/PLUS parallel paths. GF(3) conservation guaranteed on every substrate in every interaction.

Implements Heunen-style ordered locales with observational bridge types in Narya proof assistant. Bridge types model the "way below" relation U ≪ V in ordered locales, providing a foundation for:

MCP Locale: Servers as opens, dependencies as way-below
Causal structure in topological spaces
Directed homotopy theory
Sheaves respecting directional constraints
GF(3) triadic systems

Files

| File | Description | |------|-------------| | mcp_locale.py | Python: MCP ordered locale with triadic decisions | | mcp_locale.mo | Modelica: Acausal model (replaces Wolfram) | | narya/ordered_locale.ny | Core definitions: 𝟚, Bridge, WayBelow, frame ops | | narya/gf3.ny | GF(3) arithmetic and conservation | | narya/bridge_sheaf.ny | Sheaves respecting bridge structure | | narya/narya-ordered-locale.el | Emacs/Proof General integration | | ordered_locale.jl | Julia: Frame operations, cones/cocones |

MCP Locale

Every MCP server is an open set in the locale, indexed by creation-time color:

from mcp_locale import create_mcp_locale, trifurcate_decision

locale = create_mcp_locale(seed=0x42D)
# Each MCP gets deterministic color: seed → SplitMix64 → RGB → hue → trit

Triadic Decisions

Every decision trifurcates into parallel paths:

| Path | Trit | Role | Action | |------|------|------|--------| | MINUS | -1 | Validator | Check constraints | | ERGODIC | 0 | Coordinator | Find optimal route | | PLUS | +1 | Executor | Generate result |

decision = trifurcate_decision(
    "swap 10 APT",
    seed=0x42D,
    minus_fn=validate,
    ergodic_fn=coordinate,
    plus_fn=execute,
    aggregate_fn=aggregate
)
# GF(3): -1 + 0 + 1 = 0 ✓

Safe Parallelism via SplitMix64

def splitmix_ternary(seed):
    """Fork into 3 independent streams."""
    s1 = splitmix64(seed)
    s2 = splitmix64(s1)
    s3 = splitmix64(s2)
    return (s1, s2, s3)  # MINUS, ERGODIC, PLUS

Each substrate (Python, Julia, Babashka, Modelica) uses identical SplitMix64, ensuring reproducible parallel execution.

Key Concepts

Bridge Types

A bridge from A to B is a directed path through the directed interval 𝟚:

def Bridge (A B : Type) : Type := sig (
  path : 𝟚 → Type,
  start : path zero. → A,
  end : B → path one.
)

Way Below (≪)

The way-below relation U ≪ V captures "U is compact relative to V":

def WayBelow (U V : Open) : Type := sig (
  bridge : (t : 𝟚) → Open,
  at_zero : ... → U,
  at_one : V → ...,
  directed : ...
)

GF(3) Conservation

All triadic structures conserve sum ≡ 0 (mod 3):

def GF3Conserved (a b c : Trit) : Type := 
  Id Trit (trit_sum3 a b c) ergodic.

Commands

# Verify all files
~/.agents/skills/ordered-locale/narya/run_narya.sh

# Check GF(3) only
~/.agents/skills/ordered-locale/narya/run_narya.sh --gf3

# Run via headless Emacs
~/.agents/skills/ordered-locale/narya/run_narya.sh --emacs

Emacs Integration

;; Load the mode
(load "~/.agents/skills/ordered-locale/narya/narya-ordered-locale.el")

;; Key bindings
;; C-c C-n  Step forward
;; C-c C-u  Step backward
;; C-c C-v  Verify all
;; C-c C-g  Check GF(3)

Related Skills

proofgeneral-narya - Proof General + Narya integration
gf3 / gay-mcp - Triadic color systems
segal-types - Synthetic ∞-categories
unworld - Derivational chains
triad-interleave - Parallel triadic scheduling
coequalizers (0) - Sheaf gluing as dual of coequalizer

References

Heunen, C. - "Ordered Locales" (in ~/worlds/ordered-locales/heunen_orderedlocales.pdf)
Riehl-Shulman - "A type theory for synthetic ∞-categories"
Narya proof assistant - https://github.com/gwaithimirdain/narya

Mathematical Foundation

Ordered locales extend frame theory with a compatible partial order on opens. The key axiom is:

Every open V is the join of opens U with U ≪ V

This approximation property connects point-free topology to domain theory and provides a constructive foundation for causal structure.

The bridge type formalization captures ≪ as a directed homotopy: paths that flow from U toward V through the directed interval 𝟚 = {0 → 1}.

Scientific Skill Interleaving

This skill connects to the K-Dense-AI/claude-scientific-skills ecosystem:

Graph Theory

networkx [○] via bicomodule
- Universal graph hub

Bibliography References

general: 734 citations in bib.duckdb

Cat# Integration

This 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

GF(3) Naturality

The skill participates in triads satisfying:

(-1) + (0) + (+1) ≡ 0 (mod 3)

This ensures compositional coherence in the Cat# equipment structure.

Agent Skills: Ordered Locale Skill

Install this agent skill to your local

Skill Files