Alex Flom afflom

UOR Global Non-Adjacent Form (UOR-GNAF) v1

Status: Normative Draft 0.2
Provisional specification identifier: uor-gnaf/1-draft.2
Reserved stable identifier: uor-gnaf/1 — unassigned
Date: 2026-08-11

Abstract

UOR-GNAF specifies a machine process for accumulating typed content, kinds,

UOR Non-Adjacent Form (UOR-NAF) v1

Status: normative draft 0.6
Provisional spec identifier: uor-naf/1-draft.6
Reserved stable identifier: uor-naf/1 (unassigned; freeze governed by section 14)
Execution design identifier: uor-naf-plan/1-draft.6 (no registered wire)
Reserved execution identifier: uor-naf-plan/1 (unassigned)
Scope: exact integers and tensors, UOR Atlas address words, typed canonical states/operators, and a correct-and-optimal execution contract

1. Purpose

TF1 — Formalization of the Transformer over the UOR Atlas

GENERATED ARTIFACT. The source of truth is a typed registry; this file is its output. A claim's class is the type produced by discharging its proof, not a word written here. Every proof and definition below appears in full: the emitter cannot abbreviate an argument or point elsewhere for it, because the argument is a required field of the proof type. Hand edits are overwritten.

1. Definitions

UOR and Hologram: Do the Work Once

Compute less. Store less. Move less. Get the same answer everywhere, exactly.

The problem

Every large system your organization runs is a network: neural networks serving AI models, communications and transport networks moving data and goods, power grids, supply chains, sensor meshes, simulation models. Different domains, same shape: many connected parts, many paths through them, many states to track.

And they all waste resources the same way. As a network computation runs, it reaches the same intermediate results over and over by different routes, and it computes, stores, and transmits each arrival as if it were new. The redundancy grows with the size of the network. Most of the cycles, memory, and bandwidth spent on large workloads are spent rediscovering things the system already knew.

	module
	public import Init
	public import LexLeanMatmul.Core
	set_option autoImplicit false
	set_option maxRecDepth 100000
	set_option maxHeartbeats 1000000000
	namespace LexLeanMatmul.Atlas

	namespace LexLeanRuntime

	module
	public import Init
	public import LexLeanMatmul.Codec
	public import LexLeanMatmul.Core
	public import LexLeanMatmul.ExtendedProtocol
	public import LexLeanMatmul.Float
	public import LexLeanMatmul.Model
	public import LexLeanMatmul.Protocol
	set_option autoImplicit false
	set_option maxRecDepth 100000

	/-!
	# Exact Chaotic Systems in UOR — The Driftless Torus

	This file formalizes a chaotic dynamical system under the UOR paradigm, in the
	same proof style as the UOR matmul file (`UorMatMul.lean`): first pin the exact
	semantics, then prove codec-invariance as a congruence over the pinned
	semantics, and finally prove the exact closure / bijection / hyperbolicity
	facts that make the prose claim mathematical rather than heuristic. It follows
	the uor-addr / F1 Lean discipline: core Lean 4 v4.16.0, no Mathlib, no `sorry`,
	proofs by `decide` / `omega` / `rfl` / rewriting (`rw`, `rwa`, `calc`) plus

	/-!
	# MatMul in UOR — Codec-Invariance of the Exact Accumulation

	This file formalizes what "matmul in UOR" means, grounded in the runtime that
	first exhibited it (hologram `matmul_e8cb_omajor` / W8A8 / W4A8, v0.7.2) and in
	the uor-addr / F1 Lean discipline (Lean 4 v4.16.0, no Mathlib; proofs by
	`decide` / `omega` / `rfl` / rewriting (`rw`, `simp`, `calc`) plus structural
	induction and case analysis, and no `funext`; axiom base
	`{propext, Quot.sound}`).

	#!/usr/bin/env python3
	"""
	UOR Framework

	A computation engine that IS the specification.
	The JSON-LD output is proof of verified computation.

	Scales from Quantum 0 (8-bit) to arbitrary Quantum N (8×(N+1) bits).

	- T = 3 (triadic coordinates: datum, stratum, spectrum)

	{
	"@context": {
	"@base": "https://uor.foundation/categorical-x/v1/",
	"@vocab": "https://uor.foundation/categorical-x/v1#",
	"AlgebraicProperty": "cx:AlgebraicProperty",
	"ApproximateNumber": "cx:ApproximateNumber",
	"ArbitraryPrecisionContext": "cx:ArbitraryPrecisionContext",
	"AssertionStatus": "cx:AssertionStatus",
	"AutomorphismGroup": "cx:AutomorphismGroup",
	"Axiom": "cx:Axiom",