Complete Evolution Representations for Spatial Rigid-Body Contact Dynamics

We give a complete-history representation for three-dimensional rigid-body systems with finitely many contacts. Bodies are described by implicit base surfaces and prescribed normal material layers. Contact locations move over both bodies, and ordinary motion obeys the Newton–Euler equations with general inertia. For each finite contact list, we enumerate sustained-contact and zero-reaction choices, retain all solutions of the coupled equations, and determine admissible intervals by equating all material positions. Impacts follow a sequential restitution law: every round rechecks all contacts, and all finite completed orders and infinite rebound records are retained. Under local positive-duration and actual state-matching axioms, compatible candidate histories are proved to represent exactly the histories admitted by the axioms; their maximal records give all complete histories. The spatial material criterion, general-inertia impact update, local branch coverage, event matching, and complete representation have been verified in Lean. The contribution is a formally checked connection of these components within one spatial contact model, providing a common specification for model-specific solution procedures and candidate selection. This record contains the English manuscript, its LaTeX sources, and the spatial Lean 4 proof sources and verification records, together with the preserved planar development. Reproduction requires Lean 4.19.0 and mathlib v4.19.0; see the proof archive instructions. AI assistance supported Lean verification and accelerated the analysis of mathematical rigor.