Numerous additions#27

Merged

KellyJDavis merged 47 commits into

mainfrom

numina/aqft-in-lean

Jul 17, 2026

Commits on Jul 9, 2026

Agent: Add spacelike complement API with antitone and double-complement inclus…
lean-agent-app[bot]
committed
Agent: Add additive-free locality lemma: R(B') ≤ R(B)' for B' ⊆ B^⊥
lean-agent-app[bot]
committed
Agent: Add curved-net analogue of additive-free locality
lean-agent-app[bot]
committed
Agent: Refactor IsTrip/IsCausalTrip to piecewise transitive-closure definition
lean-agent-app[bot]
committed
Agent: Discharge sorry-proofs and update blueprint for precedence transitivity
lean-agent-app[bot]
committed

Commits on Jul 10, 2026

Agent: Refine doc comment to reflect identity-component bridge split
lean-agent-app[bot]
committed
Agent: Update stale deferral note in Isometry.lean to reflect implemented topo…
lean-agent-app[bot]
committed
Agent: Document geodesic placeholder divergence for trip definitions in bluepr…
lean-agent-app[bot]
committed
Update from v4.31.0-rc1 to v4.32.0-rc1
KellyJDavis
committed
Agent: Add flat covariant derivative scaffold for Levi-Civita Phase 1
lean-agent-app[bot]
committed
Agent: Add proof for `flatConnection.isCovariantDerivativeOnUniv`
lean-agent-app[bot]
committed
Agent: Add torsion-free theorem and metric-compatibility definition for flatCo…
lean-agent-app[bot]
committed
Agent: Prove `flatConnection_isMetricCompatible_const` by unfolding definitions
lean-agent-app[bot]
committed
Agent: Prove flatConnection_torsion and fix flatConnection_isMetricCompatible_…
lean-agent-app[bot]
committed

Commits on Jul 13, 2026

Agent: Add Levi-Civita connection fields to the `Spacetime` structure
lean-agent-app[bot]
committed
Agent: Replace `sorry` in `flatConnectionMinkowskiCarrier` with a structured p…
lean-agent-app[bot]
committed
Agent: Add script to replace metric-compatibility theorem proof in scratch file
lean-agent-app[bot]
committed
Agent: Remove connection fields from Spacetime structure and simplify IsMetric…
lean-agent-app[bot]
committed
Agent: Add `SpacetimeWithLeviCivita` structure extending `Spacetime`
lean-agent-app[bot]
committed
Agent: Define genuine auto-parallel geodesic condition on SpacetimeWithLeviCiv…
lean-agent-app[bot]
committed
Agent: Prove straight-line paths are geodesics in Minkowski spacetime
lean-agent-app[bot]
committed

Commits on Jul 14, 2026

Agent: Remove Connection and LeviCivita modules and their blueprint entries
lean-agent-app[bot]
committed
Agent: Add causal closure operator and complete lattice of causally complete r…
lean-agent-app[bot]
committed
Agent: Package π(A)' as a VonNeumannAlgebra (commutant/gauge algebra)
lean-agent-app[bot]
committed
Agent: Replace qualified `ContinuousLinearMap.*_apply` simp lemmas with dot-fr…
lean-agent-app[bot]
committed

Commits on Jul 15, 2026

Agent: Remove qualified `ContinuousLinearMap.*` lemma names in favour of dot-f…
lean-agent-app[bot]
committed
Updated v4.32.0-rc1 to v4.32.0
KellyJDavis
committed
Agent: Fix `Relation.TransGen.mono/lift` call sites for v4.32.0
lean-agent-app[bot]
committed
Agent: Add De Morgan / orthocomplement laws for the causal complement (bluepri…
lean-agent-app[bot]
committed
Agent: Prove spacelikeComplement_union and spacelikeComplement_iUnion
lean-agent-app[bot]
committed
Agent: Prove causal complement De Morgan laws on the lattice of causally compl…
lean-agent-app[bot]
committed
Agent: Clarify openness of chronological futures/pasts and add vacuity note
lean-agent-app[bot]
committed
Agent: Prove openness of chronological futures and pasts in Alexandrov topology
lean-agent-app[bot]
committed

Commits on Jul 16, 2026

Agent: Add Minkowski-specific unconditional openness of I⁺(p) and I⁻(p)
lean-agent-app[bot]
committed
Agent: Prove chronological future/past existence and openness for standard Min…
lean-agent-app[bot]
committed
Agent: Add double-commutant duality blueprint theorems and Lean stubs
lean-agent-app[bot]
committed
Agent: Prove four double-commutant duality theorems in Superselection.lean
lean-agent-app[bot]
committed
Agent: Fix `isFactor_gnsVonNeumann_iff_isFactor_commutant` simp call
lean-agent-app[bot]
committed
Agent: Add irreflexivity of ≪ and antisymmetry of ≺ under no-closed-causal-cur…
lean-agent-app[bot]
committed
Agent: Prove causality theorems and mark blueprint theorem as leanok
lean-agent-app[bot]
committed
Agent: Add Alexandrov genuine-basis theorems: covering, directedness, and basi…
lean-agent-app[bot]
committed
Agent: Prove four Alexandrov topology theorems and mark blueprint nodes leanok
lean-agent-app[bot]
committed
Agent: Prove `exists_future_between_standardMinkowski` and mark blueprint lemm…
lean-agent-app[bot]
committed
Updated homepage
KellyJDavis
committed

Commits on Jul 17, 2026

Agent: Mark `exists_past_between_standardMinkowski` as proved and condense `sU…
lean-agent-app[bot]
committed
Agent: Mark `alexandrov_nbhd_univ_of_no_diamond` as proved and add blueprint a…
lean-agent-app[bot]
committed
Updated homepage
KellyJDavis
committed