hyperpolymath · hyperpolymath · Jun 28, 2026 · Jun 28, 2026
@@ -3,24 +3,29 @@
 # See: https://github.com/hyperpolymath/gv-clade-index
 
 [identity]
-uuid = "a5ea1382-a34c-5334-8a46-a2ebe904c810"
+# uuid: PROVISIONAL — deterministic UUIDv5 of the canonical forge URL
+# (uuid5(URL-namespace, "https://github.com/hyperpolymath/systemet")).
+# Reproducible, not invented; confirm/register the canonical id in gv-clade-index.
+uuid = "1ade549b-a47d-5204-b74e-7d1a3fc5f9d1"
 primary-forge = "github"
 primary-owner = "hyperpolymath"
-canonical-name = "rsr-template-repo"
-prefixed-name = "rm-rsr-template-repo"
+canonical-name = "systemet"
+prefixed-name = "et-systemet"
 
 [clade]
-primary = "rm"
-secondary = ["gv"]
-assigned = "2026-03-16"
-rationale = ""
+# PROVISIONAL clade codes — confirm/assign in gv-clade-index (the authority).
+# "et" = Equality Theory (owner-stated meaning of the name). Not yet registry-verified.
+primary = "et"
+secondary = []
+assigned = "2026-06-28"
+rationale = "et = Equality Theory; systemet is the theory itself (the spec/semantic authority). PROVISIONAL pending gv-clade-index registration."
 
 [forges]
-github = "hyperpolymath/rsr-template-repo"
-gitlab = "hyperpolymath/rsr-template-repo"
-bitbucket = "hyperpolymath/rsr-template-repo"
+github = "hyperpolymath/systemet"
+gitlab = "hyperpolymath/systemet"
+bitbucket = "hyperpolymath/systemet"
 
 [lineage]
 type = "standalone"
-parent = "RSR template — scaffold for new repos"
-born = "2026-03-16"
+parent = "Split out of the combined 'EveryType' draft (2026-06-28): systemet is the theory half; the kernel half is the anytype repo."
+born = "2026-06-28"
@@ -1,45 +1,31 @@
 # SPDX-License-Identifier: MPL-2.0
-# ECOSYSTEM.a2ml — Ecosystem position (META-TEMPLATE)
-#
-# This is the ECOSYSTEM file for rsr-template-repo itself. It records the
-# TEMPLATE's own position in the estate. When consumed by a new project,
-# replace these fields with the target project's ecosystem position and
-# related projects (see the NOTE FOR CONSUMERS at the bottom).
+# ECOSYSTEM.a2ml — Ecosystem position for systemet (Equality Theory).
 
 [metadata]
-project = "rsr-template-repo"
+project = "systemet"
 ecosystem = "hyperpolymath"
 
 [position]
-type = "repository-template"
-purpose = "Canonical RSR-compliant repository template: scaffolding (CI/CD, AI manifests, ABI/FFI standards, container ecosystem, governance) that new hyperpolymath projects are instantiated from."
+type = "type-theory-specification"
+purpose = "Equality Theory: a stratified type theory keeping one primitive relation (equality is conversion) at L1 and adding discipline in layers (L0 runtime · L1 equality · L2 graded resources · L3 guarded recursion · L4 effects); the semantic authority (spec, invariants, proof obligations) for the anytype kernel."
 # IS-NOT — anti-identity (the boundary-erosion guard; each line is a real past confusion)
 what-this-is-not = [
-  "a project in its own right",
-  "Scaffoldia (the full-featured repo designer)",
-  "standards (the canon source this template operationalises)",
+  "the kernel or implementation (that is the anytype repo)",
+  "a compiler or checker (no runnable code lives here)",
+  "AffineScript (a downstream product profile of the kernel)",
+  "EveryType (the over-claiming former name that conflated theory + kernel + profile)",
 ]
 
 [pipeline]
-position = "foundation"
-chain = "standards → rsr-template-repo → (every estate repo)"
-notes = "rsr-template-repo turns the RSR standard into runnable scaffolding. New repos are created from it via `just init`, which substitutes the {{PLACEHOLDER}} tokens."
+position = "theory"
+chain = "systemet (theory) → anytype (kernel) → AffineScript (profile)"
+notes = "systemet owns the semantics; anytype is the reference implementation and must pin systemet upstream and extend-not-redefine it; AffineScript is grade=affine+cost on the anytype kernel."
 coordination = "standards"
 
 [related-projects]
 projects = [
-  { name = "standards", relationship = "standard-source", notes = "Defines the RSR standard, contractile canon, and policies that this template operationalises." },
-  { name = "stapeln", relationship = "build-tooling", notes = "Layer-based container build system; the template ships stapeln.toml scaffolding." },
-  { name = "selur-compose", relationship = "build-tooling", notes = "Service composition; the template ships selur-compose.toml scaffolding." },
-  { name = "k9-svc", relationship = "validation-tooling", notes = "Runs the self-validating k9.ncl checks (.machine_readable/self-validating/)." },
-  { name = "cerro-torre", relationship = "signing-tooling", notes = "Container/image signing provider referenced by the container scaffolding." },
-  { name = "svalinn", relationship = "verification-tooling", notes = "Supply-chain verification referenced by the container scaffolding." },
-  { name = "vordr", relationship = "verification-tooling", notes = "Build/artifact verification referenced by the container scaffolding." },
+  { name = "anytype", relationship = "reference-implementation", notes = "The kernel that implements this theory. Pins systemet upstream as semantic authority." },
+  { name = "AffineScript", relationship = "downstream-profile", notes = "One product profile (grade = affine + cost) built on the anytype kernel." },
+  { name = "standards", relationship = "standard-source", notes = "Defines the RSR standard, contractile canon, and policies this repo operationalises." },
+  { name = "proven", relationship = "verification-tooling", notes = "Idris2/proof tooling referenced for discharging systemet's proof obligations." },
 ]
-
-# ---------------------------------------------------------------------------
-# NOTE FOR CONSUMERS: When using this template to create a new repo, replace
-# the project/purpose above and rewrite [related-projects] to describe YOUR
-# project's actual ecosystem. The entries above describe the TEMPLATE's own
-# position, not yours.
-# ---------------------------------------------------------------------------
@@ -6,17 +6,23 @@
 
 [metadata]
 version = "0.1.0"
-last-updated = "2026-04-11"
+last-updated = "2026-06-28"
 
 [project-info]
-type = "library"  # TODO: update type (library|binary|service|website|monorepo)  # library | binary | monorepo | service | website
-languages = []             # e.g. ["rust", "zig", "idris2"]
+type = "specification"     # systemet is a type-theory specification, not a binary/service
+languages = ["idris2", "agda", "coq", "lean4", "tlaplus"]   # provers for the proof obligations
 license = "MPL-2.0"
 author = "Jonathan D.A. Jewell (hyperpolymath)"
 
 [architecture-decisions]
 # ADR format: status = proposed | accepted | deprecated | superseded | rejected
-# - { id = "ADR-001", title = "Use Zig for FFI", status = "accepted", date = "2026-02-14" }
+adrs = [
+  { id = "ADR-001", title = "Equality is conversion at L1 (no coercion calculus, no roles)", status = "accepted", date = "2026-06-28" },
+  { id = "ADR-002", title = "Discipline lives in layers over a pluggable L2 grade algebra, not in new type relations", status = "accepted", date = "2026-06-28" },
+  { id = "ADR-003", title = "Roles are replaced by local finite trope machines (A@t1 -> A@t2)", status = "accepted", date = "2026-06-28" },
+  { id = "ADR-004", title = "Split the combined 'EveryType' draft: theory -> systemet, kernel -> anytype", status = "accepted", date = "2026-06-28" },
+  { id = "ADR-005", title = "TEA-erasure (L4) is an OPEN proof obligation, not a claimed result", status = "accepted", date = "2026-06-28" },
+]
 
 [development-practices]
 build-tool = "just"

@@ -1,49 +1,42 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# STATE.a2ml — Project state checkpoint (META-TEMPLATE)
-#
-# This is the STATE file for rsr-template-repo itself.
-# When consumed by a new project, replace {{PLACEHOLDER}} tokens
-# and customize sections below for the target project.
+# STATE.a2ml — Project state checkpoint for systemet (Equality Theory).
 
 [metadata]
-project = "rsr-template-repo"
-version = "0.2.0"
-last-updated = "2026-02-28"
+project = "systemet"
+version = "0.1.0"
+last-updated = "2026-06-28"
 status = "active"  # active | paused | archived
 
 [project-context]
-name = "rsr-template-repo"
-purpose = "Canonical RSR-compliant repository template providing scaffolding for all hyperpolymath projects — including CI/CD, AI manifests, ABI/FFI standards, container ecosystem, and governance infrastructure."
-completion-percentage = 95
+name = "systemet"
+purpose = "Equality Theory — the stratified type theory (L1 equality-is-conversion cut, three refusal gates, roles-as-tropes, TEA-erasure obligation) that the anytype kernel implements."
+completion-percentage = 15
 
 [position]
-phase = "maintenance"      # design | implementation | testing | maintenance | archived
-maturity = "production"    # experimental | alpha | beta | production | lts
+phase = "design"           # design | implementation | testing | maintenance | archived
+maturity = "experimental"  # experimental | alpha | beta | production | lts
 
 [route-to-mvp]
 milestones = [
-  { name = "Phase 0: Core scaffolding (justfile, CI/CD, .machine_readable)", completion = 100 },
-  { name = "Phase 1: ABI/FFI standard (Idris2/Zig templates)", completion = 100 },
-  { name = "Phase 1b: AI Gatekeeper Protocol (0-AI-MANIFEST.a2ml)", completion = 100 },
-  { name = "Phase 1c: TOPOLOGY.md standard and guide", completion = 100 },
-  { name = "Phase 1d: Maintenance gate (axes, checklist, approach)", completion = 100 },
-  { name = "Phase 1e: Trustfile / contractiles", completion = 100 },
-  { name = "Phase 2: Container ecosystem templates (stapeln)", completion = 100 },
-  { name = "Phase 3: Multi-forge sync hardening", completion = 0 },
-  { name = "Phase 4: Guix reproducible shells", completion = 50 },
+  { name = "Phase 0: Split theory out of the EveryType draft; instantiate RSR repo", completion = 100 },
+  { name = "Phase 1: Specify the five layers and the three gates in prose", completion = 90 },
+  { name = "Phase 2: Formal spec of L1 (equality = conversion) + totality obligation", completion = 0 },
+  { name = "Phase 3: L2 grade-algebra laws stated precisely enough to check a candidate", completion = 0 },
+  { name = "Phase 4: Trope-preservation statement and per-API obligations", completion = 0 },
+  { name = "Phase 5 (OPEN-A): Formal TEA-erasure proof", completion = 0 },
 ]
 
 [blockers-and-issues]
-# No active blockers
+# No external blockers. Proofs are unstarted, not blocked.
 
 [critical-next-actions]
 actions = [
-  "Container templates complete — test with `just container-init`",
-  "Validate container templates across wolfi-base and static Chainguard images",
-  "Harden multi-forge sync for GitLab/Bitbucket mirroring edge cases",
-  "Expand Guix development shell templates",
+  "Write a precise L1 specification (conversion-as-equality) and name the totality assumption.",
+  "State the L2 grade-algebra laws (semiring + ordering) a candidate grade must satisfy.",
+  "Formalise the trope-preservation obligation; pick one real API as a worked finite machine.",
+  "Keep README/EXPLAINME claims inside what is proven; TEA-erasure stays 'OPEN' until proved.",
 ]
 
 [maintenance-status]
@@ -54,11 +47,6 @@ open-warnings = 0
 open-failures = 0
 
 [ecosystem]
-part-of = ["RSR Framework", "stapeln ecosystem"]
-depends-on = ["stapeln", "selur-compose", "cerro-torre", "svalinn", "vordr", "k9-svc"]
-
-# ---------------------------------------------------------------------------
-# NOTE FOR CONSUMERS: When using this template to create a new repo, reset
-# the fields above to your project's values and replace all {{PLACEHOLDER}}
-# tokens. The milestones above describe the TEMPLATE's evolution, not yours.
-# ---------------------------------------------------------------------------
+part-of = ["hyperpolymath estate"]
+depends-on = []
+implemented-by = ["anytype"]
@@ -1,41 +1,41 @@
 # SPDX-License-Identifier: MPL-2.0
-# Copyright (c) {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}>
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # ANCHOR.a2ml - authoritative anchor for this repository
 
 [metadata]
 version = "1.0.0"
-last-updated = "{{CURRENT_DATE}}"
+last-updated = "2026-06-28"
 
 [anchor]
 schema = "hyperpolymath.anchor/1"
-repo = "{{OWNER}}/{{REPO}}"
+repo = "hyperpolymath/systemet"
 authority = "upstream-canonical"
 
 purpose = [
-  "Define canonical semantics and policy boundaries for this repository.",
-  "Declare what downstream/satellite repos can extend but not redefine.",
+  "Define the canonical semantics of Equality Theory for the estate.",
+  "Declare what downstream (the anytype kernel, AffineScript) may extend but not redefine.",
   "Provide a stable golden path and invariant contract for release readiness.",
 ]
 
 [identity]
-project = "{{PROJECT_NAME}}"
-kind = "{{PROJECT_KIND}}"                # language | library | service | tool
-one-sentence = "{{PROJECT_PURPOSE}}"
-domain = "{{PROJECT_DOMAIN}}"
+project = "systemet"
+kind = "type-theory"                      # the theory/spec; downstream kernel is a 'tool'
+one-sentence = "Equality Theory: one primitive relation (equality is conversion) at the bottom, discipline added in layers, not new relations added sideways."
+domain = "programming-language theory / type theory"
 
 [semantic-authority]
 policy = "canonical"
 
 owns = [
-  "Project semantics and specification",
-  "Invariant definitions and contractiles",
-  "Reference implementation behavior",
+  "Equality Theory semantics and specification (the five layers, the three gates, the wager)",
+  "Invariant definitions and proof obligations (L1 totality, structural soundness, polarity/blame, trope preservation, TEA erasure)",
+  "The boundary of what downstream may extend vs. redefine",
 ]
 
 [implementation-policy]
-allowed = ["Rust", "Idris2", "Zig", "Scheme", "Shell", "Just", "AsciiDoc", "Markdown"]
-forbidden = ["Node.js", "npm"]
+allowed = ["Idris2", "Agda", "Coq", "Lean4", "TLAplus", "Scheme", "Shell", "Just", "AsciiDoc"]
+forbidden = ["Node.js", "npm", "TypeScript", "Python", "Go"]
 
 [golden-path]
 smoke-test-command = [
@@ -50,13 +50,15 @@ success-criteria = [
 ]
 
 [satellite-policy]
+# The anytype kernel is a satellite of this theory.
 must-pin-upstream = true
 must-declare-authority = true
 must-have-anchor = true
 must-have-golden-path = true
 
 [semantic-authority-files]
-language-spec = "SPECIFICATION.md"
-formal-proofs = "docs/proofs/PROOFS.adoc"
+# Intended locations for the formal artefacts (forward references — not yet populated).
+language-spec = "docs/theory/SPECIFICATION.adoc"
+formal-proofs = "verification/proofs/"
 type-theory = "docs/theory/THEORY.adoc"
 algorithms = "docs/theory/ALGORITHMS.adoc"
@@ -5,11 +5,11 @@
 #
 [metadata]
 version = "0.1.0"
-last-updated = "{{CURRENT_DATE}}"
+last-updated = "2026-06-28"
 
 [project]
-name = "[YOUR-REPO-NAME]"
-purpose = "{{PROJECT_DESCRIPTION}}"
+name = "systemet"
+purpose = "Equality Theory — the stratified type theory (equality is conversion at L1; discipline in layers) that the anytype kernel implements. This repo is the semantic authority; it carries the spec and proof obligations, not a compiler."
 
 [ai-allocation]
 agents = [