docs: register KitchenSpeak in LANGUAGES.a2ml, Intentfile, Mustfile

.machine_readable/LANGUAGES.a2ml

@@ -4,8 +4,8 @@
 # LANGUAGES.a2ml — Migrated from LANGUAGES.scm
 
 [metadata]
-version = "0.1.0"
-last-updated = "2026-03-16"
+version = "0.1.1"
+last-updated = "2026-06-02"
 migrated-from = "LANGUAGES.scm"
 
 [content]
@@ -383,3 +383,26 @@ migrated-from = "LANGUAGES.scm"
 # - )))
 # - The eight languages span a complete spectrum:
 # - )))
+
+# =============================================================================
+# Structured language registry — supersedes the commented s-expression content
+# above (legacy, retained for historical reference; do not parse).
+# Add new entries here as [languages.<name>].
+# =============================================================================
+
+[languages.kitchenspeak]
+name = "KitchenSpeak"
+kind = "Orchestration DSL"
+status = "proofs-first"
+phase = "Phase 1 (Dough + PoachedEgg proofs; EchoBridge smoke-test)"
+location = "kitchenspeak/"
+standalone-repo = "hyperpolymath/kitchenspeak"
+standalone-repo-status = "pending — run scripts/elevate-kitchenspeak.sh"
+proof-assistant = "Agda 2.6.4+"
+stdlib-min = "standard-library 2.3+"
+extra-deps = ["echo-types", "absolute-zero"]
+types = ["Tropical", "Linear", "Choreographic", "Echo", "Dyadic", "Ceremonial", "Primitive"]
+invariant = "Agda-Proven — proofs lead implementation"
+adrs = ["0001-proof-assistant", "0002-elevation", "0003-echo-types-dep", "0004-echo-attaches-to-linear-dyadic"]
+echo-attachment = "B-now (Linear/Dyadic consumption); C-later (full Echo fiber); A-shim (Bool bridge, non-canonical)"
+added = "2026-06-02"

contractiles/intend/Intentfile.a2ml

@@ -10,6 +10,23 @@ Declared intent and purpose for Nextgen Languages.
 
 Nextgen Languages — *Parent repository for tracking and coordinating experimental language development*
 
+Current language family:
+
+| Language / DSL | Kind | Proof status |
+|---|---|---|
+| AffineScript (Solo / Duet / Ensemble) | General-purpose, affine-typed | Concept v0.1 |
+| KitchenSpeak | Orchestration DSL, 7 types, Agda-proven | Proofs-first (Phase 1) |
+| Betlang | Experimental | Concept |
+| Ephapax | Experimental | Concept |
+| Phronesis | Ethical AI specification DSL | Concept v0.1 |
+| Eclexia | Resource-first DSL | Concept v0.1 |
+| Oblíbený | Secure-enclave DSL | Concept v0.1 |
+| Anvomidav | Hard real-time DSL | Concept v0.1 |
+| WokeLang | Human-centric DSL | Concept v0.1 |
+
+KitchenSpeak is the only member of the family with active Agda proof work
+(proofs lead implementation — the Agda-Proven invariant per ADR 0001).
+
 ## Anti-Purpose
 
 This project is NOT:

contractiles/must/Mustfile.a2ml

@@ -24,6 +24,33 @@ that MUST hold at all times.
 - run: test -f README.adoc || test -f README.md
 - severity: critical
 
+## KitchenSpeak
+
+### agda-proven-invariant
+- description: KitchenSpeak proofs directory must exist (proofs lead implementation)
+- run: test -d kitchenspeak/proofs/agda
+- severity: critical
+
+### kitchenspeak-lib-declared
+- description: kitchenspeak.agda-lib must declare echo-types dependency
+- run: grep -q 'echo-types' kitchenspeak/proofs/agda/kitchenspeak.agda-lib
+- severity: critical
+
+### kitchenspeak-postulates-annotated
+- description: All Agda postulates must be preceded by -- AXIOM: comment (trusted-base governance)
+- run: "! grep -n '^postulate' kitchenspeak/proofs/agda/*.agda | grep -v 'AXIOM' || true"
+- severity: warning
+
+### kitchenspeak-proof-needs-present
+- description: PROOF-NEEDS.md must enumerate postulate trusted base
+- run: test -f kitchenspeak/proofs/PROOF-NEEDS.md
+- severity: critical
+
+### kitchenspeak-adr-echo-attachment
+- description: ADR 0004 (Echo attaches to Linear/Dyadic) must be present
+- run: test -f kitchenspeak/decisions/0004-echo-attaches-to-linear-dyadic.adoc
+- severity: critical
+
 ## Banned
 
 ### no-hardcoded-paths