Commit 67ae5a6
docs(roadmap): right-size to solo-maintainer reality; preserve vision in appendix (#95)
## What & why
The former `ROADMAP.adoc` described a **7-year, $7.5M, 15-FTE**
programme (ISO/IEEE standards, a documentary, a SaaS offering, "10,000+
users") for a repo that is still discharging existence lemmas. The
near-term framing was wildly disproportionate to the actual state and
obscured the real next steps.
## Changes
- Rewrite the ROADMAP body as an honest solo-maintainer plan grounded in
`PROOF-STATUS.adoc`:
- Truthful proof ledger — 61 Coq + 52 Lean **axioms** disclosed; only
Coq (13 theories) + Agda (3 modules) actually reproduced; the referenced
Z3 `cno_properties.smt2` **does not exist**; Lean/Isabelle/Mizar not run
here.
- The general `reversible p ↔ ∃ p_inv, is_CNO(p;;p_inv) ∧
is_CNO(p_inv;;p)` bridge that `maa-framework` actually needs (currently
absent at the general level).
- The first three OND obligations (OND-1/2/3) as the MVP pillar.
- The CNO paper as a near-term, already-viable deliverable.
- Preserve the genuinely-accurate **OND two-pillar** section verbatim.
- Relocate the grand vision **in full** to a clearly-labelled
`Long-Horizon Vision (aspirational, unfunded)` appendix so nothing is
lost.
## Verification
Documentation-only. Figures cross-checked against `PROOF-STATUS.adoc`
and the axiom counts in `proofs/coq/**`.
## Context
Task **A9** of a broader estate assessment. No proof code changed (no
prover is available in this environment; writing unchecked `Qed`s would
reintroduce the "dashboards that lie" problem this pass fixes). Draft
pending human review.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
https://claude.ai/code/session_015qwVESTcbfanY2iJPQNoSz
---
_Generated by [Claude
Code](https://claude.ai/code/session_015qwVESTcbfanY2iJPQNoSz)_
Co-authored-by: Claude <noreply@anthropic.com>1 parent c825401 commit 67ae5a6
1 file changed
Lines changed: 140 additions & 710 deletions
0 commit comments