diff --git a/wiki/Home.adoc b/wiki/Home.adoc index a7cd86d..387136d 100644 --- a/wiki/Home.adoc +++ b/wiki/Home.adoc @@ -46,6 +46,48 @@ toc::[] affine mode. |=== +== Who is this for? + +echo-types serves three audiences. Find your lane, then follow the reading order. + +[cols="1,3", options="header"] +|=== +| You are… | Start here, in order + +| *A developer* + + (writing or extending proofs) +| 1. <> — the non-negotiable discipline + (`--safe --without-K`, zero postulates, Smoke pins, `All.agda` wiring). + + 2. `CLAUDE.md` — current rung-state + the per-arc *DO NOT reopen* lists. + + 3. <> + `docs/echo-types/MAP.adoc` — the + module map and where a new theorem belongs. + + 4. *Build:* `bash scripts/provision-agda.sh`, then + `agda -i proofs/agda proofs/agda/All.agda` (and `Smoke.agda`) must exit 0. + +| *A maintainer* + + (gates, releases, governance) +| 1. <> + `roadmap-gates.adoc` — the three identity + gates and their *failure actions* (gates are reassessed every tagged + release). + + 2. `docs/retractions.adoc` — how a failed gate is recorded (never silently + revised). + + 3. `scripts/kernel-guard.sh` + `.github/workflows/agda.yml` — the CI cone + that must stay green. + + 4. `.machine_readable/6a2/STATE.a2ml` (EI-2 record + current state) and + `docs/bridges/cross-repo-bridge-status.md` (downstream ledger). + +| *An end user* + + (wiring Echo into another language) +| 1. `FOUNDATION_CONTRACT.md` — the stable `Echo.*` interface and the boundary + invariant *Echo IS-NOT a resource instance*. Read this first. + + 2. <> — what Echo adds and, crucially, what it does + *not* add (honest scope). + + 3. *EchoTypes.jl* — the executable Julia shadow; falsifies-by-counterexample + on concrete finite data. + + 4. <> — a worked first-class echo property to + see the shape of a consumer-facing result. +|=== + == Canonical sources of truth This wiki is a *distillation*. The authoritative records are: @@ -61,11 +103,27 @@ This wiki is a *distillation*. The authoritative records are: * `.machine_readable/6a2/STATE.a2ml` — EI-2 record (permanent) + current-state block. * `docs/bridges/cross-repo-bridge-status.md` — cross-repo bridge ledger. -== One-line status (as of 2026-06-13) - -* *Composition track* — landed (Echo-comp-iso, cancel-iso, pentagon). -* *Ordinal track* — partial (Buchholz; Slice 3+4 Route A; target Bachmann–Howard ψ₀(Ω_ω)). -* *Establishment track* — Pillars A–D + Pillar F (F1–F4) closed; Pillar E paper open. +== One-line status (as of 2026-06-21) + +* *Composition track* — landed (Echo-comp-iso, cancel-iso, pentagon). No open + headline items. +* *Establishment track* — Pillars A–D and F (F1–F4) closed; the in-repo half of + Pillar E is complete at the bounded-claim level. One named *OPEN external* + problem remains: *order-type fidelity* to ψ₀(Ω_ω) (decision-log + `D-2026-06-14`). +* *Variance* — resolved (`EchoVariance.agda`, #243): an echo is a graded + *monad of accumulation* with a section/retraction adjunction exact on the + grade-0 fibre — *not* a graded comonad (that reading is the lossless + complement-storing writer). +* *Aggregation* — `EchoAggregation.agda` generalised to the monoid/group form + (`aggregation-as-fold`; #175), with `no-canonical-disaggregation` (the + Sonnenschein–Mantel–Debreu / representative-agent critique, stated + type-theoretically). +* *Ordinal track* — *RETIRED from echo-types* (owner decision `D-2026-06-21`): + the transfinite Buchholz/Veblen ladder outgrew the project. The landed + artifact is correct and stays; the disposition is *extraction to its own + ordinal-notation repo* (the physical cut is the owner's; tracking: #263). + See <>. * *Deniability track* — `EchoDeniability.agda` landed: perfect/partial duality, `IsConstantOpener` boundary, no-section / section duality as a checked theorem pair. diff --git a/wiki/Roadmap.adoc b/wiki/Roadmap.adoc index 77da45c..7df31cc 100644 --- a/wiki/Roadmap.adoc +++ b/wiki/Roadmap.adoc @@ -55,21 +55,25 @@ The base accumulation iso, cancellation iso, and pentagon coherence are all landed and packaged as `_↔_`. No open headline items; further work is consolidation / doc-threading. -=== Ordinal track — partial (the active bottleneck) - -Target: *Bachmann–Howard* ψ₀(Ω_ω). Open, in priority order: - -. *Unbudgeted `_<ᵇʳᶠ_` global WF* — the GLOBAL form over native `_<ᵇ_` - is *walled* (all five standard routes; native `_<ᵇ_` is ordinally - unsound — see `buchholz-rank-obstruction.adoc`). The SOUND-CARRIER - form is *DONE* (2026-06-14, PR #212): `RecursiveSurfaceSound.wf-<ᵇʳᶠ²` - is unbudgeted, built over `_<ᵇ²_` + the doubled-ladder `rank2` - embedding. Remaining open is only the global-over-native form, whose - realistic close-out is a falsifiable "cannot close under - `--safe --without-K`" verdict rather than a positive proof. -. *Full constructor set beyond the admitted core* — the K-limited shared-binder - cases `<ᵇ-ψα`, `<ᵇ-+2`. -. *Push the surface-route WF back* into `Order.agda`'s main `_<ᵇ_` package. +[#ordinal] +=== Ordinal track — RETIRED from echo-types (owner decision D-2026-06-21) + +The transfinite Buchholz/Veblen ascent *outgrew echo-types* and is *no longer +echo-types work*. The landed artifact is correct (`--safe --without-K`, zero +postulates, in the green closure) and *stays compiling*; *no new ordinal rung +is opened here*. The disposition is *extraction to its own ordinal-notation +repository* — the physical cross-repo cut is the owner's. Tracking: *#263*. + +* *Hand-off record* (frontier + inventory for the extracted repo, NOT a + resume-here plan): `docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc`. +* *Firewall (verified):* `OmegaMarkers` ← `Buchholz.Syntax` ← `EchoOrdinal` + STAY (Echo Core's bridge); everything else under `proofs/agda/Ordinal/` MOVES. +* *Frozen open items* (for the extracted repo only — NOT echo-types TODOs): + unbudgeted `_<ᵇʳᶠ_` global WF over native `_<ᵇ_` (the sound-carrier form + `RecursiveSurfaceSound.wf-<ᵇʳᶠ²` is already DONE, PR #212); the full + K-limited shared-binder constructor set (`<ᵇ-ψα`, `<ᵇ-+2`); and order-type + fidelity to ψ₀(Ω_ω) (`D-2026-06-14`, an OPEN *external* problem — retirement + neither closes nor over-claims it). === Establishment track — Pillar E only @@ -92,8 +96,9 @@ Pillar E is complete at the bounded-claim level. Remaining: The full debt list, with effort/impact, lives in `.machine_readable/agent_instructions/debt.a2ml`. Highlights: -* *Should:* the two ordinal WF items above; image factorisation (epi, mono) - earn-back (needs propositional truncation — a substantial design decision). +* *Should:* image factorisation (epi, mono) earn-back (needs propositional + truncation — a substantial design decision). (The ordinal WF items moved out + with the ordinal-track retirement — see #263.) * *Could:* decoration-zoo wiring (Cost/Search/Indexed/Epistemic as ResidueForm/DecorationStructure instances); the Q2.1 truncation generalisation; rsr-conformance chores (@sha256 pins, README/roadmap