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

[hyperpolymath]

Stacked on #47 (corrective reframe). Doc-only; moves no claim.

What this does

Full-repo proof-debt audit added as a single consolidated ledger in docs/echo-types/earn-back-plan.adoc. Confirmed zero postulates / zero escape pragmas across all 88 Agda modules — no hidden debt; every catalogued item is disclosed-in-comment or structural-fidelity.

Ledger (items A–E2)

• A1–A4 — Pillar F gates: F1 gc-coassoc (open, not postulated, feasibility positive); F2 StepND second model; F3 second comonad model; F4 funext-parameterised universal property.
• B — Buchholz _<ᵇ_ direct-constructor presentation incomplete (same-binder sub-cases deferred pending K-free reformulation); ExtendedOrder.agda is the honest closed WF wrapper. Off the paper critical path.
• C — characteristic/ open obligations (general recipe-non-triviality, Mode-is-loss-only, ChoreoInjective 2–5). EI-2 unaffected (terminated-negative). RoleRole.agda reclassified as a closed negative result, not a debt.
• D — docs/roadmap-gates.adoc is cited by ≥7 docs but does not exist; canonical role split across retractions.adoc / earn-back-plan / next-questions.adoc. Lead paragraph corrected; reconcile by back-link, not by fabricating retroactive gate history.
• E1 — Transport.agda two symbolic-ℚ open items; funext sidestepped via Vec ℚ n (no funext debt).
• E2 — stale MEMORY.md index line for transport Gate-3 corrected to match the (current) note body.

Includes a recommended order of attack (F4+F2 parallel → F1 coassoc → doc-integrity → Buchholz → characteristic).

🤖 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 4 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