Numerous AQFT additions#26

Merged

KellyJDavis merged 27 commits into

mainfrom

numina/aqft-in-lean

Jul 8, 2026

Commits on Jul 3, 2026

Agent: Add topology instances for Isom on both spacetime bridges
lean-agent-app[bot]
committed
Agent: Add bundled unitary rep theorems at the net and stabilizer level
lean-agent-app[bot]
committed
Agent: Confirm `ContinuousSMul` is automatic for identity-component subgroups
lean-agent-app[bot]
committed
Updated image
KellyJDavis
committed
Revert "Updated image"
KellyJDavis
committed
Updated image
KellyJDavis
committed

Commits on Jul 4, 2026

Agent: Add `SmoothPath.tangent` accessor and restate causal predicates through…
lean-agent-app[bot]
committed
Agent: Add causal scaling-invariance lemmas and reparametrisation chain rule
lean-agent-app[bot]
committed
Agent: Add reparametrisation-invariance of `IsTimelikeAt` via chain rule
lean-agent-app[bot]
committed

Commits on Jul 6, 2026

Agent: Add reparametrisation-invariance theorems for timelike and causal paths
lean-agent-app[bot]
committed
Agent: Add OrientedSmoothPathEquiv and prove orientation invariance under it
lean-agent-app[bot]
committed
Agent: Lift causal/orientation predicates to SmoothCurve and OrientedSmoothCur…
lean-agent-app[bot]
committed
Agent: Add projection OrientedSmoothCurve → SmoothCurve with causal compatibil…
lean-agent-app[bot]
committed
Agent: Add `UnitaryEquiv` for representations and prove it is an equivalence r…
lean-agent-app[bot]
committed
Agent: Add disjointness and quasi-equivalence of representations
lean-agent-app[bot]
committed

Commits on Jul 7, 2026

Agent: Add blueprint definitions for unitary equivalence, disjointness, and qu…
lean-agent-app[bot]
committed
Agent: Add `lpDiag` diagonal operator with *-algebra-hom laws
lean-agent-app[bot]
committed
Agent: Add direct-sum representation and summand subrepresentation results
lean-agent-app[bot]
committed
Agent: Add GNS amplification and reducibility corollary for direct sums
lean-agent-app[bot]
committed
Agent: Add blueprint entries for direct-sum, amplification, and reducibility
lean-agent-app[bot]
committed
Agent: Add blueprint entries for curve reparametrisation-invariance theorems
lean-agent-app[bot]
committed
Agent: Prove Schur's lemma and the irreducible dichotomy for unitary represent…
lean-agent-app[bot]
committed

Commits on Jul 8, 2026

Agent: Add irreducible dichotomy theorem to superselection blueprint section
lean-agent-app[bot]
committed
Agent: Add Schur multiplicity lemma: intertwiner space between irreducibles is…
lean-agent-app[bot]
committed
Agent: Add End(irreducible) = ℂ·1 lemma and curved irreducible dichotomy corol…
lean-agent-app[bot]
committed
Agent: Add pure-state dichotomy theorem to blueprint and Lean formalization
lean-agent-app[bot]
committed
Updated homepage
KellyJDavis
committed