Goal
Track the product work required after the corresponding replacement PRs listed in the frozen reference PR #8 land, using formal-math as the first multi-project consumer.
The governing model is:
- Git-tracked Markdown and the workspace manifest are authoritative.
- Obsidian and the published site are views of that state.
- GitHub PRs are durable collaboration records.
- Autoform claims are short-lived coordination leases.
- CI validates the exact candidate commit and fails closed on drift.
Follow-up issues
Completion scenario
A new contributor can fresh-clone formal-math, run one repository-pinned bootstrap command, select ready work, coordinate from a fork, open a PR, and receive exact semantic and Lean verification. Disjoint work composes; overlapping or stale work fails with an actionable explanation. A verified merge publishes one aggregate wiki without state that exists only on a contributor's machine.
Relationship to #8
#8 is the frozen reference implementation and checklist; its replacement PRs are the landing path. Every issue above assumes the corresponding baseline primitives have landed through that path and does not replace those baseline slices. In particular, the replacement PRs remain responsible for the baseline runtime, provenance, project creation and repair, transactional per-project publication, CAS claims, coverage v2, workspace read/mutation, and ready/orchestration surfaces.
Goal
Track the product work required after the corresponding replacement PRs listed in the frozen reference PR #8 land, using formal-math as the first multi-project consumer.
The governing model is:
Follow-up issues
Completion scenario
A new contributor can fresh-clone formal-math, run one repository-pinned bootstrap command, select ready work, coordinate from a fork, open a PR, and receive exact semantic and Lean verification. Disjoint work composes; overlapping or stale work fails with an actionable explanation. A verified merge publishes one aggregate wiki without state that exists only on a contributor's machine.
Relationship to #8
#8 is the frozen reference implementation and checklist; its replacement PRs are the landing path. Every issue above assumes the corresponding baseline primitives have landed through that path and does not replace those baseline slices. In particular, the replacement PRs remain responsible for the baseline runtime, provenance, project creation and repair, transactional per-project publication, CAS claims, coverage v2, workspace read/mutation, and ready/orchestration surfaces.