Numina/aqft in lean - #31

Merged

KellyJDavis merged 91 commits into

mainfrom

numina/aqft-in-lean

Aug 24, 2026

Commits on Jul 20, 2026

Agent: Simplify `sUnion_alexandrovBasis_eq_univ` proof by delegating to helper
lean-agent-app[bot]
committed
0eb0f5f
Agent: Add causal and chronological diamond definitions and key properties
lean-agent-app[bot]
committed
968e377
Agent: Prove causal diamond membership and structural property lemmas
lean-agent-app[bot]
committed
83fb063
Agent: Mark `chronologicalDiamond_subset_causalDiamond` and `mem_alexandrovBas…
lean-agent-app[bot]
committed
97087d3
Agent: Add causal convexity definition and relate it to diamonds and causally…
lean-agent-app[bot]
committed
2de4516
Agent: Mark causal-convexity theorems as proved and close blueprint sorries
lean-agent-app[bot]
committed
660c2ae
Agent: Add causal-convex hull and closure-structure lemmas
lean-agent-app[bot]
committed
f6d4d3b
Agent: Prove causal-convex hull and closure-system lemmas; mark blueprint lean…
lean-agent-app[bot]
committed
6fc9b08

Commits on Jul 21, 2026

Agent: Add relative commutant of nested local algebras to blueprint and Lean
lean-agent-app[bot]
committed
0389f8d
Agent: Mark relative commutant declarations as proved in blueprint and Lean
lean-agent-app[bot]
committed
0bc44e3
Agent: Fix `relativeCommutant` carrier equality proof
lean-agent-app[bot]
committed
860ab33
Agent: Add relative commutant definition and basic lemmas to curved net
lean-agent-app[bot]
committed
d01a871
Agent: Mark relative commutant theorems as proved in blueprint and Lean
lean-agent-app[bot]
committed
d946bb6
Agent: Add `IsIrreducibleInclusion` and factor consequence on flat and curved…
lean-agent-app[bot]
committed
6a16355
Agent: Mark isFactor_of_isIrreducibleInclusion proved in flat and curved space…
lean-agent-app[bot]
committed
ed0c278

Commits on Jul 22, 2026

Agent: Add self-inclusion ↔ factor theorems for flat and curved nets
lean-agent-app[bot]
committed
199eec1
Agent: Remove unproved `isIrreducibleInclusion_self_iff_isFactor` theorems and…
lean-agent-app[bot]
committed
6253b85
Agent: Add self-inclusion iff factor theorems (flat and curved spacetime)
lean-agent-app[bot]
committed
8ac1b7e
Agent: Remove unproved self-inclusion iff factor theorems from blueprint and L…
lean-agent-app[bot]
committed
dbffdd8
Agent: Add self-inclusion ↔ factor theorem for both flat and curved nets
lean-agent-app[bot]
committed
27714fe
Agent: Revert blueprint proof status for self-inclusion irreducibility theorems
lean-agent-app[bot]
committed
4642316
Agent: Mark `isIrreducibleInclusion_self_iff_isFactor` proved in blueprint for…
lean-agent-app[bot]
committed
c9f7392
Agent: Remove unproved `isIrreducibleInclusion_self_iff_isFactor` theorems and…
lean-agent-app[bot]
committed
121cf94

Commits on Jul 23, 2026

Agent: Add prover subsystem smoke test
lean-agent-app[bot]
committed
8748cc5
Agent: Remove temporary prover smoke-test file
lean-agent-app[bot]
committed
cf6707c
Agent: Add self-inclusion ↔ factor theorems for flat and curved nets
lean-agent-app[bot]
committed
7fe41be
Agent: Replace sorry proofs for isIrreducibleInclusion_self_iff_isFactor
lean-agent-app[bot]
committed
4f71d79
Agent: Add GNS state-pullback functoriality definition and stubs
lean-agent-app[bot]
committed
adb53c7
Agent: Replace sorry placeholders with complete proofs for state pullback
lean-agent-app[bot]
committed
7bdb915
Agent: Add Zeeman-lite: dilations are causal automorphisms but not isometries
lean-agent-app[bot]
committed
d4e8c3e
Agent: Prove minkowskiBackwardCone_smul, minkowskiForm_smul, and exists_minkow…
lean-agent-app[bot]
committed
0978d39
Agent: Prove `minkowskiForwardCone_smul` and `alexandrovBasis_image_smul`, rem…
lean-agent-app[bot]
committed
9d2203d
Agent: Add blueprint theorem and Lean stubs for isPure_comp_iff
lean-agent-app[bot]
committed
40cefc4
Agent: Prove purity-invariance theorems and fix blueprint annotation
lean-agent-app[bot]
committed
a016eb2
Agent: Add abelian-iff-self-commuting lemma and blueprint entry
lean-agent-app[bot]
committed
1b23d48

Commits on Jul 24, 2026

Agent: Add center of von Neumann algebra and factor-abelian characterizations
lean-agent-app[bot]
committed
fb0831a
Agent: Add curved-spacetime specializations of abelian local von Neumann algeb…
lean-agent-app[bot]
committed
a3a2fb9
Agent: Add theorems linking the center, commutant, and factor condition
lean-agent-app[bot]
committed
b25e804
Agent: Add center-duality specialization for curved local von Neumann algebras
lean-agent-app[bot]
committed
fc9de95

Commits on Jul 27, 2026

Agent: Add GNS covariance theorems under a *-isomorphism
lean-agent-app[bot]
committed
202f475
Agent: Add GNS sector-transport theorems and covariance corollaries for nets
lean-agent-app[bot]
committed
4943747

Commits on Jul 28, 2026

Update 9 files
lean-agent-app[bot]
committed
17129f6
Agent: Simplify proofs in ExtremeState and Irreducibility
lean-agent-app[bot]
committed
0caa6c1

Commits on Jul 29, 2026

Agent: Golf proof terms in Irreducibility and Superselection
lean-agent-app[bot]
committed
d01c1e1
Agent: Introduce `GNSTriple` structure bundling π, Ω, cyclic, and reproducing
lean-agent-app[bot]
committed
d60978e
Agent: Remove unused GNSTriple bundled structure and its import
lean-agent-app[bot]
committed
e52792d

Commits on Jul 31, 2026

Agent: Add blueprint section on pullback metrics and cross-metric isometries
lean-agent-app[bot]
committed
dbb1565

Commits on Aug 3, 2026

Agent: Remove pullback-metrics section from blueprint content
lean-agent-app[bot]
committed
d136fdf
rm unused file
KellyJDavis
committed
ae90ebd
Agent: Restructure blueprint proofs in sections 10-1 through 10-4 into proper…
lean-agent-app[bot]
committed
fb5f5e9
Agent: Refactor blueprint: extract lemmas from definitions and clarify referen…
lean-agent-app[bot]
committed
8c70335
Agent: Fix Isotony axiom to use non-strict inclusion ⊆ in both spacetime setti…
lean-agent-app[bot]
committed
2ec72a3

Commits on Aug 4, 2026

Agent: Restructure Axiom 2/3 in LaTeX: Axiom 2 owns the isotony family, Axiom…
lean-agent-app[bot]
committed
aa653b5
Update 4 files
lean-agent-app[bot]
committed
aa31175

Commits on Aug 5, 2026

Agent: Fix LaTeX rendering of subscript digits in \texttt spans
lean-agent-app[bot]
committed
8df0cde
Update 8 files
lean-agent-app[bot]
committed
ef908ca
Agent: Parametrise QuasilocalAlgebra by the Axiom 2 isotony family
lean-agent-app[bot]
committed
24e7c49

Commits on Aug 6, 2026

Agent: Add three quasilocal-algebra supporting lemmas to blueprint
lean-agent-app[bot]
committed
69fce66
Agent: Collapse blueprint nodes subsumed by Mathlib's DirectLimit instances
lean-agent-app[bot]
committed
0b987d4
Agent: Resolve open API question for smoothness of x ↦ dψ_x in hom-bundle
lean-agent-app[bot]
committed
9acacb6

Commits on Aug 10, 2026

Renamed files in prep for addition of the Spectral Theorems
KellyJDavis
committed
ab6b8e9
Agent: Update blueprint section path in LocalAlgebras docstring
lean-agent-app[bot]
committed
a7e3d22

Commits on Aug 11, 2026

Update 10 files
lean-agent-app[bot]
committed
c855aff
Agent: Add scratch Lean files to .gitignore
lean-agent-app[bot]
committed
887b039

Commits on Aug 12, 2026

Update 13 files
lean-agent-app[bot]
committed
e1eb83e
Agent: Expand blueprint proof notes for bilinearComp smoothness node
lean-agent-app[bot]
committed
8d2c3b1
Agent: Add `\uses` dependencies to isotony and local-commutativity definitions
lean-agent-app[bot]
committed
768e5fd
Agent: Fix over-claim in thrm:causally-complete-lattice by listing actual Lean…
lean-agent-app[bot]
committed
7ea9bc2
Agent: Consolidate blueprint completion-block nodes and record construction-ro…
lean-agent-app[bot]
committed
77908d7

Commits on Aug 13, 2026

Agent: Prove `bicommutant_inter_eq` and mark blueprint lemma as formalized
lean-agent-app[bot]
committed
079be98
Agent: Add QuasilocalColimit file with Diamond index type and DirectedSystem i…
lean-agent-app[bot]
committed
d4ab2ec
Agent: Mark quasilocal colimit norm and common-representatives lemmas as proved
lean-agent-app[bot]
committed
c7b5386
Agent: Document colimit instance synthesis obstacle for quasilocal norm constr…
lean-agent-app[bot]
committed
7403b04

Commits on Aug 17, 2026

Agent: Mark colimit norm, normed algebra, and C*-ring lemmas as proved
lean-agent-app[bot]
committed
d116264
Agent: Add C*-completion file and mark blueprint nodes as proved
lean-agent-app[bot]
committed
d9cf352
Agent: Add `CStarCompletion` abbreviation and link blueprint node
lean-agent-app[bot]
committed
acad753

Commits on Aug 18, 2026

Agent: Move misattributed Lean citations to correct blueprint nodes
lean-agent-app[bot]
committed
4992bf2
Agent: Add frontier/endpoint lemmas and mark blueprint nodes as proved
lean-agent-app[bot]
committed
1f0c306
Agent: Restructure Axiom 4 into separate conceptual nodes
lean-agent-app[bot]
committed
fcb7b4b

Commits on Aug 19, 2026

Agent: Restrict `QuasilocalAlgebra.ι` to Alexandrov-basis sets only
lean-agent-app[bot]
committed
7b6f4b3
Agent: Make HaagKastlerNet and related structures universe-polymorphic
lean-agent-app[bot]
committed
cb215a0
Agent: Update blueprint to reflect completed universe-tying fixes
lean-agent-app[bot]
committed
00fad42

Commits on Aug 20, 2026

Agent: Add quasilocal existence theorem and supporting embedding lemmas
lean-agent-app[bot]
committed
9fe1676

Commits on Aug 24, 2026

Agent: Promote `QuasilocalCompleteness` to a theorem and encode Axiom 4 as a b…
lean-agent-app[bot]
committed
340ca7a
Moved QuasilocalCompleteness.lean to QuasilocalObservable.lean
KellyJDavis
committed
7872756
Removed scratch placeholder
KellyJDavis
committed
f66ff58
Fixed many little problems created by Fuse
KellyJDavis
committed
3d9c4ef
More small fixes
KellyJDavis
committed
169a318
Fixing many small Fuse errors
KellyJDavis
committed
b51d0fb
Update using the blueprint pdf
KellyJDavis
committed
1bf6a1a
Update using the blueprint LaTeX
KellyJDavis
committed
eb800b5