Documentation Verification Report

Basic

📁 Source: PhysLean/Relativity/Special/TwinParadox/Basic.lean

Statistics

Metric	Count
Definitions `InstantaneousTwinParadox`, `ageGap`, `ageGap_nonneg`, `endPoint`, `example1`, `properTimeTwinA`, `properTimeTwinB`, `startPoint`, `twinBMid`	9
Theorems `endPoint_causallyFollows_startPoint`, `endPoint_causallyFollows_twinBMid`, `example1_ageGap`, `example1_properTimeTwinA`, `example1_properTimeTwinB`, `twinBMid_causallyFollows_startPoint`	6
Total	15

SpecialRelativity

Definitions

Name	Category	Theorems
`InstantaneousTwinParadox` 📖	CompData	—

SpecialRelativity.InstantaneousTwinParadox

Definitions

Name	Category	Theorems
`ageGap` 📖	CompOp	1 math math: `example1_ageGap`
`ageGap_nonneg` 📖	CompOp	—
`endPoint` 📖	CompOp	2 math math: `endPoint_causallyFollows_startPoint`, `endPoint_causallyFollows_twinBMid`
`example1` 📖	CompOp	3 math math: `example1_properTimeTwinB`, `example1_ageGap`, `example1_properTimeTwinA`
`properTimeTwinA` 📖	CompOp	1 math math: `example1_properTimeTwinA`
`properTimeTwinB` 📖	CompOp	1 math math: `example1_properTimeTwinB`
`startPoint` 📖	CompOp	2 math math: `endPoint_causallyFollows_startPoint`, `twinBMid_causallyFollows_startPoint`
`twinBMid` 📖	CompOp	2 math math: `endPoint_causallyFollows_twinBMid`, `twinBMid_causallyFollows_startPoint`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`endPoint_causallyFollows_startPoint` 📖	mathematical	—	`Lorentz.Vector.causallyFollows` `startPoint` `endPoint`	—	—
`endPoint_causallyFollows_twinBMid` 📖	mathematical	—	`Lorentz.Vector.causallyFollows` `twinBMid` `endPoint`	—	—
`example1_ageGap` 📖	mathematical	—	`ageGap` `example1`	—	`example1_properTimeTwinA` `example1_properTimeTwinB`
`example1_properTimeTwinA` 📖	mathematical	—	`properTimeTwinA` `example1`	—	`Lorentz.Vector.minkowskiProduct_toCoord`
`example1_properTimeTwinB` 📖	mathematical	—	`properTimeTwinB` `example1`	—	`Lorentz.Vector.minkowskiProduct_toCoord`
`twinBMid_causallyFollows_startPoint` 📖	mathematical	—	`Lorentz.Vector.causallyFollows` `startPoint` `twinBMid`	—	—

---

← Back to Index