docs: machine-doc currency sweep + wiki depth (tutorial + maintainer runbook)

[hyperpolymath]

What

Session close-out, options 2 + 3 (follow-on to the merged #265 wiki refresh and #267 6a2 currency fix).

Option 2 — machine-doc currency sweep

• META.a2ml: add adr-012 recording the ordinal/Buchholz track retirement (D-2026-06-21) + extraction disposition (tracking Extract the retired ordinal/Buchholz/Veblen ladder to its own ordinal-notation repo #263), per the ADR-versioning discipline; bump last-updated → 2026-06-21.
• cross-repo-bridge-status.md: the Tropical row's long-game "Tropical_Ordinal_Bridge.thy ↔ echo-types ordinal track" alignment now notes it moves with the ordinal extraction (Extract the retired ordinal/Buchholz/Veblen ladder to its own ordinal-notation repo #263), it is not an echo-types deliverable; bump Last updated.

Option 3 — wiki depth (the "beyond basic run-through" layer)

• wiki/Tutorial-Consuming-Echo.adoc (new) — end-user from-the-outside-in walkthrough: the one idea, the one definition, making/reading an echo (echo-intro), the totality completion A ↔ Σ B (Echo f), the no-section boundary, and four real in-estate consumers (phronesis verdict-provenance, KitchenSpeak @-witness, Invariant Path, EchoAggregation), plus honest scope.
• wiki/Maintainer-Runbook.adoc (new) — build cone, the three identity gates + failure actions, rung-consolidation policy, machine-doc currency discipline (with the 2026-06-21 ordinal sweep as the worked example), release checklist, CI lanes + parked scorecard/mirror billing-wall failures, and branch hygiene.
• wiki/Home.adoc — both pages wired into the Start-here index and the maintainer / end-user audience lanes.

Why

Completes the close-out: the human↔machine docs are now consistent on the ordinal retirement across STATE.a2ml (#267), META.a2ml, the bridge ledger, and the wiki; and each audience lane now has a real deep-dive page, not just a reading order.

Scope

Docs-only (3 prose files + 2 machine-doc files). No Agda touched; proof cone unchanged. New prose pages are CC-BY-SA-4.0 (estate long-form prose licence).

Refs #263.

🤖 Generated with Claude Code

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 6 issues detected

Severity	Count
🔴 Critical	0
🟠 High	3
🟡 Medium	3

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": "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": "Repository has 9 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Scorecard): TokenPermissionsID -- Token-Permissions -- 19 day(s) old [STALE]",
    "type": "CSA001",
    "file": ".github/workflows/scorecard.yml",
    "action": "escalate",
    "rule_module": "code_scanning_alerts",
    "severity": "high"
  },
  {
    "reason": "Code-scanning alert TokenPermissionsID (high) at .github/workflows/scorecard.yml is 19 days old (threshold: 7 days) -- overdue for remediation",
    "type": "CSA003",
    "file": ".github/workflows/scorecard.yml",
    "action": "escalate",
    "rule_module": "code_scanning_alerts",
    "severity": "high"
  },
  {
    "reason": "Code-scanning alert hypatia/code_safety/agda_postulate dismissed as 'false positive' -- ensure dismissal is documented and justified",
    "type": "CSA004",
    "file": "proofs/agda/EchoImageFactorizationPropPostulated.agda",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence