refactor(verification): complete formal verifier retirement

[stevenobiajulu]

Summary

• complete the residual cleanup after the substantive Lean verifier removal already landed on main
• archive the deployed remove-lean-verification OpenSpec change and record the retirement inventory and TypeScript coverage map
• remove stale formal-verifier contributor guidance and the obsolete lean.* advanced-revision classification bypass
• update the verification roadmap to describe the maintained runtime and TypeScript assurance boundary

Scope

This PR does not restore, replace, or invoke Lean. It closes the remaining repository-policy, documentation, and OpenSpec loose ends after the checker, workflow, proof project, runtime API, and production integration were removed. Historical archived records remain intact.

Verification

• repository build: passed
• workspace lint: passed
• strict OpenSpec validation: passed
• spec coverage and conformance checks: passed
• @usejunior/docx-compare: 911 passed, 27 skipped
• @usejunior/docx-markdoc: 59 passed
• @usejunior/docx-mcp: 1,007 passed
• release verifier: 56 passed
• cross-implementation suite: 8 passed, 1 expected skip (rerun with required LibreOffice/IPC permissions)
• render verifier: 56 passed (rerun with required permissions)

Relationship to other work

This is independent of structural-validation PR #970. Neither PR should be merged as part of this operation.

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated
site	Ready	Preview	Sep 3, 2026 12:25pm UTC

[usejunior-llm-gate]

LLM gate (advisory)

All evaluated rules passed - 3 pass, 0 warn, 0 error, 13 skipped, 16 total

Findings

None.

All 16 rules (3 evaluated, 13 skipped)

Rule	Verdict	Detail
read_file response metadata parity	SKIPPED	paths not touched by this PR
Live DOM namespace-safe OOXML writes	SKIPPED	paths not touched by this PR
Complex-field revisions preserve complete accept/reject state machines	PASS	The PR does not touch field atomization, validateFieldStructure, w:fldChar, w:instrText, w:delInstrText, or collapsed-field comparison logic, as it only removes the Lean verification subsystem and updates associated documentation.
Field validation per story, not global	SKIPPED	paths not touched by this PR
Revision IDs seeded from all revision-bearing side parts	SKIPPED	paths not touched by this PR
Accept/reject sweep side parts and caches	PASS	The PR only removes the Lean formal-verification subsystem (modifying scripts, specifications, and documentation) and does not touch accept/reject logic or side-part revision markup.
DocumentViewNode.heading stays canonical	SKIPPED	paths not touched by this PR
AI-author parity across entry points	SKIPPED	paths not touched by this PR
Property-change wrapper discipline	SKIPPED	paths not touched by this PR
SUPPORT.md Table A drift vs. implementation	SKIPPED	paths not touched by this PR
Table A / Table B boundary on side-part revisions	SKIPPED	paths not touched by this PR
Canonical-emission surface completeness	SKIPPED	paths not touched by this PR
Unit-test quality (avoid tautological / change-detector tests)	SKIPPED	paths not touched by this PR
Re-derived facts vs canonical sources	PASS	The PR does not meet the precondition as it only modifies documentation, specifications, and script configurations to retire the Lean verification subsystem, and does not add any production logic or re-derive any facts.
.openspec tag ↔ test-assertion drift	SKIPPED	paths not touched by this PR
Library stays general (no downstream-domain leakage)	SKIPPED	paths not touched by this PR

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

[stevenobiajulu]

✅ Post-merge smoke passed

Merged: 2aafaed15428e7c3e9433b42909141d9a698b28d
Built from: main @ 2aafaed15428e7c3e9433b42909141d9a698b28d
Smoke: npm ci && npm run build && npm run lint:workspaces && npm run test:run && npm run check:spec-coverage && npm run check:conformance-citations && npm run check:conformance-doc

Steps

• ✅ clean dependency install
• ✅ build
• ✅ lint/typecheck (0 errors; 6 pre-existing unused-disable warnings)
• ✅ full workspace test suite
• ✅ strict OpenSpec coverage checks
• ✅ ECMA-376 citation and conformance-document checks
• ✅ advisory LLM gate: 3 pass, 0 warn, 0 error
• ✅ Vercel commit status: deployment completed

Visual evidence: n/a — verifier-retirement change is structurally invisible in rendered documents.

Cleanup

• ⚠️ branch/worktree deletion was not performed because destructive cleanup authorization was not granted.
• ✅ unrelated PR feat(docx-markdoc): validate structural insertions #970 was left unchanged.