theory: AntiEcho × IsArgmin tropical decomposition

[hyperpolymath]

Summary

Cashes the headline claim from /tmp/echo-types-exploration/coecho.md §3 ("Resolution of the EchoTropical tension") at the structural level: TropEcho / IsArgmin decompose into Echo evidence + a Π-quantified complement bound, with an AntiEcho-flavoured corollary exposing that bound as a Π of negative data over the candidate set.

New module proofs/agda/AntiEchoTropical.agda. Neither AntiEcho.agda (from #69) nor EchoTropical.agda is modified — the bridge stays isolated so PR scope is tight.

Headline theorem (both directions, both round-trips refl, packaged as _↔_)

antiecho-tropical-decompose :
  ∀ (y : ℕ) → TropEcho y ↔ (Echo score y × (∀ z → y ≤ score z))

The forward direction projects (x , p , bnd) ↦ ((x , p) , bnd) — pure Σ-re-association because the optimality factor ∀ z → y ≤ score z doesn't depend on x. The backward direction undoes it. Both round-trips are definitionally refl. No decidability, no funext, no path algebra. Packaged via stdlib Function.Bundles._↔_ and mk↔ₛ′, matching the convention from Echo-comp-iso / cancel-iso.

IsArgmin-level restatement (the per-element identity)

isargmin-decompose :
  ∀ (x : Candidate) (y : ℕ) →
  IsArgmin x y ↔ ((score x ≡ y) × (∀ z → y ≤ score z))

IsArgmin IS the product by definition, so the iso to the product is the identity. Pinned for callers thinking in IsArgmin-shaped terms.

AntiEcho-flavoured corollary (the Π-bound as a Π of misses)

The optimality factor ∀ z → y ≤ score z is equivalent on ℕ to the AntiEcho-shaped statement "no candidate witnesses a value strictly below y":

optimality-as-antiecho-flavour-to   : (∀ z → y ≤ score z) → (∀ z → score z < y → ⊥)
optimality-as-antiecho-flavour-from : (∀ z → score z < y → ⊥) → (∀ z → y ≤ score z)

with the small order-conversion lemmas ≤⇒¬< / ¬<⇒≤ shipped in-module. Composite version (Echo + Π-of-negation):

tropdecomp-antiecho-to   : TropEcho y → Echo score y × (∀ z → score z < y → ⊥)
tropdecomp-antiecho-from : Echo score y × (∀ z → score z < y → ⊥) → TropEcho y

This is the Π-form AntiEcho variant from coecho.md §1(c) (AntiEcho_Π = ¬ Echo), specialised to the strict-below stratum. The Σ-form AntiEcho carrier from AntiEcho.agda is the witness-recording primitive; the Π-form above is the exhaustive global statement that names what IsArgmin was carrying implicitly.

Scope notes

• Specialised to the concrete Candidate → ℕ setting of EchoTropical.agda. A generic-codomain version would need a ≤-bearing ordered codomain and the decidability hypothesis from coecho.md §3 closing remark — deferred.
• Smoke.agda pins all 14 headlines via using so silent renames or a slide back to ad-hoc tropical decoration trips CI fast.
• --safe --without-K clean. No postulates. No funext. No path algebra beyond constructor-driven trichotomy on _≤_/_<_.

PR base / stacking

Branched from origin/theory/antiecho-thin-slice (so AntiEcho is in scope) but PR base is main per the stacked-PR-orphan-trap policy. The cumulative diff currently includes #69's content; when #69 merges the diff simplifies automatically.

Test plan

• CI runs agda -i proofs/agda proofs/agda/All.agda — exits 0.
• CI runs agda -i proofs/agda proofs/agda/Smoke.agda — exits 0.
• All 14 pinned headlines in Smoke.agda resolve.
• No new postulates / escape pragmas introduced.

Note on local verification. Settings restrictions in this sandbox blocked local agda invocation on this worktree (the project's Bash(agda *) allow rule did not apply to this session). Proofs are pure Σ-currying / pattern-matching + two small ℕ order-conversion lemmas — expected to typecheck on the existing CI gate.

Refs

• Refs theory: AntiEcho thin slice — Σ-dual of Echo (carrier + map-over + disjointness) #69 — depends on the AntiEcho module from the AntiEcho thin slice.
• Refs docs/echo-types/roadmap.md CoEcho entry ("Possibly resolves the quantitative / structural tension hinted at by EchoTropical").
• Refs /tmp/echo-types-exploration/coecho.md §3 ("Resolution of the EchoTropical tension") + §5 obligation 6 (coecho-tropical-decompose).

Does NOT Close anything. The CoEcho roadmap entry stays open until decided by the owner; this PR cashes the structural half.

🤖 Generated with Claude Code

[hyperpolymath]

Build verified from parent session (sandbox quirk blocked the agent's local agda run; same workaround as PR #71):

$ cd /tmp/echo-types-worktrees/tropical-decomp
$ LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/All.agda; echo "exit: $?"
... (full module check, including Checking AntiEchoTropical and Checking Smoke)
exit: 0

$ LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/Smoke.agda; echo "exit: $?"
exit: 0

--safe --without-K invariants intact (Agda would have errored otherwise). Both round-trips of antiecho-tropical-decompose and the AntiEcho-flavoured corollary are well-typed; the 14 Smoke.agda pins resolve at top-level.

[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