Repository navigation
[Epic] Principia source-critical corpus → verifier-gated formal mechanics #17
Description
Plan of record
Turn the Principia campaign into a source-critical MathCorpus implementation and a reusable verifier-gated classical-mechanics library.
Parent: #11
Prerequisite: merge #16 or land equivalent active Lean-kernel and generated-artifact gates on main
Coordinates with: #15 for Proof Search → MCIP → packet evidence patterns
Required trust boundary
The campaign must distinguish:
- what the pinned edition literally says;
- an edition-faithful reviewed restatement;
- a modern specialization or generalization;
- a conditional theorem verified by Lean;
- a physical, empirical, or approximation claim that Lean does not make true merely by checking a derivation.
Historical source objects never carry proof authority. Source review is fidelity review, not mathematical truth or empirical confirmation. Modern restatements must disclose strengthened, weakened, specialized, generalized, or newly introduced assumptions.
Code due-diligence findings
Audit baseline: main at a0d08c9 on 2026-07-24, plus open PRs #15 and #16.
mainexplicitly disables its Lean job withif: ${{ false }}. Python checks can therefore pass while changed Lean artifacts are not kernel checked.schema/packet.schema.jsonis closed and theorem-oriented. It has no canonical source-object kind, source-only status, structured locator, textual layer, or source-to-modern relation grammar.- A focused policy probe showed that a generic
conceptwithempirical_onlyand no proof authority passes current policy, but adding a top-level source object is rejected by the schema. Current code can hide a historical item inside a generic concept, but cannot enforce source semantics. tools/author_packet.pyhard-codeskernel_verified, Lean fields, MathCorpus authorship, Apache/CC licensing,public_train, and proof export. Reusing it for historical source records could fabricate authority, authorship, rights, and training eligibility.- MCIP literature and retrieved-passage records are child evidence, not canonical packet data. Reviewed source objects and mappings must be canonical MathCorpus packet data.
validate_packets.pyresolves Proof Search episode/trajectory evidence only when an optional artifact index is supplied. Principia releases must require the authoritative artifact index.- Existing policy does not enforce source roles, locators, mapping endpoint types, rights state, or authority leakage through mappings.
- Generated Lean root and campaign indexes need no-op enforcement in CI.
- PR feat(corpus): NumberTheory/PrimeDistribution wave 1 — Erdős-647 analytic core (#12) #16 surfaced an unresolved import-versus-reproof policy. The mechanics spine needs an explicit cross-packet reuse policy before implementation.
Actionable child issues
- [Principia M0] Freeze the 1846 edition, source normalization, rights, and campaign ADRs #18 — M0: freeze the 1846 edition, normalization, rights, and campaign ADRs
- [Principia M1] Add canonical source-object packets, mappings, safe authoring, and validation #19 — M1: add source-object schema, mappings, safe authoring, validation, and CI
- [Principia M2] Review the Definitions, Laws, and Book I source map #20 — M2: review Definitions, Laws, and Book I source map
- [Principia M3] Audit pinned Mathlib and build the reusable mechanics prerequisite spine #21 — M3: audit pinned Mathlib and build the reusable mechanics spine
- [Principia M4] Verify the first source → modern theorem vertical slices #22 — M4: complete verified source → modern theorem vertical slices
- [Principia M5] Add approximation and empirical-premise governance #23 — M5: govern approximation and empirical-premise boundaries
- [Principia M6] Publish a reproducible campaign release and whole-work backlog #24 — M6: publish a reproducible campaign release and whole-work backlog
Definition of Done
This epic is complete only when:
- active Lean kernel CI and generated-artifact no-op gates are on
main; - source-only packet semantics and source mappings are enforced by schema and policy;
- source authoring is fail-closed and cannot silently claim proof authority, MathCorpus authorship, public-domain status, or training eligibility;
- the source file, edition, translation/editorial layers, scan provenance, page map, and rights state are hash pinned;
- every pilot source object has a structured locator, role, segment hash, textual layer, review state, and rights state;
- every mapping resolves and passes predicate-aware type checks without propagating authority;
- the pinned-Mathlib inventory is reviewed before new mechanics wrappers merge;
- all pilot formal packets pass changed-module CI and a clean full-root/release replay;
- all Proof Search provenance resolves against an authoritative artifact index;
- public and audit exports are separate and rights/redaction checks fail closed;
- four end-to-end slices are complete: inertial motion, momentum, central-force area law, and one explicit model/empirical boundary;
- the campaign release, coverage report, formalization walls, and remaining-work backlog are reproducible from committed inputs.
The linked child issues are the actionable implementation plan. Material changes to the trust model, data model, phase order, or Definition of Done must be recorded here or in a linked ADR.
Activity