Merge origin/main into claude/quirky-gauss-GaGZo

Resolve the single Smoke.agda aggregator conflict: keep both the
PR's RankDoubledLadder import block (Slice 1 doubled-ladder rank
foundation) and main's Slice-3 prerequisite/headline blocks. Pure
import-ordering; no proof content changed on either side.

Verified against CI-pinned deps (agda-stdlib v2.3 +
absolute-zero@3ff5cee): tools/check-guardrails.sh OK (165 modules);
`agda All.agda` and `agda Smoke.agda` both typecheck clean.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/agent_instructions/README.adoc

@@ -0,0 +1,47 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com>
+= Agent Instructions (echo-types)
+:toc: preamble
+
+Methodology-aware configuration for AI agents working on echo-types. Read by
+any AI agent (Claude, Gemini, Copilot, etc.) at session start, alongside the
+top-level `CLAUDE.md` (which carries the authoritative current-rung-state) and
+`.machine_readable/6a2/`.
+
+== Files
+
+[cols="1,3"]
+|===
+| File | Purpose
+
+| `methodology.a2ml`
+| Default mode, the proof-discipline invariants (`--safe --without-K`, zero
+  postulates, ceilings), priority weights, convergent budget, known constraints.
+
+| `coverage.a2ml`
+| Session coverage tracking — which workstreams/modules were visited, what was
+  skipped, what has open MUSTs.
+
+| `debt.a2ml`
+| Meander debt — proof obligations and chores found but not discharged, carried
+  between sessions.
+|===
+
+== How Agents Use These
+
+1. Read `CLAUDE.md` first — it has the live rung-state and the "DO NOT reopen" lists.
+2. Read `methodology.a2ml` — know mode, invariants, ceilings.
+3. Read `coverage.a2ml` and `debt.a2ml` — know what was visited and what is outstanding.
+4. At session end, update `coverage.a2ml` and `debt.a2ml`, and (on a landed rung)
+   the `CLAUDE.md` current-rung-state + the `6a2/STATE.a2ml` current-state block.
+
+== Relationship to Other Files
+
+* `6a2/AGENTIC.a2ml` says WHAT agents can do (gating, escalation, redo-traps).
+* `agent_instructions/` says HOW agents should work (methodology).
+* `bot_directives/` says what the gitbot-fleet / Hypatia does (fleet-specific).
+* `CLAUDE.md` says how Claude specifically should work (Claude-specific, authoritative state).
+
+== Reference
+
+ADR-002 in `standards/agentic-a2ml/docs/ADR-002-methodology-layer.adoc`.

.machine_readable/agent_instructions/coverage.a2ml

