docs(machine-readable): bring echo-types governance scaffold to estate standard

echo-types had only 6a2/ — add the full estate scaffold (modelled on nextgen-typing;
content from CLAUDE.md + roadmap-gates + the cross-repo bridge ledger), keeping
echo-types' committed Guile-Scheme house style for the 6a2 set (no schema drift):
- anchors/ANCHOR.a2ml — clade uuid/primary/assigned = 'TODO: assign via gv-clade-index
  registry' (NOT fabricated); trust/Trustfile asserts the clade stays TODO until assigned.
- contractiles/ README + must/trust/dust/bust (harmonised with the root contractiles/).
- svc/k9/ README + methodology-guard + kennel/yard/hunt templates + 3 examples.
- agent_instructions/ README + methodology/coverage/debt.
- integrations/ echotypes-jl, arghda-core, panll, groove, verisim.
- bot_directives/ hypatia/gitbot-fleet/git-private-farm (no fabricated tokens).
- 0-AI-MANIFEST + 6a2 STATE/META/ECOSYSTEM refreshed; EI-2 record preserved.

FLAG: echo-types has NO clade assigned — needs a gv-clade-index registry assignment.

https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7

Author: claude

.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -15,13 +15,21 @@
 ;;;
 ;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+;;;
+;;; NOTE (refreshed 2026-06-12): `panll-constellation` and
+;;; `companion-and-bridge-projects` blocks added at the END to record the
+;;; concrete hyperpolymath / PanLL ecosystem position from CLAUDE.md and
+;;; docs/bridges/cross-repo-bridge-status.md (2026-06-02). The generic
+;;; sibling-projects block above is retained as historical context.
 
 (define-module (echo-types ecosystem)
   #:export (constellation-membership
             schema-dependencies
             sibling-projects
             cross-repo-conventions
-            integrity-checks))
+            integrity-checks
+            panll-constellation
+            companion-and-bridge-projects))
 
 ;;; ============================================================
 ;;; Constellation membership
@@ -155,6 +163,75 @@
      (current-status . pass)
      (verification . "Cross-checked at last update."))))
 
