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

[KevorkianPhilippe]

AI disclosure

AI disclosure. This PR was generated with Claude Fable 5.1 (Claude Code) under my
supervision, following AI-POLICY.md and AGENTS.md. I have read every definition and lemma
statement and vouch that they state what the docstrings say. The statements were fixed before
the proofs were written; the elementary inequality at the core was checked symbolically.

Stacked on #1642 (twin-paradox-11): the diff includes its commit; only the last commit is new here.

Resolves the TODO "conditions for which the age gap is zero".

Added to CausallyFollows.lean (section D, the equality cases):

• minkowskiProduct_eq_iff_of_causallyFollows: for u, v in the causal future of the origin, equality
  ⟪u, v⟫ₘ = √⟪u, u⟫ₘ √⟪v, v⟫ₘ holds if and only if ∃ μ ≥ 0, v = μ • u ∨ u = μ • v
  (light-like cases included).
• sqrt_add_eq_iff_of_causallyFollows: equality in the reverse triangle inequality if and only if equality in the
  reverse Cauchy-Schwarz inequality.

Added next to the definitions they are about: minkowskiProduct_smul_self,
sqrt_minkowskiProduct_smul_self in MinkowskiProduct.lean; eq_zero_of_timeComponent_of_spatialPart,
apply_inr_eq_zero_of_norm_spatialPart in Vector/Basic.lean.

Added to TwinParadox/Basic.lean:

• ageGap_eq_zero_iff: T.ageGap = 0 ↔ ∃ μ ∈ [0, 1], T.twinBMid = T.startPoint + μ • (T.endPoint - T.startPoint), i.e. the age gap vanishes exactly when Twin B does not turn.
• example1_ageGap_ne_zero.

Reviewer map: minkowskiProduct_eq_iff_of_causallyFollows (the case analysis, the longest proof), then
sqrt_add_eq_iff_of_causallyFollows, then ageGap_eq_zero_iff.

Update (Sept 11). Review remarks of #1642 applied (third commit): causallyFollows 0 u instead of a new predicate, lemmas placed next to the definitions of their objects, file renamed CausallyFollows.lean.

Update (Sept 11, later). Second review remark applied: the lemmas whose hypotheses are causallyFollows 0 u now end with _of_causallyFollows.

Update (Sept 11, evening). Review remark applied: the expression of the age gap in terms of the two legs of Twin B is now its own lemma, ageGap_eq, used by ageGap_eq_zero_iff and by the merged ageGap_nonneg.

🤖 Generated with Claude Code

[github-actions]

Thank you for this pull-request (PR). If this is your first PR, welcome to the community!

Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.

1. Some automated checks will be run on your PR. You can see the results of these checks at the buttom of your PR page. If any of these checks fail, you will need to fix the issues before your PR can be merged. You can learn more about these here, including how to run them locally, which is sometimes quicker than relying on the GitHub Actions. If you have never had a PR merged before, you may have to wait for a reviewer to manually start these checks (this is for security).

2. A reviewer will look at your PR and may ask you to make changes. This may happen a couple of days after you submit your PR, so you may need to be patient. But it should not be longer than that - if it is please bring it to the attention of the community on the Zulip. The level of review will depend on where your PR is submitted. If it is submitted to ./Physlib or ./QuantumInfo, the review will be more thorough than if it is submitted to ./PhyslibAlpha. You can find out more about what the review process is looking for in our review guidelines. If a reviewer adds an awaiting-author label to your PR, address the review comments, then please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

3. The reviewer will either approve your PR, or request more changes (in which case we return to step 2). Once your PR is approved, it will be merged by a maintainer, this should happen shortly after approval, though you may get more comments at this stage.

Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages.

If you have any problems or questions, please reach out to the community on the Zulip.

[jstoobysmith]

One more comment from me here.

[jstoobysmith]

I think it might be useful to extract this as its own separate lemma, as it might be useful for other circumstances as well.

[KevorkianPhilippe]

Extracted as ageGap_eq in 3244cbd (statement indentation fixed in 2b85826); it is now also used by ageGap_nonneg.

-awaiting-author

[jstoobysmith]

I've approved this. This looks good, and many thanks for splitting up the two different changes into different commits and linking to them here. I wonder if we should actually add something like that to our agents.md because it makes the review process easier, especially if one can click through the commits to see

[KevorkianPhilippe]

Thanks! Happy to make that a habit, and I agree it would help reviewers: one commit per review comment, each commit named after what it changes, and the PR comment that answers a review thread pointing to the commit hash. It costs the author nothing if the fix is done right after reading the comment. If you would like, I can open a small PR adding three lines to AGENTS.md (under "Commits"), roughly:

• When addressing review comments, make one commit per comment (or per group of closely related comments), titled after the change, and do not squash or force-push during review.
• In the reply to each review thread, link the commit that addresses it; if a comment turns out to need no change, say so and why.
• Keep the follow-up commits separate from any merge of master, so that each one shows only the requested change.

Say the word and I will open it.