Elevate KitchenSpeak toward standalone repo; commence proofs-first work (#63)

## What this does

Prepares **KitchenSpeak**'s elevation from an in-tree directory to its
own canonical repository (matching every sibling language), lists it as
a **DSL** in the monorepo `README.adoc` and `EXPLAINME.adoc`, examines
where **AffineScript** is up to, and **commences the development work**
to bring KitchenSpeak to AffineScript's position — leading,
deliberately, **with proofs**.

## Where AffineScript is (the target)

The standalone `hyperpolymath/affinescript` repo is outside this
session's GitHub scope, so its position is taken from the monorepo's own
authoritative docs (`EXPLAINME.adoc` §Claim 1, `TOOLING-STATUS.adoc`,
`PROOF-NEEDS.md`):

- Full front end + toolchain: OCaml compiler, `affine-lsp`/`affine-dap`
(Rust), linter, formatter (stub), tree-sitter, doc-gen, pkg-mgr,
conformance ✓
- ABI/FFI (`src/abi/`, Idris2 + Zig) **in progress**; targets WasmGC
- Grades `ARG-D`, `FRG-E`, `RSR FULL`
- **Formal proofs are its known gap** — "claims affine types but lacks
proofs"; no `formal/` dir

That gap is exactly why KitchenSpeak (identity: *Agda-Proven*) **leads
with proofs**: it honours the language's invariant *and* overtakes the
target on the axis that matters most for a safety DSL.

## Changes

**New standalone-repo content under `kitchenspeak/`** (moves with the
directory when elevated):
- `README.adoc` (standalone), `LICENSE` (Palimpsest/MPL-2.0),
`.gitignore`, `CHANGELOG.adoc`
- `ROADMAP.adoc` — proofs-first, 8-phase plan to AffineScript parity,
with a per-axis **parity scorecard**
- `decisions/0002-elevation-to-standalone-repo.adoc` — ADR for the
elevation

**Proofs commenced (ROADMAP Phase 1):**
- `proofs/agda/PoachedEgg.agda` — lowers `examples/poached-egg.ks`;
discharges termination, `on_fail` totality (ABORT + RECOVER),
echo-witness extraction for both `sync` blocks, **and the first Tropical
refinement** (the GENTLE controller never crosses the boil envelope).
Linear + Tropical + Echo.
- `proofs/Makefile` + `proofs/agda/kitchenspeak.agda-lib` — proof build
harness (`make -C proofs`)

**Monorepo:**
- `README.adoc`, `EXPLAINME.adoc` — KitchenSpeak listed as an
experimental **DSL** in the project list / language tables / file map

## ⚠️ One step needs your hands: creating the remote repo

I could not finish the literal "create `hyperpolymath/kitchenspeak` +
flip to submodule" step from here: the GitHub App backing this session
is not permitted to create repositories (`POST /user/repos → 403
Resource not accessible by integration`). Rather than leave the monorepo
pointing at a submodule that doesn't exist, I kept the content in-tree
(so the repo stays valid and the proofs are reviewable) and provided the
mechanical finisher:

```bash
./scripts/elevate-kitchenspeak.sh
```

It creates the public repo, **preserves history** via `git subtree
split`, pushes, then converts `kitchenspeak/` into a submodule and
commits. Run it locally (or anywhere with `gh` + repo-create rights).
ADR 0002's status documents this precisely.

## Proof caveat

Agda isn't installed in this environment, so `PoachedEgg.agda` is
**hand-verified, not yet machine-checked** — the same standard the
existing `Dough.agda` is held to (see `proofs/README.adoc`). ROADMAP
Phase 1a adds Agda to CI so `make -C proofs` runs on every push.

## Test plan
- [ ] `./scripts/elevate-kitchenspeak.sh` (needs `gh` + repo-create
permission)
- [ ] `make -C proofs` (needs Agda 2.6.4+ / stdlib 2.0+) → zero unsolved
goals

https://claude.ai/code/session_01RZWK1vf9QfP2H2JTFWCdJY

---
_Generated by [Claude
Code](https://claude.ai/code/session_01RZWK1vf9QfP2H2JTFWCdJY)_

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

EXPLAINME.adoc

@@ -86,8 +86,21 @@ Ephapax (which is dyadic: affine + linear).
 | `let x = ...` (affine) vs `let! x = ...` (linear). Targets WebAssembly.
 Gossamer backend. Rust compiler, Coq proofs.
 | Rust (17 crates), Coq proofs
+
+| *KitchenSpeak* _(experimental DSL)_
+| Applied type-theory teaching DSL
+| Seven-type kitchen-orchestration DSL: Tropical (refinement), Linear,
+Choreographic (session), Echo (postulated oracle), Dyadic (tensor),
+Ceremonial (effect), Primitive (units). `max_duration` / `on_fail` /
+`proving @w` make every block a total, witnessed function. Proofs-first.
+| Agda proofs (OCaml front end planned)
 |===
 
+NOTE: *KitchenSpeak* is an experimental teaching DSL, not one of the ten
+core languages. It is maintained as the standalone `hyperpolymath/kitchenspeak`
+repository and develops proofs-first (see its `ROADMAP.adoc`); the canonical
+recipes (Dough, Poached Egg) already have Agda lowerings.
+
 === Most mature: Ephapax
 
 `ephapax/` is the most advanced implementation. It is a Cargo workspace with
@@ -273,6 +286,12 @@ from Julia the data language to avoid confusion.
 | `error-lang/`
 | Pedagogical language for teaching systems thinking via error conditions.
 
+| `kitchenspeak/`
+| Experimental, formally-verified kitchen-orchestration DSL (submodule:
+`hyperpolymath/kitchenspeak`). Seven-type system; proofs-first. Agda
+lowerings of the Dough and Poached Egg recipes; `ROADMAP.adoc` targets
+AffineScript-level toolchain parity, leading with the proof library.
+
 | `tangle/`
 | Literate programming / tangling tool shared across the language ecosystem.
 

PROOF-NEEDS.md

@@ -21,6 +21,21 @@
 | Tangle Lean proofs | Extend Tangle.lean coverage | Existing Lean proofs are partial |
 | Oblibeny ABI | Extend Interface.idr with full package proofs | Current ABI is minimal |
 
+## KitchenSpeak Trusted Base (Agda postulates)
+
+KitchenSpeak's proofs are deliberately built on a small, explicit trusted
+base: the *postulated echo-oracles* (sensors) and the GENTLE *controller
+spec*. These are not soundness gaps to close but documented trust
+boundaries (see each proof's final section and `COMMENTARY.adoc §Echo`).
+A production lowering replaces each with a verified HAL binding.
+
+| Postulate | File | What it trusts | Production replacement |
+|-----------|------|----------------|------------------------|
+| `viscosity-at` | `kitchenspeak/proofs/agda/Dough.agda` | Torque sensor stream | Verified HAL torque binding |
+| `temp-at` | `kitchenspeak/proofs/agda/PoachedEgg.agda` | Hob thermometer stream | Verified HAL thermal binding |
+| `white-set-at` | `kitchenspeak/proofs/agda/PoachedEgg.agda` | Visual albumen classifier | Verified/empirically-bounded classifier |
+| `gentle-bounded` | `kitchenspeak/proofs/agda/PoachedEgg.agda` | GENTLE controller never overshoots target cap | Integrator bound on the slope |
+
 ## Recommended Prover
 
 **Coq** for Ephapax (existing proof infrastructure). **Lean4** for Tangle (existing). **Idris2** for ABI layers. **OCaml** extraction from Coq for AffineScript type checker verification.

README.adoc

@@ -94,6 +94,26 @@ A multi-dialect experimental language family exploring different levels of abstr
 
 Status: partially implemented.
 
+---
+
+=== KitchenSpeak (DSL)
+
+An experimental, formally-verified orchestration *DSL* for the domestic
+kitchen, used as a teaching vehicle for advanced type theory (linearity,
+session/choreographic types, refinement types, effect systems, postulated
+oracles). Programs translate culinary expert intent into machine-executable
+appliance actions while a seven-type system keeps them physically and
+digitally safe.
+
+Its invariant: every ingredient is consumed exactly once, every loop
+terminates on a wall-clock bound, and every physical step is witnessed by a
+local sensor. Development leads with proofs (Agda) per the language's
+`ROADMAP.adoc`.
+
+Status: specification stable at v1.0; proof library commenced (Dough,
+Poached Egg), toolchain in progress. Maintained as the standalone
+`hyperpolymath/kitchenspeak` repository.
+
 == Common Principles
 
 Across these languages:

kitchenspeak/.gitignore

@@ -0,0 +1,48 @@
+# SPDX-License-Identifier: MPL-2.0
+# RSR-compliant .gitignore
+
+# OS & Editor
+.DS_Store
+Thumbs.db
+*.swp
+*.swo
+*~
+.idea/
+.vscode/
+
+# Agda
+*.agdai
+/proofs/agda/_build/
+/_build/
+.agda-stash
+
+# Build
+/target/
+/build/
+/dist/
+/out/
+
+# OCaml / dune (future front end)
+/_opam/
+*.install
+*.merlin
+
+# Rust (future LSP/DAP)
+# Cargo.lock  # keep for binaries
+
+# Secrets
+.env
+.env.*
+*.pem
+*.key
+secrets/
+
+# Logs / temp
+*.log
+/logs/
+/tmp/
+*.tmp
+*.bak
+
+# asdf version manager
+.tool-versions

kitchenspeak/CHANGELOG.adoc

@@ -0,0 +1,38 @@
+// SPDX-License-Identifier: MPL-2.0
+= KitchenSpeak Changelog
+:icons: font
+
+All notable changes to the KitchenSpeak DSL.
+
+== Unreleased
+
+=== Added
+
+* Elevated KitchenSpeak from an in-tree directory of `nextgen-languages`
+  to a standalone canonical repository (ADR 0002).
+* `ROADMAP.adoc` — proofs-first plan to reach AffineScript toolchain
+  parity.
+* `proofs/agda/PoachedEgg.agda` — second core-library proof; lowers the
+  poached-egg worked example and discharges the first Tropical
+  refinement obligation (no-binary-overheat envelope) alongside Linear
+  and Echo.
+* `proofs/Makefile` and `proofs/agda/kitchenspeak.agda-lib` — proof
+  build harness (`make -C proofs`).
+* Standalone-repo scaffolding: `README.adoc`, `LICENSE`, `.gitignore`,
+  this changelog.
+
+== v1.0 — Specification (class deliverable)
+
+=== Added
+
+* `SPEC.adoc` — class v1.0 specification, reproduced verbatim.
+* `grammar.ebnf` — class grammar (Section A) plus three marked additive
+  patches (Section B).
+* `COMMENTARY.adoc` — type-theoretic companion mapping the seven types
+  onto standard foundations.
+* `examples/poached-egg.ks` — the minimal Linear + Tropical + Echo
+  worked example.
+* `decisions/0001-proof-assistant.adoc` — ADR selecting Agda for v1.0,
+  Lean 4 reserved as successor.
+* `proofs/agda/Dough.agda` — first proof (Linear + Dyadic +
+  Choreographic + Echo).