theory: antiecho-partition-dec — per-element classification (deferred obligation 5)

[hyperpolymath]

Summary

Lands obligation 5 of coecho.md §5, deferred since the original
AntiEcho thin slice (PR #69, commit 428b4b8): the per-element
partition of A into the Echo-side and the AntiEcho-side, given
decidability of f x ≡ y.

antiecho-partition-dec : ∀ {A B} {f : A → B} {y : B}
  (x : A) → Dec (f x ≡ y) → Echo f y ⊎ AntiEcho f y

antiecho-partition-codomain-dec : ∀ {A B} {f : A → B} {y : B}
  → (∀ b → Dec (b ≡ y)) → (x : A) → Echo f y ⊎ AntiEcho f y

Companion to the existing antiecho-disjoint (per-element). Together
they exhibit A as the disjoint union of the Echo-side and AntiEcho-
side parameterised by y: every x classifies to one side, and no
x appears on both.

Correction to the prior preamble

The earlier comment claimed the asymmetric joint statement
Echo f y → AntiEcho f y → ⊥ (with possibly distinct domain
witnesses) "requires decidability on the codomain to collapse the two
witnesses". That joint statement is not a theorem at any
decidability strength — counterexample with f : Bool → Bool,
f = id: both Echo f true (via (true, refl)) and AntiEcho f true
(via (false, false≢true)) are inhabited, so the joint statement is
refuted by the model. The actual content of the deferred "obligation
5" is the per-element classification above; the preamble is corrected
to say so explicitly.

Test plan

• agda proofs/agda/AntiEcho.agda exit 0
• agda proofs/agda/All.agda exit 0 under --safe --without-K
• agda proofs/agda/Smoke.agda exit 0 under --safe --without-K
• Both new lemmas pinned in Smoke.agda
• No postulates, no funext, no escape pragmas

Scope

Tiny additive change. Disjoint from any open PR (#88 F3 touches
EchoGradedComonad* modules; this touches AntiEcho only).

The companion small deferral — generic-codomain antiecho-tropical-decompose
(lifting AntiEchoTropical.agda's concrete ℕ-scored version to an
abstract ordered-codomain interface) — is not addressed here; it
requires designing the interface and is a separate slice.

🤖 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