Expansion of spacetime related lemmas, definition of covariant states, and the beginnings of a vacuum defintion#12
Merged
Merged
Conversation
added 30 commits
June 18, 2026 09:22
- Add `isTimelike_or_isNull_or_isSpacelike` (trichotomy via `lt_trichotomy`), mutual exclusion lemmas between the three classes, and `isNull_zero`. - Add `isTimelike_or_isNull_of_isFuturePointing/isPastPointing` and `not_isFuturePointing_and_isPastPointing_of_isTimelike` for the time-orientation layer. - All proofs reduce to ordered-field / `lt_asymm` / `ne_of_lt` lemmas already in Mathlib. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
- Prove that timelike paths are causal and lift this to trips, giving `causallyPrecedes_of_chronologicallyPrecedes` and the two subset lemmas for futures/pasts. - Prove `isSpacelikeRelated_comm` and `isCompletelySpacelike_comm` showing spacelike relatedness and complete spacelike separation are symmetric. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
- Prove `chronologicalFutureSet_mono`, `chronologicalPastSet_mono`, `causalFutureSet_mono`, and `causalPastSet_mono`: each set-valued causal/chronological future or past is monotone with respect to subset inclusion. - Add `isOpen_alexandrov_of_mem_basis`, showing every Alexandrov basis set is open in the generated topology, directly via `GenerateOpen.basic`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
…rentzianS… Add `isCompletelySpacelike_comm` and `isOpen_alexandrov_of_isBasisSet` as theorems on the bundled `LorentzianSpacetime` structure, delegating to the corresponding `Spacetime`-layer results. This makes both facts available without unwrapping the bundle at call sites. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
Records six new lemmas in the spacetime blueprint section: - Causal Classification: trichotomy and mutual exclusivity of timelike/null/spacelike vectors, with zero being null - Orientation of Pointing Vectors: future/past-pointing implies timelike or null; a timelike vector cannot be both - Chronological Implies Causal Precedence: trips are causal trips, giving I⁺ ⊆ J⁺ and I⁻ ⊆ J⁻ - Monotonicity of Futures and Pasts: set-valued I± and J± are monotone under set inclusion - Symmetry of Spacelike Separation: spacelike relatedness and complete spacelike separation are symmetric - Basis Sets Are Alexandrov-Open and their lift to LorentzianSpacetime Each lemma is linked to its Lean declarations, source file, and dependency chain via `\lean`, `\leanfile`, `\leanok`, and `\uses`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
Prove that spacetime isometries preserve the metric square of tangent vectors and, as immediate corollaries, preserve the timelike, null, and spacelike classifications. These lemmas form the foundational link between the isometry group and the causal structure required by Axiom 5. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
…equisite Prove that a path's parameter space satisfies `UniqueDiffOn ℝ` by showing it is convex (via `OrdConnected`) with non-empty interior (witnessed by the midpoint of the two distinct points guaranteed by `nontrivial`). This lemma is needed to apply the `mfderivWithin` chain rule when differentiating compositions along a path, forming the first link in the basis-set-preservation chain for isometries. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
…e preserv… - Introduce `pushforwardPath` constructing `g ∘ μ` as a `SmoothPath`, with smoothness from `ContMDiff.comp_contMDiffOn` and non-vanishing tangent via injectivity of the isometry differential. - Prove `mfderivWithin_comp_diffeo` using `uniqueDiffOn_parameterSpace` and the manifold chain rule, then derive timelike/causal/endpoint preservation lemmas. - Build up to `alexandrovBasis_image`, showing orientation-preserving isometries carry Alexandrov basis sets to Alexandrov basis sets, as the geometric core of Axiom 5. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
…tion - Prove `preservesFutureOrientation_one`: the identity isometry trivially preserves any time orientation via `mfderiv_id`. - Prove `preservesFutureOrientation_mul`: composition of two orientation-preserving isometries is orientation-preserving, using `mfderiv_comp_apply` to unfold the derivative of the composite. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
…on and pr… - Define `futureOrientationPreserving` as a subgroup closing over both `g` and `g⁻¹`, avoiding any appeal to the C⁰ group topology. - Define `orientedIdentityComponent` as the meet of the identity component and `futureOrientationPreserving`, making orientation-preservation a structural axiom rather than a derived fact. - Add `alexandrovBasis_image_of_mem` and `alexandrovBasis_image_of_mem_orientedIdentityComponent` to give unconditional Alexandrov-basis preservation for elements of these subgroups, providing the geometric basis for Axiom 5's covariance action. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
…and smul… - Prove `smul_set_eq_image` to equate the pointwise `g • B` action with the diffeomorphism image, enabling rewriting between the two forms. - Lift `alexandrovBasis_image_of_mem_orientedIdentityComponent` to `LorentzianSpacetime.isBasisSet_image` and `isBasisSet_smul`, providing the `g • B` form required by the abstract Axiom 5 interface. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
- Replace `identityComponent` with `orientedIdentityComponent` (future-orientation-preserving subgroup) in `toAbstractIdentityComponent`, making the isometry group match Axiom 5 exactly. - Add `toAbstractIdentityComponent_isBasisSet_smul`, which wires `isBasisSet_smul` directly through the bridge so that Axiom 5 basis-set preservation `φ(𝐁) ∈ 𝐁` is a proved theorem rather than an assumption. - Import `IsometryCausality` to bring the oriented component and its API into scope. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
…nent - Introduce `toAbstractIdentityComponent_Isom` as a `@[simp]` lemma, exposing the definitional equality between `(bridge).Isom` and `↥(orientedIdentityComponent ...)`. - Re-state `toAbstractIdentityComponent_isBasisSet_smul` entirely over the abstract interface, so `φ`, `B`, and `hB` all live in the bridge type; the proof delegates to the concrete lemma via the `simp`-rewriteable coercion. - Trim the docstring to remove the now-redundant explanation of the Isom-vs-subgroup identification. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
…on results Six new lemma environments covering: - Isometries preserving causal classification of tangent vectors - Unique differentials on path parameter spaces - Pushforward of paths under isometries (tangent, type, endpoints) - Isometries preserving chronological order and futures/pasts - Isometries mapping Alexandrov-basis diamonds to diamonds - Axiom 5 basis-set preservation for the oriented identity component Also consolidates previously split `\uses` directives onto single lines throughout the section for consistency. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
…f Axiom 5 Notes that the Lean formalization explicitly intersects the identity component with the orientation-preserving isometry subgroup, rather than relying on the automatic time-orientation preservation that follows from connectedness. This is a temporary implementation choice pending a Myers–Steenrod rigidity result in Mathlib, and does not affect the mathematical content of the axiom. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
…m through…
All blueprint lemma and definition environments that had multiple separate `\uses{...}` lines now use a single comma-separated `\uses{..., ...}` line. This ensures the dependency graph is fully and consistently represented across the GNS construction, spacetime, Haag-Kastler flat, and Haag-Kastler curved spacetime sections.
Blueprint: aqft-in-lean
Repository: physicslib/physicslib4
Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427
Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
Swap `IsometryCausality` and `IsometryTopology` import order so that the dependency graph resolves cross-references correctly when building the blueprint PDF/web output. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
Replace `width=\linewidth` with `width=345pt` on both Schwarzschild Penrose diagram figures to use an absolute width that plasTeX handles without warnings. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
- Monotonicity under subset inclusion of either region - `simp` lemmas for empty left/right regions - Union characterizations on left and right - Bundled restatements on `LorentzianSpacetime` delegating to `Spacetime` Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
Introduce a new lemma environment documenting monotonicity, empty-region, and union properties of complete spacelike separation, for both the unbundled and bundled (LorentzianSpacetime) variants. The proof notes that each property follows directly from the pointwise definition. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e6dcc73e-d501-4839-88f2-615dbbd9d427 Conversation: 44c9bc92-39d0-4c6a-a70d-e9fd7f090a22
- New blueprint lemma `lmm:reverse-cauchy-schwarz` states `g(v,v)·g(w,w) ≤ g(v,w)²` for timelike vectors in a Lorentzian bilinear form, with a coordinate proof using the algebraic identity `(pq−rs)²−(p²−r²)(q²−s²) = (ps−rq)²`. - New file `LorentzCauchySchwarz.lean` provides the abstract result `reverse_cauchy_schwarz_of_lorentzianAt` (via `nlinarith` after choosing a Lorentzian basis) and the spacetime specialisation `Spacetime.reverse_cauchy_schwarz`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 1cd9f50a-6503-49d3-930c-9dc78aacd69f Conversation: 784066e3-5aa0-4cf7-b57b-488e51fd55d1
…k bluepri… - Rename unused hypotheses `hsymm`/`hv` to `_hsymm`/`_hv` to suppress linter warnings. - Introduce `hb'` as a beta-reduced alias for the Gram-matrix hypothesis so `rw` can apply it directly inside the `step2` block. - Replace the broken `simp`/`norm_num` call with `rw [step1, Fin.sum_univ_four]` followed by a `simp` with the correct lemma set and a closing `ring`, fixing the coordinate-expansion step. - Update the wrapper signature to match (unused parameter names prefixed with `_`). - Mark the corresponding blueprint theorem with `\leanok` now that the Lean proof compiles. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e4f0f62c-54e0-44bb-9d79-d7b301116b95 Conversation: 784066e3-5aa0-4cf7-b57b-488e51fd55d1
Introduce `lmm:timelike-cone-convexity` in the blueprint and the new file `Physicslib4/Spacetime/LorentzCone.lean`, establishing: - `add_isTimelike_of_lorentzianAt`: the sum of two aligned timelike vectors is timelike (consumes only bilinearity and symmetry). - `reverse_triangle_of_lorentzianAt`: the reverse Lorentzian triangle inequality `√(-g(v,v)) + √(-g(w,w)) ≤ √(-g(v+w,v+w))`, which consumes `reverse_cauchy_schwarz_of_lorentzianAt`. - `Spacetime.add_isTimelike` and `Spacetime.reverse_triangle`: pointwise specialisations to the metric `g|_p` of any spacetime. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e4f0f62c-54e0-44bb-9d79-d7b301116b95 Conversation: 784066e3-5aa0-4cf7-b57b-488e51fd55d1
…nvexity - Introduce `LorentzOrthogonal.lean` with the `t`-orthogonal projection identity, positive semidefiniteness of the spacelike complement, forward Cauchy-Schwarz on that complement, and the algebraic core lemma `sign_algebra`. - Prove `bilin_neg_of_inner_t_neg` (abstract sign lemma) and its spacetime instance `inner_neg_of_future_timelike`, then use them to derive `isFuturePointing_add` (convexity of the future timelike cone). - Add corresponding blueprint lemmas for the sign lemma and future-cone convexity, with `\leanok` annotations and cross-references to reverse Cauchy-Schwarz. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e4f0f62c-54e0-44bb-9d79-d7b301116b95 Conversation: 784066e3-5aa0-4cf7-b57b-488e51fd55d1
…elike com… - Prove `eq_zero_of_forall_bilin_eq_zero`: a Lorentzian form is nondegenerate by reading off coordinates in the signature basis, where the diagonal entries of `diag(-1,1,1,1)` are all nonzero. - Prove `pos_of_orthogonal_timelike`: semidefiniteness plus a Cauchy-Schwarz/nondegeneracy argument forces `B u u > 0` for any nonzero `u` orthogonal to a timelike vector. - Derive `isSpacelike_of_orthogonal_timelike` at the `Spacetime` level, and add the corresponding blueprint lemma with proof sketch. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e4f0f62c-54e0-44bb-9d79-d7b301116b95 Conversation: 784066e3-5aa0-4cf7-b57b-488e51fd55d1
- Add `exists_seq_of_isFuturePointing`, which witnesses every future-pointing vector (timelike or null) as a limit of future-pointing timelike vectors. - Add `inner_t_nonpos_of_future` and `inner_nonpos_of_future` to extend the sign lemma from strict (timelike) to non-strict (causal) inequalities via continuity. - Add `isFuturePointing_add_general`, proving that the full future cone (including null boundary) is closed under addition, by approximating both summands with timelike sequences and passing to the limit. - Update the blueprint lemma statement and proof sketch to cover the general case. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: e4f0f62c-54e0-44bb-9d79-d7b301116b95 Conversation: 784066e3-5aa0-4cf7-b57b-488e51fd55d1
- Prove `isPastPointing_iff_isFuturePointing_neg`: a vector is past-pointing iff its negation is future-pointing, covering both timelike and null cases. - Derive `inner_neg_of_past_timelike` (past-cone sign lemma) and `isPastPointing_add` (past-cone convexity) by reducing to their future-pointing counterparts through negation. - Fold the new Lean declarations into the corresponding blueprint lemma entries for the sign lemma and convexity of the future/past cone. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 499ad7b5-4ec8-48c2-adde-dfe2ac36cc7e Conversation: 784066e3-5aa0-4cf7-b57b-488e51fd55d1
- Prove `isFuturePointing_smul_pos`: a positive scalar multiple of a future-pointing vector is future-pointing, handling both timelike and null cases. - Derive `isFuturePointing_pos_combination` as the full convex-cone closure under positive linear combinations, consuming `isFuturePointing_add_general`. - Mirror both results for past-pointing vectors via the negation equivalence. - Update the blueprint lemma entry to list all four new Lean declarations and extend the prose to state the convex-cone characterisation explicitly. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 499ad7b5-4ec8-48c2-adde-dfe2ac36cc7e Conversation: 784066e3-5aa0-4cf7-b57b-488e51fd55d1
…time decl… Both `Spacetime.LorentzianSpacetime` (geometric bundle) and `HaagKastlerCurved.LorentzianSpacetime` (axiom-facing interface) now document their relationship: the geometric structure is exposed to the curved Haag-Kastler axioms via `toAbstract`, and both correspond to the same blueprint definition `def:lorentzian-spacetime`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 499ad7b5-4ec8-48c2-adde-dfe2ac36cc7e Conversation: 784066e3-5aa0-4cf7-b57b-488e51fd55d1
- Expose `HaagKastlerNet.algebra` and empty-region properties as top-level `abbrev`/theorems inside a `HaagKastlerNet` namespace for ergonomic access. - Prove `exists_injective_self` (isotony is reflexive via `StarAlgHom.id`) and `Isotony.trans` (composition of injective star-hom embeddings) in `Isotony.lean`. - Wire both into `HaagKastlerNet.isotony_refl` and `HaagKastlerNet.isotony_trans` as convenient net-level lemmas. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 03ea39e0-9e50-41db-a79e-9502976780e3 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…etry to b… - Add `norm_covEquiv` and `commute_covEquiv_iff` to flat and curved nets, showing the covariance StarAlgEquiv preserves norms and commutation relations - Expose `commAlgebra`/`commIsotony` helpers that extract the local-commutativity witness from the axiom, along with injectivity of the curved isotony embeddings - Add `commute_ι_of_spacelike_symm` and `commute_of_spacelike_symm` deriving that spacelike commutativity holds in either order via `Commute.symm` Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 1e271c4f-8885-4bbe-bb12-17dd3d08820c Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
Add a new `Observables` section inside `HaagKastlerNet` that re-exposes the `HaagKastler`-level quasilocal-observable lemmas (characterisation iff, identity, addition, real-scalar scaling, and linear combinations) as theorems stated directly on a `HaagKastlerNet` and its quasilocal algebra, delegating proofs to the existing lower-level results. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: aea39373-6801-4dda-9604-8ab26bef73da Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
Prove `commute_of_spacelike_mono`, showing that completely-spacelike commutativity is inherited by sub-basis-sets. The proof reduces to `commute_of_spacelike` after applying the supplied `mono` hypothesis to shrink the spacelike pair, with inclusion transitivity handling the containment conditions. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: aea39373-6801-4dda-9604-8ab26bef73da Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…pothesis Introduce `commute_of_spacelike_mono_geometric`, a specialisation of `commute_of_spacelike_mono` for nets over `L.toAbstract`. The monotonicity side condition is satisfied automatically via `LorentzianSpacetime.isCompletelySpacelike_mono`, so callers working with a concrete Lorentzian spacetime no longer need to supply that proof manually. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: aea39373-6801-4dda-9604-8ab26bef73da Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…flat and… Expose the group-action coherence conditions stored inside the covariance witness as named theorems in both `HaagKastler.Net` and `HaagKastlerCurved.Net`. `covEquiv_one` states that the identity transformation acts as the identity automorphism, and `covEquiv_mul` states that composition of group elements corresponds to composition of automorphisms, both modulo the canonical `one_smul`/`mul_smul` identifications. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: aea39373-6801-4dda-9604-8ab26bef73da Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
… nets Introduces `IsCovariantFamily`, predicate asserting that a fiberwise assignment of states to local algebras is intertwined by the covariance equivalences (`covEquiv`). Proves `IsCovariantFamily.one` (covariance at the identity via `covEquiv_one`) and `IsCovariantFamily.comp` (composition of covariance through two Lorentz transformations). Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: aea39373-6801-4dda-9604-8ab26bef73da Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
Introduce `HaagKastlerNet.IsCovariantFamily` in a new `CovariantState` module, mirroring the flat Minkowski construction. A covariant family assigns a state `ω B` to each local algebra such that `ω B a = ω (φ·B) (covEquiv φ B a)` for every isometry `φ`. Coherence lemmas `IsCovariantFamily.one` and `IsCovariantFamily.comp` establish behaviour at the identity and under composition of isometries. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: aea39373-6801-4dda-9604-8ab26bef73da Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…Lorentz l…
Introduces `HaagKastlerNet.QuasilocalLift`, a structure recording a `*`-automorphism `β` of the quasilocal algebra that intertwines the fiberwise covariance equivalences with the local embeddings (`β (ι_B a) = ι_{L·B} (α_L a)`).
- Proves `QuasilocalLift.unique`: any two lifts of the same `L` agree, by continuity of `*`-automorphisms and density of the union of local images.
- Derives `instSubsingletonQuasilocalLift` as an immediate corollary.
- Existence of the lift (uniform-continuity extension to the completion) is deferred.
Blueprint: aqft-in-lean
Repository: physicslib/physicslib4
Agent job: aea39373-6801-4dda-9604-8ab26bef73da
Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…*-homs Introduces `Physicslib4.Analysis.CStarDenseExtend`, a new file proving `exists_starAlgHom_extend_of_dense`: a uniformly continuous `StarAlgHom` on a dense `StarSubalgebra` of a C*-algebra extends to a `StarAlgHom` on the whole algebra. The proof uses the uniform-space extension machinery and recovers all algebraic structure (add, mul, smul, star, zero, one) by continuity and agreement on the dense subalgebra. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: aea39373-6801-4dda-9604-8ab26bef73da Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…ial net - Add `inclusion` field: a chosen family of StarAlgHom embeddings `𝔘(B₁) →⋆ₐ[ℂ] 𝔘(B₂)` for each basis-set inclusion `B₁ ⊆ B₂`. - Add `ι_inclusion` field enforcing coherence: `ι B₂ ∘ inclusion = ι B₁`, ensuring elements embed into the quasilocal algebra independently of the chosen basis set. - Provide the trivial instances (`StarAlgHom.id ℂ ℂ` / `rfl`) for `trivialQuasilocalAlgebra` so it compiles as a prerequisite for the intertwiner construction. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: aea39373-6801-4dda-9604-8ab26bef73da Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…pacetime - Introduce `MinkowskiDirected.lean` proving that any two Alexandrov-basis diamonds `I⁺(p₁)∩I⁻(q₁)` and `I⁺(p₂)∩I⁻(q₂)` are contained in a common diamond. - Key lemmas: cone transitivity (`minkowskiForwardCone_subset`, `minkowskiBackwardCone_subset`), existence of a common chronological predecessor/successor (`exists_common_past`, `exists_common_future`) via an explicit point on the time axis displaced by a radius derived from the spatial norms. - The main result `alexandrovBasis_directed` assembles these pieces and is needed for the directedness condition when lifting the covariance action to a quasilocal algebra. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: aea39373-6801-4dda-9604-8ab26bef73da Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…r intertw… - Introduce `IsAlexandrovBasisSet.directed` as a Haag-Kastler-level wrapper around `Spacetime.alexandrovBasis_directed`, confirming any two basis sets sit inside a common one. - Add `dense_adjoin_iUnion_range_ι` showing the `*`-subalgebra generated by the union of all local images is dense in the quasilocal algebra, supplying the domain needed for the dense-extension step of the intertwiner construction. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: aea39373-6801-4dda-9604-8ab26bef73da Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Define `localImages` as the union of all local algebra images over Alexandrov-basis sets, with a `mem_localImages` simp lemma. - Prove `exists_common_image`, which uses basis directedness and isotony coherence to find a common local algebra routing two elements. - Construct `localStarSubalgebra`, closing under all `StarSubalgebra` axioms; binary operations use `exists_common_image`, constants use a trivial basis set. - Add `dense_localStarSubalgebra` from the existing quasilocal density hypothesis. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: aea39373-6801-4dda-9604-8ab26bef73da Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…edness
- Introduce `IsCovariantQuasilocal` asserting that local embeddings intertwine the covariance action with isotony inclusions.
- Prove `ι_covEquiv_congr`: if two local representatives agree in the quasilocal algebra, their images under the covariance action agree, using directedness and `ι_injective`.
- Define `intertwiner` by choosing a local preimage and applying `covEquiv`, defaulting to 0 off local images.
- Prove `intertwiner_ι`: the defining equation `intertwiner N Q L (ι_B a) = ι_{L·B}(α_L a)` holds for any covariance-compatible net.
Blueprint: aqft-in-lean
Repository: physicslib/physicslib4
Agent job: aea39373-6801-4dda-9604-8ab26bef73da
Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
Using `exists_common_image`, establish that the intertwiner preserves addition, multiplication, zero, one, star, and scalar multiplication on `Q.localImages`. Each proof routes both operands through a common basis algebra `ι_C` and applies the corresponding `map_*` lemmas. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: cb6edf0b-bad0-45e7-94da-c1945db9b4f1 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
… a `StarAlgHom` Introduce `intertwinerHom`, a `StarAlgHom` from `Q.localStarSubalgebra` into `Q.carrier`, by packaging the previously proved `intertwiner_one/mul/zero/add/star/smul` lemmas into the algebraic structure fields. Also add a `@[simp]` unfolding lemma `intertwinerHom_apply`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: cb6edf0b-bad0-45e7-94da-c1945db9b4f1 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf The agent turn did not complete cleanly; this commit preserves the partial changes made before the error.
…l quasilo… - Prove `intertwiner_norm`: the intertwiner is norm-preserving on local images, using isometricity of the local embeddings and the covariant action. - Derive `intertwinerHom_isometry`: the bundled map on the local `*`-subalgebra is an isometry. - Use `exists_starAlgHom_extend_of_dense` to obtain `exists_intertwiner_extend`, producing a `*`-homomorphism on the full quasilocal algebra extending the local intertwiner. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 46c26caa-0499-4a69-add9-7560c84580f5 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
… also return continuity Add `Continuous F` to the existential conclusion so callers can use the continuity of the extended map directly. This is needed to assemble the `StarAlgEquiv` from the `L` and `L⁻¹` extensions when inhabiting `QuasilocalLift`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 46c26caa-0499-4a69-add9-7560c84580f5 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf The agent turn did not complete cleanly; this commit preserves the partial changes made before the error.
…IsCovaria… - Introduce `IsCovariant` (covariance for all `L`) and `extendHom`, the chosen continuous extension of the fiberwise intertwiner to all of `𝔘`. - Prove `extendHom_one` and `extendHom_comp`, then derive left/right inverse laws to assemble a `StarAlgEquiv` via `StarAlgEquiv.ofStarAlgHom`. - Define `quasilocalLift` and `nonempty_quasilocalLift`, completing the passage from local covariance data to a global `*`-automorphism inhabiting `QuasilocalLift`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 5476ba80-7d10-4f0a-9d3a-d89e7631be92 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…tional li… - Prove `isCovariant_trivial`: every local algebra is `ℂ` and every `ℂ`-star-algebra automorphism of `ℂ` is the identity, so the covariance compatibility condition holds trivially. - Define `trivialQuasilocalLift` and `nonempty_trivialQuasilocalLift` so the quasilocal lift can be constructed without the caller supplying an `IsCovariant` hypothesis. - Factor the anonymous `HaagKastlerNet` record into a named `trivialHaagKastlerNet` definition to make it reusable across both files. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 5476ba80-7d10-4f0a-9d3a-d89e7631be92 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Introduce covariant families of local states and their composition lemmas for both the Minkowski and curved-spacetime Haag-Kastler settings, linked to their Lean counterparts. - Add the quasilocal covariance automorphism definition, its uniqueness lemma, and existence theorems (including the trivial-net witness) to the Minkowski section. - Annotate all new entries with `\lean`, `\leanfile`, `\leanok`, and `\uses` tags to keep the dependency graph current. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 5476ba80-7d10-4f0a-9d3a-d89e7631be92 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…ition Bundle a Haag-Kastler net, a quasilocal algebra, and the covariance-compatibility proof into a single `CovariantQuasilocalAlgebra` structure. Add namespace lemmas `lift`, `action`, and `action_ι` so the Lorentz covariance automorphism `β_L` is directly accessible. Provide the trivial instance and nonemptiness theorem. Mirror the definition in the blueprint with full `\uses` dependencies, promoting the covariance hypothesis from a side condition to structural data. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 5476ba80-7d10-4f0a-9d3a-d89e7631be92 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Prove `action_one` and `action_mul` showing the covariance automorphism map satisfies `β₁ = id` and `β_{L'L} = β_{L'} ∘ β_L`, reducing to `extendHom_one` and `extendHom_comp`.
- Add pointwise variants `action_one_apply` and `action_mul_apply` as stepping stones, and `action_apply` connecting the action to `extendHom`.
- Record the result in the blueprint as lemma `lmm:quasilocal-action-coherence`.
Blueprint: aqft-in-lean
Repository: physicslib/physicslib4
Agent job: 5476ba80-7d10-4f0a-9d3a-d89e7631be92
Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Define `IsInvariantState` as the condition that a state ω is fixed by the dual covariance action: ω(β_L a) = ω(a) for all L and a. - Prove `IsInvariantState.inner_invariant`: for an invariant state the GNS sesquilinear form ω(a* b) is preserved under the action, using star and mul preservation of the algebra map. This is the key algebraic step toward unitarity of the implementing operators U(L) on the GNS Hilbert space. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 5476ba80-7d10-4f0a-9d3a-d89e7631be92 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…(Step 2) Proves `IsInvariantState.exists_gns_unitary`: for any Lorentz-invariant state ω, there exists a family of linear isometric equivalences `U L : H ≃ₗᵢ[ℂ] H` on the GNS Hilbert space satisfying `U L (π a Ω) = π (β_L a) Ω` and `U L Ω = Ω`. The unitaries are built via `LinearEquiv.extendOfIsometry` applied to the dense cyclic map `a ↦ π a Ω`, with isometricity following from `inner_invariant`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 5476ba80-7d10-4f0a-9d3a-d89e7631be92 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…theorem - Define Poincaré-invariant states on covariant quasilocal algebras as fixed points of the dual covariance action. - State the GNS unitary implementation theorem: invariance of ω guarantees a family of unitaries U(L) on the GNS space intertwining the representation and fixing the cyclic vector. - Both entries are marked `\leanok` and linked to their Lean sources in `QuasilocalIntertwiner.lean`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 5476ba80-7d10-4f0a-9d3a-d89e7631be92 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.