examples: Example 9 — parser residue (balanced parens)

[hyperpolymath]

Adds proofs/agda/EchoExampleParser.agda — Example 9 from the
presentation-dependence cluster identified by PR #76
(docs/echo-types/examples.md §9).

What lands

• Toy Token (LP/RP) and parses : List Token → Bool (depth-counter
  balanced-parens decider — left-to-right state machine that aborts on
  negative depth and accepts iff final depth is zero).
• Three concrete distinct token streams both parsing successfully:
  []ₜ, paren-pair = ()(), paren-nested = (()).
• Headlines:
  • parses-non-injective — Σ-witness that distinct streams collapse
    to the same Boolean.
  • echo-parse-empty / echo-parse-pair / echo-parse-nested — three
    concrete Echo parses true carriers.
  • echo-parse-nested≢echo-parse-pair — the distinct-presentations
    headline; same shadow, distinct echoes.
  • parser-residue — the residue Σ-pair tying back to the
    EchoResidue-style framing (Boolean shadow forgets the stream).
• BalancedClosed grammar inductive (four concrete constructors) +
  the four named grammar witnesses (empty-balanced,
  paren-empty-balanced, paren-nested-balanced,
  paren-pair-balanced) for the derivation-tree side of the residue.
• Wired into All.agda + Smoke.agda (every headline pinned).

Model-shape choices

• Took the pragmatic Bool-shadow path (per the prompt's suggested
  alternative): parses is a recursive depth-counter, not a full
  Σ-style derivation extractor. This avoids _++_ reasoning that
  the example's headline (presentation-dependence) does not need.
• BalancedClosed enumerates the three concrete shapes we exhibit
  rather than passing through _++_-based concatenation — the
  closed-form constructors discharge each witness by case, keeping
  the file self-contained (no ++-lemma machinery, no rebuild of
  Balanced.bal-cat).
• parser-residue is the lightweight Σ-pair shape (cf.
  EchoResidue.collapse-residue-same); the full
  Cert-relation + section lowering apparatus is overkill for
  Example 9 — the point is that the shadow is non-injective on
  Echo, witnessed concretely.

Cluster relationship

Parsers are the canonical example of "structured loss" — the
parsed/not-parsed Boolean forgets the actual derivation tree. Echo
carries what's lost. Per examples.md §9, this is the example that
forces the presentation-dependent axis (taxonomy axis 4): the same
parse shadow can be reached from different token streams, and the
Echo distinguishes them.

Invariants

• --safe --without-K; no postulates, no funext, no escape pragmas.
• Clean-worktree Agda build green: agda --safe --without-K proofs/agda/{EchoExampleParser,All,Smoke}.agda exit 0.
• Base = main.

🤖 Generated with Claude Code

Co-Authored-By: Claude Opus 4.7 (1M context) noreply@anthropic.com

[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