feat(Relativity): equality case of the reverse triangle inequality, twin paradox age gap zero - #1643

Merged

jstoobysmith merged 7 commits into

leanprover-community:masterfrom

KevorkianPhilippe:twin-paradox-12

Sep 12, 2026

Commits on Sep 10, 2026

feat(Relativity): reverse Cauchy-Schwarz and triangle inequalities, twin paradox age gap nonnegative

Philippe Kevorkian
and
claude
committed
68abc2e
feat(Relativity): equality case of the reverse triangle inequality, twin paradox age gap zero

Philippe Kevorkian
and
claude
committed
32b99e7

Commits on Sep 11, 2026

style(Relativity): use causallyFollows 0 u, file named after the structure, lemmas next to their definitions

Philippe Kevorkian
and
claude
committed
0da6b2a
style(Relativity): name the lemmas after their causallyFollows hypothesis

Philippe Kevorkian
and
claude
committed
ce1add9
Merge master into twin-paradox-12 (after the merge of the PR this branch is stacked on)
Philippe Kevorkian
committed
80909ff
refactor(Relativity): extract ageGap_eq, the age gap in terms of the two legs of Twin B

Philippe Kevorkian
and
claude
committed
3244cbd
style(Relativity): indent the statement of ageGap_eq

Philippe Kevorkian
and
claude
committed
2b85826