docs: Pillar E paper — Evaluation section (clears [EXPAND])

[hyperpolymath]

Summary

Fills the Evaluation and discussion [EXPAND] stub in
docs/echo-types/paper.adoc with the content the NOTE explicitly
asked for:

• Per-pillar proof-size table (LOC / top decls / subst+rewrite /
  postulates) sourced from the modules at this commit.
• An honest reading of the common-upper-bound idiom — it removes
  subst because the equations carry no comonadic coherence (the
  modality is thin), not as a clever encoding saving. Reading the
  short proofs as a thesis-strengthening trick was retracted on
  2026-05-18 (R-2026-05-18); this section keeps the honest framing.
• Three honest bounds (where the construction does not
  extend): the EI-2 negative result; the funext-relative mediator
  property; the thinness-only content. Stated as bounds, not
  re-spun as features.
• Threats to validity, including the Gate-2 audit's own
  "single recipe" finding (docs/gate-2-handoff.adoc Observation
  G), consumer-evidence sample-size, the conservativity-is-evidence
  caveat, and the gate-discipline meta-caveat.

Adds [#ordinal-appendix] anchor + tightens the status banner to
note that the ordinal-appendix [EXPAND] is now the only one left
and is gated on Bachmann–Howard.

Refs: paper.adoc Pillar E [EXPAND] clear-out (CLAUDE.md priority
item 3 — "Evaluation: proof-size/cost table; quantify
common-upper-bound idiom vs naive subst").

Test plan

• agda proofs/agda/All.agda exit 0 under --safe --without-K
• agda proofs/agda/Smoke.agda exit 0 under --safe --without-K
• No postulates introduced (prose-only change)
• AsciiDoc renders: anchor <<ordinal-appendix>> resolves; table
  columns match
• (owner) review the proof-size numbers against the actual
  modules — table is a fingerprint, not a comparison-with-others
  claim

Non-overlap with parallel sessions

Touches only docs/echo-types/paper.adoc. Stays well clear of:

• The Brouwer-arithmetic / _<ᵇ⁻_ / rank-mono slices in
  proofs/agda/Ordinal/** (another session's Slices 1–5 territory).
• The ordinal-appendix [EXPAND] at line ~1200 (gated on
  Bachmann–Howard, firewalled per roadmap.md).
• docs/echo-types/types-abstract.adoc (submission-ready, hands
  off).

🤖 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