docs: refresh stale "22 open" → "12 open" + CHANGELOG closure entry

[hyperpolymath]

Closure sweep after PR #116 took preservation from 22 → 12 open goals and PR #121 landed Phase 1 scaffold. Updates the preservation-count claims across docs to reflect 12, and adds a CHANGELOG entry summarising the full 2026-05-20 → 2026-05-21 reduction campaign.

Files updated

File	What changed
README.adoc	Coq formal-foundations paragraph; reduction chain now lists all 8 PRs through #121; clear pointer to ROADMAP closure plan
ROADMAP.adoc	Formal-proof status table row (12 open goals); v0.1 blocker entry; v1.0 status; 97.6% → 98.7% reduction figure
EXPLAINME.adoc	Coq theorem table; reduction-story bullets extended through #114, #116, #121
CHANGELOG.md	New "Proof state" + "Documentation" sections under [Unreleased] tracking the full PR chain (#92, #102, #104, #106, #114, #115, #116, #117, #121) + the Idris2 totality campaign (#89–#100) + doc/wiki refresh (#113 + wiki)

Companion wiki update

Home.md, Proof-status.md, What-can-go-wrong.md updated in the wiki repo with the same 22 → 12 figures + extended reduction story. Pushed separately to wiki master.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 30 issues detected

Severity	Count
🔴 Critical	7
🟠 High	6
🟡 Medium	17

⚠️Action Required: Critical security issues found!

View findings

[
{
"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": "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": "Admitted leaves proof hole (4 occurrences, CWE-704)",
"type": "admitted",
"file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Coq admit tactic leaves goal unproven (3 occurrences, CWE-704)",
"type": "coq_admit_tactic",
"file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (2 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
"type": "believe_me",
"file": "/home/runner/work/ephapax/ephapax/src/formal/Ephapax/Formal/RegionLinear.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "assert_total bypasses totality checker (1 occurrences, CWE-704)",
"type": "assert_total",
"file": "/home/runner/work/ephapax/ephapax/src/formal/Ephapax/Formal/RegionLinear.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "expect() in hot path (1 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/ephapax/ephapax/src/ephapax-repl/src/lib.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "from_raw constructs types from raw pointers without safety checks (1 occurrences, CWE-676)",
"type": "from_raw",
"file": "/home/runner/work/ephapax/ephapax/src/ephapax-vram-cache/src/lib.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
}
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence