feat(ClassicalMechanics): add the total kinetic energy and prove the König decomposition - #1401

Merged

jstoobysmith merged 4 commits into

leanprover-community:masterfrom

giuseppesorge:rigidbody-koenig

Jul 10, 2026

Commits on Jul 8, 2026

feat(ClassicalMechanics): add the total kinetic energy and prove the König decomposition

giuseppesorge
and
claude
committed
bc9b2a2

Commits on Jul 9, 2026

refactor(ClassicalMechanics): address König review — Space d velocity, moved lemmas, extracted split

giuseppesorge
and
Claude Opus 4.8
committed
f5befc8

Commits on Jul 10, 2026