Skip to content

Commit ff206ac

Browse files
claudeclaude
committed
docs(wiki): refresh status to 2026-06-21 + add developer/maintainer/end-user split
- Home.adoc: add a "Who is this for?" tri-split with reading orders for developers (proof discipline + build), maintainers (gates + CI cone + 6a2), and end users (FOUNDATION_CONTRACT + Overview + EchoTypes.jl). Refresh the one-line status to 2026-06-21: ordinal track RETIRED (D-2026-06-21); variance resolved (#243); aggregation generalised (#175); establishment Pillar E in-repo half complete with order-type fidelity the one named OPEN external problem (D-2026-06-14). - Roadmap.adoc: reframe the ordinal track from "active bottleneck" to RETIRED, with the extraction disposition, verified firewall, and frozen open items (tracking #263); fix the carried-debt line that still pointed at the moved ordinal WF items. Refs #263. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PWMMxryCcPrAjJ8tuGvygG
1 parent f67fbe6 commit ff206ac

2 files changed

Lines changed: 85 additions & 22 deletions

File tree

‎wiki/Home.adoc‎

Lines changed: 63 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,48 @@ toc::[]
4646
affine mode.
4747
|===
4848

49+
== Who is this for?
50+
51+
echo-types serves three audiences. Find your lane, then follow the reading order.
52+
53+
[cols="1,3", options="header"]
54+
|===
55+
| You are… | Start here, in order
56+
57+
| *A developer* +
58+
(writing or extending proofs)
59+
| 1. <<Working-Rules.adoc#,Working-Rules>> — the non-negotiable discipline
60+
(`--safe --without-K`, zero postulates, Smoke pins, `All.agda` wiring). +
61+
2. `CLAUDE.md` — current rung-state + the per-arc *DO NOT reopen* lists. +
62+
3. <<Architecture.adoc#,Architecture>> + `docs/echo-types/MAP.adoc` — the
63+
module map and where a new theorem belongs. +
64+
4. *Build:* `bash scripts/provision-agda.sh`, then
65+
`agda -i proofs/agda proofs/agda/All.agda` (and `Smoke.agda`) must exit 0.
66+
67+
| *A maintainer* +
68+
(gates, releases, governance)
69+
| 1. <<Roadmap.adoc#,Roadmap>> + `roadmap-gates.adoc` — the three identity
70+
gates and their *failure actions* (gates are reassessed every tagged
71+
release). +
72+
2. `docs/retractions.adoc` — how a failed gate is recorded (never silently
73+
revised). +
74+
3. `scripts/kernel-guard.sh` + `.github/workflows/agda.yml` — the CI cone
75+
that must stay green. +
76+
4. `.machine_readable/6a2/STATE.a2ml` (EI-2 record + current state) and
77+
`docs/bridges/cross-repo-bridge-status.md` (downstream ledger).
78+
79+
| *An end user* +
80+
(wiring Echo into another language)
81+
| 1. `FOUNDATION_CONTRACT.md` — the stable `Echo.*` interface and the boundary
82+
invariant *Echo IS-NOT a resource instance*. Read this first. +
83+
2. <<Overview.adoc#,Overview>> — what Echo adds and, crucially, what it does
84+
*not* add (honest scope). +
85+
3. *EchoTypes.jl* — the executable Julia shadow; falsifies-by-counterexample
86+
on concrete finite data. +
87+
4. <<Deniability.adoc#,Deniability>> — a worked first-class echo property to
88+
see the shape of a consumer-facing result.
89+
|===
90+
4991
== Canonical sources of truth
5092

5193
This wiki is a *distillation*. The authoritative records are:
@@ -61,11 +103,27 @@ This wiki is a *distillation*. The authoritative records are:
61103
* `.machine_readable/6a2/STATE.a2ml` — EI-2 record (permanent) + current-state block.
62104
* `docs/bridges/cross-repo-bridge-status.md` — cross-repo bridge ledger.
63105

64-
== One-line status (as of 2026-06-13)
65-
66-
* *Composition track* — landed (Echo-comp-iso, cancel-iso, pentagon).
67-
* *Ordinal track* — partial (Buchholz; Slice 3+4 Route A; target Bachmann–Howard ψ₀(Ω_ω)).
68-
* *Establishment track* — Pillars A–D + Pillar F (F1–F4) closed; Pillar E paper open.
106+
== One-line status (as of 2026-06-21)
107+
108+
* *Composition track* — landed (Echo-comp-iso, cancel-iso, pentagon). No open
109+
headline items.
110+
* *Establishment track* — Pillars A–D and F (F1–F4) closed; the in-repo half of
111+
Pillar E is complete at the bounded-claim level. One named *OPEN external*
112+
problem remains: *order-type fidelity* to ψ₀(Ω_ω) (decision-log
113+
`D-2026-06-14`).
114+
* *Variance* — resolved (`EchoVariance.agda`, #243): an echo is a graded
115+
*monad of accumulation* with a section/retraction adjunction exact on the
116+
grade-0 fibre — *not* a graded comonad (that reading is the lossless
117+
complement-storing writer).
118+
* *Aggregation* — `EchoAggregation.agda` generalised to the monoid/group form
119+
(`aggregation-as-fold`; #175), with `no-canonical-disaggregation` (the
120+
Sonnenschein–Mantel–Debreu / representative-agent critique, stated
121+
type-theoretically).
122+
* *Ordinal track* — *RETIRED from echo-types* (owner decision `D-2026-06-21`):
123+
the transfinite Buchholz/Veblen ladder outgrew the project. The landed
124+
artifact is correct and stays; the disposition is *extraction to its own
125+
ordinal-notation repo* (the physical cut is the owner's; tracking: #263).
126+
See <<Roadmap.adoc#ordinal,Roadmap § Ordinal>>.
69127
* *Deniability track* — `EchoDeniability.agda` landed: perfect/partial duality,
70128
`IsConstantOpener` boundary, no-section / section duality as a checked theorem pair.
71129

‎wiki/Roadmap.adoc‎

Lines changed: 22 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -55,21 +55,25 @@ The base accumulation iso, cancellation iso, and pentagon coherence are all
5555
landed and packaged as `_↔_`. No open headline items; further work is
5656
consolidation / doc-threading.
5757

58-
=== Ordinal track — partial (the active bottleneck)
59-
60-
Target: *Bachmann–Howard* ψ₀(Ω_ω). Open, in priority order:
61-
62-
. *Unbudgeted `_<ᵇʳᶠ_` global WF* — the GLOBAL form over native `_<ᵇ_`
63-
is *walled* (all five standard routes; native `_<ᵇ_` is ordinally
64-
unsound — see `buchholz-rank-obstruction.adoc`). The SOUND-CARRIER
65-
form is *DONE* (2026-06-14, PR #212): `RecursiveSurfaceSound.wf-<ᵇʳᶠ²`
66-
is unbudgeted, built over `_<ᵇ²_` + the doubled-ladder `rank2`
67-
embedding. Remaining open is only the global-over-native form, whose
68-
realistic close-out is a falsifiable "cannot close under
69-
`--safe --without-K`" verdict rather than a positive proof.
70-
. *Full constructor set beyond the admitted core* — the K-limited shared-binder
71-
cases `<ᵇ-ψα`, `<ᵇ-+2`.
72-
. *Push the surface-route WF back* into `Order.agda`'s main `_<ᵇ_` package.
58+
[#ordinal]
59+
=== Ordinal track — RETIRED from echo-types (owner decision D-2026-06-21)
60+
61+
The transfinite Buchholz/Veblen ascent *outgrew echo-types* and is *no longer
62+
echo-types work*. The landed artifact is correct (`--safe --without-K`, zero
63+
postulates, in the green closure) and *stays compiling*; *no new ordinal rung
64+
is opened here*. The disposition is *extraction to its own ordinal-notation
65+
repository* — the physical cross-repo cut is the owner's. Tracking: *#263*.
66+
67+
* *Hand-off record* (frontier + inventory for the extracted repo, NOT a
68+
resume-here plan): `docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc`.
69+
* *Firewall (verified):* `OmegaMarkers` ← `Buchholz.Syntax` ← `EchoOrdinal`
70+
STAY (Echo Core's bridge); everything else under `proofs/agda/Ordinal/` MOVES.
71+
* *Frozen open items* (for the extracted repo only — NOT echo-types TODOs):
72+
unbudgeted `_<ᵇʳᶠ_` global WF over native `_<ᵇ_` (the sound-carrier form
73+
`RecursiveSurfaceSound.wf-<ᵇʳᶠ²` is already DONE, PR #212); the full
74+
K-limited shared-binder constructor set (`<ᵇ-ψα`, `<ᵇ-+2`); and order-type
75+
fidelity to ψ₀(Ω_ω) (`D-2026-06-14`, an OPEN *external* problem — retirement
76+
neither closes nor over-claims it).
7377

7478
=== Establishment track — Pillar E only
7579

@@ -92,8 +96,9 @@ Pillar E is complete at the bounded-claim level. Remaining:
9296
The full debt list, with effort/impact, lives in
9397
`.machine_readable/agent_instructions/debt.a2ml`. Highlights:
9498

95-
* *Should:* the two ordinal WF items above; image factorisation (epi, mono)
96-
earn-back (needs propositional truncation — a substantial design decision).
99+
* *Should:* image factorisation (epi, mono) earn-back (needs propositional
100+
truncation — a substantial design decision). (The ordinal WF items moved out
101+
with the ordinal-track retirement — see #263.)
97102
* *Could:* decoration-zoo wiring (Cost/Search/Indexed/Epistemic as
98103
ResidueForm/DecorationStructure instances); the Q2.1 truncation
99104
generalisation; rsr-conformance chores (@sha256 pins, README/roadmap

0 commit comments

Comments
 (0)