Repository navigation
[Principia M3] Audit pinned Mathlib and build the reusable mechanics prerequisite spine #21
Description
Parent: #17
Blocked by: #18, #19
Coordinates with: #20
Objective
Build only the missing reusable mathematical infrastructure needed for the pilot, after auditing the exact pinned Lean/Mathlib environment.
Mathlib-first inventory
Create docs/campaigns/principia/mathlib_inventory.md recording:
- searched concepts and exact declaration/module names;
- direct
#checkor build evidence; - reusable declarations already available;
- thin adapters actually needed;
- missing abstractions;
- rejected duplicate designs;
- generalizations that belong upstream in Mathlib rather than MathCorpus;
- import-cost and performance notes.
Do not claim that a declaration is absent from fuzzy search alone.
Intended mechanics spine
Kinematics
- time parameter and trajectories;
- regularity assumptions;
- velocity and acceleration;
- uniform rectilinear motion.
Dynamics
- mass and constant-mass assumptions;
- momentum;
- force-law interfaces;
- conditional formulations of laws.
Geometry
- affine and Euclidean structure;
- oriented area and determinant formulations;
- only the conic geometry required by approved pilot slices.
Central force
- radial/central-force predicates;
- angular momentum;
- areal velocity.
Model boundaries
- point-mass versus extended-body assumptions;
- explicit approximation hooks;
- empirical-bridge interfaces carrying no proof authority.
Design constraints
- Prefer finite-dimensional real inner-product spaces when practical.
- Prefer a 2D determinant/oriented-area formulation for the area-law pilot if it is smaller and more reusable than an early 3D cross-product API.
- Do not create a new packet
definitionkind only for this campaign; use the existing formal concept behavior unless Expand the packet curriculum taxonomy across mathematics and add a generic first-principles-to-frontier authoring prompt #11 changes the general model. - Prefer importing stable sibling packets to duplicating local lemmas, following the M0 ADR.
- Every physics-facing theorem must be conditional on explicit regularity and model assumptions.
- Lean verifies the implication; it does not verify that a real planet or measured system satisfies the hypotheses.
Deliverables
- reviewed Mathlib inventory;
- dependency graph for mechanics prerequisites;
- minimal new Lean modules and matching packets;
- import/reuse audit showing no unjustified duplicate foundations;
- tests and changed-module kernel builds;
- formalization-wall packets for missing infrastructure that is not completed.
Acceptance criteria
- The inventory is reviewed before foundational wrappers merge.
- Every new abstraction has a concrete pilot consumer.
- No shadow copy of an existing Mathlib abstraction is added without a written reason.
- The generated Lean root imports all new modules.
- The pinned kernel accepts every completed theorem in CI and clean replay.
Activity