docs: tidy after earn-back closure + theory-work closure + examples cluster landed

[hyperpolymath]

Summary

Three small accuracy passes through docs/echo-types/ after the
earn-back programme, the §"Theory work — no proof assistant needed"
section, and the canonical examples cluster (5/9/10) all closed in
this session. Pure prose; no Agda changes.

1. roadmap.md §"Theory work" — two stale items refreshed

• Axis 8 line said the decidability-respecting candidate had
  shipped but listed the other three as still candidate refinements.
  All four have now shipped: EchoDecidable, EchoCost (theory: EchoCost — Axis 8 cost-indexed refinement (thin slice) #85),
  EchoAccess (theory: Axis 8 graded access modality — thin slice (Access, ≤a, ≤a-trans, ≤a-prop) #68 / theory: Axis 8 sweep — join + composition trio (Rungs A + B; Rung C deferred) #75), EchoSearch (theory: EchoSearch — Axis 8 witness-search machine (thin slice) #80). Updated to credit all
  four.
• Negative / co-echoes line was [unblocked]; now [landed] —
  AntiEcho (theory: AntiEcho thin slice — Σ-dual of Echo (carrier + map-over + disjointness) #69), tropical decomposition concrete + generic (theory: AntiEcho × IsArgmin tropical decomposition #72 +
  theory: AntiEchoTropicalGeneric — generic-codomain lift of the tropical decomposition #91), antiecho-partition-dec (theory: antiecho-partition-dec — per-element classification (deferred obligation 5) #90). Names the coecho.md §5
  obligation-5 / obligation-6 closures explicitly.

After these edits, every item in §"Theory work — no proof assistant
needed" is either [landed] or [ruled out]/[refreshed] — the
section is genuinely closed.

2. roadmap.md §"Example work" — three items landed

• ex. 5 (EchoExampleProvenance, examples: Example 5 — database provenance (K-provenance semiring) #81) → [landed]
• ex. 9 (EchoExampleParser, examples: Example 9 — parser residue (balanced parens) #83) → [landed]
• ex. 10 (EchoExampleAbsInt, examples: Example 10 — abstract interpretation (Sign lattice) #82) → [landed]

Only ex. 6 (approximate-echo numeric example) remains [unblocked].

3. earn-back-plan.adoc — stale roadmap-gates.adoc claim corrected

• Header note used to say "the gate discipline was historically
  attributed to a roadmap-gates.adoc; that file does not exist
  in-tree". The file does exist (created 2026-05-18; see its
  preamble). Header rewritten to list roadmap-gates.adoc alongside
  retractions.adoc / this plan / next-questions.adoc as the four
  canonical loci.
• Ledger row D (the "doesn't exist" entry) marked CLOSED 2026-05-20
  with the cite reflecting current reality.

Test plan

• Pure docs / .adoc / .md edits — no Agda touched
• agda proofs/agda/All.agda exit 0 (confirms docs match code)
• agda proofs/agda/Smoke.agda exit 0
• No retracted-claim language moved; no earned-back claim
  overclaimed; paper.adoc / types-abstract.adoc /
  conservativity.adoc untouched

Scope

Disjoint from all currently-open PRs:

• F3 PASSED: GradedComonadStructure + two non-isomorphic-grade-monoid instances #88 (F3) — touches Agda + retractions.adoc (different sections)
  • earn-back-plan.adoc Status (different section from header /
    ledger-D)
• theory: antiecho-partition-dec — per-element classification (deferred obligation 5) #90 (partition-dec) — touches Agda only
• theory: AntiEchoTropicalGeneric — generic-codomain lift of the tropical decomposition #91 (generic-codomain) — touches Agda + preamble comments

No retracted claim is moved. No earned-back claim is overclaimed.
paper.adoc / types-abstract.adoc / conservativity.adoc are
intentionally untouched (owner-gated, per the posture set by #86 /
#88).

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 10 issues detected

Severity	Count
🔴 Critical	0
🟠 High	5
🟡 Medium	5

View findings

[
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/cache@v4 needs attention",
    "type": "unpinned_action",
    "file": "agda.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "No dependabot.yml or renovate.json found in echo-types",
    "type": "DependencyUpdate",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "high",
    "remediation": "Add .github/dependabot.yml or renovate.json configuration.",
    "scorecard_check": "Dependency-Update-Tool"
  },
  {
    "reason": "Nominal-only SAST in echo-types: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
    "type": "StaticAnalysis",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Add CodeQL or equivalent SAST workflow.",
    "scorecard_check": "SAST"
  },
  {
    "reason": "1 workflow(s) with tag-pinned (not SHA-pinned) actions in echo-types",
    "type": "DependencyPinning",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Pin GitHub Actions and Docker base images by SHA hash.",
    "scorecard_check": "Pinned-Dependencies"
  },
  {
    "reason": "Repository has 1 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence