theory: EchoCost — Axis 8 cost-indexed refinement (thin slice)

[hyperpolymath]

Adds proofs/agda/EchoCost.agda (and EchoCostInstance.agda for
smoke pins), the cost-indexed refinement of Echo named in
docs/echo-types/taxonomy.md §Axis 8 (refinement 1: full
cost-tracking via an explicit cost algebra). Sits orthogonal to the
already-landed qualitative Axis-8 artefacts (EchoDecidable,
EchoFiberCount, EchoAccess); names the resource-budget dimension
of the axis.

What lands

• CostAlgebra — ordered commutative-monoid-flavoured cost carrier
  (Cost, zero, _+_, _≤_, ≤-refl, ≤-trans, +-identityˡ,
  +-mono-≤). Right-identity / associativity / commutativity
  deliberately omitted — the headlines close without them; layering
  pattern matches BalancedTolerance in EchoApprox.agda.

• EchoC cost c f y := Σ A (λ x → f x ≡ y × cost x ≤ c)

• Headlines:

  • echo-cost-intro / -≤ — zero-budget intro
  • echo-cost-relax — monotone in budget
  • echo-cost-forget — Axis-8 → Axis-1 projection (the shadow obligation of every Axis-8 refinement)
  • echo-cost-compose — two-source additive composition (combiner + image-equation + cost-receipt triple, no funext)
  • echo-cost-compose-mono — single-source specialisation
  • echo-cost-forget-compose-mono-A — compose-then-forget agrees with the bare composite on the A-component
  • echo-cost-relax-zero — (zero + c) ≡ c (the budget lever)

• Wired into All.agda (alphabetical, between EchoApproxInstance and EchoIndexed) and Smoke.agda (per-lemma using clause on EchoCostInstance, mirroring the EchoApproxInstance pattern).

Design judgement calls

• CostAlgebra field minimality. Took only the laws needed to
  close the four headlines (+-identityˡ for the budget round-trip,
  +-mono-≤ for compose). Right-identity / commutativity / associativity
  belong on a separate BalancedCostAlgebra record if a downstream
  proof needs them — same layering as BalancedTolerance.

• Composition shape (echo-cost-compose). Took the more general
  two-source first-order shape with an explicit combine : A → B → A'',
  caller-supplied image-eq, and caller-supplied cost-bound. Strictly
  more general than restricting to an endomorphic outer leg
  (the EchoApprox.echo-approx-compose shape, g : B → B); the
  single-source corner falls out as echo-cost-compose-mono. No
  funext used; image equation is supplied, not derived from a
  pointwise homotopy.

• Trivial-on-⊤ instance via EchoCostInstance.agda. Closes the
  CLAUDE.md "Working rules" invariant for parameterised modules
  (EchoCost.Cost is parameterised over K : CostAlgebra ℓ).
  Exact recipe of EchoApproxInstance.agda post-PR-hygiene: per-lemma Smoke pins for EchoApprox via concrete instance module #71.

Invariants

• --safe --without-K on every new module
• No postulates, no funext, no escape pragmas, no believe_me
• Clean-worktree Agda build green: EchoCost.agda + EchoCostInstance.agda + All.agda + Smoke.agda all exit 0 (verified after find . -name '*.agdai' -delete)

🤖 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