From 2a2ec9000d7360162b2ffa25be818859d33a7df7 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 19:37:14 +0100 Subject: [PATCH] docs: tidy after earn-back closure + theory-work closure + examples cluster landed MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three small accuracy passes through `docs/echo-types/`: 1. `roadmap.md` §"Theory work — no proof assistant needed" — the section is now genuinely closed. Updated two stale items: * Axis 8 line said "the *decidability-respecting* candidate has shipped" and listed the other three as still candidate refinements. All four have now shipped: EchoDecidable (decidability), EchoCost (cost-indexed, #85), EchoAccess (graded access, #68/#75), EchoSearch (witness-search, #80). * Negative / co-echoes line was [unblocked]; now [landed] — AntiEcho (#69), tropical decomposition concrete + generic (#72 + #91), antiecho-partition-dec (#90). Names the obligation-5 / obligation-6 closures explicitly. 2. `roadmap.md` §"Example work" — three [unblocked] items now [landed]: ex. 5 (EchoExampleProvenance, #81), ex. 9 (EchoExampleParser, #83), ex. 10 (EchoExampleAbsInt, #82). Only ex. 6 (approximate-echo numeric example) remains [unblocked]. 3. `earn-back-plan.adoc`: * Header note "the gate discipline was historically attributed to a `roadmap-gates.adoc`; that file does not exist in-tree" is stale — the file IS in tree (created 2026-05-18). Header rewritten to list `roadmap-gates.adoc` alongside `retractions.adoc` / this plan / `next-questions.adoc` as the four canonical loci. * Ledger row D ("roadmap-gates.adoc does not exist") marked CLOSED 2026-05-20; cite reflects current reality. Pure prose / docs only. No Agda content changes. `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` exit 0 under `--safe --without-K` (verified — confirms the docs say what the code does). Refs the closure side of #84 / #86 / #88 / #90 / #91 — does not modify any Agda module, does not move any earned-back / retracted claim. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/echo-types/earn-back-plan.adoc | 26 +++++++++------ docs/echo-types/roadmap.md | 50 ++++++++++++++++++----------- 2 files changed, 47 insertions(+), 29 deletions(-) diff --git a/docs/echo-types/earn-back-plan.adoc b/docs/echo-types/earn-back-plan.adoc index 5d3d6e6..92216d4 100644 --- a/docs/echo-types/earn-back-plan.adoc +++ b/docs/echo-types/earn-back-plan.adoc @@ -12,11 +12,13 @@ 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. 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`.) +abandon criteria, outcomes logged in `docs/retractions.adoc`. The +canonical loci of the gate discipline are +`docs/roadmap-gates.adoc` (the protocol document, created 2026-05-18 +to resolve the earlier dangling reference), `docs/retractions.adoc` +(the append-only retraction + earn-back log), this plan (the +falsifiable program), and `docs/next-questions.adoc` (the open +questions register). toc::[] @@ -237,11 +239,15 @@ single index; it moves no claim. 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). +| Doc-integrity: previously this entry recorded that + `docs/roadmap-gates.adoc` was cited as the canonical gate ledger + but did not exist in-tree. The file *does* exist (created + 2026-05-18; see its preamble) and the dangling-reference issue is + resolved. +| *CLOSED 2026-05-20.* `docs/roadmap-gates.adoc` is in tree as the + Gates Protocol. The canonical-loci list at the top of this plan + has been updated to include it explicitly alongside + `retractions.adoc` / `next-questions.adoc`. | E1 | `examples/Transport.agda` (Gate-3): two disclosed open items, both diff --git a/docs/echo-types/roadmap.md b/docs/echo-types/roadmap.md index af4306d..d0d13f1 100644 --- a/docs/echo-types/roadmap.md +++ b/docs/echo-types/roadmap.md @@ -37,17 +37,23 @@ Paths marked **[unblocked]** can proceed today. Paths marked lane C tracks the `taxonomy.md` §Axis-2 write-up). - **[landed]** Axis 8 (information-theoretic vs computational access): promoted from the candidates list to a numbered axis. - *Three* remaining candidate refinements of `Echo` - (cost-indexed, graded access modality, witness-search abstract - machine); the *decidability-respecting* candidate has shipped - as `proofs/agda/EchoDecidable.agda` (`EchoDec f y = Dec (Echo f - y)` with six headline lemmas including `echo-dec-intro`, - `echo-dec-fin`, `echo-dec-compose-iso`; see `taxonomy.md` §8). - Follow-up: pick one of the remaining three refinements and - formalise. -- **[unblocked]** Negative / co-echoes: formulate `CoEcho(f)` and its - relationship to `Echo(f)`. Possibly resolves the quantitative / - structural tension hinted at by `EchoTropical`. + Every candidate refinement is now mechanised. Decidability- + respecting: `proofs/agda/EchoDecidable.agda`. Cost-indexed (over + an abstract `CostAlgebra`): `EchoCost.agda` + `EchoCostInstance.agda` + (PR #85). Graded access modality: `EchoAccess.agda` (PRs #68 + + #75). Witness-search abstract machine: `EchoSearch.agda` + + `EchoSearchInstance.agda` (PR #80). See `taxonomy.md` §8. +- **[landed]** Negative / co-echoes: `AntiEcho f y := Σ A (λ x → f x ≢ y)` + shipped as `proofs/agda/AntiEcho.agda` (PR #69) with + `antiecho-{intro, disjoint, map-over}`, plus per-element + classification `antiecho-partition-dec` (PR #90, closes + `coecho.md` §5 obligation 5). Distinct from `EchoFiberTriangulation.CoEcho` + (which is the trivial opposite-orientation fibre); see naming + rationale in `AntiEcho.agda`'s preamble. The tropical decomposition + `TropEcho y ↔ Echo score y × (∀ z → y ≤ score z)` lands at the + concrete ℕ-scored level in `AntiEchoTropical.agda` (PR #72) and at + an abstract `OrderedCodomain` interface in `AntiEchoTropicalGeneric.agda` + (PR #91, closes `coecho.md` §5 obligation 6). - **[ruled out — see docs/echo-types/decisions/no-2-cat.adoc]** 2-categorical shape. Every would-be 2-cell in the landed code is `refl` or forced trivial by propositionality (`≤g-prop`, @@ -178,14 +184,20 @@ Paths marked **[unblocked]** can proceed today. Paths marked - **[unblocked]** Complete worked numeric example (ex. 6) with the approximate-echo shape, once the definition lands. -- **[unblocked]** Parser residue example (ex. 9) as a toy Agda - example: parse of balanced parens, echo carries token stream. -- **[unblocked]** Abstract-interpretation example (ex. 10) via a - Sign lattice. -- **[unblocked]** Database provenance example (ex. 5) via - K-provenance semiring — text-only pass first, Agda optional. -- **[unblocked]** Extend `EchoExamples.agda` with two to three - further canonical entries. +- **[landed]** Parser residue example (ex. 9) — `EchoExampleParser.agda` + (PR #83): balanced parens, Boolean shadow `parses : List Token → + Bool` non-injective on `(())` vs `()()`, echo retains the token + stream. +- **[landed]** Abstract-interpretation example (ex. 10) — + `EchoExampleAbsInt.agda` (PR #82): Sign lattice `{neg, zero, pos}` + over a hand-rolled five-element integer carrier; collapses + `{m1, m2} ↦ neg`, `{z} ↦ zero`, `{p1, p2} ↦ pos`. +- **[landed]** Database provenance example (ex. 5) — + `EchoExampleProvenance.agda` (PR #81): K-provenance semiring, + distinct Bool-provenance rows projecting to the same payload. +- **[unblocked]** Extend `EchoExamples.agda` with further canonical + entries (post-#81/#82/#83 the cluster has good coverage; only + ex. 6 remains). ---