@@ -0,0 +1,72 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com>
+#
+# coverage.a2ml — Session coverage tracking (echo-types)
+# Updated at the end of each AI agent session.
+# Tracks which workstreams/modules were visited and which have open MUSTs.
+#
+# Reference: ADR-002 in standards/agentic-a2ml/docs/
+
+[metadata]
+version = "1.0.0"
+last-updated = "2026-06-12"
+
+# ============================================================================
+# COVERAGE STATE
+# ============================================================================
+# "Components" here = the three workstreams + the cross-repo bridge surface.
+# Authoritative per-rung detail lives in CLAUDE.md current-rung-state.
+
+[coverage]
+total-components = 4
+visited-components = 4
+coverage-percent = 100
+note = "All three workstreams + the bridge ledger have current status; the open work is named in debt.a2ml."
+
+# ============================================================================
+# VISITED COMPONENTS (workstream → last-known status)
+# ============================================================================
+
+[coverage.visited.composition-track]
+date = "2026-04-28"
+status = "landed"
+notes = "Echo-comp-iso + cancel-iso + pentagon (Echo-comp-pent-Σ-assoc) all packaged as _↔_."
+
+[coverage.visited.ordinal-track]
+date = "2026-05-30"
+status = "partial"
+notes = "Slice 3+4 Route A arc (PRs #165-#170): RankMonoUnion umbrella + wf of _<ᵇᵘ_ via rank-embedding transport (#170). Target: Bachmann-Howard."
+
+[coverage.visited.establishment-track]
+date = "2026-05-27"
+status = "partial"
+notes = "Pillars A-D complete (2026-05-17); Pillar F closed (2026-05-20); Tier-1+2+3 spine + audience moves + EchoCanonicalIdentitySuite. Pillar E open."
+
+[coverage.visited.cross-repo-bridges]
+date = "2026-06-02"
+status = "ledgered"
+notes = "cross-repo-bridge-status.md current: CNO done, Ephapax NARROW, EchoTypes.jl shipped, Janus name-only, Tropical citation-level, Valence/Ochrance exploratory."
+
+# ============================================================================
+# SKIPPED / OPEN MUSTS (P1 inputs for next session's Phase 0)
+# ============================================================================
+
+[coverage.skipped-musts.ordinal-unbudgeted-wf]
+priority = "P1"
+issue = "Unbudgeted _<ᵇʳᶠ_ global WF — eliminate the ℕ budget from wf-<ᵇʳᶠᵇ without leaving --safe --without-K. Solo, not swarmable; named next bottleneck."
+discovered = "2026-05-20"
+
+[coverage.skipped-musts.full-buchholz-constructor-set]
+priority = "P2"
+issue = "K-limited shared-binder cases (<ᵇ-ψα, <ᵇ-+2) beyond the admitted core; push surface-route WF back into Order.agda's main _<ᵇ_."
+discovered = "2026-04-28"
+
+# ============================================================================
+# CHERRY-PICKING AUDIT (accountability for the weighted priority system)
+# ============================================================================
+# At session end agents report whether they chose easy work over hard work.
+#
+# [coverage.cherry-picking]
+# easy-high-completed = 0
+# hard-high-completed = 0
+# assessment = "..."

.machine_readable/agent_instructions/debt.a2ml

