Repository navigation

Harmonized Axiom 3 for Minkowski and Lorentz spacetimes - #44

Merged

KellyJDavis merged 6 commits into

mainfrom

numina/aqft-in-lean

Oct 8, 2026

Merged

Harmonized Axiom 3 for Minkowski and Lorentz spacetimes#44
KellyJDavis merged 6 commits into
mainfrom
numina/aqft-in-lean

Commits on Oct 8, 2026
- Blueprint: state Minkowski Axiom 3 in a common containing diamond
  
  KellyJDavis
  and
  claude
  committed
  7af7383
- Chapter 5: tighten two remarks on the common containing diamond
  
  KellyJDavis
  and
  claude
  committed
  0c90000
- Restate Minkowski Axiom 3 in a common containing diamond (statements)
  
  KellyJDavis
  and
  claude
  committed
  3113668
- Prove the common-diamond form of Axiom 3 implies the quasilocal form and conversely
  
  KellyJDavis
  and
  claude
  committed
  b37cbe1
- Refresh the home page for Axiom 3 in a common containing diamond; add the audit memo
  
  KellyJDavis
  and
  claude
  committed
  f72b8fa
- Remove web.paux and ignore it in future
  KellyJDavis
  committed
  c0e1c24