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

[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.

Turns the informal lemma ageGap_nonneg (tag 7ROVE) of
Physlib/Relativity/Special/TwinParadox/Basic.lean into a proved lemma, through the reverse
triangle inequality of Minkowski space, which was not in Physlib.

New file Physlib/Relativity/Tensors/RealTensor/Vector/Causality/CausallyFollows.lean
(namespace Lorentz.Vector), about vectors in the causal future of the origin, causallyFollows 0 u:

• causallyFollows_zero_iff: causallyFollows 0 u ↔ 0 ≤ ⟪u, u⟫ₘ ∧ 0 ≤ u.timeComponent;
  causallyFollows_zero_sub: causallyFollows p q → causallyFollows 0 (q - p).
• norm_spatialPart_le_timeComponent_of_causallyFollows: ‖u_spatial‖ ≤ u⁰.
• sqrt_mul_sqrt_le_minkowskiProduct_of_causallyFollows: the reverse Cauchy-Schwarz inequality
  √⟪u, u⟫ₘ √⟪v, v⟫ₘ ≤ ⟪u, v⟫ₘ for u, v in the causal future of the origin (Euclidean
  Cauchy-Schwarz on the spatial parts plus the elementary inequality
  √(a² - c²) √(b² - d²) ≤ a b - c d for 0 ≤ c ≤ a, 0 ≤ d ≤ b, inlined in the proof).
• sqrt_add_sqrt_le_sqrt_add_of_causallyFollows: the reverse triangle inequality
  √⟪u, u⟫ₘ + √⟪v, v⟫ₘ ≤ √⟪u + v, u + v⟫ₘ; causallyFollows_zero_add_of_causallyFollows.

Added to MinkowskiProduct.lean, next to minkowskiProduct_self_eq_timeComponent_spatialPart:
minkowskiProduct_self_eq_sq_sub (⟪u, u⟫ₘ = (u⁰)² - ‖u_spatial‖²) and minkowskiProduct_add_self.

TwinParadox/Basic.lean: informal_lemma ageGap_nonneg replaced by
lemma ageGap_nonneg : 0 ≤ T.ageGap. Physlib.lean: the new file registered.

Reviewer map: CausallyFollows.lean sections B (reverse Cauchy-Schwarz, with the elementary
inequality inlined) and C; then the four-line proof of ageGap_nonneg.

Update (Sept 11). Review remarks applied (second commit): no separate predicate, everything is
stated with causallyFollows 0 u; the file is named after that structure; the Minkowski product
lemmas moved next to the definition of the product; the elementary inequality is inlined. The same
rules were applied to the other open PRs of mine.

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

🤖 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]

Some comments here are specific to this pull request but probably extend throughout all of the pull requests that you've made. Could you make sure that these are addressed in all of them, because it would make the review process a lot quicker or easier? If you have any ideas of how you can make the review process easier for us, that would also be great.

[jstoobysmith]

If possible, we shouldn't include lemmas like this. It's best just to include them in the proofs of our results because they mess up the code.

[jstoobysmith]

This should go near the definition of Minkowski products.

[jstoobysmith]

Likewise with some of the other definitions in this file.

[jstoobysmith]

I would rename this file "IsFutureCausal" because that is the data structure that the results in this file are about, rather than naming it after the lemma or the property.

[jstoobysmith]

Or if it's just the same as "causally follows" with one of the vectors zero, we should just use that instead.

[jstoobysmith]

Should have also said: many thanks for these. They look, in general, very good. Just one or two things probably need changing with each of them.

[KevorkianPhilippe]

Thank you for the review. The four points are now applied across all my open PRs (one extra commit per branch, no force-push): no isolated general-purpose lemma, lemmas next to the definition of their object, files named after the structure, and causallyFollows 0 u instead of a new predicate. Each PR body carries an "Update (Sept 11)" note describing the change. To make reviewing easier I will keep one file or one section per PR, a short reviewer map at the top of each body, and an explicit note whenever a PR touches a file outside its topic.

-awaiting-author

[jstoobysmith]

Looks and sounds good to me. I've added one more comment here, but otherwise this pull request looks good.

[jstoobysmith]

This lemma and the ones that follow it should end with _of_causallyFollows

[KevorkianPhilippe]

Renamed as requested (_of_causallyFollows), in 5d60cb3 here and ce1add9 on #1643.

-awaiting-author

[jstoobysmith]

Approved. This now looks good to me. I will merge it shortly. Could you update the pull requests that depend on this after this merger has gone through. I think you're probably aware of this already, but PhyslibAlpha has a much quicker process to get stuff in, where we don't have to go through quite as detailed a review process. If you want to skip that phase and put stuff straight into PhyslibAlpha, that's fine. Obviously, we appreciate you taking the time to go through these reviews.

[KevorkianPhilippe]

Thank you. The dependent pull requests are updated: master merged into #1643 and into the cosmology stack #1633 to #1641 (no force-push). Since #1632 was merged before its review fixes were pushed, #1633 now carries those fixes for the de Sitter part; this is noted in its body. I will keep the series that fill Physlib TODO items under the full review, and use PhyslibAlpha for material outside the TODO list.