Skip to content

Harmonized Axiom 3 for Minkowski and Lorentz spacetimes - #44

Merged
KellyJDavis merged 6 commits into
mainfrom
numina/aqft-in-lean
Oct 8, 2026
Merged

KellyJDavis merged 6 commits into
mainfrom
numina/aqft-in-lean

Conversation

@KellyJDavis

Copy link
Copy Markdown
Contributor

No description provided.

KellyJDavis and others added 6 commits October 8, 2026 07:58
Restate local commutativity through the isotony maps into any diamond
containing both regions, parallel to the curved Axiom 3, and record the
quasilocal form as an equivalent lemma. Move the canonical embeddings into the
quasilocal-algebra definition, and correct Chapter 5's argument that isotony
cannot place two spacelike algebras in a common algebra.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
LocalCommutativity now asks that completely spacelike local algebras commute in
every Alexandrov diamond containing both, as in the curved axiom. State the
equivalence with the former quasilocal form; proofs follow.

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

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… the audit memo

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@KellyJDavis
KellyJDavis merged commit 32a1472 into main Oct 8, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant