From 3da894343bc01d7bb5967cdfc9e1323b1087f22c Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 28 Jun 2026 10:30:52 +0000 Subject: [PATCH] Instantiate as systemet (Equality Theory); receive theory split from anytype MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Turn this repo from a raw RSR template into systemet — Equality Theory ("system" + "ET"). It is the theory half of the split out of the combined "EveryType" draft: one primitive relation (equality is conversion) at L1, discipline added in layers, the three refusal gates, roles-as-tropes, and TEA-erasure as an open proof obligation. The kernel that implements it is the anytype repo; this repo is the semantic authority. - README/EXPLAINME authored for the theory (the five layers, the L1 cut, the three gates, the wager, the proof obligations), replacing the {{PLACEHOLDER}} template prose. - AFFIRMATION instantiated honestly: theory is specified, proofs are OPEN, no compiler lives here, TEA-erasure is not a result. - Identity descriptiles instantiated: CLADE/ECOSYSTEM/ANCHOR/STATE/META, 0-AI-MANIFEST, CITATION. ANCHOR declares systemet canonical (semantic authority); downstream may extend-not-redefine. - CLAUDE.md regenerated from the descriptiles via the arrival-pack projection (extract.sh + faithful render of arrival-pack.ncl; nickel/just unavailable here). Diff is the identity block + provenance hashes only — drift-safe. uuid is a PROVISIONAL deterministic UUIDv5 of the forge URL; clade is PROVISIONAL ("et" = Equality Theory, owner-stated) — both must be confirmed/ registered in gv-clade-index. The generic RSR {{TOKEN}} scaffolding (shared with the template) is intentionally left for `just init`: it collides with Just's own {{var}} syntax and needs owner-only values. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01J1XmMC49T8sZ3uUuvrgB7y --- .machine_readable/6a2/CLADE.a2ml | 29 +- .machine_readable/6a2/ECOSYSTEM.a2ml | 44 +-- .machine_readable/6a2/META.a2ml | 14 +- .machine_readable/6a2/STATE.a2ml | 58 ++-- .machine_readable/6a2/anchors/ANCHOR.a2ml | 34 +-- 0-AI-MANIFEST.a2ml | 6 +- AFFIRMATION.adoc | 103 +++---- CHANGELOG.md | 21 ++ CITATION.cff | 21 +- CLAUDE.md | 16 +- EXPLAINME.adoc | 201 +++++++++----- README.adoc | 321 +++++++++++++++++----- 12 files changed, 546 insertions(+), 322 deletions(-) diff --git a/.machine_readable/6a2/CLADE.a2ml b/.machine_readable/6a2/CLADE.a2ml index b14389c..67de495 100644 --- a/.machine_readable/6a2/CLADE.a2ml +++ b/.machine_readable/6a2/CLADE.a2ml @@ -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" diff --git a/.machine_readable/6a2/ECOSYSTEM.a2ml b/.machine_readable/6a2/ECOSYSTEM.a2ml index 0757418..14dc337 100644 --- a/.machine_readable/6a2/ECOSYSTEM.a2ml +++ b/.machine_readable/6a2/ECOSYSTEM.a2ml @@ -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. -# --------------------------------------------------------------------------- diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml index d66fb7b..593ef67 100644 --- a/.machine_readable/6a2/META.a2ml +++ b/.machine_readable/6a2/META.a2ml @@ -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" diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 3d2d647..b783caf 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -1,49 +1,42 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # -# 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"] diff --git a/.machine_readable/6a2/anchors/ANCHOR.a2ml b/.machine_readable/6a2/anchors/ANCHOR.a2ml index 8723899..88b9a86 100644 --- a/.machine_readable/6a2/anchors/ANCHOR.a2ml +++ b/.machine_readable/6a2/anchors/ANCHOR.a2ml @@ -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) # # 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" diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 68aad8c..1617ffd 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -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 = [ diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 3a840b4..525fa3a 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -1,94 +1,67 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -= AFFIRMATION — {{PROJECT_NAME}}, as of += AFFIRMATION — systemet, as of :toc: macro :toclevels: 2 _the No-Bullshit file: what we affirm was true and checkable at this moment._ -[NOTE] -==== -*This file is a template.* Replace the `{{…}}` placeholders and the `<…>` anchor -fields, then re-run your project's own checks in the same session before signing. - -An *affirmation* is a solemn declaration of the truth of a statement, made by -someone who _declines to swear an oath_ — our truth-as-best-believed at a stamped -instant, binding on our honesty, not a claim of infallibility. It is the third of -the README / EXPLAINME / AFFIRMATION trio: - -[cols="1,3,2",options="header"] -|=== -| File | Answers | Tense -| `README.adoc` | _Where is this going, and why?_ — steering, intent, vision | future / aspirational -| `EXPLAINME.adoc` | _How is it built, and what's the evidence?_ — engineering | descriptive / mechanism -| *`AFFIRMATION.adoc`* (this file) | _What can we honestly affirm was *true and checkable* at a stamped moment?_ | a frozen instant, falsifiable -|=== -==== - toc::[] -== What this is, and how it works - -*What it is.* A short, dated, signed snapshot of what {{OWNER}} can honestly and -verifiably claim about *{{PROJECT_NAME}}* at one exact commit. Nothing here is -marketing and nothing is a promise about the future — those live in the README. -This file is the receipt. +== What this is -*How it stays trustworthy.* Three moving parts: +A short, dated, signed snapshot of what can be honestly and verifiably claimed +about *systemet* (Equality Theory) at one exact commit. The README is the vision; +`EXPLAINME.adoc` is the mechanism; this file is the receipt. It is our best honest +belief at a stamped instant, binding on our honesty, not a claim of infallibility. -. *Ground truth, not memory.* Every claim below must be produced by _running the - project's own checks_ in the session that writes this file (build, tests, - typecheck, `just audit`). Where a status doc, the `Justfile`, or memory says - otherwise, the live run wins and the contradiction is flagged here. -. *A frozen anchor.* The file names the exact commit SHA, branch, UTC timestamp, - and toolchain (see <>), so "true" always means "true _at - this point_". Move the SHA and this file is a draft until it is re-run. -. *A real signature.* It is landed by a *signed git commit*; that signature over - this content at the anchored SHA is what makes the affirmation tamper-evident - and attributable — not the prose alone. - -*We are fallible.* This is our best honest belief, not a proof of its own -correctness. Treat it as a falsifiable claim, not gospel. - -== The epistemic contract (read this before you trust _or_ attack) - -This document records {{OWNER}}'s *best belief* at the timestamp below. It is -*not a guarantee of correctness.* The only guarantee is *no intentional -overclaim*: where something is proven we say "proven"; where it is a documented -trust boundary, an experiment, or an unwired module, we say so; where a claim is -the README's aspiration rather than a checked result, we say so. An honest claim -that later turns out false is an *error to be fixed* — not a lie. - -*Standing invitation to refute.* You are invited to bulldoze any claim in this -file. Bring a counter-example, a failing run, or a contradicting source. +[NOTE] +==== +The anchor below carries `<…>` fields (commit SHA, timestamp, toolchain) that are +filled in *at signing time*, in the same session that runs the checks. Until then +this file is a draft. +==== -== What we affirm (fill in — delete the examples) +== What we affirm -[cols="2,1,3",options="header"] +[cols="3,1,3",options="header"] |=== -| Claim | Status | Evidence (command / `file:line`) -| _e.g. The library builds clean_ | affirmed | `just build` at the anchor SHA -| _e.g. The ABI seam typechecks_ | affirmed | `idris2 --typecheck abi.ipkg` -| _e.g. Feature X is complete_ | aspiration | README §… (not yet checked) +| Claim | Status | Evidence +| The repository is RSR-shaped and validates | affirmed-pending-run | `just validate` at the anchor SHA +| Equality Theory is *specified* (five layers, three gates, the wager) | affirmed | `README.adoc`, `EXPLAINME.adoc` +| The theory is the semantic authority; `anytype` is the implementation | affirmed | `.machine_readable/6a2/anchors/ANCHOR.a2ml`, `ECOSYSTEM.a2ml` |=== == What we do NOT claim -* List the known gaps, trust boundaries, postulates, unwired modules, and stale - docs here. Silence is not affirmation — name what you have *not* verified. +* *No completed formal proofs.* `verification/proofs/` holds prover *scaffolding* + (Agda/Coq/Idris2/Lean4/TLA+), not finished systemet developments. +* *L4 TEA-erasure is OPEN.* It is a target, not a theorem. Do not cite it as proven. +* *No compiler or checker lives here.* The reference kernel is the separate + link:https://github.com/hyperpolymath/anytype[anytype] repository, itself early. +* *L1 totality* is currently a specified requirement, not a discharged proof. +* The `src/`, `tests/`, and most `docs/` trees are RSR *scaffolding* inherited from + the template, not systemet-specific content yet. + +== Provenance note + +This repository was split out of an earlier combined draft that conflated three +things under the over-claiming name "EveryType": the theory, the kernel, and a +product profile. systemet is now the *theory* (Equality Theory); the kernel is +link:https://github.com/hyperpolymath/anytype[anytype]; the profile is AffineScript. [#verifiable-anchor] == Verifiable anchor [cols="1,3"] |=== -| Project | {{PROJECT_NAME}} -| Repository | https://{{FORGE}}/{{OWNER}}/{{REPO}} +| Project | systemet +| Repository | https://github.com/hyperpolymath/systemet | Commit (SHA) | -| Branch | {{MAIN_BRANCH}} +| Branch | main | Timestamp (UTC) | -| Toolchain | -| Affirmed by | {{AUTHOR}} <{{AUTHOR_EMAIL}}> +| Toolchain | +| Affirmed by | Jonathan D.A. Jewell |=== _Landed by a signed git commit. Verify with `git log --show-signature` that the diff --git a/CHANGELOG.md b/CHANGELOG.md index ec7f2e1..364e199 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,3 +13,24 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] + +### Added +- Instantiated this repository as **systemet — Equality Theory** (`system` + `ET`), + the stratified type theory the `anytype` kernel implements. +- Authored `README.adoc` and `EXPLAINME.adoc` for the theory: the five layers, the + L1 equality-is-conversion cut, the three gates (Totality/Structural/Polarity), + roles-as-tropes, and TEA-erasure as an open proof obligation. +- Instantiated identity descriptiles (CLADE/ECOSYSTEM/ANCHOR/STATE/META) and the + AFFIRMATION honesty snapshot with the systemet identity and an honest status + (theory specified; proofs OPEN; no compiler here). + +### Changed +- Split the theory out of the earlier combined "EveryType" draft. The over-claiming + "EveryType" name is retired; the kernel half now lives in the `anytype` repo and + this repo holds the theory. + +### Notes +- `uuid` is a PROVISIONAL deterministic UUIDv5 of the forge URL; `clade` is + PROVISIONAL. Both must be confirmed/registered in `gv-clade-index`. +- `CLAUDE.md` is generated from the descriptiles — run `just claude-md` to refresh + it where `nickel`/`just` are available. diff --git a/CITATION.cff b/CITATION.cff index 5de4710..f74a28a 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -1,17 +1,20 @@ cff-version: 1.2.0 message: "If you use this software, please cite it as below." authors: -- family-names: "{{AUTHOR_LAST}}" - given-names: "{{AUTHOR_FIRST}}" - orcid: "https://orcid.org/0000-0000-0000-0000" # Placeholder -title: "{{PROJECT_NAME}}" +- family-names: "Jewell" + given-names: "Jonathan D.A." + orcid: "https://orcid.org/0000-0000-0000-0000" # TODO(owner): replace with real ORCID +title: "systemet — Equality Theory" version: 0.1.0 -date-released: "{{CURRENT_DATE}}" -url: "https://{{FORGE}}/{{OWNER}}/{{REPO}}" -repository-code: "https://{{FORGE}}/{{OWNER}}/{{REPO}}" +date-released: "2026-06-28" +url: "https://github.com/hyperpolymath/systemet" +repository-code: "https://github.com/hyperpolymath/systemet" license: MPL-2.0 keywords: + - "type-theory" + - "equality-theory" + - "graded-modal-types" + - "guarded-recursion" + - "effect-erasure" - "rsr" - "formal-verification" - - "neurosymbolic" - - "provenance" diff --git a/CLAUDE.md b/CLAUDE.md index b352a59..9f316e4 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -6,7 +6,7 @@ SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell - + # You are in the hyperpolymath estate — orient before acting @@ -54,14 +54,14 @@ Deny: **Nix, Node/npm, TypeScript, Python, Go, AGPL**. (Guix, not Nix.) --- -# This repo: `rsr-template-repo` · clade `rm-rsr-template-repo` +# This repo: `systemet` · clade `et-systemet` -- **Identity** — uuid `a5ea1382-a34c-5334-8a46-a2ebe904c810`; clade `rm` (secondary `gv`); born 2026-03-16; forge `hyperpolymath/rsr-template-repo`. -- **IS** — Canonical RSR-compliant repository template: scaffolding (CI/CD, AI manifests, ABI/FFI standards, container ecosystem, governance) that new hyperpolymath projects are instantiated from. -- **IS-NOT** — a project in its own right · Scaffoldia (the full-featured repo designer) · standards (the canon source this template operationalises) -- **Where it sits** — pipeline position **foundation**; chain `standards → rsr-template-repo → (every estate repo)`; coordination = `standards`. +- **Identity** — uuid `1ade549b-a47d-5204-b74e-7d1a3fc5f9d1`; clade `et` (secondary ``); born 2026-06-28; forge `hyperpolymath/systemet`. +- **IS** — 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** — 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) +- **Where it sits** — pipeline position **theory**; chain `systemet (theory) → anytype (kernel) → AffineScript (profile)`; coordination = `standards`. - **Constraints here** (AGENTIC) — fail-closed; evidence-per-step; no-silent-skip; rerun-after-fix; release-claim-requires-hard-pass. Never: banned langs (above), secrets, state files in repo root, AGPL. Details: `.machine_readable/bot_directives/{methodology,coverage,debt}.a2ml`. - **Golden path** (ANCHOR) — `just test && just quality` → Core tests pass; Quality gates pass; No unresolved critical security findings. -- **State** — phase maintenance; maturity production; 95% complete; status active. +- **State** — phase design; maturity experimental; 15% complete; status active. - + diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 5ea33fa..d22e440 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -1,118 +1,181 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -= RSR Template Repo - Explainme -image:https://img.shields.io/badge/License-MPL_2.0-blue.svg[License: MPL-2.0,link="https://opensource.org/licenses/MPL-2.0"] - -:toc: +// SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell (hyperpolymath) += systemet — EXPLAINME +How the README claims map to artefacts, proof obligations, and current evidence. +:toc: left +:sectnums: :icons: font -This file explains how the key template claims map to real files. +The README is the public orientation: where Equality Theory is going and why. This +file is the engineering account: where each claim actually lives, what is specified +versus proven, and where the evidence stops today. -== Central Session Protocol Authority +[IMPORTANT] +==== +*Boundary.* systemet is the theory. It does *not* contain a compiler or checker. +The reference implementation is the link:https://github.com/hyperpolymath/anytype[anytype] +kernel. Claims about *running* code belong to anytype's `EXPLAINME.adoc`, not this +one. Claims here are about the *specification* and its *proof obligations*. +==== -Claim: -Session protocols are centrally maintained and not duplicated in this template. +== Equality Theory (the name) -How this is implemented: +Claim: systemet is `system` + `ET`, where ET = Equality Theory. -* The local dispatcher (`session/dispatch.sh`) maps canonical commands to central - protocol paths in `standards/session-management-standards`. -* Local files (`session/custom-checks.k9`, `session/local-hooks.sh`, - `coordination.k9`) are integration-only. +What this means: + +* The single primitive relation kept at the bottom of the system is *equality*. +* Equality is *conversion*: `normalize` then `compare`. It is not a proof-carrying + subsystem and not a coercion calculus. +* Everything else is a *layer discipline* above equality, never a new relation + beside it. That is the wager, and it is the reason for the name. Caveat: -* If `SESSION_STANDARDS_DIR` is unset and no adjacent standards checkout exists, - the dispatcher records the command but cannot resolve central checklist paths. +* "Equality is conversion" is only as strong as a totality guarantee at L1. Where + totality is assumed rather than proven, it is an assumption to be discharged, and + it is named as such in `AFFIRMATION.adoc`. -== Canonical Command Surface +== The five-layer stratification -Claim: -Template bindings align to one canonical command model. +Claim: L0 runtime, L1 equality, L2 graded resources, L3 guarded recursion, L4 +effects — each defined over the one below. -How this is implemented: +Where it lives: -* `Justfile` provides thin aliases (`intake-repo`, `checkpoint-change`, - `verify-maintenance`, `verify-substantial`, `verify-release`, `close-planned`, - `close-urgent`, `recover-repo`, `handover-*`). -* Every alias calls `session/dispatch.sh` with canonical verb-object pairs. +* The layering is *specified in prose* in `README.adoc` and in this file. +* The intended formal artefacts live under `verification/proofs/` and + `docs/theory/`. Today those are *scaffolding*: prover stubs (Agda, Coq, Idris2, + Lean4, TLA+) and empty theory directories, not completed systemet developments. Caveat: -* Recipes are wrappers only. They do not replace protocol content from - the central standards repo. +* Do not read a populated `verification/proofs/` tree as "the layers are proven". + The tree is the place the proofs will go; the dated state is in `AFFIRMATION.adoc`. -== Runtime State Is Local +== The Totality Gate (L1) -Claim: -Session state is per-repository runtime output, not standards text. +Claim: at L1 type-level functions terminate, so equality is decidable as +normalize-then-compare, with no coercion language. -How this is implemented: +Proof obligation: -* `session/dispatch.sh` writes command and continuity-core capture stubs to - `.session/LAST-CANONICAL-COMMAND.md` in the target repository path. +* Totality of L1 type-level computation (no non-terminating type-level functions + admitted). +* Soundness and completeness of conversion-as-equality relative to the intended + model. Caveat: -* Runtime files are intentionally lightweight and require human/agent completion. +* Any accepted escape hatch must be recorded as an explicit assumption or unsafe + boundary, never folded silently into "equality". -== Template Token Policy +== The Structural Gate (L2) -Claim: -Placeholders are explicit template content until initialization. +Claim: shallow `CAR`/`CDR` projection from an additive product `&` is admitted; +deep co/contravariant rewriting is refused. -How this is implemented: +Proof obligation: -* `README.adoc` and bootstrap recipes keep `{{TOKEN}}` placeholders visible. -* `just init` performs token replacement. +* Soundness of shallow structural projection. +* A precise statement of the refused class (deep variance through function spaces, + effects, resources, lifetimes, linear positions) and why admitting it would + reopen the Coherence Cliff. Caveat: -* Uninitialized placeholders must not be treated as project-specific truth. +* This is a design boundary. A contribution that reintroduces deep variance must + carry the argument that it does not recreate the anti-stack. -== Dependency Updates (Dependabot) +== The Polarity Gate -Claim: -Dependency bumps land fast and safely, without manual chasing. +Claim: forward casts `A -> ?` are lossless forgetting; backward casts `? -| A` are +lossy and carry a blame grade `!_{blame}`; there is no universal `any`. -How this is implemented: +Proof obligation: -* `dependabot.yml` watches the Dependabot-supported ecosystems the estate - actually uses: `github-actions`, `cargo`, `mix` (Elixir), `docker`. -* `dependabot-automerge.yml` auto-merges *every* bump (patch/minor/major, - security or routine) **once the required checks are green** — a broken bump - fails CI and stays open (you get an email); it never lands on a red `main`. +* The blame grade is genuinely part of the L2 resource accounting (not cosmetic). +* Backward recovery cannot launder loss into an untracked position. + +== Pluggable grades (L2 algebra) + +Claim: a new discipline is a change of grade algebra, not a change of checker. + +Proof obligation: + +* The laws a candidate grade algebra must satisfy (semiring/ordering structure and + the operations the rules use) stated precisely enough to check a candidate. +* A demonstration that the *same* rules instantiate to distinct disciplines (affine, + cost, information-flow lattice, privacy budget, latency×billing). Caveat: -* Dependabot has **no Deno or Bun ecosystem**, and `pnpm` only rides under the - `npm` ecosystem (itself banned). For this Deno-first estate Dependabot cannot - watch the runtime dependencies; the `npm`/`pip` entries are retained only for - transitional/legacy manifests and are otherwise inert. Deno dependency - currency is managed via `deno.json`/`deno.lock`, not Dependabot. -* Do **not** add Dependabot as a ruleset *bypass* actor: that lets bumps skip - the required checks (secret-scanning, SAST), removing the safety gate and the - "it broke" signal. Auto-merge-on-green gives fast merges without it. +* "Pick the algebra" is bounded by those laws. Arbitrary metadata that does not + satisfy them is not a grade. -== Julia Registry Packages — Standalone Repo Requirement +== Roles to tropes -Claim: -If this template is used to create a Julia package, it must remain a standalone repository registered with the Julia package registry. +Claim: global roles/coercions are replaced by local finite trope machines +`A@t1 -> A@t2 -> A@t3`. -How this is implemented: +Proof obligation: -* Julia's package registry (General.jl or other) expects each package to be a standalone GitHub repository with `Project.toml` at the repository root. -* Installation via `Pkg.add()`, dependency resolution, and automated CI/CD all depend on this canonical structure. +* A trope-preservation result: well-typed movement through a finite machine + preserves the relevant invariants. +* Per-API obligations: each real protocol (file handle, socket, transaction, + stream, capability) needs its own finite machine and preservation argument. Caveat: -* Do NOT move this repository into a monorepo or subdirectory, as this breaks registry registration and package discoverability. -* Julia packages published to a registry must each remain a standalone top-level repository (registry registration and package discovery require it). -* Non-registry Julia packages can be organized differently if they are not published to any registry. +* Tropes do not "solve roles automatically". They relocate the burden to explicit, + checkable state movement. + +== TEA erasure (L4) +Claim: a Total + Effect-graded + Affine handler should erase completely. + +Status: *OPEN*. This is the headline open problem, not a result. + +* The intended erasure condition is T ∧ E ∧ A. +* Effects are not assumed free merely because they are typed. +* The README and any paper must describe TEA erasure as a *target*/amber claim + until a formal proof exists and is recorded in `AFFIRMATION.adoc`. + +== Relationship to anytype and AffineScript + +Claim: systemet is the theory; anytype is the reference kernel; AffineScript is a +profile. + +How this is kept honest: + +* systemet owns the semantics and is the *semantic authority* (see + `.machine_readable/6a2/anchors/ANCHOR.a2ml`). Downstream may *extend* but not + *redefine* the theory. +* anytype must *pin* systemet upstream and implement it; it may not silently change + the theory to match the implementation. If implementation pressure forces a + theory change, it is an ADR in systemet, not a quiet edit in anytype. +* AffineScript is `grade = affine + cost` on the anytype kernel; it is downstream of + both. + +== RSR integration + +Claim: systemet uses the Rhodium Standard Repository structure without that +infrastructure being part of the theory. + +How this is implemented: + +* `0-AI-MANIFEST.a2ml` is the AI-agent entry point; `.machine_readable/` holds + metadata, policy, contractiles, anchors, and agent-readable state; `just validate` + checks repository shape; `AFFIRMATION.adoc` is the dated honesty snapshot; + `AUDIT.adoc` is the release gate. + +Caveat: -== License +* Passing RSR validation proves the *repository* is well-formed. It proves nothing + about systemet's *soundness*. Those are separate claims with separate evidence. -This project is licensed under the Mozilla Public License, v. 2.0. See the `LICENSE` file for details. +== Licence -SPDX-License-Identifier: CC-BY-SA-4.0 +* Prose documentation: `CC-BY-SA-4.0`. Code/config/scripts: `MPL-2.0`. +* Per-file `SPDX-License-Identifier` headers are authoritative; the root `LICENSE` + controls GitHub's detected licence. diff --git a/README.adoc b/README.adoc index 6deeae5..379b127 100644 --- a/README.adoc +++ b/README.adoc @@ -1,99 +1,276 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -// SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell (hyperpolymath) -= {{PROJECT_NAME}} -:toc: -:toc-placement: preamble +// SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell (hyperpolymath) += systemet +Equality Theory: one relation at the bottom, discipline in the layers. +:toc: left +:sectnums: +:icons: font -image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity[OpenSSF Best Practices,link="https://www.bestpractices.dev/en/projects/new?repo_url=https://{{FORGE}}/{{OWNER}}/{{REPO}}"] image:https://img.shields.io/badge/License-MPL_2.0-blue.svg[License: MPL-2.0,link="https://opensource.org/licenses/MPL-2.0"] -image:https://raw.githubusercontent.com/hyperpolymath/palimpsest-license/main/assets/badges/svg/badge-quantum-safe.svg[Quantum-Safe Provenance,link="https://github.com/hyperpolymath/palimpsest-license/blob/main/v1.0/exhibits/EXHIBIT-B-QUANTUM-SAFE.txt"] image:https://img.shields.io/badge/Docs-CC--BY--SA--4.0-blue.svg[Docs: CC-BY-SA-4.0,link="https://creativecommons.org/licenses/by-sa/4.0/"] -image:https://api.thegreenwebfoundation.org/greencheckimage/{{FORGE}}[Green Web,link="https://www.thegreenwebfoundation.org/green-web-check/?url={{FORGE}}"] image:https://img.shields.io/badge/RSR-Rhodium_Standard-9C27B0[Rhodium Standard Repository,link="https://github.com/hyperpolymath/rhodium-standard-repositories"] -image:https://img.shields.io/badge/Idris-Inside-5E5086?logo=idris&logoColor=white[Idris Inside,link="https://github.com/hyperpolymath/proven"] +image:https://img.shields.io/badge/status-theory_(no_proofs_yet)-orange[Status: theory, proofs open] -{{PROJECT_DESCRIPTION}} +*systemet* is a stratified type **theory**. The name is `system` + `ET`, where *ET* +stands for **Equality Theory** — because the one primitive relation the whole system +keeps at the bottom is *equality*, and everything else is layered above it as +discipline rather than added as new relations. [IMPORTANT] ==== -*This file is a template.* You are reading `README.adoc` from the *RSR template repo* -(or a freshly-cloned copy of it). Run `just init` to replace every `{{PLACEHOLDER}}` -token with your project's details, then delete this admonition. Until you do, the -`{{...}}` markers below are intentional placeholders, not content. +*systemet is the theory, not an implementation.* It defines the semantics, the +invariants, and the proof obligations. The reference kernel that *implements* +systemet is a separate repository, link:https://github.com/hyperpolymath/anytype[*anytype*]. +A downstream product profile of that kernel is *AffineScript*. + +[cols="1,3",options="header"] +|=== +| Repository | Role +| `systemet` (this repo) | The theory — Equality Theory. Semantic authority: the spec, invariants, and proof obligations. +| `anytype` | The kernel — the reference engine that implements this theory. "Pick the algebra, get the discipline." +| AffineScript | One opinionated product profile built on the `anytype` kernel (`grade = affine + cost`). +|=== ==== -== What this is +== The wager + +Modern type systems usually grow by adding *new relations on types*: equality +evidence, roles, variance, subtyping, gradual escape hatches, region constraints. +Each new relation has to cohere with every other one. Two features do not create +two obligations; they create a *square* of interactions. Three create a grid. +Eventually the compiler is no longer checking programs — it is managing a treaty +between equality, subtyping, variance, effects, resources, inference, and runtime +casts. systemet calls that failure mode the *Coherence Cliff*, and the underlying +shape the *anti-stack*: + +> features accrete sideways as new type relations instead of stacking vertically +> as disciplined layers. -A new repository scaffolded from the *Rhodium Standard Repository (RSR)* template: -a batteries-included starting point that ships with CI/CD, machine-readable project -metadata, an AI-agent gatekeeper protocol, a formally-typed ABI/FFI seam -(Idris2 + Zig), container and reproducible-build scaffolding, and governance -infrastructure — all wired and passing the RSR validators on day one. +The systemet wager is one sentence: -Replace this section with a description of *your* project once initialised. +> *Do not add a new type relation when a layer discipline will do.* -== Quick start +So systemet keeps exactly one primitive relation at the bottom — equality — and +moves expressive pressure *upward* into layers, not *sideways* into new relations. + +== The five layers + +systemet is stratified. Each layer is defined in terms of the one below it; the +relation set never grows. + +[cols="1,2,3",options="header"] +|=== +| Layer | Meaning | Theory status -[source,bash] +| *L4 · effects `◇`* +| Effect handlers under an erasure discipline +| *OPEN* — the target is to prove when a Total + Effect-graded + Affine (TEA) handler erases completely + +| *L3 · recursion `▶`* +| Guarded recursion +| specified + +| *L2 · resources `□`* +| Graded-modal substrate over a pluggable grade algebra (semiring) +| specified — this is where the discipline lives + +| *L1 · equality* +| The totality cut: equality *is* conversion +| specified — no coercions, no roles, no representational-equality calculus + +| *L0 · runtime* +| Lowering target (e.g. WASM/C) +| specified +|=== + +The defining move is *L1*. In System F~c~ a great deal of expressive pressure is +pushed *into* equality, which becomes a proof-carrying subsystem. systemet cuts +earlier: + +[source,text] +---- +System Fc: equality becomes a proof-carrying subsystem. +systemet: equality remains conversion; discipline moves into layers. ---- -# 1. Create a repo from this template (or clone it), then from the repo root: -just init # interactive bootstrap: fills every {{PLACEHOLDER}} -# 2. See the available tasks: -just # lists all phases (build, test, validate, audit, ...) +== The three gates -# 3. Check the repo still satisfies the RSR shape: -just validate # structure + metadata checks +systemet works by *refusing three tempting collapses*. Each gate is a boundary, +not an omission. + +=== 1. The Totality Gate (L1) + +At L1, type-level functions must terminate. Therefore equality is decidable by: + +[source,text] +---- +normalize +compare +done +---- + +No coercion language. No roles. No representational-equality proof calculus. No +"trust me, these two types are the same at runtime." If a type-level function does +not terminate, it does not belong at L1. + +=== 2. The Structural Gate (L2) + +systemet admits *shallow structural subtyping* exactly where it is just projection +— `CAR`/`CDR`-style access from an additive product `&`, covering width-like +behaviour for rows, variants, refinements, and record-like products. + +[source,text] +---- +Shallow CAR/CDR projection is allowed. +Deep co/contravariant rewriting is not. +---- + +Deep variance pushes structure through function spaces, resources, effects, +lifetimes, and linearity — which is exactly where coherence starts to leak. The +gate allows the shallow case and refuses the deep one. + +=== 3. The Polarity Gate + +systemet admits *polarized casts*, not a universal gradual `any`: + +[source,text] +---- +A -> ? forward, lossless, forgetful +? -| A backward, lossy, blame-graded ---- -`just init` prompts for the project name, owner, author, licence contact, and the -other values listed in `.machine_readable/ai/PLACEHOLDERS.adoc`, substitutes them -across the tree, validates the result, and (if available) runs the `k9-svc` checks. - -== What you get - -* *Machine-readable metadata* (`.machine_readable/6a2/`) — `STATE`, `META`, - `ECOSYSTEM`, `PLAYBOOK`, `AGENTIC`, `NEUROSYM`, `CLADE`, and `anchors/ANCHOR`, - in a2ml, so tools and agents can read the project's state and boundaries. -* *AI gatekeeper protocol* — `0-AI-MANIFEST.a2ml` is the universal entry point that - tells an AI agent how to work in this repo before it touches anything. -* *Typed ABI/FFI seam* — `src/interface/Abi/` (Idris2 type + layout proofs) over - `src/interface/ffi/` (Zig implementation), with generated C headers. -* *CI/CD* — GitHub Actions for quality, security (CodeQL, Scorecard, secret - scanning), multi-forge mirroring, and RSR anti-pattern enforcement. -* *Supply-chain & reproducibility* — container layering (stapeln), Guix shells, - SBOM, and signing hooks. -* *Governance* — `GOVERNANCE.adoc`, `MAINTAINERS.adoc`, `.github/` community health - files, and a release `AUDIT.adoc` gate. - -== Repository map - -[cols="1,3"] +The forward direction is ordinary forgetting. The backward direction is *not* +treated as a magical runtime check: it carries a blame grade `!_{blame}` that is +part of the resource story. There is no universal `any` that silently punches a +hole through the type system — only directed loss, explicit polarity, and graded +blame. + +== What the theory makes cheap + +=== Disciplines as a one-line change of algebra + +Because the discipline lives at L2 over a pluggable grade algebra, a new +discipline is a change of algebra, not a change of checker: + +[source,text] +---- +grade = Affine +grade = Cost * Nat +grade = Low <= High (an information-flow lattice) +grade = [0,1] (a probability-like grade) +grade = PrivacyBudget +grade = Latency x Billing +---- + +Same rules. Different algebra. Different discipline. A proposed grade is only +admissible if it satisfies the laws the theory requires (the relevant operations +and ordering) — "pick the algebra" is not "attach arbitrary metadata". + +=== Roles become tropes + +System F~c~ asks whether two types are representationally equal under a global role +discipline. systemet avoids that question. Instead of a global `coerce`, it uses +local, finite, model-checkable state transitions: + +[source,text] +---- +A@t1 -> A@t2 -> A@t3 +---- + +A *trope* is a finite transition machine. The burden moves from global +representational equality to explicit, local state movement: no `coerce`, no role +inference, no hidden representational treaty. Each real API (file handles, sockets, +transactions, streams, capabilities) gets a finite machine and a preservation +obligation. + +=== Effects erase only when proven harmless + +A handler that is *Total*, *Effect-graded*, and *Affine* is a *TEA* handler. The L4 +goal is to prove *when* such a handler erases completely. This is not "effects are +free"; it is: + +> effects erase only when the layer discipline proves them observationally harmless. + +=== Dependent types, rows, and refinements without new relations + +They do not need new primitive relations. They live at L2 as structured uses of the +graded substrate — which is the whole wager restated. + +== systemet vs the world + +[cols="1,2,2,2,2",options="header"] |=== -| Path | What lives there - -| `0-AI-MANIFEST.a2ml` | Universal entry point for AI agents (read first). -| `.machine_readable/` | Project metadata, policies, contractiles, AI configs. -| `src/interface/` | Typed ABI (Idris2) + FFI (Zig) + generated headers. -| `docs/` | Onboarding, status, governance, practice, decisions. -| `build/`, `Justfile` | Task orchestration (`just` phases delegate to `build/just/*.just`). -| `.github/` | Workflows + community health files. -| `tests/`, `benches/` | Test suites and benchmarks. +| | systemet | Haskell / System Fc | Idris2 | Rust + +| *L1 equality* +| conversion +| coercion proofs / equality evidence +| conversion +| trait & region solving + +| *Coercions* +| *none* +| *yes* +| mostly none at the core +| lifetime/representation-sensitive + +| *L2 resources* +| *pluggable semiring* +| limited / plugin-dependent +| quantity discipline `0,1,ω` +| affine ownership + +| *Roles* +| *tropes `A@t`* +| global role system +| none +| lifetime / variance discipline + +| *Deep variance* +| *refused* +| controlled, external to this wager +| limited +| *yes* + +| *Effects erase* +| TEA-purity target (open) +| no general erasure theorem +| no general erasure theorem +| no general erasure theorem |=== -== Where to go next +== Status — read this honestly + +systemet is, at this commit, a *theory written down*, not a proven one. + +* The semantics, the layering, the three gates, and the wager are *specified* in + this repository (this README and `EXPLAINME.adoc`). +* The formal proofs are *open*. The `verification/proofs/` tree holds prover + scaffolding (Agda/Coq/Idris2/Lean4/TLA+), not completed systemet proofs. +* L4 TEA-erasure is an *open problem*, not a result. Do not cite it as proven. +* There is *no compiler here*. The reference kernel is link:https://github.com/hyperpolymath/anytype[anytype], + and it is itself at an early stage. + +For the dated, signed honesty snapshot see link:AFFIRMATION.adoc[AFFIRMATION]; +for the claim-to-artefact mapping see link:EXPLAINME.adoc[EXPLAINME]; for the +release gate see link:AUDIT.adoc[AUDIT]. + +== Contributing + +The useful contributions are theory and proof, not syntax: + +* new L2 grade algebras (security lattices, differential-privacy budgets, + latency/cost models, information-flow grades) *with their laws*; +* proofs — TEA erasure, trope preservation, shallow-structural soundness, the + interaction of guarded recursion with grades; +* finite trope machines for real APIs (file handles, sockets, database + transactions, web streams, WASM capabilities). -* `EXPLAINME.adoc` — the engineering deep-dive: how the pieces actually work. -* `AFFIRMATION.adoc` — the dated, signed honesty snapshot of the repo's true state. -* `AUDIT.adoc` — the release audit gate. -* `.machine_readable/ai/PLACEHOLDERS.adoc` — the full placeholder reference. +Open issues with one of: `[ET-L2]`, `[ET-L3]`, `[ET-L4]`, `[TROPE]`, `[TEA]`. == Licence -Code, configuration and scripts are link:LICENSE[Mozilla Public License 2.0] -(`MPL-2.0`); prose documentation is `CC-BY-SA-4.0`. Both texts live in -`LICENSES/`, and per-file `SPDX-License-Identifier` headers are authoritative. -The GitHub-detected licence is MPL-2.0 (the root `LICENSE`). Long-term -attribution uses Quantum-Safe Provenance — see -link:https://github.com/hyperpolymath/palimpsest-license/blob/main/v1.0/exhibits/EXHIBIT-B-QUANTUM-SAFE.txt[PMPL Exhibit B]. +Prose documentation is licensed `CC-BY-SA-4.0`; any code, configuration, and +scripts are `MPL-2.0`. Per-file `SPDX-License-Identifier` headers are +authoritative. The GitHub-detected licence is MPL-2.0 via the root `LICENSE`. +Long-term attribution uses Quantum-Safe Provenance (PMPL Exhibit B where present).