Merge branch 'main' into feat/echo-displayed-packaging

Author: hyperpolymath

.claude/hooks/session-start.sh

@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SessionStart hook: provision the Agda proof-checker toolchain so Claude Code
+# on the web can typecheck this repo (agda proofs/agda/All.agda, Smoke.agda).
+#
+# Thin wrapper around scripts/provision-agda.sh (idempotent). Web-only; local
+# developers manage their own toolchain. Synchronous so the toolchain is ready
+# before the agent loop starts.
+set -euo pipefail
+
+# Only provision in the remote (web) environment.
+if [ "${CLAUDE_CODE_REMOTE:-}" != "true" ]; then
+  exit 0
+fi
+
+exec bash "${CLAUDE_PROJECT_DIR:-$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)}/scripts/provision-agda.sh"

.claude/settings.json

@@ -0,0 +1,14 @@
+{
+  "hooks": {
+    "SessionStart": [
+      {
+        "hooks": [
+          {
+            "type": "command",
+            "command": "$CLAUDE_PROJECT_DIR/.claude/hooks/session-start.sh"
+          }
+        ]
+      }
+    ]
+  }
+}

.github/workflows/agda.yml

@@ -146,6 +146,14 @@ jobs:
       - name: Typecheck examples lane (Gate #3 canonical examples)
         run: agda -i proofs/agda proofs/agda/examples/All.agda
 
+      # Cubical lane: the (epi, mono) truncation discharge. A --cubical
+      # --safe island (zero postulates) that CONSTRUCTS ∥_∥ as a HIT —
+      # it cannot be imported by the --safe --without-K All.agda, so it
+      # is typechecked directly here. Its --without-K-profile shadow is
+      # EchoImageFactorizationPropPostulated (proof-debt (a)/(c)).
+      - name: Typecheck cubical lane (epi/mono truncation discharge)
+        run: agda -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda
+
   cold-check:
     # Belt-and-braces: NO interface cache, --ignore-interfaces cold
     # build. A green here cannot be a stale-.agdai artefact (matters
@@ -189,3 +197,4 @@ jobs:
           agda --ignore-interfaces -i proofs/agda proofs/agda/Smoke.agda
           agda --ignore-interfaces -i proofs/agda proofs/agda/characteristic/All.agda
           agda --ignore-interfaces -i proofs/agda proofs/agda/examples/All.agda
+          agda --ignore-interfaces -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda

.github/workflows/codeql.yml

@@ -31,11 +31,10 @@ jobs:
       fail-fast: false
       matrix:
         include:
-          - language: javascript-typescript
-            build-mode: none
-          # Also analyse the GitHub Actions workflows themselves
-          # (CodeQL `actions` language) — directly relevant given the
-          # workflow-hardening in this PR, and closes the Hypatia
+          # CodeQL `actions` language scans the GitHub Actions workflow
+          # files (present in every repo). The repo has no JS/TS source,
+          # so the prior JS/TS matrix entry recorded zero results /
+          # failed "no source files"; closes the Hypatia
           # `codeql_missing_actions_language` finding.
           - language: actions
             build-mode: none

.gitignore

@@ -1,6 +1,9 @@
 *.agdai
 _build/
-.claude/
+# Ignore personal Claude config but share the SessionStart toolchain hook.
+.claude/*
+!.claude/hooks/
+!.claude/settings.json
 .agda/
 
 # direnv / nix local cache

.machine_readable/agent_instructions/README.adoc

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MPL-2.0
-// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com>
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 = Agent Instructions (echo-types)
 :toc: preamble
 

.machine_readable/agent_instructions/coverage.a2ml

@@ -1,5 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com>
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # coverage.a2ml — Session coverage tracking (echo-types)
 # Updated at the end of each AI agent session.

.machine_readable/agent_instructions/debt.a2ml

@@ -1,5 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com>
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # debt.a2ml — Meander debt list (echo-types)
 # Proof obligations and chores found but not discharged. Carried between
@@ -11,41 +11,68 @@
 
 [metadata]
 version = "1.0.0"
-last-updated = "2026-06-12"
+last-updated = "2026-06-14"
+
+# ============================================================================
+# OUTSTANDING PROOFS — the live frontier (single inventory, 2026-06-14)
+#
+# Status legend:
+#   OPEN-EXTERNAL  — mechanisable, but needs new external mathematics
+#                    (no in-repo route exists yet).
+#   WALLED         — proven not closable on the current object under
+#                    --safe --without-K; close-out is a falsifiable verdict.
+#   OPEN-DESIGN    — closable, but gated on a substantial design decision
+#                    (e.g. truncation / Cubical).
+#   MECHANICAL     — closable now, bounded, no new ideas needed.
+#
+# 2026-06-14 progress note: the two long-standing ordinal "should"
+# items (unbudgeted _<ᵇʳᶠ_; K-limited shared-binder; surface-route WF)
+# are now DONE in their ACHIEVABLE (sound-carrier) form — wf-<ᵇ²,
+# wf-<ᵇʳᶠ², wf-<ᵇ⁺² (PRs #208/#212/#214). What remains of them is the
+# native-order form, which is WALLED. All four paper.adoc [EXPAND]
+# tags are cleared (#215). The genuine remaining ordinal frontier is
+# now order-type fidelity (D-2026-06-14).
+# ============================================================================
 
 # ============================================================================
 # 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."
+component = "ordinal-track / Bachmann-Howard order-type fidelity"
+issue = "Order-type fidelity: prove the well-formed Buchholz notation IS the Bachmann-Howard ordinal order, not merely well-founded. Either (a) a verified order-preserving denotation ‖·‖ : BT → 𝒪 of height ψ₀(Ω_ω) with s <ᵇ t iff ‖s‖ < ‖t‖ on the well-formed fragment, or (b) a direct order-type computation (fundamental sequences / collapsing-function correctness)."
+status = "OPEN-EXTERNAL"
 effort = "hard"
 impact = "high"
-discovered = "2026-05-20"
-note = "Solo, not swarmable; the named next bottleneck toward Bachmann-Howard."
+discovered = "2026-06-14"
+note = "Decision-log D-2026-06-14 (decisions/ordinal-bh-order-type-fidelity-open.adoc). The genuine remaining ordinal-strength frontier; WF (done, sound-carrier) is the prerequisite, not the result. Gates the Pillar E ordinal appendix's strong reading (the WF-milestone appendix is already written, #215)."
 
 [[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)."
+component = "ordinal-track / Order.agda (native _<ᵇ_)"
+issue = "Global-native well-foundedness: unbudgeted wf-<ᵇʳᶠ AND the K-limited shared-binder cases (<ᵇ-ψα, <ᵇ-+2) over NATIVE _<ᵇ_ (not the sound carrier)."
+status = "WALLED"
 effort = "hard"
-impact = "high"
+impact = "low"
 discovered = "2026-04-28"
+note = "Native _<ᵇ_ is ordinally unsound (the <ᵇ-+Ω counterexample); all five rank/direct/lex/tower/inverse-image routes are walled (RankBrouwer.agda preamble + buchholz-rank-obstruction.adoc), and rank2 does not escape it. The ACHIEVABLE (sound-carrier) forms are DONE: wf-<ᵇ² / wf-<ᵇʳᶠ² / wf-<ᵇ⁺². Realistic close-out for the native form is a FALSIFIABLE VERDICT, not a positive proof — write it when this item is next picked up."
 
 [[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."
+component = "establishment-track / EchoImageFactorization (epi, mono)"
+issue = "Image factorisation (epi, mono) earn-back requires propositional truncation. The postulated-interface placeholder lives in EchoImageFactorizationPropPostulated.agda (the tree's ONLY postulate; not in All.agda)."
+status = "OPEN-DESIGN"
 effort = "hard"
 impact = "medium"
 discovered = "2026-05-27"
+note = "Cubical Agda (different --safe flag profile) OR a postulated ∥_∥ interface with scoped honest-scope. Substantial design decision; the (equivalence, projection) upper form is already done (Tier 1 + F5)."
+
+[[debt.should]]
+component = "earn-back-track / examples/Transport.agda (Gate-3)"
+issue = "Two disclosed open items in the transport/Gate-3 example, pending a K-free reformulation (coe-cong-R ∘ sym push). Stated in-file as precise OPENs."
+status = "OPEN-DESIGN"
+effort = "medium"
+impact = "low"
+discovered = "2026-05-20"
+note = "See earn-back-plan.adoc; nothing is postulated — the items are honestly-stated gaps awaiting a K-free route."
 
 # ============================================================================
 # COULD — would fix eventually
@@ -54,16 +81,19 @@ discovered = "2026-05-27"
 [[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."
+status = "MECHANICAL"
 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."
+status = "OPEN-DESIGN"
 effort = "medium"
 impact = "medium"
 discovered = "2026-04-29"
+note = "Shares the propositional-truncation design decision with the (epi, mono) earn-back; resolving one likely informs the other."
 
 [[debt.could]]
 component = "rsr-conformance (root Intentfile)"

.machine_readable/agent_instructions/methodology.a2ml

@@ -1,5 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com>
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # methodology.a2ml — AI agent methodology configuration (echo-types)
 # Declares how agents should approach work in this Agda proof library.

.machine_readable/anchors/ANCHOR.a2ml

@@ -1,5 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com>
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # ANCHOR.a2ml - authoritative anchor for the echo-types repository.
 # Canonical identity + policy boundaries for downstream/satellite repos.