theory: AntiEchoTropicalGeneric — generic-codomain lift of the tropical decomposition

[hyperpolymath]

Summary

Lifts the concrete ℕ-scored tropical decomposition from
AntiEchoTropical.agda to an arbitrary ordered codomain. Closes the
"generic-codomain version is deferred (would need a `≤`-bearing
ordered codomain)" remark that has lived in AntiEchoTropical's
preamble since #72.

What lands

AntiEchoTropicalGeneric.agda — new module

record OrderedCodomain : Set₁ where
  field
    B    : Set
    _≤_  : B → B → Set
    _<_  : B → B → Set
    ≤⇒¬< : ∀ {y n : B} → y ≤ n → n < y → ⊥
    ¬<⇒≤ : ∀ {y n : B} → (n < y → ⊥) → y ≤ n

The first three fields are pure structure; the latter two are the
order conversions. ≤⇒¬< is always available; ¬<⇒≤ is the entire
content of the "decidable order" hypothesis in the concrete ℕ case —
factored out as a field rather than baked into the codomain.

Three theorems in module Generic (OC : OrderedCodomain):

• antiecho-tropical-decompose-gen — pure Σ-reshape iso between
  TropEchoG s y and Echo s y × (∀ z → y ≤ s z). refl round-trips,
  does NOT use the order at all (structural only).
• optimality-as-antiecho-flavour-gen-to/from — (∀ z → y ≤ s z)
  ↔ (∀ z → s z < y → ⊥). Uses ≤⇒¬< / ¬<⇒≤ from the interface.
• tropdecomp-antiecho-gen-to/from — composite
  TropEchoG ↔ Echo × (Π-of-AntiEcho-flavoured-misses).

Sanity instance ℕ-ordered-codomain : OrderedCodomain pinned in
Smoke.agda so the interface is demonstrably inhabitable.

Preamble updates (zero Agda content change)

• AntiEcho.agda — obligation 6 line updated to point at both the
  concrete and generic landings
• AntiEchoTropical.agda — "generic-codomain version is deferred"
  replaced by pointer to the new module

Test plan

• agda proofs/agda/AntiEchoTropicalGeneric.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
• OrderedCodomain, ℕ-ordered-codomain, module Generic pinned
• No postulates, no funext, no escape pragmas

Scope

The concrete AntiEchoTropical.agda module is unchanged (only its
preamble comment updated). The two coexist: concrete remains the
canonical landing for ℕ-scored tropical; generic is the abstract
sibling for downstream users at other ordered codomains.

Dependencies

Depends on #90 (antiecho-partition-dec). Branch based on
antiecho-partition-dec; will rebase onto main once #90 lands.
Disjoint from #88 (F3).

🤖 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