Elevate KitchenSpeak toward standalone repo; commence proofs-first work

Prepare KitchenSpeak's elevation from an in-tree directory to its own
canonical repository (matching every sibling language), list it as a DSL
in the monorepo README/EXPLAINME, and commence the roadmap to bring it to
AffineScript-level toolchain parity — leading with proofs.

Standalone-repo scaffolding under kitchenspeak/:
- README.adoc (standalone), LICENSE (Palimpsest/MPL-2.0), .gitignore,
  CHANGELOG.adoc
- ROADMAP.adoc: proofs-first plan to AffineScript parity, with a
  per-axis parity scorecard
- decisions/0002: ADR recording the elevation

Proofs commenced (Phase 1):
- proofs/agda/PoachedEgg.agda: lowers examples/poached-egg.ks; discharges
  termination, on_fail totality, echo-witness extraction, and the first
  Tropical refinement (no-binary-overheat 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
- scripts/elevate-kitchenspeak.sh: runnable final elevation step
  (create repo + git subtree split + convert to submodule). Split out
  because repo creation needs permissions/network this session lacked.

Author: claude

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.
 

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).