therefore
Sign up
Open navigation

Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 3 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

3 results

Clear filters
Project-declaredLean 4.32.0

Mass Distribution center Of Mass

RigidBodyMotion.massDistribution_centerOfMass

Plain-language statement

The centre of mass of the moving mass distribution tracks the prescribed trajectory: for a body of nonzero mass, the centre of mass of massDistribution M t is exactly comTrajectory t. This is the decisive check that comTrajectory and orientation are wired correctly in RigidBodyMotion.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Velocity eq deriv orientation

RigidBodyMotion.velocity_eq_deriv_orientation

Plain-language statement

The velocity of a body point decomposes as v = Ṙ (y − c) + V: the rate of change of the orientation acting on the body-frame position, plus the centre-of-mass velocity.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Velocity of orientation const

RigidBodyMotion.velocity_of_orientation_const

Plain-language statement

A rigid body in pure translation (constant orientation) has every point moving with the centre-of-mass velocity: v = V.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record