feat(SpaceTime): the spacetime algebra and its Taylor series by nateabr · Pull Request #1702 · leanprover-community/physlib

nateabr · 2026-09-30T17:33:31Z

Adds the spacetime algebra, formal power series in the four spacetime directions. Compared with
#1415, the repeated foldl is now the definition iteratedPDeriv, and Taylor's formula and
taylorEquiv are new. The remaining lemmas are carried over from #1415, renamed to use
iteratedPDeriv. I would appreciate a careful review of the documentation as well. I used AI to
help with this PR.

github-actions · 2026-09-30T17:34:05Z

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.

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).
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.
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 · 2026-10-01T04:54:25Z

+    ring
+
+/-- The factorial `s!` is nonzero. -/
+lemma prod_factorial_ne_zero (s : Multiset (Fin 1 ⊕ Fin 3)) :


This seems like a rewrite of a Mathlib proof, and we should likely just include it directly in lemmas rather then making it seperate here

jstoobysmith · 2026-10-01T04:56:50Z

+-/
+
+/-- The series whose base-point derivative values are `F`. -/
+noncomputable def taylorSeries (F : Multiset (Fin 1 ⊕ Fin 3) → ℂ) : SpaceTimeAlgebra :=


If possible, I think we should define taylorSeries as a map from a smooth function SpaceTime → ℂ and give this another name.

jstoobysmith · 2026-10-01T04:57:21Z

awaiting-author

nateabr · 2026-10-01T16:47:44Z

I've renamed the derivative-values construction to ofDerivValues, so taylorSeries is now the actual Taylor series of a smooth function in the new file, SpaceTimeAlgebra/TaylorSeries.lean.

-awaiting-author

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

jstoobysmith · 2026-10-02T04:35:05Z

+open scoped ContDiff
+
+/-- The `ℂ`-subalgebra of smooth complex-valued functions on `SpaceTime d`. -/
+def smoothFunctions (d : ℕ := 3) : Subalgebra ℂ (SpaceTime d → ℂ) where


I wouldn't define smooth functions here.

jstoobysmith · 2026-10-02T04:36:18Z

+-/
+
+/-- The Taylor series at `x₀` of a smooth complex-valued function on spacetime. -/
+noncomputable def taylorSeries (x₀ : SpaceTime) : smoothFunctions →ₗ[ℂ] SpaceTimeAlgebra where


I think to prevent the need for smooth functions (unless they are already bundled as a type in Mathlib), we should define this function for all functions. And then show that on smooth functions it has the desired properties.

…data

nateabr · 2026-10-02T09:12:11Z

I'm wondering what is the best way to move forward with this @jstoobysmith

There is a Mathlib type C^∞⟮…⟯, but for ℂ-valued functions on spacetime it's only an ℝ-module and not a ring
The two options I see are:

go with the all-functions version (ie. the method that you have recommended), and add a bundled version out of C^∞⟮…⟯ later if we need one (e.g. a ring hom for the matrix stuff), or
use C^∞⟮…⟯ as the domain directly by using the current version I have with a ring instance?

I'm leaning towards options 1 but would like your opinion on this

-awaiting-author

jstoobysmith · 2026-10-02T09:14:30Z

I also think 1 makes more sense here. It ends up being easier in the long run I think.

awaiting-author

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

nateabr · 2026-10-02T09:43:37Z

Have made this change

-awaiting-author

jstoobysmith · 2026-10-02T10:00:27Z

If we can get away without making these definitions or making them general properties of derivatives on SpaceTime I think this would be better.

have addressed, this was honestly quite dim from my side. I got far too excited to add something to the new mathlib folder

jstoobysmith · 2026-10-02T10:00:48Z

awaiting-author

nateabr · 2026-10-02T10:48:05Z

-awaiting-author

jstoobysmith

Approved. Will merge shortly.

feat(SpaceTime): the spacetime algebra and its Taylor series

b2ce877

github-actions Bot added the medium label Sep 30, 2026

github-actions Bot added the t-space-and-time label Sep 30, 2026

nateabr requested a review from jstoobysmith September 30, 2026 17:36

docs: improve documentation

36ae8ad

This was referenced Sep 30, 2026

chore: remove unused simp arguments in SuccSuccAbove #1703

Merged

chore: import cleanup (lake shake, redundant_imports, remove import Mathlib) #1701

Merged

jstoobysmith reviewed Oct 1, 2026

View reviewed changes

github-actions Bot added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 1, 2026

feat(SpaceTime): Taylor series of smooth functions and review changes

b4c5024

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 1, 2026

docs: clarify base-point values of iterated derivatives

4238b84

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

jstoobysmith reviewed Oct 2, 2026

View reviewed changes

jstoobysmith added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 2, 2026

Merge remote-tracking branch 'upstream/master' into spacetime-taylor-…

c833bdd

…data

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 2, 2026

github-actions Bot added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 2, 2026

feat(SpaceTime): define Taylor series for all functions

f79942f

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

github-actions Bot added large and removed medium labels Oct 2, 2026

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 2, 2026

jstoobysmith reviewed Oct 2, 2026

View reviewed changes

github-actions Bot added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 2, 2026

refactor(SpaceTime): order independence of derivatives on spacetime

ed23733

github-actions Bot added medium and removed large labels Oct 2, 2026

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 2, 2026

jstoobysmith approved these changes Oct 2, 2026

View reviewed changes

jstoobysmith added the ready-to-merge This PR is approved and will be merged shortly label Oct 2, 2026

jstoobysmith added this pull request to the merge queue Oct 2, 2026

Merged via the queue into leanprover-community:master with commit 70e4037 Oct 2, 2026
11 checks passed

Conversation

nateabr commented Sep 30, 2026

Uh oh!

github-actions Bot commented Sep 30, 2026

Uh oh!

jstoobysmith Oct 1, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith Oct 1, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith commented Oct 1, 2026

Uh oh!

nateabr commented Oct 1, 2026

Uh oh!

jstoobysmith Oct 2, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith Oct 2, 2026

Choose a reason for hiding this comment

Uh oh!

nateabr commented Oct 2, 2026

Uh oh!

jstoobysmith commented Oct 2, 2026

Uh oh!

nateabr commented Oct 2, 2026

Uh oh!

jstoobysmith Oct 2, 2026

Choose a reason for hiding this comment

Uh oh!

nateabr Oct 2, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith commented Oct 2, 2026

Uh oh!

nateabr commented Oct 2, 2026

Uh oh!

jstoobysmith left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants