Roadmap: consolidated proof-debt ledger (full-repo audit 2026-05-18)

docs/echo-types/earn-back-plan.adoc

@@ -11,9 +11,12 @@ This plan defines the falsifiable program to convert the retracted
 claims back into theorems — or to confirm, on the project's own gate
 discipline, that they cannot be earned. Nothing in `paper.adoc` /
 `conservativity.adoc` / `types-abstract.adoc` moves until the
-corresponding gate here passes. Same methodology as
-`roadmap-gates.adoc`: explicit pass/fail, abandon criteria, outcomes
-logged in `docs/retractions.adoc`.
+corresponding gate here passes. Methodology — explicit pass/fail,
+abandon criteria, outcomes logged in `docs/retractions.adoc`. (The
+gate discipline was historically attributed to a `roadmap-gates.adoc`;
+that file does not exist in-tree — see proof-debt ledger item *D*
+below. The canonical loci are `docs/retractions.adoc`, this plan, and
+`docs/next-questions.adoc`.)
 
 toc::[]
 
@@ -32,8 +35,11 @@ its grade-unit object — not redefining Echo.
 [#gate-F1]
 === Gate F1 — Genuine graded comonad (MAKE-OR-BREAK)
 
-*Everything else is gated on F1.* The other gates are not attempted
-until F1 passes.
+*F1 is make-or-break for the graded-comonad claim*, and *F3* is gated
+on it (F3 is not attempted until F1 passes). *F2* and *F4* are
+independent of F1 and proceed in parallel — they earn back
+qualified/real claims regardless of F1 (see "Recommended order of
+attack").
 
 .Claim
 ****
@@ -169,9 +175,103 @@ property, stated as such.
 * "Triage over partial hack": if a gate is close but not closed, it
   is *failed and logged*, not shipped behind softened wording.
 
+== Consolidated proof-debt ledger
+
+Full-repo audit 2026-05-18. The `--safe --without-K` build carries
+*zero postulates and zero escape pragmas* (CI-grep-enforced); every
+item below is therefore either a disclosed-in-comment open obligation
+or a structural-fidelity gap, not hidden debt. This ledger is the
+single index; it moves no claim.
+
+[cols="1,4,1",options="header"]
+|===
+| Id | Debt | State
+
+| A1
+| *F1* — `gc-coassoc` (graded-comonad coassociativity),
+  `proofs/agda/EchoGradedComonadF1.agda`. Needs an explicit
+  δ-naturality-over-`R` lemma. Spike not wired into `All`/`Smoke`.
+| Open, *not postulated*. Feasibility decided *positive* (see Status).
+
+| A2
+| *F2* — real second model of the bare Echo functor via
+  `EchoRelational.StepND`, non-`refl` agreement lemma.
+| Unstarted. Independent of F1. Rated tractable.
+
+| A3
+| *F3* — independent second model of the comonad at a different grade
+  monoid (no `× ⊤` carrier, no `⊑-prop`-equivalent field).
+| Unstarted. Gated on F1.
+
+| A4
+| *F4* — strict universal property as a function of an explicit
+  `funext` *module parameter* (never a postulate).
+| Unstarted. Independent of F1. Expected tractable.
+
+| B
+| Buchholz order: `Ordinal/Buchholz/Order.agda` `_<ᵇ_` compares ψ by
+  Ω-index only and asserts `<ᵇ-ψΩ≤` as a constructor; same-binder
+  sub-cases (`bpsi ν α <ᵇ bpsi ν β` with `α <ᵇ β`;
+  `bplus x y₂ <ᵇ bplus x z₂` with `y₂ <ᵇ z₂`) are not constructible
+  pending a K-free reformulation. Direct-constructor totality / WF do
+  not land; `ExtendedOrder.agda` is the honest closed wrapper (WF via
+  the comparison *measure* `_<ᵇ⁺_`).
+| Disclosed structural-fidelity gap. *Off the echo-types paper
+  critical path.* Long-tail workstream.
+
+| C
+| `characteristic/` open obligations: general recipe-non-triviality
+  over arbitrary axes and `Mode-is-loss-only` (`RecipeNonTriviality.agda`);
+  obligations 2–5 of `ChoreoInjective.agda`. Concrete n=2 cases
+  proved. `RoleRole.agda`'s "REAL OBSTRUCTION" is a *closed negative
+  result* (no uniform total `applyRole₁`), not a debt.
+| Disclosed. Does *not* block EI-2 (terminated-negative).
+  Completeness nice-to-have, lowest priority.
+
+| D
+| Doc-integrity: `docs/roadmap-gates.adoc` is cited as the canonical
+  gate ledger by ≥7 docs but does not exist in-tree. Role now split
+  across `retractions.adoc` / this plan / `next-questions.adoc`.
+| Open drift vector. Cheap to reconcile (back-link the citing docs;
+  do not fabricate retroactive gate history).
+
+| E1
+| `examples/Transport.agda` (Gate-3): two disclosed open items, both
+  blocked only by symbolic-ℚ machinery, not design — (1) the general
+  `∀n` 5a/5b case needs `rotL/rotR (nyquist n) ≡ map -_ (nyquist n)`;
+  (2) Step C (kernel = Nyquist line at n=4) needs a 4×4 ℚ linear
+  solve. Containment results stand; funext was sidestepped via the
+  `Vec ℚ n` carrier (no funext debt).
+| Disclosed. Lowest priority; not paper-blocking.
+
+| E2
+| Doc-integrity (external): the `MEMORY.md` one-liner for
+  `project-echo-types-transport-gate3` says "stops at Rung 2,
+  Fin n→ℚ forces funext" — stale; Rungs 1–6 landed with the
+  `Vec ℚ n` carrier. The note *body* is current.
+| Fixed in this session (index line corrected to match the body).
+|===
+
+=== Recommended order of attack
+
+. *F4 + F2 in parallel* (A4, A2) — tractable, independent of F1, each
+  earns back a qualified/real claim regardless of F1. Highest ROI.
+. *F1 coassoc* (A1) — one obligation, feasibility decided; closes the
+  make-or-break and unlocks *F3* (A3).
+. *Doc-integrity* (D) — reconcile alongside step 1; removes a drift
+  vector at near-zero cost.
+. *Buchholz* (B) — separate long-tail; keep the `ExtendedOrder`
+  wrapper load-bearing. Not paper-blocking.
+. *`characteristic/`* (C) — lowest priority; EI-2 already terminated.
+
 == Status
 
 * *2026-05-18 — created.* Pillar F opened post-R-2026-05-18.
+* *2026-05-18 — full-repo proof-debt audit.* Added the consolidated
+  ledger above (items A–E). Confirmed zero postulates / zero escape
+  pragmas across all 88 modules; no hidden debt. No claim moved. F1
+  feasibility spike is the immediate next action. No gate passed yet;
+  no reframed claim has moved.
 * *2026-05-18 — F1 feasibility spike run* (`proofs/agda/EchoGradedComonadF1.agda`,
   typechecks `--safe --without-K`, *zero postulates*). Result: **F1
   NOT YET PASSED, feasibility strongly positive (evidence-based, not