hyperpolymath · hyperpolymath · Jun 19, 2026 · Jun 19, 2026
@@ -0,0 +1,75 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+= AFFIRMATION — JtV
+Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+:revdate: 2026-06-19
+:revnumber: 1.0
+:toc: macro
+
+[.lead]
+A point-in-time affirmation of the verified state and standard-compliance of the
+*JtV* repository (`hyperpolymath/jtv`, formerly `julia-the-viper`), recorded per
+the Rhodium Standard Repositories (RSR) / hyperpolymath estate convention.
+
+[NOTE]
+====
+The hyperpolymath `standards` repository was not in this session's working scope,
+so this document follows the apparent RSR/estate convention and the in-repo
+contractile structure (`Mustfile`/`Intentfile`/`Trustfile`). Reconcile against
+the canonical `AFFIRMATION` template in `standards` when available.
+====
+
+== Affirmation
+
+As of *2026-06-19*, at commit `fff9689` on `main`, the following is affirmed of
+this repository.
+
+=== Core guarantees (the normative MUSTs)
+
+* *Harvard separation* — the Control language (Turing-complete) and the Data
+  language (Total, addition-only) are grammatically separated; code injection is
+  structurally — not heuristically — excluded.
+* *Totality* — the Data language is addition-only and provably halting.
+* *Reversibility / Echo soundness* — the `reverse {}` admissibility gate
+  classifies against the *actual* (carrier-aware, inferred) Echo grade;
+  annotations cannot loosen it. Float locals are soundly rejected (ADR-0010).
+* *ADR-0009 effect surface complete* — Echo and Epistemic are first-class graded
+  function effects, on declarations (`@echo(...)` / `@epi(...)`) and in function
+  types, with an upper-bound check against the composed grade.
+
+=== Verification status
+
+* *Rust* — `cargo build --workspace`, `cargo fmt --check`, and `cargo clippy`
+  clean; *142 jtv-core lib tests* plus integration suites green.
+* *Lean 4* — the proof suite compiles with *0 `sorry` / `admit` / `axiom`*.
+* *Idris2* — the ABI definitions type-check.
+
+=== Standard-compliance
+
+* *Language policy* — Rust (core), Lean 4 / Idris2 (proofs), per the hyperpolymath
+  standard; no banned languages introduced.
+* *Licensing* — MPL-2.0 (code) + CC-BY-SA-4.0 (docs), full per-file SPDX
+  (gap-006 resolved).
+* *Provenance* — contractiles present; `.machine_readable/6a2/STATE.a2ml` current.
+
+=== Honest open items (NOT yet affirmed)
+
+* First-class function *values* (lambdas) — required to make the function-type
+  effect check active (currently latent / representational).
+* `gap-005` — value-level number-system semantics beyond `τ = int`.
+* The GitHub repository-slug rename `julia-the-viper → jtv` (manual settings step,
+  still pending).
+
+== Signatory
+
+Affirmed for the maintainer:
+
+[%hardbreaks]
+Name: Jonathan D.A. Jewell (hyperpolymath)
+Date: 2026-06-19
+Commit: `fff9689`
+Repository: `hyperpolymath/jtv`
+
+_Prepared during an automated (Claude Code) session and submitted for the
+maintainer's affirmation._
@@ -0,0 +1,96 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+= Ecosystem Status — Musts / Intends / Wishes
+Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+:revdate: 2026-06-19
+:revnumber: 1.0
+:toc: left
+:sectnums:
+
+[.lead]
+A point-in-time status of four hyperpolymath projects, each grouped into the
+normative tiers *MUST* (invariants / required), *INTEND* (declared, in-progress),
+and *WISH* (aspirational). JtV is the normative anchor.
+
+Legend: ✅ done · ◑ partial · ◻ planned · ⚠ gap · ○ aspirational.
+
+Sources / freshness: JtV is live (this session, commit `fff9689`); Absolute Zero
+from `STATE.a2ml` (2026-05-27); JanusKey from `STATE.a2ml` (2026-04-04, older) +
+README; maa-framework not yet in working scope (see §5).
+
+== JtV — the normative anchor
+
+Harvard-architecture language: Control (Turing-complete) vs Data (Total,
+addition-only); code injection grammatically impossible. Echo + Epistemic effect
+system for reversibility / structured loss.
+
+[cols="1,5,3",options="header"]
+|===
+| Tier | Item | Where we are
+| MUST | Harvard separation → code injection *grammatically* impossible | ✅ structural
+| MUST | Data language addition-only & Total (provably halting) | ✅
+| MUST | Reversibility / Echo soundness — `reverse` gate on the *actual* grade; Lean proofs 0 `sorry/admit/axiom` | ✅ (carrier-aware + float-locals, ADR-0010)
+| MUST | ADR-0009 effect surface: Echo + Epistemic on declarations *and* function types | ✅ (#48–#50)
+| INTEND | First-class function *values* (lambdas) → activates the function-type effect check | ◻ next rung
+| INTEND | `gap-005`: value-level number-system semantics beyond `τ=int` | ◻ open
+| INTEND | `Settings → jtv` repo-slug rename (make the rebrand live) | ◻ manual
+| INTEND | PataCL Phase 1 → coprocessor implementation | ◻ external dep
+| WISH | v2 reversible-computing / quantum-algorithm simulation (Landauer, Grover/Shor) | ○ spec only
+| WISH | Router-visualization playground (the "killer demo") | ○
+|===
+
+== Absolute Zero
+
+Multi-prover formal verification of Certified Null Operations (CNO). ~65%,
+proof-completion phase.
+
+[cols="1,5,3",options="header"]
+|===
+| Tier | Item | Where we are
+| MUST | Proofs green across provers: Coq 11/11 (0 `Admitted`), Lean 1631/1632, Agda `CNO.agda` clean | ✅ (2026-05-27)
+| MUST | Core CNO + category theory + statistical mechanics fully proven | ✅
+| MUST | Trusted-base discipline — 72 Coq axioms triaged (52 trusted / 17 discharge / 3 property-test) | ◑ Phase 1 (PR #58)
+| MUST | No Python (RSR) | ⚠ currently violated (high blocker)
+| INTEND | v0.8 compliance sprint (40%); discharge 17 §a Coq backlog axioms; Phase-2 triage (Lean 52 + Idris2 7) | ◻ in progress
+| INTEND | Migrate Python→Rust; physics-constant dedup; v0.9 container verification | ◻
+| WISH | v1.0 publication release + paper draft | ○
+| WISH | Mizar (10% stub) + Isabelle (40%) brought to parity | ○
+|===
+
+== JanusKey
+
+Architecturally-reversible file operations (data loss "impossible" by design, not
+backups). ~60%; content-addressed (SHA256), Rust.
+
+[cols="1,5,3",options="header"]
+|===
+| Tier | Item | Where we are
+| MUST | 100% reversible file ops by *architecture* | ◑ implemented — *formal proofs still pending* (per README)
+| MUST | Content-addressed (SHA256) storage, audit trail, transactions | ✅
+| MUST | Coverage across p2p / e2e / aspect-security / concurrency | ✅ 56 tests / 64 points (CRG D→C blitz)
+| MUST | License = MPL-2.0 | ✅ migrated (a740439, #52); PMPL stragglers retired (#65)
+| INTEND | API stability review (stated current phase) | ◻
+| INTEND | Land the formal reversibility proofs; climb CRG grade (D→C→…) | ◻
+| WISH | Broader packaging / adoption | ○ thin in current state
+|===
+
+== maa-framework — Mutually Assured Accountability
+
+The *Mutually Assured Accountability* framework. ⚠ *Not yet groundable from this
+session:* it is not in the current working repo scope, not cloned locally, and the
+repo-management tooling (`list_repos`/`add_repo`) was unavailable — so no MUST /
+INTEND / WISH rows are recorded here rather than invent them. Add it to scope
+(when the tooling is available) to populate this section from its own `STATE` and
+contractiles.
+
+== Where we are (synthesis)
+
+* *JtV* is the most mature and the only one advanced this session: core guarantees
+  and the full Echo + Epistemic effect surface are done and proven; remaining work
+  is feature-reach (function values) plus one manual rename.
+* *Absolute Zero* is deep in proof-completion — green across provers, grinding down
+  axiom / Python debt toward a publishable v1.0.
+* *JanusKey* is feature- and test-complete in architecture but has not yet *proven*
+  its headline reversibility claim; its license migration is now finished.
+* *maa-framework* awaits inclusion in working scope.
@@ -0,0 +1,52 @@
+<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
+<!-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
+<!-- Prepared 2026-06-19 as a handoff prompt for a future Claude session on wokelang. -->
+
+# Kickoff prompt — wokelang
+
+Paste the block below to the next Claude session that has the **wokelang** repo
+(`hyperpolymath/wokelang`, one of the nextgen-languages portfolio) in scope.
+
+---
+
+You are continuing work on **wokelang**, a language in the hyperpolymath /
+nextgen-languages portfolio. Work on the designated `claude/...` feature branch;
+commit with clear messages; push; open a **draft** PR when a rung lands.
+
+**First, orient yourself (read before changing anything):**
+1. `.claude/CLAUDE.md` and any root `CLAUDE.md` — project-specific rules override defaults.
+2. `.machine_readable/6a2/STATE.a2ml` — current state, milestones, blockers, next-actions.
+3. `README.adoc` / `README.md` and `docs/` — purpose and design.
+4. `contractiles/` — `Mustfile` (invariants that MUST hold), `Intentfile` (declared intent), `Trustfile` (provenance).
+5. The build entrypoint — `Justfile` (run `just --list`), `guix.scm` (primary) / `flake.nix` (fallback).
+
+**Then produce a status before diving in:** a short table grouped into **MUST /
+INTEND / WISH** (mirror `hyperpolymath/jtv:docs/ecosystem-status.adoc`), grounded
+in `STATE.a2ml` + contractiles — and propose the single smallest useful next rung.
+Confirm direction if it's ambiguous or architecturally significant.
+
+**Hyperpolymath standards to hold to:**
+- **Language policy:** AffineScript (primary app code) · Rust (systems/CLI/WASM) ·
+  Deno (runtime/pkg) · Gleam (BEAM services) · Julia (batch/data) · Guile Scheme
+  (state/meta `.a2ml`) · Nickel (config) · OCaml/Ada where specified.
+  **Banned:** TypeScript, ReScript (→ AffineScript), Node/npm/bun/pnpm/yarn (→ Deno),
+  Go (→ Rust), Python (→ Julia/Rust), Java/Kotlin/Swift/RN/Flutter (→ Rust/Tauri/Dioxus).
+- **Licensing:** MPL-2.0 (code) + CC-BY-SA-4.0 (docs), full per-file SPDX headers.
+  The PMPL-1.0 / Palimpsest *license* is retired across the estate (keep "Palimpsest"
+  only as philosophy/name, never as an SPDX id or a separate `LICENSE`).
+- **Hygiene (RSR):** `Justfile` not `Makefile`; `Containerfile` not `Dockerfile`;
+  no hardcoded developer paths; HTTPS only; SHA256+ (no MD5/SHA1); no hardcoded
+  secrets; SHA-pinned deps; Guix primary / Nix fallback.
+
+**Working discipline (mirror the JtV cadence):**
+- Every change ends with the relevant build/test command **run**, with captured output.
+- Headline results pinned (tests/CI green) — no overclaiming; if something is
+  partial or representational, say so explicitly.
+- Update `.machine_readable/6a2/STATE.a2ml` (session-history + next-actions) and the
+  contractiles when a rung lands.
+- One concern per PR; draft PRs; never push to `main`.
+
+Start by reading the orientation files above and reporting wokelang's current
+MUST/INTEND/WISH status + your proposed first rung.
+
+---