Complete Evolution Representations for Planar Rigid-Body Contact Dynamics

We give a complete representation of the evolution of planar rigid-body systems with finitely many contacts. The model specifies implicit generating boundaries, normal-layer materials, an initial state, ordinary external forces, and a sequential restitution rule. Material positions, moving contact points, reaction-force distributions, impact orders, and terminal outcomes are recorded together. Ordinary-motion candidates retain all solutions of the joint Newton equations and satisfy material coincidence tests throughout their intervals. Impacts update the common velocity state one round at a time, retaining every admissible subsequent order. Under explicit local positive-duration and state-matching axioms, we prove that coherent candidate records represent exactly all histories admitted by the axiom system; maximal records give complete histories. The connections between material tests, branch coverage, event matching, and complete representation have been checked in Lean. A circular track, a rod sliding in a corner, and three-body rebounds illustrate the calculation steps. A smooth alternating-contact example explains the positive-duration axiom. The resulting formalization supplies a reusable correctness specification for specialized contact solvers. This record contains the English manuscript, its LaTeX sources, and the planar Lean 4 proof sources and verification records, including the worked examples. 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.