@@ -0,0 +1,86 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com>
+#
+# debt.a2ml — Meander debt list (echo-types)
+# Proof obligations and chores found but not discharged. Carried between
+# sessions; becomes the next session's Phase 0 input.
+#
+# Items are consumed (removed) when discharged. New items added at session end.
+#
+# Reference: ADR-002 in standards/agentic-a2ml/docs/
+
+[metadata]
+version = "1.0.0"
+last-updated = "2026-06-12"
+
+# ============================================================================
+# SHOULD — would fix next wave
+# ============================================================================
+
+[[debt.should]]
+component = "ordinal-track / Ordinal.Buchholz"
+issue = "Unbudgeted _<ᵇʳᶠ_ global WF: eliminate the explicit ℕ budget from wf-<ᵇʳᶠᵇ without leaving --safe --without-K."
+effort = "hard"
+impact = "high"
+discovered = "2026-05-20"
+note = "Solo, not swarmable; the named next bottleneck toward Bachmann-Howard."
+
+[[debt.should]]
+component = "ordinal-track / Order.agda"
+issue = "Push the surface-route WF back into Order.agda's main _<ᵇ_ package; close the K-limited shared-binder cases (<ᵇ-ψα, <ᵇ-+2)."
+effort = "hard"
+impact = "high"
+discovered = "2026-04-28"
+
+[[debt.should]]
+component = "establishment-track / docs/echo-types/paper.adoc"
+issue = "Clear remaining [EXPAND] tags (related work; evaluation; ordinal consumer-evidence appendix)."
+effort = "medium"
+impact = "medium"
+discovered = "2026-05-17"
+note = "Author-driven; the ordinal appendix is gated on the Bachmann-Howard milestone. Do NOT auto-run outreach / Zenodo / packaging."
+
+[[debt.should]]
+component = "establishment-track / EchoImageFactorization"
+issue = "Image factorisation (epi, mono) earn-back requires propositional truncation (Cubical Agda, or a postulated ∥_∥ interface with scoped honest-scope). Substantial design decision."
+effort = "hard"
+impact = "medium"
+discovered = "2026-05-27"
+
+# ============================================================================
+# COULD — would fix eventually
+# ============================================================================
+
+[[debt.could]]
+component = "establishment-track / decoration zoo"
+issue = "Wire the remaining decoration modules (Cost / Search / Indexed / Epistemic) as ResidueForm / DecorationStructure instances; mechanical per-module work."
+effort = "medium"
+impact = "low"
+discovered = "2026-05-27"
+
+[[debt.could]]
+component = "establishment-track / Q2.1 truncation generalisation"
+issue = "Generalise echo-not-prop: for non-injective f with two distinct preimages of y, is-prop (Echo f y) → ⊥. High-leverage for the truncation distinctness argument but currently low-priority."
+effort = "medium"
+impact = "medium"
+discovered = "2026-04-29"
+
+[[debt.could]]
+component = "rsr-conformance (root Intentfile)"
+issue = "Pin @sha256: digests on stapeln.toml + Containerfile base images; resolve readme.adoc/README.md and roadmap.adoc/roadmap-gates.adoc duplication; migrate doc-format-rule .md → .adoc."
+effort = "easy"
+impact = "low"
+discovered = "2026-04-28"
+
+[[debt.could]]
+component = "cross-repo bridges / JanusKey"
+issue = "Rewrite EchoJanusBridge.JanusOp from the 4-variant local enum to the 8-variant Idris2 OpKind (Copy/Move/Delete/Modify/Obliterate/KeyGen/KeyRotate/KeyRevoke); add IsFileOp/IsKeyOp analogues; re-pin in Smoke.agda."
+effort = "medium"
+impact = "low"
+discovered = "2026-06-02"
+
+# ============================================================================
+# PARKED — explicitly out of scope (do not treat as debt to clear)
+# ============================================================================
+# - Recipe extension (coupled state across axes): v0.2+, NOT EI-2 follow-up. File as EI-3 when v0.2 begins.
+# - Full 2D iff for recipe-non-triviality: not formalisable in safe Agda without postulates (PATH B accepted).

.machine_readable/agent_instructions/methodology.a2ml

