chore(governance): add missing estate pieces — Dust/Bust contractiles, bot_directives trio, self-validating k9 set

Inventory of PR #185's estate supply found three gaps; this fills them:

- contractiles/Dustfile.a2ml: TOML-A2ML, ports the full content of the
  pre-estate root contractiles/Dustfile.a2ml (deleted by #185) into the
  flat layout; cleanup/hygiene/reversibility sections populated from
  repo reality (not-applicable keys carry explicit reasons).
- contractiles/Bustfile.a2ml: no bust reference exists anywhere in the
  estate; written fully from repo-true gates (All/Smoke suite,
  kernel-guard, guardrails, append-only history, proof-debt exceptions).
- bot_directives/{README.adoc,hypatia.a2ml,gitbot-fleet.a2ml,
  git-private-farm.a2ml}: net-new trio per the estate standard;
  accepted-findings mirror .hypatia-ignore rationales + PR #156/#172
  adjudications; propagation disabled (no instant-sync.yml).
- self-validating/: shared k9 template set copied from the
  nextgen-typing reference (maa-framework precedent), adapted only in
  repo-identity fields; examples point at the real build commands.

All new .a2ml files tomllib-verified. nickel binary unavailable;
k9 .ncl files syntax-checked by eye against the reference set.

Author: claude

.machine_readable/bot_directives/README.adoc

@@ -0,0 +1,38 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+= Bot directives — echo-types
+:toc:
+
+== Purpose
+
+Per-repo directives for automated agents operating on
+`hyperpolymath/echo-types`. These files tell bots what this repository
+considers safe, what is forbidden, and which findings are already
+adjudicated, so automated runs do not relitigate settled decisions or
+touch protected surfaces.
+
+== Precedence
+
+. Maintainer instruction (see `MAINTAINERS.adoc`) — always wins.
+. These directives.
+. Bot built-in defaults.
+
+== Scope
+
+These directives apply to:
+
+* the *Hypatia* scanner (`hypatia.a2ml` — scanner config pointers and
+  accepted findings with reasons);
+* the *gitbot fleet* (`gitbot-fleet.a2ml` — fleet roster, branch policy,
+  never-touch paths, per-bot constraints);
+* *.git-private-farm propagation* (`git-private-farm.a2ml` — propagation
+  is currently disabled here; the file records the contract for if/when
+  an `instant-sync.yml` workflow is added).
+
+== Repo-specific ground rules (summary)
+
+* This is a proof repository: `proofs/`, `tutorial/`, `All.agda`,
+  `Smoke.agda`, and `.github/workflows/agda.yml` are bot-off-limits.
+* CI green precedes merge; bots never auto-merge and never delete
+  branches.
+* Escalation channel is an issue, not PR-comment spam.

.machine_readable/bot_directives/git-private-farm.a2ml

@@ -0,0 +1,31 @@
+# SPDX-License-Identifier: MPL-2.0
+# git-private-farm.a2ml — .git-private-farm propagation directives for
+# echo-types. Net-new at the 2026-06-12 governance checkpoint per the
+# estate bot_directives standard.
+
+[metadata]
+repo = "echo-types"
+last-updated = "2026-06-12"
+owner = "hyperpolymath"
+
+[propagation]
+enabled = false
+# echo-types has NO .github/workflows/instant-sync.yml as of 2026-06-12
+# (workflows present: agda, codeql, governance, hypatia-scan, mirror,
+# scorecard, secret-scanner). The keys below record the estate contract
+# that applies if/when the workflow is added.
+workflow = ".github/workflows/instant-sync.yml"   # absent; enabled = false until it exists
+target = "hyperpolymath/.git-private-farm"
+event-type = "propagate"
+secret = "FARM_DISPATCH_TOKEN"                    # secret NAME only; value lives in repo secrets
+presence-gated = false                            # no workflow present, so no gate exists yet; gate it on addition
+
+[never-propagate]
+items = [
+  "secrets",
+  "unmerged branches",
+  "work-in-progress",
+]
+
+[on-token-rotation]
+command = "gh secret set FARM_DISPATCH_TOKEN --repo hyperpolymath/echo-types"   # name only; paste the new value when prompted

.machine_readable/bot_directives/gitbot-fleet.a2ml

@@ -0,0 +1,62 @@
+# SPDX-License-Identifier: MPL-2.0
+# gitbot-fleet.a2ml — gitbot fleet directives for echo-types.
+# Net-new at the 2026-06-12 governance checkpoint per the estate
+# bot_directives standard.
+
+[metadata]
+repo = "echo-types"
+last-updated = "2026-06-12"
+owner = "hyperpolymath"
+
+[fleet]
+bots = ["rhodibot", "echidnabot", "sustainabot", "glambot", "seambot", "finishbot"]
+
+[fleet.roles]
+rhodibot = "git operations"
+echidnabot = "code quality"
+sustainabot = "dependency updates"
+glambot = "documentation"
+seambot = "integration"
+finishbot = "task completion"
+
+[branch-policy]
+working-branch-pattern = "<bot>/<topic>"     # human sessions use session/<topic>; bots use their own prefix
+draft-PRs-only = true
+ci-green-before-merge = true                 # repo-level discipline: admin-merge-before-CI-green is a recorded anti-pattern (CLAUDE.md, PR #133 note)
+never-touch = [
+  ".claude/CLAUDE.md",
+  "CLAUDE.md",
+  "proofs/",
+  "tutorial/",
+  "*.agda",
+  ".github/workflows/agda.yml",
+  "docs/retracted/",
+]
+
+# ============================================================
+# Per-bot constraints where this repo gives specific reason;
+# defaults apply otherwise.
+# ============================================================
+
+[per-bot.rhodibot]
+deny = ["force-push to main", "branch deletion", "history rewrites"]
+note = "History is append-only here; superseded docs get SUPERSEDED banners, reverts are git-revert."
+
+[per-bot.echidnabot]
+deny = ["editing proof code", "introducing postulates", "weakening --safe --without-K"]
+note = "Code quality in this repo is gated by the Agda typechecker + scripts/kernel-guard.sh + tools/check-guardrails.sh; the only sanctioned postulates are the enumerated proof-debt module (docs/proof-debt.md)."
+
+[per-bot.sustainabot]
+allow = ["GitHub Actions group bumps (precedent: PRs #179 and the codeql-action bump)"]
+deny = ["bumping the Agda or agda-stdlib pins without a green full-suite run"]
+note = "CI installs agda-stdlib v2.3 (see .github/workflows/agda.yml); the proof suite is the compatibility gate."
+
+[per-bot.glambot]
+deny = ["resurrecting anything under docs/retracted/", "moving claims past the R-2026-05-18 narrowings"]
+note = "Docs are AsciiDoc by convention (README.md is the GitHub-render exception and the canonical README after the 2026-06-12 dedup). Honest labels (Landed/Partial/Open) per CLAUDE.md."
+
+[per-bot.seambot]
+note = "Cross-repo bridge edits follow docs/echo-types/cross-repo-bridge-status.md; bridge stubs are NARROW by design (META adr-011) — do not widen scope mechanically."
+
+[per-bot.finishbot]
+note = "Task completion must respect the repo's gate ledger (docs/echo-types/earn-back-plan.adoc, roadmap-gates.adoc); gates pass only with explicit ledger entries, never silently."

.machine_readable/bot_directives/hypatia.a2ml

@@ -0,0 +1,74 @@
+# SPDX-License-Identifier: MPL-2.0
+# hypatia.a2ml — Hypatia scanner directives for echo-types.
+# Net-new at the 2026-06-12 governance checkpoint per the estate
+# bot_directives standard.
+
+[metadata]
+repo = "echo-types"
+last-updated = "2026-06-12"
+owner = "hyperpolymath"
+
+[scanner]
+ignore-file = ".hypatia-ignore"   # present at repo root; each entry carries a verified-false-positive rationale
+workflow = ".github/workflows/hypatia-scan.yml"
+
+# ============================================================
+# Accepted findings (known false positives / adjudicated advisories).
+# Each entry mirrors an in-repo rationale; do not re-raise these.
+# ============================================================
+
+[[accepted-findings]]
+rule = "code_safety/agda_postulate"
+path = "proofs/agda/Smoke.agda"
+status = "verified-false-positive"
+reason = """
+The rule is a naive \\bpostulate\\b regex over raw file content that does
+not strip comments. The only 'postulate' tokens in Smoke.agda are in
+comments documenting the suite's postulate-free discipline; there is no
+postulate declaration. The repo's own guardrail (tools/check-guardrails.sh)
+strips comments before checking and is the real gate. Suppressed in
+.hypatia-ignore with full rationale.
+"""
+
+[[accepted-findings]]
+rule = "code_safety/js_http_url_in_code"
+path = "tools/banner/build-banner.mjs"
+status = "verified-false-positive"
+reason = """
+The flagged http:// is the SVG XML namespace identifier
+xmlns="http://www.w3.org/2000/svg" — a constant namespace URI never
+dereferenced over the network; changing it to https would be semantically
+wrong and break SVG handling. Not CWE-319. Suppressed in .hypatia-ignore.
+"""
+
+[[accepted-findings]]
+rule = "code_safety/agda_postulate"
+path = "proofs/agda (Exploratory cohort)"
+status = "scope-narrowed"
+reason = """
+The agda_postulate alert on the Exploratory module was scope-narrowed via
+inline allow in PR #156. The four propositional-truncation postulates in
+proofs/agda/EchoImageFactorizationPropPostulated.agda are enumerated
+proof debt under Disposition (c) NECESSARY AXIOM (docs/proof-debt.md,
+PR #172); the module is isolated and not imported by All.agda/Smoke.agda.
+"""
+
+[[accepted-findings]]
+rule = "workflow hardening (general)"
+path = ".github/workflows/"
+status = "resolved-at-source"
+reason = """
+PR #178 hardened CI workflows and resolved the then-outstanding Hypatia
+findings at source rather than by suppression. New findings in workflows
+should be fixed at source in the same spirit, not added here.
+"""
+
+# ============================================================
+# Prohibited actions
+# ============================================================
+
+[prohibited-actions]
+auto-delete-branches = false
+auto-merge = false
+modify-workflows = false
+escalation = "open an issue, do not spam PR comments"

.machine_readable/contractiles/Bustfile.a2ml

@@ -0,0 +1,100 @@
+# SPDX-License-Identifier: MPL-2.0
+# Bustfile.a2ml — breakage contract for echo-types: what counts as a
+# busted state, how it is detected, and how to respond.
+#
+# Format: TOML-A2ML (parses with tomllib; `#` comments, [section], key = "value")
+#
+# Provenance: the flat-contractile completion of the estate layout
+# (PR #185 supplied Adjustfile/Intentfile/Justfile/Mustfile/Trustfile but
+# no Bustfile, and no nested bust/ contractile ever existed in this repo
+# or its visible siblings). Written fully from repo-true obligations on
+# 2026-06-12: the busted-state definitions, detection commands, and
+# response ladder below are the repo's own existing gates (Agda suite,
+# kernel-guard, guardrail scripts, CI workflows), not new policy.
+
+[bustfile]
+version = "1.0.0"
+format = "a2ml"
+repo = "echo-types"
+last-updated = "2026-06-12"
+
+# ============================================================
+# Busted-state definition (any one of these means the repo is busted)
+# ============================================================
+
+[definition]
+busted-states = [
+  "proofs/agda/All.agda fails to typecheck under --safe --without-K",
+  "proofs/agda/Smoke.agda fails to typecheck (a pinned headline theorem broke)",
+  "a postulate appears outside the enumerated proof-debt module (docs/proof-debt.md: proofs/agda/EchoImageFactorizationPropPostulated.agda)",
+  "scripts/kernel-guard.sh fails (kernel/derived classification drift)",
+  "tools/check-guardrails.sh fails (guardrail policy violation)",
+  "a retracted claim from docs/retractions.adoc reappears in canonical docs",
+  "main is red on the agda / governance / hypatia-scan workflows",
+]
+
+# ============================================================
+# Detection (run these to decide whether the repo is busted)
+# ============================================================
+
+[[detection]]
+name = "full-suite"
+doc = "The verified suite: every module imported by All.agda typechecks."
+run = "agda -i proofs/agda proofs/agda/All.agda"
+severity = "critical"
+
+[[detection]]
+name = "smoke-pins"
+doc = "Every headline theorem pinned via `using` clauses still exists."
+run = "agda -i proofs/agda proofs/agda/Smoke.agda"
+severity = "critical"
+
+[[detection]]
+name = "kernel-guard"
+doc = "Kernel-vs-derived module classification is consistent (docs/echo-types/echo-kernel-note.adoc)."
+run = "scripts/kernel-guard.sh"
+severity = "high"
+
+[[detection]]
+name = "guardrails"
+doc = "Repo guardrail checks (incl. comment-stripping postulate check, the real postulate gate)."
+run = "tools/check-guardrails.sh"
+severity = "high"
+
+[[detection]]
+name = "no-unsafe"
+doc = "No unsafe escape hatches outside the documented exceptions."
+run = "scripts/check-no-unsafe.sh"
+severity = "high"
+
+# ============================================================
+# Response ladder (in order; stop at the first step that restores green)
+# ============================================================
+
+[response]
+step-1 = "Do not merge anything while a critical detection fails on main; CI green precedes merge (admin-merges before CI green are a known anti-pattern in this repo's history — see CLAUDE.md PR #133 note)."
+step-2 = "If the breakage is uncommitted local work: run the Dustfile source-rollback task (git checkout HEAD -- .) and clean-build, then re-run detection."
+step-3 = "If the breakage landed on a branch: fix forward on that branch or close it as superseded at the next rung consolidation; never force-push over another session's work without re-fetching first."
+step-4 = "If the breakage landed on main: git revert the offending commit (history is append-only; no force-push to main)."
+step-5 = "Record the incident: open an issue with the failing command + output; if a proof rung was lost, note it in the session ledger per the CLAUDE.md rung-consolidation policy."
+
+[escalation]
+owner = "hyperpolymath"
+contact = "MAINTAINERS.adoc"
+bot-rule = "automated agents open an issue and stop; they do not auto-revert main, do not auto-merge fixes, and do not spam PR comments"
+
+# ============================================================
+# Known exceptions (NOT busted states; do not 'fix' these)
+# ============================================================
+
+[[known-exceptions]]
+name = "proof-debt-postulates"
+detail = "The four propositional-truncation postulates in proofs/agda/EchoImageFactorizationPropPostulated.agda are enumerated proof debt under Disposition (c) NECESSARY AXIOM (docs/proof-debt.md, PR #172). The module is isolated, guardrail-exempt by design, and not imported by All.agda or Smoke.agda."
+
+[[known-exceptions]]
+name = "hypatia-verified-false-positives"
+detail = "The entries in .hypatia-ignore (agda_postulate on Smoke.agda comments; the SVG xmlns http:// constant in tools/banner/build-banner.mjs) are verified false positives with in-file rationale; see bot_directives/hypatia.a2ml."
+
+[[known-exceptions]]
+name = "ordinal-track-open-gates"
+detail = "Ordinal-track Gate 1 (tail-rank-equality discharge, CHECKED-REFUTED unblock routes per PR #146) and Gate 3 (Path-4+ extensions) are documented OPEN work, not breakage. See STATE [blockers]."

.machine_readable/contractiles/Dustfile.a2ml

@@ -0,0 +1,76 @@
+# SPDX-License-Identifier: MPL-2.0
+# Dustfile.a2ml — cleanup, hygiene & recovery contract for echo-types
+#
+# Format: TOML-A2ML (parses with tomllib; `#` comments, [section], key = "value")
+#
+# Provenance: the flat-contractile completion of the estate layout
+# (PR #185 supplied Adjustfile/Intentfile/Justfile/Mustfile/Trustfile but
+# no Dustfile). The [[tasks]] entries below PORT the full content of the
+# pre-estate root `contractiles/Dustfile.a2ml` (S-expression form,
+# deleted by PR #185); section shape follows the estate dust reference
+# (nextgen-languages contractiles/dust/Dustfile.a2ml). Added 2026-06-12.
+
+[dustfile]
+version = "1.0.0"
+format = "a2ml"
+repo = "echo-types"
+last-updated = "2026-06-12"
+
+# ============================================================
+# Recovery & rollback tasks (ported from the pre-estate root Dustfile)
+# ============================================================
+
+[[tasks]]
+name = "source-rollback"
+doc = "Revert all source changes to last commit."
+tag = "rollback"
+cmd = "git checkout HEAD -- ."
+
+[[tasks]]
+name = "clean-build"
+doc = "Remove all build artifacts (Agda .agdai files)."
+tag = "clean"
+cmd = "find proofs -name '*.agdai' -delete"
+
+[[tasks]]
+name = "resync-from-template"
+doc = "Re-run scaffold-component.{py,my} to restore drifted boilerplate."
+tag = "scaffold"
+cmd = "echo 'Manual: run scaffold-component for echo-types resync.'"
+
+# ============================================================
+# Cleanup policy
+# ============================================================
+
+[cleanup]
+build-artifacts = "Agda interface files (*.agdai) under proofs/ and tutorial/; never committed (.gitignore); removed by the clean-build task"
+generated-dirs = "_build/ is gitignored (commit 9c00087); safe to delete at any time"
+stale-branch-policy = "session/* and consolidation branches are enumerated and dispositioned (landing / superseded / abandoned) at each rung consolidation, per the CLAUDE.md rung-consolidation policy; bots never delete branches"
+artifact-retention = "not-applicable"
+artifact-retention-reason = "echo-types publishes no build artifacts; the proof suite is re-checked from source on every CI run"
+cache-policy = "CI caches the Agda toolchain + stdlib only; cache invalidation follows .github/workflows/agda.yml"
+
+# ============================================================
+# Hygiene
+# ============================================================
+
+[hygiene]
+proof-hygiene = "agda All.agda + Smoke.agda must exit 0 under --safe --without-K; zero postulates outside the enumerated proof-debt module (docs/proof-debt.md)"
+guardrails = "tools/check-guardrails.sh + scripts/kernel-guard.sh are the repo-native hygiene gates; scripts/check-no-unsafe.sh supplements"
+dead-code-rule = "modules that compile but are not imported by proofs/agda/All.agda are treated as dead code (CLAUDE.md working rules)"
+todo-tracking = "inline TODOs on the ordinal track are slice-scoped and tracked in the obstruction docs (docs/echo-types/buchholz-rank-obstruction.adoc); repo-wide notes go to issues"
+linting = "not-applicable"
+linting-reason = "no general-purpose linter for Agda; the typechecker + guardrail scripts fill the role"
+formatting = "not-applicable"
+formatting-reason = "no enforced Agda formatter; .editorconfig + .gitattributes (LF, .agdai binary) carry the file-hygiene load"
+
+# ============================================================
+# Reversibility
+# ============================================================
+
+[reversibility]
+backup-before-destructive = true
+rollback-mechanism = "git-revert (history is append-only; superseded docs get SUPERSEDED banners rather than deletion, per STATE standing-decision sd-006)"
+retracted-content-policy = "retractions are recorded in docs/retractions.adoc + docs/retracted/ and are never silently resurrected (R-2026-05-18 discipline)"
+data-retention-policy = "not-applicable"
+data-retention-reason = "echo-types holds no runtime data; everything reproducible is derived from source under version control"