docs(proof-debt): refresh stale variance bullet — resolved by wired EchoVariance (#243)

[hyperpolymath]

What

A one-line-spirit refresh of docs/proof-debt.md: the 2026-06-16 ground-truth-audit bullet still flagged the monad/comonad/adjunction variance question as "genuinely open" — but it was settled four days later by the wired EchoVariance.agda (#243, 2026-06-20).

The fix

The bullet now:

• preserves the dated audit observation (true as of 2026-06-16: the only variance material was the orphaned experimental/echo-additive/ track + VarianceGate.agda, which self-declares "NO proven theorems");
• records the resolution: EchoVariance.agda (in All.agda, --safe --without-K, zero postulates) — echo is a graded monad of accumulation + a section/retraction adjunction exact on the grade-0 fibre, and is NOT a graded comonad (no-bare-recovery the obstruction; sharpens R-2026-05-18 from "withdrawn" to "decided against");
• points at the wired EchoVariance + docs/echo-types/variance-resolution.adoc as the citation, and notes the orphaned experimental track is the retired earlier attempt.

This keeps the audit's honesty (it was accurate when written) while removing the stale "open" status that contradicted the later wired result.

Docs-only; kernel-guard PASS. Verified EchoVariance is wired (All.agda:107) and variance-resolution.adoc exists.

🤖 Generated with Claude Code

https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 6 issues detected

Severity	Count
🔴 Critical	0
🟠 High	3
🟡 Medium	3

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": "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": "Repository has 8 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Scorecard): TokenPermissionsID -- Token-Permissions -- 18 day(s) old [STALE]",
    "type": "CSA001",
    "file": ".github/workflows/scorecard.yml",
    "action": "escalate",
    "rule_module": "code_scanning_alerts",
    "severity": "high"
  },
  {
    "reason": "Code-scanning alert TokenPermissionsID (high) at .github/workflows/scorecard.yml is 18 days old (threshold: 7 days) -- overdue for remediation",
    "type": "CSA003",
    "file": ".github/workflows/scorecard.yml",
    "action": "escalate",
    "rule_module": "code_scanning_alerts",
    "severity": "high"
  },
  {
    "reason": "Code-scanning alert hypatia/code_safety/agda_postulate dismissed as 'false positive' -- ensure dismissal is documented and justified",
    "type": "CSA004",
    "file": "proofs/agda/EchoImageFactorizationPropPostulated.agda",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence