Repository navigation
[Principia M4] Verify the first source → modern theorem vertical slices #22
Description
Parent: #17
Blocked by: #20, #21
Objective
Complete end-to-end, verifier-gated slices that start from reviewed source objects and end in replayable Lean theorems with explicit assumptions.
Required slices
1. Inertial-motion slice
Source law/object → faithful restatement → modern trajectory formulation → Lean theorem for uniform rectilinear motion or zero acceleration under explicit assumptions.
2. Momentum slice
Source quantity-of-motion/law object → modern constant-mass specialization → derivative-of-momentum theorem with all regularity assumptions stated.
3. Central-force/area slice
Source proposition chain → modern radial-force model → kernel-verified 2D angular-momentum conservation or constant-areal-velocity theorem.
Prefer determinant/oriented-area machinery unless the reviewed Mathlib inventory supports a cleaner reusable alternative.
4. Model-boundary slice
Choose one source physical claim and split it into:
- a mathematical conditional theorem;
- a physical/model-assumption packet;
- an empirical-premise packet;
- an approximation/error target, or a precise formalization-wall packet.
Provenance requirements
Each slice must preserve:
- source-object IDs and segment hashes;
- reviewed source-to-restatement and restatement-to-formalization mappings;
- all assumptions introduced during modernization;
- Lean module and declaration identity;
- packet and artifact hashes;
- Proof Search episode/trajectory references where used;
- resolution against the authoritative artifact index;
- failed proof routes and repairs as governed evidence.
Verification gates
- changed modules pass
lake build <module>in CI; - generated Lean root includes every module and regenerates with no diff;
- complete
lake build MathCorpuspasses in scheduled/release replay; - packet manifests regenerate with no diff;
- source mapping checks pass;
- clean-location replay reproduces packet and release hashes.
Scope control
Kepler/conic-orbit classification is not required for this milestone unless the Mathlib inventory shows the prerequisites are already mature enough that it does not displace the four required slices. Otherwise it belongs in the generated backlog.
Acceptance criteria
- All four slices are complete, or replaced by explicitly approved slices of equal evidentiary strength.
- Every theorem is conditional and faithful to its stated model.
- No source wording, physical model, approximation, or empirical premise is mislabeled as kernel verified merely because a downstream implication compiled.
- Every completed theorem is replayable from committed inputs under the pinned verifier.
Activity