Resolve the monad/comonad/adjunction variance of loss in --safe Agda

[hyperpolymath]

What & why

The sharpened understanding of an echo-type — a tropically-graded modality of structured information loss over the min-plus semiring (ℕ∪{∞}, min, +), recoverable exact on a homotopy fibre rather than complement-storing — left a precise live question:

the combining direction of loss is monadic (accumulation is μ : D_r (D_s A) → D_{r+s} A), so whether the right word is "graded comonad", "graded monad", or "graded adjunction (with the section as unit/counit)" is unsettled and is being resolved in --safe Agda rather than asserted.

R-2026-05-18 already retracted the unqualified "graded comonad" claim (a reindexing modality, no nested D_r D_s); this PR builds the nested maps the question is actually about and lets the type-checker decide.

The verdict (each clause a pinned theorem in EchoVariance.agda)

Clause	Theorem	Reuses
(1) Accumulation is monadic — μ total + canonical (definable from layered data alone)	accumulate	Echo-comp-iso-from
(2) Exact on the fibre — fixed-factoring round-trips are refl	accumulate-split-id, split-accumulate-id	Echo-comp-iso-{to,from}
(2′) Grade-0 section/retraction adjunction	recoverable-fibre	A↔ΣEcho
(3) Comonad direction fails for genuine loss — no recovery from a bare residue	no-bare-recovery, fibre-retains-lost-bit	no-section-of-collapsing-map
(4) "Graded comonad" = lossless complement-storing writer — F1's δ is coe along a type equality, inverted by μ-writer	μ-writer, writer-μ-section, writer-δ-section	EchoGradedComonadF1.{δ,D-+,coe}

One-line resolution. Echo (fibre-based loss) is a graded monad of accumulation (the + axis) with a fibre-exact section/retraction adjunction; it is not a graded comonad. The min axis (order / degrade) carries the reindexing modality; the + axis (accumulation) carries the monad. The graded-comonad reading is available only on the complement-storing writer, which is lossless — the resource neighbour echo-types is not. This sharpens R-2026-05-18 from "graded comonad withdrawn" to "decided against".

Informs the redesign

docs/echo-types/variance-resolution.adoc records the verdict and four consequences: keep the modality(min)/measure(+) split (it is the variance answer); name the accumulation monad on the measure axis; read EchoGradedComonad/F1/F3 as the complement-storing neighbour on the record; state recoverability as the grade-0 adjunction, never an all-grade comonadic extract/duplicate.

Files

• proofs/agda/EchoVariance.agda (new) — --safe --without-K, zero postulates, reuses only existing kernel theorems.
• All.agda import; Smoke.agda pin block (10 headlines).
• docs/echo-types/variance-resolution.adoc (new) — the verdict + redesign consequences + honest-scope NotProved-*.
• echo-kernel-note.adoc + MAP.adoc — EchoVariance classified [REAL].
• paper.adoc Reframing note — follow-up F-2026-06-19.

Verification

• agda proofs/agda/All.agda → exit 0
• agda proofs/agda/Smoke.agda → exit 0
• scripts/kernel-guard.sh → PASS (Check A funext-free cone; Check B classification in sync)
• zero postulates; --safe --without-K throughout

🤖 Generated with Claude Code

https://claude.ai/code/session_01Rw1RpYXU5Q7rzy2bVofVeB

---

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 6 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 -- 17 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 17 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