Repository navigation
[Principia M6] Publish a reproducible campaign release and whole-work backlog #24
Description
Parent: #17
Blocked by: #18, #19, #20, #21, #22, #23
Objective
Produce a frozen, independently replayable Principia pilot release and generate the remaining whole-work formalization backlog from governed packet data.
Release contents
The release must include:
- pinned source asset hash and edition/literature-record hashes;
- source normalization version and page map;
- reviewed source-object packets for the pilot scope;
- source mapping graph and reverse relation index;
- mechanics prerequisite packets and Lean source;
- pinned Lean/Mathlib environment identifiers;
- proof receipts and authoritative Proof Search artifact-index resolution;
- failed attempts, repairs, and formalization-wall evidence;
- rights and redaction audit;
- public export and separate restricted audit export;
- generated source-map coverage report;
- known fidelity, mathematical, approximation, empirical, and infrastructure gaps;
- generated child backlog for the remainder of the work.
Required replay
From a clean location and committed inputs only:
- validate schemas and policies;
- regenerate source and relation indexes;
- regenerate the Lean root and packet manifests;
- build changed Lean modules;
- run the complete
lake build MathCorpusrelease gate; - validate Proof Search evidence against the authoritative artifact index;
- build public and audit exports;
- run rights/redaction checks;
- reproduce release hashes and coverage reports.
Whole-work backlog generation
Generate dependency-ordered issues or machine-readable work items for source objects outside the pilot. Each item must identify:
- source locator and role;
- prerequisite source objects and modern packets;
- expected Mathlib coverage;
- required new definitions/lemmas;
- fidelity risk;
- physical/model assumptions;
- approximation and empirical boundaries;
- expected verification route;
- blockers and estimated formalization wall class.
Do not count generated prose, empty directories, or packet stubs as completed formalization.
Scale decision
The release report must recommend one of:
- proceed to the next dependency-ordered Principia section;
- harden shared source-critical infrastructure before scaling;
- upstream missing abstractions to Mathlib;
- pause a branch at a documented formalization wall;
- replace an unfaithful or unproductive formalization route.
Acceptance criteria
- Clean replay produces the same governed manifests and release hashes.
- Every public artifact passes rights and redaction checks.
- Every formal proof claim replays through the pinned kernel.
- Every Proof Search provenance claim resolves against the authoritative ledger export.
- Coverage metrics derive from canonical packets and relations, not a hand-maintained spreadsheet.
- The remaining backlog is dependency ordered and does not overclaim fidelity, completion, or proof authority.
- [Epic] Principia source-critical corpus → verifier-gated formal mechanics #17 is not closed until all of its Definition of Done conditions are met.
Activity