@@ -0,0 +1,114 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com>
+#
+# methodology.a2ml — AI agent methodology configuration (echo-types)
+# Declares how agents should approach work in this Agda proof library.
+# Read at session start by any AI agent, alongside CLAUDE.md.
+#
+# Reference: ADR-002 in standards/agentic-a2ml/docs/
+
+[metadata]
+version = "1.0.0"
+last-updated = "2026-06-12"
+spec = "https://github.com/hyperpolymath/standards/blob/main/agentic-a2ml/docs/ADR-002-methodology-layer.adoc"
+
+# ============================================================================
+# MODE SELECTION
+# ============================================================================
+# convergent: find gaps, fill them, build infrastructure
+# divergent:  find what's strongest, push it further (research/proof)
+# hybrid:     audit a slice of budget, then focus on top MUSTs
+#
+# echo-types is a research proof library: the default is divergent — deepen
+# the structured-loss identity (canonical-identity spine, ordinal milestone),
+# do not broaden into parallel formalisms.
+
+[methodology]
+default-mode = "divergent"
+ring-ceiling = 2              # Hard ceiling for ring expansion (0-3)
+wave-cap = 2                  # Max waves before requiring user "keep going"
+spike-required = true         # Every session must land verified Agda, not just designs
+
+# ============================================================================
+# PROOF INVARIANTS (the riverbanks — non-negotiable)
+# ============================================================================
+
+[methodology.proof-invariants]
+safe-without-k = true                 # --safe --without-K on every module
+postulate-ceiling = 0                 # zero in load-bearing tracks (outside Ordinal/)
+believe-me-ceiling = 0                # no believe_me / primTrustMe / primEraseEquality
+escape-hatch-ceiling = 0              # no sorry / Admitted / unsafeCoerce / Obj.magic
+escape-pragma-ceiling = 0             # no TERMINATING / NON_TERMINATING / allow-unsolved-metas
+funext-policy = "explicit-parameter-only"   # never a postulate; isolated from the trusted base
+pin-every-headline = true             # each headline pinned in Smoke.agda via `using`
+wire-every-module = true              # each module in All.agda; orphans are dead code
+kernel-cone-guard = "scripts/kernel-guard.sh"
+
+# ============================================================================
+# PRIORITY WEIGHTS
+# ============================================================================
+# MUST (3x): blocking current proof work → fix immediately
+# SHOULD (2x): degrading quality of current work → fix if in zone
+# COULD (1x): improving adjacent work → add to debt list
+
+[methodology.priority-weights]
+must = 3
+should = 2
+could = 1
+
+# ============================================================================
+# CONVERGENT BUDGET (when mode = convergent or hybrid)
+# ============================================================================
+
+[methodology.convergent-budget]
+structural = 70   # new modules / proofs / wiring / Smoke pins
+corrective = 20   # broken imports, stale doc tags, drift
+perfective = 10   # SPDX headers, doc polish, formatting
+
+# ============================================================================
+# UNIQUE STRENGTH (when mode = divergent)
+# ============================================================================
+
+[methodology.unique-strength]
+description = "Echo as the proof-relevant fiber of structured loss: Echo f y := Σ (x : A) , (f x ≡ y), characterised as a reindexing modality (coeffect/quantitative lineage). The strength is the machine-checked, --safe --without-K, postulate-free identity claim plus its honest matched-negatives."
+deepen-not-broaden = true
+
+# ============================================================================
+# DIVERGENT INVARIANTS
+# ============================================================================
+# Test before any divergent action:
+#   "Does this deepen the existing identity, or add a parallel strength?"
+#   If parallel → stop. Note as cross-project insight.
+
+[methodology.divergent-invariants]
+rules = [
+  "Agda only for the formal core — no Lean4 / Coq / Idris2 inside this repo (cross-prover work is citation-level bridges only).",
+  "Never weaken --safe or --without-K to land a proof.",
+  "Never introduce a postulate in a load-bearing track; exploratory truncation postulates, if any, go in docs/proof-debt.md and stay out of All.agda's trusted closure.",
+  "Honest scope: every identity claim ships with its matched-negatives; narrow-true beats broad-easy.",
+  "Do not reopen retracted claims (R-2026-05-18) or closed gates (Pillars A-D, F1-F4, EI-2).",
+]
+language-invariant = "agda"
+
+# ============================================================================
+# KNOWN CONSTRAINTS (help Phase 0 find the critical chain faster)
+# ============================================================================
+
+[methodology.known-constraints]
+constraints = [
+  "stdlib >= 2.3 is required (apt's 1.7.3 lacks Data.Product.Base) — see CLAUDE.md § Build.",
+  "The ordinal track is solo, not swarmable; the unbudgeted _<ᵇʳᶠ_ global WF is the named next bottleneck.",
+  "Multiple Claude sessions may run concurrently — respect declared territory; use `--only <paths>` if both commit before sync.",
+  "Pillar E paper [EXPAND] tags are author-driven; the ordinal consumer-evidence appendix is gated on the Bachmann-Howard milestone.",
+]
+
+# ============================================================================
+# STATE FILE VALIDATION
+# ============================================================================
+
+[methodology.state-validation]
+reject-if-contains = ["{{PLACEHOLDER}}", "rsr-template-repo"]
+reject-if-project-name-mismatch = true
+staleness-threshold-days = 120
+authoritative-state = "CLAUDE.md (current-rung-state) + .machine_readable/6a2/STATE.a2ml (current-state block)"
+fallback-files = ["roadmap-gates.adoc", "roadmap.adoc", "docs/echo-types/MAP.adoc", "README.md"]