Skip to content

Roadmap.adoc

Latest commit

 

History

History
121 lines (94 loc) · 5.16 KB

Roadmap.adoc

File metadata and controls

121 lines (94 loc) · 5.16 KB
Raw

Roadmap

Two layers: the identity-claim gates (the falsifiable conditions the project must keep meeting) and the live open work per track. Authoritative sources: roadmap-gates.adoc and CLAUDE.md current-rung-state.

Table of Contents

Identity-claim decision gates

The identity claim rests on three gates. Each has an explicit failure action; failure is recorded in docs/retractions.adoc, not silently revised. Gates are reassessed at each tagged release — surviving one round does not grant immunity in the next.

Gate Condition Failure action

1. Distinct phenomenon

Echo types name structured loss under non-injective computation as distinct from refinement types, lens/optic theory, HoTT fibers, setoid quotients, provenance semirings. Carried by the truncation argument (echo-not-prop) + the 2-cell argument (Sophisticated.* in EchoVsQuotient / EchoVsGalois).

Drop identity claim; retain as Agda exposition.

2. Characteristic theorems

At least two theorems are naturally echo-shaped and not reducible to generic Σ lemmas. Current nominees: EchoGraded.degrade-via-join, EchoGraded.degrade-compose, EchoChoreo.applyChoreo-compose, EchoLinear.degradeMode-compose (survives the audit 4-of-4).

Drop claim of a distinct theorem family; modules remain.

3. Canonical examples

At least one fully worked example where echo types are the right explanatory unit (preferable to, not merely compatible with, existing framings).

Reframe as theoretical scaffolding awaiting application.
Note
 The integration recipe across the five decoration axes does not carry the Gate 1 distinctness load — that was established (negatively) by EI-2 and is terminated. Do not reopen it under any reframing in .machine_readable/6a2/STATE.a2ml § forbidden-rebrandings.

Live open work per track

Composition track — landed

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:

  1. 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.

  2. Full constructor set beyond the admitted core — the K-limited shared-binder cases <ᵇ-ψα, <ᵇ-+2.

  3. Push the surface-route WF back into Order.agda’s main `<ᵇ package.

Establishment track — Pillar E only

Pillars A–D and F (F1–F4) are closed. All four paper.adoc [EXPAND] tags are cleared, the last (ordinal consumer-evidence appendix) on 2026-06-14 — written at the well-foundedness milestone, with order-type fidelity recorded as a named OPEN problem (decision-log D-2026-06-14), NOT claimed. The in-repo half of Pillar E is complete at the bounded-claim level. Remaining:

  1. Order-type fidelity (the named open problem D-2026-06-14): a verified order-preserving denotation BT → 𝒪 of height ψ₀(Ω_ω), or a direct order-type computation. The genuine remaining ordinal-strength frontier; no current module establishes it.

  2. Then, author-driven and not auto-run: Zenodo DOI, installable library packaging, outreach. Flag to the user; do not start unprompted.

Carried debt (machine-readable)

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).

  • Could: decoration-zoo wiring (Cost/Search/Indexed/Epistemic as ResidueForm/DecorationStructure instances); the Q2.1 truncation generalisation; rsr-conformance chores (@sha256 pins, README/roadmap de-duplication, doc-format migration); the JanusKey 4→8-variant enum mirror.

Explicitly parked (not debt to clear)

  • Recipe extension (coupled state across axes): v0.2+, not EI-2 follow-up. File as EI-3 when v0.2 work begins.

  • Full 2D iff for recipe-non-triviality: not formalisable in safe Agda without postulates; PATH B (partial formalisation) accepted.

Gate resolution

Outcome Action

All three gates pass

Identity claim upheld; proceed to peer review.

Any gate fails

Identity claim retracted in README + on Zenodo (new version, revised abstract). Modules remain; the claim does not.
Tip
 Retractions are not failures of the repository. They are the mechanism by which the identity claim is made falsifiable in the first place.