docs(wiki): refresh to 2026-06-21 + developer/maintainer/end-user split

[hyperpolymath]

What

Session close-out: bring the wiki up to date and give it the audience structure it was missing.

wiki/Home.adoc

• New "Who is this for?" tri-split — reading orders for the three audiences:
  • Developers (proof discipline → CLAUDE.md rung-state → module map → build);
  • Maintainers (identity gates + failure actions → retractions → CI cone → 6a2/EI-2);
  • End users (FOUNDATION_CONTRACT.md → Overview honest-scope → EchoTypes.jl → a worked Deniability result).
• One-line status refreshed 2026-06-13 → 2026-06-21: ordinal track RETIRED (D-2026-06-21); variance resolved (Resolve the monad/comonad/adjunction variance of loss in --safe Agda #243, graded monad of accumulation, not comonad); aggregation generalised (Add EchoAggregation module — Monoid + GroupAggregator carriers for SQL aggregation-as-fold (consumer: affinescript db-theory #3) #175); establishment Pillar E in-repo half complete with order-type fidelity (D-2026-06-14) the one named OPEN external problem.

wiki/Roadmap.adoc

• Ordinal track reframed from "the active bottleneck" to RETIRED, with the extraction disposition, the verified firewall (OmegaMarkers ← Buchholz.Syntax ← EchoOrdinal STAY; rest of Ordinal/ MOVES), and the frozen open items. Tracking: Extract the retired ordinal/Buchholz/Veblen ladder to its own ordinal-notation repo #263.
• Carried-debt line fixed — the ordinal WF items moved out with the retirement.

Why

The wiki status block predated the D-2026-06-21 ordinal retirement and still pointed users at Bachmann–Howard as live work, and there was no developer/maintainer/end-user navigation.

Scope

Docs-only (two wiki/*.adoc files). No Agda touched; the proof cone is unchanged.

Companion allocation issues filed this session: #263 (ordinal extraction), #264 (real-valued entropy).

🤖 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