+;;; ============================================================
+;;; PanLL constellation position (refreshed 2026-06-12)
+;;; Sourced from CLAUDE.md "Ecosystem context".
+;;; ============================================================
+
+(define panll-constellation
+  '((node . "echo-types")
+    (role . "Foundational formal-verification library: constructive Agda formalisation of fiber-based structured loss. A theoretical artefact and downstream consumer of HoTT + category-theoretic concepts; not a runtime component of any HTI.")
+    (neighbours
+     (((name . "PanLL")
+       (one-line . "Three-pane cognitive-relief HTI; Ambient / Symbolic / Neural / World panes.")
+       (repo . "github.com/hyperpolymath/panll")
+       (relation . "Top-level interface consumer of the constellation; echo-types is a foundation it can cite, not a build dependency."))
+      ((name . "Gossamer")
+       (one-line . "Zig + WebKitGTK webview shell used by PanLL (~5 MB binary).")
+       (relation . "PanLL presentation substrate; no echo-types dependency."))
+      ((name . "Burble")
+       (one-line . "Self-hostable voice-comms platform; Zig SIMD audio, IEEE-1588 PTP sync, browser-based, configurable topology.")
+       (relation . "PanLL team-replication service alongside Gossamer; no echo-types dependency."))
+      ((name . "Ephapax")
+       (one-line . "Programming language with a linear type system guaranteeing WASM memory safety (compile-time no use-after-free / no leaks).")
+       (repo . "github.com/hyperpolymath/ephapax")
+       (relation . "ACTIVE BRIDGE — EchoEphapaxBridge.agda (L3, content bridge NARROW); ephapax/formal/Echo.v ports EchoLinear + EchoResidue under a K-free zero-axiom discipline."))
+      ((name . "VeriSim / VeriSimDB")
+       (one-line . "Identity-state capture with filesystem fallback; VCL-total is its next-gen interaction language (10 levels of type safety).")
+       (relation . "Constellation database / state layer; potential consumer, no current echo-types dependency."))
+      ((name . "Groove protocol")
+       (one-line . "HTTP-based service-discovery; capabilities announce themselves for automatic detection + integration.")
+       (relation . "Constellation snap-on/snap-off discovery mechanism; echo-types exposes no service yet (port unassigned)."))
+      ((name . "Echidna (hyperpolymath)")
+       (one-line . "Planned high-assurance interface verification. NOT the Ethereum fuzzer of the same name.")
+       (relation . "Conceptual sibling — broader prover ecosystem; exact repo still to confirm."))))))
+
+;;; ============================================================
+;;; Companion + bridge projects (refreshed 2026-06-12)
+;;; Concrete, verifiable from the cross-repo bridge ledger.
+;;; ============================================================
+
+(define companion-and-bridge-projects
+  '(((name . "EchoTypes.jl")
+     (repo . "github.com/hyperpolymath/EchoTypes.jl")
+     (kind . executable-companion)
+     (version . "0.2.0 (pinned to commit e7dded6)")
+     (relation . "Executable Julia companion mirroring the finite-domain shadow of the Tier-1+Tier-2 spine + the unconditional F5 OFS fragment. Falsifies-by-counterexample on concrete data; makes NO proof claims — the Agda here remains the source of truth. R-2026-05-18 retracted surface + funext-qualified F5 clauses NOT mirrored.")
+     (registry . "julia-professional-registry")
+     (ci-coupling . "none in either direction"))
+
+    ((name . "arghda-core")
+     (repo . "github.com/hyperpolymath/arghda-core")
+     (kind . extracted-tool)
+     (relation . "Language-agnostic proof-workspace engine (triage folders inbox→working→proven/rejected, linter, DAG view). Extracted from echo-types 2026-05-30 (see echo-types#159); the arghda-core/ subtree + cross-refs were removed from this repo (PR #160). arghda-panll (Gossamer/ReScript presentation) is planned.")
+     (motivating-pipeline . "docs/buchholz-plan.adoc appendix"))
+
+    ((name . "absolute-zero")
+     (kind . cross-prover-bridge)
+     (relation . "EchoCNOBridge.agda imports IsCNO / empty-is-cno / halt-is-cno / cno-composition / absolute-zero-is-cno / seq-comp from absolute-zero/proofs/agda/CNO.agda; content-bridge done. Cross-prover Coq/Lean4 statement alignment table drafted in cross-repo-bridge-status.md."))
+
+    ((name . "januskey")
+     (kind . name-bridge)
+     (relation . "EchoJanusBridge.agda — name-bridge only; structural-mirror to the 8-variant Idris2 OpKind ABI decided; content-bridge gated on januskey/PROOF-NEEDS.md."))
+
+    ((name . "tropical-resource-typing")
+     (kind . citation-level-alignment)
+     (relation . "EchoTropical.agda ↔ Tropical.thy / TropicalSessionTypes.lean; Agda cannot import .thy/.lean, so alignment is statement-correspondence with independent per-language proof. First pair: ⊕-idem ↔ trop_add_idem ↔ add_comm_trop + add_assoc_trop."))
+
+    ((name . "valence-shell / ochrance")
+     (kind . exploratory-downstream-consumer)
+     (relation . "Citation-level ONLY. Echo's structured-loss vocabulary (EchoResidue / EchoResidueTaxonomy / EchoLossTaxonomy / EchoObservationalEquivalence / EchoNoSectionGeneric) may classify shell state transitions; Ochránce may supply receipt evidence. Core Affect = NO: no bridge module, nothing wired into All.agda / Smoke.agda. echo-types makes no claim about their implementation correctness."))))
+
 ;;; ============================================================
 ;;; END OF ECOSYSTEM
 ;;; ============================================================

.machine_readable/6a2/META.a2ml

@@ -8,11 +8,18 @@
 ;;;
 ;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+;;;
+;;; NOTE (refreshed 2026-06-12): adr-001..adr-006 capture the EI-2 closure;
+;;; adr-007..adr-009 capture the Pillar F earn-back programme (CLOSED
+;;; 2026-05-20). The `current-practices` block at the END of this file
+;;; states the live working-rules surface for a fresh session. No ADR was
+;;; reshaped in the 2026-06-12 governance sweep.
 
 (define-module (echo-types meta)
   #:export (architecture-decisions
             development-practices
-            design-rationale))
+            design-rationale
+            current-practices))
 
 ;;; ============================================================
 ;;; Architecture Decision Records
@@ -148,6 +155,51 @@
     (why-state-not-ad-hoc-handover
      "Earlier sessions used ad-hoc handover documents (text files, conversation summaries). This session captures the termination in state-a2ml STATE.scm form so it is machine-readable, schema-validated against standards/state-a2ml/spec/abnf/state.abnf, and joins the ecosystem of *-a2ml documents the user maintains. Future Claude sessions can parse and consult it programmatically.")))
 
+;;; ============================================================
+;;; Current practices (refreshed 2026-06-12) — the live working-rules
+;;; surface. Sourced from CLAUDE.md "Working rules in this repo".
+;;; ============================================================
+
+(define current-practices
+  '((build-invariant
+     (rule . "Every edit ends with an Agda compile command and captured output.")
+     (target . "agda -i proofs/agda proofs/agda/All.agda + proofs/agda/Smoke.agda both exit 0 under --safe --without-K."))
+
+    (proof-discipline
+     (safe-without-k . "--safe --without-K throughout — mandatory, no exceptions.")
+     (no-postulates . "No postulates unless explicitly isolated and justified. Load-bearing tracks carry zero. Exploratory truncation postulates, where they exist, are enumerated in docs/proof-debt.md.")
+     (no-escape-hatches . "No believe_me / primTrustMe / primEraseEquality / sorry / Admitted / unsafeCoerce / Obj.magic anywhere.")
+     (no-funext-in-trusted-base . "funext is never a postulate; where strict forms need it (e.g. F4 / F5 strict clauses) it is taken as an explicit module parameter, isolated from the trusted base.")
+     (kernel-cone . "The funext-free kernel cone is exactly { Echo, EchoKernel }, enforced by scripts/kernel-guard.sh against docs/echo-types/echo-kernel-note.adoc."))
+
+    (smoke-and-all-discipline
+     (pin-every-headline . "Every headline theorem must be pinned in Smoke.agda via a `using` clause, under its own open-import block with a header comment.")
+     (wire-every-module . "Every new module goes into All.agda as an open import. Orphan modules that compile but are not in All.agda are treated as dead code."))
+
+    (rung-consolidation-policy
+     (when . "Each time a new proof rung lands on the composition or ordinal tracks (a named theorem or iso-shape).")
+     (steps . ("branch housekeeping; cherry-pick to a consolidation branch in dependency order"
+               "update human docs (composition.md, roadmap.adoc, overview.md, cross-repo-bridge-status.md) — sweep stale (Open)/[unblocked] tags; honest labels (Landed)/(Partial)/(Open)"
+               "update machine docs (CLAUDE.md current-rung-state + these 6a2 files)"
+               "verify All.agda + Smoke.agda exit 0; no postulates introduced"
+               "fast-forward main; session ledger records rung name + commits + remaining open pieces + smallest useful next advance")))
+
+    (naming-traps
+     (mode-graded . "ModeGraded (with trailing 'd') is canonical; proofs/agda/characteristic/ModeGrade.agda is FORBIDDEN (see STATE do-not-redo + AGENTIC G-003).")
+     (decoration-join . "Abstract join field in DecorationStructure is `join`, not `_⊔_` (avoids Level._⊔_ collision); per-decoration modules keep suffixed forms (_⊔g_, _⊔m_, _⊔a_)."))
+
+    (parallel-session-discipline
+     (rule . "Multiple Claude sessions may work the repo concurrently. Stay clear of another session's declared territory; use `--only <paths>` when both sessions must commit before sync.")
+     (admin-merge . "Ordinal-track admin-merges should wait for CI green before merging — the same gate-discipline the rest of the repo follows (lesson from PR #133/#134)."))
+
+    (estate-conventions
+     (license . "MPL-2.0 for code and docs (CC-BY-4.0 on some prose docs); SPDX header on every file.")
+     (forge . "GitHub canonical; GitLab + Codeberg as read-only mirrors (sd-003 / adr-005).")
+     (docs . "AsciiDoc preferred over Markdown (README.md is the GitHub-render exception).")
+     (config . "Nickel/CUE/Dhall preferred over YAML (YAML only where GitHub Actions forces it).")
+     (containers . "Containerfile (Podman), never Dockerfile; base images @sha256-pinned.")
+     (build-driver . "Justfile (not Makefile); flake.nix + stapeln.toml present."))))
+
 ;;; ============================================================
 ;;; END OF META
 ;;; ============================================================

.machine_readable/6a2/STATE.a2ml

@@ -12,6 +12,13 @@
 ;;; concluded; the verdict is negative; the documentation cascade has been
 ;;; applied; the recipe is no longer a candidate locus of distinctness.
 ;;;
+;;; NOTE (refreshed 2026-06-12): the original body of this file is the EI-2
+;;; termination capture (2026-04-29). It is PERMANENT RECORD and is referenced
+;;; by AGENTIC gates G-001/G-005 and by Trustfile check `ei-2-record-intact`.
+;;; Do not delete it. The `current-state` block at the END of this file brings
+;;; the project's three active workstreams up to current reality without
+;;; disturbing the historical record.
+;;;
 ;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
@@ -24,7 +31,10 @@
             cascade-applied
             do-not-redo
             next-actions
-            forbidden-rebrandings))
+            forbidden-rebrandings
+            earn-back-summary
+            theory-work-summary
+            current-state))
 
 ;;; ============================================================
 ;;; Project identity
@@ -353,6 +363,89 @@
         (example-10-abstract-interp    . "EchoExampleAbsInt.agda (PR #82)")
         (example-6-numeric             . "still unblocked, only remaining example item")))))
 
+;;; ============================================================
+;;; Current state (refreshed 2026-06-12) — the three active
+;;; workstreams. Sourced from CLAUDE.md rung-state + roadmap-gates.adoc
+;;; + docs/bridges/cross-repo-bridge-status.md (2026-06-02).
+;;; ============================================================
+;;;
+;;; This block is the up-to-date status surface. The EI-2 record above
+;;; is permanent history; this block is the living state. Honest labels
+;;; are (landed) / (partial) / (open) per the rung-consolidation policy.
+
+(define current-state
+  '((as-of . "2026-06-12")
+    (one-line . "Constructive Agda formalisation of fiber-based structured loss (\"echo types\"): Echo f y := Σ (x : A) , (f x ≡ y). --safe --without-K throughout; zero postulates in load-bearing tracks; gated identity-claim development.")
+    (build-invariant
+     . "agda -i proofs/agda proofs/agda/All.agda and proofs/agda/Smoke.agda both exit 0 under --safe --without-K. Every headline theorem pinned in Smoke.agda via a `using` clause; every module wired into All.agda. scripts/kernel-guard.sh PASS.")
+    (toolchain
+     . ((agda . ">= 2.6.3")
+        (stdlib . ">= 2.3 (CI installs v2.3)")
+        (ci-workflow . ".github/workflows/agda.yml")))
+
+    (workstreams
+     ((composition-track
+       (doc . "Echo.agda + docs/echo-types/{composition,fibration-package,universal-property}.adoc")
+       (status . landed)
+       (highlights
+        . ("Base accumulation iso Echo-comp-iso (packaged _↔_)"
+           "Cancellation iso cancel-iso parameterised by s-left/s-right + both triangle identities (PR #25)"
+           "Pentagon coherence complete: Echo-comp-iso-pent-{B,echo} as refl; full Σ-associativity iso Echo-comp-pent-Σ-assoc packaged via stdlib Function.Bundles._↔_")))
+
+      (ordinal-track
+       (doc . "docs/echo-types/buchholz-plan.adoc + buchholz-rank-obstruction.adoc")
+       (status . partial)
+       (target . "Bachmann–Howard ψ₀(Ω_ω) as first credible milestone; stretch ψ(Ω_Ω) ≈ TFBO")
+       (highlights
+        . ("E1–E7 landed (OT syntax, ℕ-staged closure, CNF, pedagogical ψ, Buchholz scaffold, well-formedness, echo bridge)"
+           "WfCNF restriction + limit-shaped ω-power rank: RankPow / RankPowDomination / HeadOmega / HeadOmegaInversion landed"
+           "Slice 3+4 Route A arc landed (PRs #165–#170): RankMonoUnion umbrella over source-rule extensions; well-foundedness of _<ᵇᵘ_ via rank-embedding transport (#170)"
+           "WF-0 partial Buchholz order _<ᵇ_ and WF-1 well-foundedness wf-<ᵇ landed for the admitted core"))
+       (open
+        . ("Full constructor set beyond the admitted core (K-limited shared-binder cases <ᵇ-ψα, <ᵇ-+2)"
+           "Unbudgeted _<ᵇʳᶠ_ global WF — eliminate the explicit ℕ budget from wf-<ᵇʳᶠᵇ without leaving --safe --without-K"
+           "Push the surface-route WF back into Order.agda's main _<ᵇ_ package")))
+
+      (establishment-track
+       (doc . "docs/echo-types/establishment-plan.adoc + earn-back-plan.adoc + paper.adoc + types-abstract.adoc")
+       (status . partial)
+       (thesis . "Echo characterised as a *reindexing modality of structured loss* (coeffect/quantitative lineage) — explicitly NOT the linear/dependent judgmental ladder; Echo adds no new judgment, it is definitionally fib.")
+       (highlights
+        . ("Pillars A–D internal programme COMPLETE + verified (2026-05-17): EchoFiberBridge, EchoPullback, EchoGradedComonad, EchoSeparating, EchoRelModel"
+           "Pillar F earn-back programme CLOSED (2026-05-20): F4+F2 (2026-05-18), F1+F3 (2026-05-20) — see earn-back-summary + META adr-007/008/009"
+           "Tier-1+2+3 canonical-identity spine + audience moves + EchoCanonicalIdentitySuite (2026-05-27)"
+           "R-2026-05-18 retractions discipline: five claims retracted, four earned back at honest strength, conservativity metatheorem stays retracted"))
+       (open
+        . ("Pillar E only: clear paper.adoc [EXPAND] tags (background primer landed; related-work / evaluation / ordinal consumer-evidence appendix pending — last gated on Bachmann–Howard)"
+           "THEN offline/author-driven: Zenodo DOI + installable library packaging + outreach (flag to user; do NOT auto-run)")))))
+
+    (cross-repo-bridges
+     ;; Source of truth: docs/bridges/cross-repo-bridge-status.md (2026-06-02).
+     ((cno-bridge        . "content-bridge done (EchoCNOBridge.agda ↔ absolute-zero/CNO.agda); cross-prover Coq/Lean4 alignment is the next row")
+      (janus-bridge      . "name-bridge only; structural-mirror to januskey Idris2 OpKind decided, content-bridge deferred")
+      (tropical          . "citation-level alignment (Agda cannot import .thy/.lean); first alignable pair identified")
+      (echotypes-jl      . "executable companion shipped — EchoTypes.jl v0.2.0 (pinned e7dded6); finite-domain shadow, no proof claims; Agda is source of truth")
+      (ephapax-l3        . "navigability bridge done, content bridge NARROW (EchoEphapaxBridge.agda; L3 only)")
+      (valence-ochrance  . "exploratory downstream consumer; citation-level only, NO bridge module, Core Affect = NO")))
+
+    (governance-artefacts-added
+     ;; This 2026-06-12 machine-readable / governance sweep.
+     ((6a2 . "AGENTIC/NEUROSYM/PLAYBOOK already present (Guile Scheme); STATE/META/ECOSYSTEM refreshed to current reality")
+      (anchors . "anchors/ANCHOR.a2ml created; clade assignment is a TODO (gv-clade-index registry)")
+      (contractiles . ".machine_readable/contractiles/{must,dust,bust,trust} created, harmonised with the existing root contractiles/")
+      (svc-k9 . "svc/k9 self-validation templates added")
+      (agent-instructions . "agent_instructions/{methodology,coverage,debt,README} added")
+      (integrations . "integrations/{echotypes-jl,arghda-core,panll,groove,verisim} added from real bridge facts")
+      (bot-directives . "bot_directives/{hypatia,gitbot-fleet,git-private-farm} hook directives added")
+      (wiki . "in-tree wiki/ authored: Home + Overview + Architecture + Working-Rules + Roadmap (AsciiDoc)")))
+
+    (do-not-reopen-current
+     . ("Pillars A–D internal programme (complete since 2026-05-17)"
+        "Pillar F gates F1–F4 (closed 2026-05-20; F1 via EchoGradedComonadF1, F3 via two non-iso grade-monoid instances)"
+        "the R-2026-05-18 retraction narrowings (conservativity metatheorem stays retracted)"
+        "the closed Buchholz constructor set under WfCNF + admissibility + lex-pair"
+        "EI-2 (terminated 2026-04-29; see terminated-questions above)"))))
+
 ;;; ============================================================
 ;;; END OF STATE
 ;;; ============================================================