bridges(tropical): citation-level correspondence appendix (EchoTropical ↔ tropical-resource-typing)

[hyperpolymath]

Summary

• New sibling doc docs/echo-types/tropical-correspondence.md recording the first citation-level cross-prover correspondence between proofs/agda/EchoTropical.agda (this repo) and the adjacent hyperpolymath/tropical-resource-typing repo (Isabelle Tropical.thy + Lean4 TropicalSessionTypes.lean).
• Closes the "Adjacent repo not recently audited" blocker on the Tropical row of cross-repo-bridge-status.md (already noted as a follow-up by sibling PR docs(bridges): refresh cross-repo bridge status; bake in CNO Agda↔Coq↔Lean4 correspondence #64).
• First alignable theorem pair: Agda ⊕-idem ↔ Isabelle trop_add_idem. Both proved clean (Agda --safe --without-K, Isabelle simp lemma).
• Research-phase correction: Lean has no named idempotence theorem on tAdd; the closest analog is tropical_grade_le_sequentialTotal as the downstream dioid consumer of add_idem. The Lean cell is therefore — for the bare law, with the consumer theorem noted.
• Carrier divergence (Agda ℕ vs Isabelle/Lean lifted carrier with −∞ bottom) recorded as intentional. Adjacent-side multiplicative structure marked unilateral adjacent-side; echo-side Echo/Candidate/bridge headlines marked unilateral Agda-side.
• Long-game target Tropical_Ordinal_Bridge.thy ↔ echo-types ordinal track firewalled behind Bachmann–Howard per roadmap.md.
• Citation-level only: no FFI surface between Agda and Isabelle/Lean. Each side carries its own independent proof.

Coordination

• Sibling PR docs(bridges): refresh cross-repo bridge status; bake in CNO Agda↔Coq↔Lean4 correspondence #64 (branch docs/cross-repo-bridge-status-sweep-2026-05-20) owns cross-repo-bridge-status.md; this PR does NOT touch that file.
• Sibling Lane 3 owns the ⊕-idem Smoke pin; this PR does NOT touch proofs/agda/Smoke.agda or any .agda file.
• This PR only adds the new file docs/echo-types/tropical-correspondence.md.

Test plan

• No .agda files touched, so no Agda build is required; sanity check that EchoTropical.agda still parses under LC_ALL=C.UTF-8 agda --safe --without-K -i proofs/agda proofs/agda/EchoTropical.agda (it should, since this PR makes no Agda edits).
• Visual review of the correspondence table for name-by-name accuracy against the three source files.
• Confirm no merge conflict with sibling PR docs(bridges): refresh cross-repo bridge status; bake in CNO Agda↔Coq↔Lean4 correspondence #64 (different file).

🤖 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