Numerous additions#27
Merged
Merged
Conversation
…nt inclus… - Define `spacelikeComplement B` as the set of points spacelike-separated from all of B, the geometric basis of locality and Haag duality. - Prove antitonicity (`B₁ ⊆ B₂ → B₂⊥ ⊆ B₁⊥`), `B ⊆ B⊥⊥`, the triple-complement identity `B⊥⊥⊥ = B⊥`, and the Galois bridge `B₁ ⊆ B₂⊥ ↔ IsCompletelySpacelike B₁ B₂`. - Add matching blueprint definition and lemma with `\leanok` tags and dependency annotations. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: d734bd15-bdb6-4750-83b0-b96629ba37d2 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Introduce `Spacetime.spacelikeComplement` and the Galois bridge lemma `subset_spacelikeComplement_iff` at the abstract `Spacetime` level, decoupled from the Lorentzian structure. - Add `localVonNeumannAlgebra_le_commutant_of_subset_spacelikeComplement`, which repackages bundled microcausality: if B' lies in the spacelike complement of B then R(B') ≤ R(B)', without ever attaching an algebra to the unbounded complement. - Record the corresponding blueprint theorem referencing the Galois bridge and the existing bundled-order result. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: d734bd15-bdb6-4750-83b0-b96629ba37d2 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Introduce `localVonNeumannAlgebra_le_commutant_of_subset_spacelikeComplement_geometric` in `Concrete.lean`, specialising the abstract additive-free locality theorem to a concrete Lorentzian spacetime via the `subset_spacelikeComplement_iff` Galois bridge. - Add the corresponding blueprint theorem `thrm:additive-free-locality-in-curved-spacetime` in section 10-4, marked `\leanok`, with uses linking it to the abstract locality result, the bundled von Neumann order, and the spacelike-complement definition. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: d734bd15-bdb6-4750-83b0-b96629ba37d2 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…efinition - Replace the monolithic `IsTrip`/`IsCausalTrip` predicates (one smooth curve + cut points) with a two-level design: `IsTripSegment`/`IsCausalTripSegment` for a single geodesic piece, and `IsTrip`/`IsCausalTrip` as `Relation.TransGen` of the corresponding single-segment precedence relations. - This makes transitivity of chronological and causal precedence trivially provable via `Relation.TransGen.trans`, and adds `chronologicallyPrecedes_trans` / `causallyPrecedes_trans` as immediate corollaries. - Lift single-segment Lorentz/isometry invariance lemmas to the full transitive-closure level (proofs left as `sorry` pending `TransGen.lift`/`TransGen.mono` wiring); update `ChronologicallyPrecedes`/`CausallyPrecedes` to unfold to `IsTrip`/`IsCausalTrip` directly. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: d734bd15-bdb6-4750-83b0-b96629ba37d2 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…nsitivity - Replace three `sorry` placeholders with `Relation.TransGen.lift`-based proofs for `chronologicallyPrecedes_pushforward`, `causallyPrecedes_smul`, and `chronologicallyPrecedes_smul`. - Prove `chronologicalFuture_standardMinkowski_subset` by induction on `TransGen`, using a Cauchy-Schwarz-style `nlinarith` argument for the cone inequality under concatenation. - Prove `minkowskiForwardCone_subset_chronologicalFuture_standardMinkowski` via `Relation.TransGen.single`. - Expand blueprint definitions of `Trip`/`CausalTrip` to mention segment vs. piecewise structure and add a new theorem node for transitivity of chronological and causal precedence. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: d734bd15-bdb6-4750-83b0-b96629ba37d2 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
The `Concrete.lean` header comment is updated to clarify that this bridge uses the full isometry group, while the proper-orthochronous identity-component restriction (Axiom 5) is handled by the new sibling bridge in `IdentityComponent.lean` via `Spacetime.Isometry.orientedIdentityComponent`. Notes which axioms (e.g. microcausality) still hold under the full group, and retains the one outstanding deferral on the bundled differential. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: ed575792-9451-4cb5-bbf3-9c37e481aa43 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…nted topo… The old note described the identity-component restriction as entirely deferred due to missing Mathlib support. The audit found that `IsometryTopology.lean` and `IsometryCausality.lean` already implement the topological group structure, `identityComponent`, and `orientedIdentityComponent`. Replace the deferral note with an accurate cross-reference explaining how the full group here serves as substrate and where the identity-component subgroup is defined and used. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: ed575792-9451-4cb5-bbf3-9c37e481aa43 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…in bluepr… Add a remark after `def:trip`/`def:causal-trip` explaining that `IsGeodesic` is currently defined as `True` in the Lean formalization. The remark clarifies that the geodesic condition (auto-parallelism via the Levi-Civita connection) cannot yet be enforced because the pinned Mathlib version lacks a Lorentzian Levi-Civita connection, while the endpoint, causal/timelike, and future-orientation content remains faithful. This documents the single known divergence between the blueprint definitions and their Lean implementations. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: ed575792-9451-4cb5-bbf3-9c37e481aa43 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
Introduces `Physicslib4.Spacetime.flatConnection`, a `CovariantDerivative` instance on the tangent bundle of a self-modelled manifold `E` that defines `∇σ := mvfderiv 𝓘(ℝ, E) σ`. The build-verification stub (proof deferred via `sorry`) confirms the Mathlib API is importable and the type signature compiles before proceeding to the full Levi-Civita design. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 6ab0ae22-ab22-48ac-ae2a-6dfe31a89ea6 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
Replace the `sorry` with a complete proof of the Leibniz and additivity axioms, reducing each to `mvfderiv_add` and `mvfderiv_smul` after unfolding the section differentiability hypothesis via `mdifferentiableAt_section`. Also register the new file in the top-level import list. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 6ab0ae22-ab22-48ac-ae2a-6dfe31a89ea6 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…or flatCo… - Introduce `flatConnection_torsion` (stub) asserting the flat connection has zero torsion, with a doc-comment outlining the proof strategy via `mlieBracketWithin_eq_lieBracketWithin` and `mfderiv_eq_fderiv`. - Define `IsMetricCompatible` for indefinite (Lorentzian) metric fields, filling the gap left by Mathlib's positive-definite-only `CovariantDerivative.IsMetricCompatible`. - Add `flatConnection_isMetricCompatible_const` (stub) showing compatibility with any constant metric, noting the bilinear product rule as the key step. - Import required Mathlib modules for Lie brackets and bilinear FDeriv lemmas. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 6ab0ae22-ab22-48ac-ae2a-6dfe31a89ea6 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…efinitions Replace the `sorry` with a complete calc-style proof that chains `mvfderiv` through `fderiv`, applies `ContinuousLinearMap.fderiv_of_bilinear` for the Leibniz product rule, and then rewrites using `precompR`/`precompL` to match the `IsMetricCompatible` goal. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 6ab0ae22-ab22-48ac-ae2a-6dfe31a89ea6 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…mpatible_… - Replace the `sorry` in `flatConnection_torsion` with a full proof that reduces the manifold torsion condition to the ordinary Lie bracket via `mlieBracketWithin_eq_lieBracketWithin` and the `mvfderiv`/`fderiv` bridge. - Add `omit [FiniteDimensional ℝ E] in` to `flatConnection_isMetricCompatible_const` so the theorem no longer requires the finite-dimensionality instance. - Reformat two long calc steps to stay within line-length limits. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 6ab0ae22-ab22-48ac-ae2a-6dfe31a89ea6 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Introduce `connection`, `connection_torsionFree`, and `connection_metricCompatible` fields in `Spacetime`, enforcing that the stored connection is torsion-free and metric-compatible and therefore cannot contradict the metric. - Generalise `IsMetricCompatible` in `Connection.lean` to work over an arbitrary model with corners `I` instead of only `modelWithCornersSelf`, enabling its use in `Spacetime` where the model is an opaque field. - Wire up both `StandardMinkowskiSpacetime` and `MinkowskiSpacetime` with their respective flat connections, torsion-freeness, and metric-compatibility proofs (the latter two deferred to `sorry` for the `MinkowskiSpacetimeCarrier`-native connection). Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: f469deb9-6243-41f7-a26d-3716ee42092f Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…uctured p… Fills in the `isCovariantDerivativeOnUniv` obligation by unpacking the `add` and `leibniz` fields separately. Each branch converts the section-differentiability hypothesis via `mdifferentiableAt_section`, resolves the chart/trivialization to the identity using `chartAt_minkowskiCarrier`, and then applies `mvfderiv_add` / `mvfderiv_smul` to close the goal. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: f469deb9-6243-41f7-a26d-3716ee42092f Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…ratch file Updates the proof of `flatConnectionMinkowskiCarrier_metricCompatible` in the scratch Lean file by patching it in-place via a Python script. The new proof uses chain-rule decomposition through `mfderiv_comp`, `mfderiv_prodMk`, and `ContinuousLinearMap.BilinearMap.fderiv` to reduce the goal to a pointwise bilinear identity, then closes with `simpa`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: f469deb9-6243-41f7-a26d-3716ee42092f Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
… IsMetric… - Drop the `connection`, `connection_torsionFree`, and `connection_metricCompatible` fields from the `Spacetime` structure, along with the `Connection` import that supported them; the Levi-Civita connection is not yet ready to be bundled as structure data. - Specialize `IsMetricCompatible` to the self-modelled case (`modelWithCornersSelf ℝ E`) to remove the problematic implicit `[IsManifold]` argument that was causing elaboration failures. - Remove the corresponding `flatConnectionMinkowskiCarrier` definitions and sorry-filled theorems from `Minkowski.lean`, and drop the connection fields from both `StandardMinkowskiSpacetime` and `MinkowskiSpacetime`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: f469deb9-6243-41f7-a26d-3716ee42092f Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Introduce `SpacetimeWithLeviCivita`, which bundles a `Spacetime` with a covariant derivative constrained to be torsion-free and metric-compatible (i.e. the Levi-Civita connection). - Provide `standardMinkowski` as the canonical example, using `flatConnection` with its existing torsion-free and metric-compatibility proofs. - Generalise `IsMetricCompatible` to arbitrary `ModelWithCorners` so it works outside the self-model setting. - Make `Spacetime.isManifold` instance-implicit to allow downstream structures to synthesise tangent-bundle instances automatically. - Add corresponding blueprint definitions for `SpacetimeWithLeviCivita` and `standardMinkowski`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: f469deb9-6243-41f7-a26d-3716ee42092f Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…thLeviCiv…
Replace the `IsGeodesic := True` placeholder with a real auto-parallel
condition. A smooth path `μ` is a geodesic if there exists a global
vector field `V` restricting to the velocity `μ.tangent` along `μ`
such that `∇_V V` vanishes on `μ`. The docstring and blueprint entry
explain why the extension `V` is independent of choice (germ-dependence
of `∇`), making this equivalent to the classical `∇_{μ'}μ' = 0`.
Blueprint: aqft-in-lean
Repository: physicslib/physicslib4
Agent job: f469deb9-6243-41f7-a26d-3716ee42092f
Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
Add `standardMinkowski_lineSegment_isGeodesic`, showing that the path `s ↦ p + s(q-p)` satisfies `IsGeodesic` for `standardMinkowski`. The constant velocity `q-p` serves as the global vector field extension; its covariant derivative vanishes because `mvfderiv` of a constant is zero. This confirms `IsGeodesic` is inhabited and that the auto-parallel definition is non-trivial. The corresponding blueprint theorem is added with `\leanok` and appropriate `\uses` links. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: f469deb9-6243-41f7-a26d-3716ee42092f Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…ntries Delete `Spacetime/Connection.lean`, `Spacetime/LeviCivita.lean`, and the helper `replace_theorem.py` script, and remove the corresponding four blueprint definitions/theorem blocks. Update the root import list and simplify the `isManifold` doc-string in `Spacetime/Basic.lean` (dropping the now-irrelevant instance-implicit note). The code and prose are superseded or no longer needed at this stage of the formalization. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 4761ee00-e61b-451a-8feb-00782fcfc3f8 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…omplete r… - Define `causalClosure` as a `ClosureOperator` via the double spacelike complement `B ↦ B^⊥⊥`, using monotonicity, extensivity, and idempotency already established for `spacelikeComplement`. - Introduce `IsCausallyComplete` (fixed points of the closure), show spacelike complements and intersections of causally complete regions are causally complete, and lift the complete lattice structure via the Galois insertion. - Define `causalComplement` as an order-reversing involution on `CausallyCompleteRegion` and prove `B^⊥⊥ = B`; note the full orthocomplement law is not claimed at this generality. - Add matching blueprint definitions and theorem for the lattice of causally complete regions. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 4761ee00-e61b-451a-8feb-00782fcfc3f8 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Introduce `commutantVonNeumann π` constructing the centralizer of `π(A)` as a `VonNeumannAlgebra` via `vonNeumannOfSelfAdjoint`, using self-adjointness of the range and the triple-centralizer identity `S''' = S'`. - Add `coe_commutantVonNeumann` and `mem_commutantVonNeumann_iff_intertwines` to expose the underlying set and characterize membership as being a self-intertwiner. - State `isIrreducible_iff_commutantVonNeumann_eq_scalars` (von Neumann form of Schur's lemma): π is irreducible iff its commutant algebra equals ℂ·1. - Add corresponding blueprint theorem `thrm:commutant-von-neumann` with Lean references and dependency on `lmm:endomorphism-scalar`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: f8abe6c8-605e-49ad-85e5-2401e7ad7076 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…th dot-fr… Resolve warnings caused by deprecated or namespace-qualified simp lemma names (e.g., `ContinuousLinearMap.add_apply`, `smul_apply`, `mul_apply`, etc.) by using the shorter unqualified aliases (`add_apply`, `smul_apply`, `mul_apply_eq_comp`, `one_apply_eq_self`, `sub_apply`, `neg_apply`, `zero_apply`) throughout the GNS and Spacetime files. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: f8abe6c8-605e-49ad-85e5-2401e7ad7076 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
… of dot-f… Replace occurrences of `ContinuousLinearMap.mul_apply`, `ContinuousLinearMap.one_apply`, `ContinuousLinearMap.zero_apply`, `ContinuousLinearMap.add_apply`, `ContinuousLinearMap.smul_apply`, `ContinuousLinearMap.sub_apply`, and `Set.mem_diff_of_mem` with their shorter, unqualified counterparts (`mul_apply_eq_comp`, `one_apply_eq_self`, `zero_apply`, `add_apply`, `smul_apply`, `sub_apply`, and `Set.mem_sdiff_of_mem`). Also drop a now-redundant `change` tactic in `QuasilocalLift.unique`. These are pure lint/warning cleanups with no logical changes. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 1671ae84-b950-4e99-a442-f5d2f87969f7 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
Explicit universe/implicit arguments `_ _` are now required before the relation proof in `Relation.TransGen.mono` and `Relation.TransGen.lift`; add them at all four affected call sites to clear the resulting errors. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 1671ae84-b950-4e99-a442-f5d2f87969f7 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
… (bluepri… - Add `spacelikeComplement_union` and `spacelikeComplement_iUnion` (set-level De Morgan) with blueprint lemma `lmm:spacelike-complement-de-morgan` and pointwise proof sketch. - Add `causalComplement_antitone`, `_bot`, `_top`, `_sup`, `_inf`, `_iSup`, `_iInf` as `sorry`-stubbed Lean theorems with a corresponding blueprint theorem `thrm:causal-complement-de-morgan`, detailing the derivation via the triple-complement identity and the set-level lemmas. - Blueprint proofs explain why antitonicity alone is insufficient and how the involution `B^⊥⊥ = B` upgrades inequalities to equalities and finite laws to infinitary ones. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 1671ae84-b950-4e99-a442-f5d2f87969f7 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
Replace `sorry` placeholders in both De Morgan theorems for the spacelike complement with complete proofs. The union case reduces to `isCompletelySpacelike_union_right`; the indexed-union case uses `isCompletelySpacelike_mono` for the forward direction and `isCompletelySpacelike_singleton_left_iff` together with `Set.mem_iUnion` for the reverse. Mark the blueprint lemma and its proof block with `\leanok`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 1671ae84-b950-4e99-a442-f5d2f87969f7 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…lly compl… - Replace all `sorry` placeholders in `CausalComplement.lean` with complete proofs for `causalComplement_antitone`, `causalComplement_bot`, `causalComplement_top`, `causalComplement_sup`, `causalComplement_inf`, `causalComplement_iSup`, and `causalComplement_iInf`. - Add helper lemmas `coe_inf`, `coe_sup`, `coe_top`, `coe_bot`, `coe_iSup`, `coe_iInf` and `isCausallyComplete_iInter` to support the proofs. - Mark the corresponding blueprint theorem and proof with `\leanok`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 1671ae84-b950-4e99-a442-f5d2f87969f7 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…y note - Add three Lean stubs (`isOpen_chronologicalFuture_inter_chronologicalPast`, `isOpen_chronologicalFuture`, `isOpen_chronologicalPast`) in the Alexandrov topology section. - Add the corresponding blueprint lemma with proof sketch, explaining that the per-point hypotheses are vacuously satisfied when the set is empty (so the empty set case is consistent), and that the unconditional claim is false in general due to future-endpoint points. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 1671ae84-b950-4e99-a442-f5d2f87969f7 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…v topology - Replace three `sorry` stubs with complete proofs for `isOpen_chronologicalFuture_inter_chronologicalPast`, `isOpen_chronologicalFuture`, and `isOpen_chronologicalPast`. - The future/past proofs decompose the set as a union of basis open sets (using the no-endpoints hypothesis) then apply `isOpen_iUnion`. - Mark the corresponding blueprint lemma `\leanok` in both the statement and proof environments. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 1671ae84-b950-4e99-a442-f5d2f87969f7 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Blueprint: new lemma `minkowski-chronological-open` with a three-part statement and proof sketch covering existence of future/past points via the ±e₀ cone argument, Euclidean openness via continuity of the Minkowski quadratic form, and Alexandrov openness by discharging the per-point hypothesis of the general lemma. - Lean: six corresponding theorem stubs (existence, Euclidean openness, Alexandrov openness, and their past duals) with `sorry` placeholders, linked to the blueprint via `\lean` tags. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 6a21e04b-14ed-4488-a72c-683db0e8b953 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…ndard Min… - Fill six `sorry`-bearing theorems: existence of chronological future/past points (via `x ± e₀`), Euclidean openness of `I⁺`/`I⁻` (via `isOpen_minkowskiForwardCone`/`isOpen_minkowskiBackwardCone`), and Alexandrov openness of `I⁺`/`I⁻` (via the generic `isOpen_chronologicalFuture`/`Past` lemmas). - Mark the corresponding blueprint lemma and its proof block with `\leanok` now that all six Lean declarations are proved. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 6a21e04b-14ed-4488-a72c-683db0e8b953 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Introduce `thrm:double-commutant-duality` in the blueprint, covering `S''' = S'` and the bicommutant identity for the pair `π(A)''`, `π(A)'`. - Introduce `thrm:commutant-factor-duality`, linking the factor property and triviality across the duality. - Add four corresponding Lean declarations (`commutant_gnsVonNeumannAlgebra`, `commutant_commutantVonNeumann`, `isFactor_gnsVonNeumann_iff_isFactor_commutant`, `commutantVonNeumann_eq_scalars_iff_gnsVonNeumann_eq_univ`) as `sorry`-stubs, ready for proof. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: b5416268-912b-49a0-b603-4c75f879ad21 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
….lean - Replace `sorry` in `commutant_gnsVonNeumannAlgebra` and `commutant_commutantVonNeumann` with `SetLike.coe_injective` + `simp [gnsVonNeumann]` proofs. - Prove `isFactor_gnsVonNeumann_iff_isFactor_commutant` by unfolding definitions and using `Set.inter_comm`. - Prove `commutantVonNeumann_eq_scalars_iff_gnsVonNeumann_eq_univ` by chaining the two existing irreducibility iff lemmas. - Mark the corresponding blueprint theorems `\leanok` now that the Lean proofs are complete. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: b5416268-912b-49a0-b603-4c75f879ad21 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
Replace bare `simp` with `simp only [Set.centralizer_centralizer_centralizer]` to avoid timeouts and make the proof more robust. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: b5416268-912b-49a0-b603-4c75f879ad21 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…ausal-cur… - Introduce `NoClosedCausalCurve` (the causality condition `¬ p ≺ p`) in both the blueprint and Lean source, with docstrings explaining its place in the hierarchy of causality conditions. - State `chronologicallyPrecedes_irrefl`, `causallyPrecedes_asymm`, and `causallyPrecedes_antisymm` as `sorry`-stubbed theorems, establishing that under the causality condition `≺` is a strict partial order. - Add matching blueprint definition and theorem with full `\lean`, `\uses`, and `\leanok` annotations. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: b5416268-912b-49a0-b603-4c75f879ad21 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
Replace `sorry` stubs in `chronologicallyPrecedes_irrefl`, `causallyPrecedes_asymm`, and `causallyPrecedes_antisymm` with one-line proofs that unfold `NoClosedCausalCurve` directly. Move `\leanok` after `\uses` in the corresponding blueprint theorem to reflect the completed formalization. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: b5416268-912b-49a0-b603-4c75f879ad21 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
… and basi… - Blueprint: add lemmas for no-diamond neighbourhood, Hausdorff-implied covering, past/future interpolation on Minkowski, downward intersection property, and two `IsTopologicalBasis` theorems (general Lorentzian and standard Minkowski). - Lean: stub out `sUnion_alexandrovBasis_eq_univ`, `isTopologicalBasis_alexandrovBasis` (with explicit directedness hypothesis) in `LorentzianSpacetime`, and the Minkowski-specific interpolation, intersection, and basis lemmas in `MinkowskiDirected`, all marked `sorry` pending proof. - Import `Mathlib.Topology.Bases` where needed to expose `IsTopologicalBasis`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: b5416268-912b-49a0-b603-4c75f879ad21 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…es leanok - `sUnion_alexandrovBasis_eq_univ`: uses Hausdorff separation to derive a contradiction if any point is covered by no diamond, then applies T₂ separation to force U = univ. - `isTopologicalBasis_alexandrovBasis`: follows immediately by forwarding the covering lemma and the directedness hypothesis to `IsTopologicalBasis.mk`. - `exists_past_between_standardMinkowski`: constructs the interpolating point `a = x - ε·e₀` using an explicit slack `ε = min(δ₁/2T₁, δ₂/2T₂)` and verifies all three cone memberships by arithmetic. - `alexandrovBasis_exists_subset_inter_standardMinkowski` and `isTopologicalBasis_alexandrovBasis_standardMinkowski`: assemble past/future interpolation and covering witnesses to discharge the basis conditions. - Blueprint `\leanok` annotations added to all four lemma/theorem statements and their proof blocks. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: b5416268-912b-49a0-b603-4c75f879ad21 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…rint lemm… - Replace the `sorry` in `exists_future_between_standardMinkowski` with a complete proof: construct `b = x + ε·e₀` where ε = min(δ₁/(2T₁), δ₂/(2T₂)), then verify all three backward-cone memberships via explicit arithmetic estimates. - Add `\leanok` to both the lemma statement and its proof block in the blueprint. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: b5416268-912b-49a0-b603-4c75f879ad21 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…dense `sU… - Add `\leanok` to the lemma and proof environments for `exists_past_between_standardMinkowski` in the blueprint. - Condense the `sUnion_alexandrovBasis_eq_univ` Lean proof using term-mode rewrites and `obtain` patterns, eliminating verbose intermediate `have` chains. - Add a stub (with `sorry`) for `alexandrov_nbhd_univ_of_no_diamond`, extracting the no-diamond neighbourhood argument into a reusable named lemma. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: aecb92c3-ae1f-4a6c-b9fa-35d9c249bb7b Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…ueprint a… - Replace the `sorry` in `Causality.lean` with a complete induction proof over `TopologicalSpace.GenerateOpen`, handling the basic, univ, inter, and sUnion cases. - Clean up the redundant `hx'` auxiliary in `LorentzianSpacetime.lean`, inlining the contradiction directly. - Add `\lean`, `\leanfile`, and `\leanok` tags to the corresponding blueprint lemma and proof block. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: aecb92c3-ae1f-4a6c-b9fa-35d9c249bb7b Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.