This checklist is the only in-repo path to mark
registry/capabilities/algebra.rational_equality.json "status": "stable".
Do not flip stable from documentation alone. Each box requires an
artifact or CI-green evidence. Capability JSON remains "experimental" until
every box below is checked with real human artifacts and a separate governance
PR lands.
BLOCKED (Wave 0 / ME-RV-003): Do not flip
status: stablewhile the real-vision acceptance matrix (docs/audits/2026-07-26-real-vision/15_ACCEPTANCE_MATRIX.md) remains open, or while human gates indocs/security/KNOWN_TRUST_GAPS.mdremain open (0 external confirmations today). Engineering packaging is not human confirmation. CI truth for audited headc7040e6is recorded underdocs/validation/ci/—mainis not branch-protected. Ownership reality:.github/CODEOWNERSis still a single-owner stub — seeGOVERNANCE.md.
Local gate: just check (see justfile). Public workflows under
.github/workflows/ (index: .github/workflows/README.md).
Do not re-tick boxes from memory. Prefer immutable workflow URLs on the
candidate commit plus forensic-green evidence under tests/forensic/.
- Conformance suite
evidence/conformance/rfc0001passing in immutable CI on the candidate commit (not only localjust conformance) - Checker soundness with coverage⇒Defined bridge (ℚ)
- Offline kernel replay with Lean-recomputed request digests and
theorem-producing Certification Record (Wave 0
mathevidence-verify-bundleis operationalchecker_acceptedonly — does not close this box) - Adversarial + forensic suites green (
tests/forensic/) - Compiled axiom + import-graph audits preferred over regex-only
- Agent
bundleId-only public surface + registry-driven dispatch - Live request-digest binding; checker theorem remains closing authority
- Typed digests / receipts present
- Branch protection with required checks on the release branch (see CI truth)
- Signed promotion record under
registry/promotions/matchingschemas/promotion-record.schema.json(enforced byscripts/validate_registry.py— docs checkboxes alone are insufficient) - Domain review: independent mathematical review using
docs/validation/expert-review-rubric.md(completed packet underdocs/validation/review-packets/, real reviewer identity). Start fromreview-packets/SAMPLE-rational-equality-unsigned.md(copy without-unsigned) +review-packets/TEMPLATE.md. - Trust-model review: second maintainer from a different area confirms
replay, digest binding, and claim-strength guarantees are not weakened
(
GOVERNANCE.md). Fillreview-packets/TRUST-MODEL-TEMPLATE.md. - Milestone 0 external confirmations: ≥3 non-maintainer entries in
docs/validation/user-confirmation.md. Process:docs/validation/outreach-checklist.md. Status: 0/3. - Project Spec §21 item 10: at least one external Lean contributor or
project confirms a real workflow win. Log:
docs/validation/workflow-win-log.md. Status: 0 entries. - Capability JSON update PR: status →
stable,knownLimitationsupdated, reviewers from Core/trust + domain recorded in the PR (two-area approvals perGOVERNANCE.mdonce teams exist).
- Funding or Foundry frontier acceleration claims
- Live Mathematica/Sage availability on public CI runners
- Fake maintainer sign-off or fabricated user confirmations
- Complete every box above with links to CI runs / review packets / log entries.
- Open a PR that only changes registry status (+ limitation text) after gates.
- Require two approvals from different maintainer areas before merge (when multi-area CODEOWNERS is real; until then, do not pretend dual-area review happened).
just check
pytest tests/forensic -q
Minimum CI workflows that must be green on the PR:
| Workflow | Engineering boxes covered |
|---|---|
lean.yml |
soundness build path, import-boundary, sorry-audit |
adapter-conformance.yml |
RFC 0001 conformance, registry validate, Agent tests |
offline-replay.yml |
SymPy/Mathematica offline replay + Tactic.Examples |
adversarial.yml |
adversarial seed catalog |
Do not treat a green just check as permission to set "status": "stable".
Human governance boxes must still be filled with real artifacts.