Numerous AQFT additions#26
Merged
Merged
Conversation
Both `toAbstract` and `toAbstractIdentityComponent` bridges now expose `[TopologicalSpace M.Isom]` instances by forwarding the existing topology from the concrete isometry group and its oriented identity-component subgroup. A small `example` proof confirms both instances are found by `inferInstance`, so downstream covariance and KMS results requiring this typeclass are satisfied automatically over any concrete Lorentzian spacetime. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 13d47222-6d29-4e0b-a0b6-a4d13b47c7c1 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Introduce `IsInvariantState.exists_gns_unitaryRep` and its strongly-continuous variant by forwarding `C.actionHom` to `GNS.exists_gns_unitaryRep_of_invariant`. - Introduce `exists_gns_unitaryRep_stabilizer` and its strongly-continuous variant by forwarding `N.stabAutMonoidHom B` to the same core lemma, giving the stabilizer group a bundled `G →* (H ≃ₗᵢ[ℂ] H)` output. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 13d47222-6d29-4e0b-a0b6-a4d13b47c7c1 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…ubgroups Add a small `example` that checks `ContinuousSMul` holds by `inferInstance` for both `identityComponent` and `orientedIdentityComponent`, confirming these subgroups inherit continuous scalar multiplication from the ambient isometry group without extra work. This matters because they are the concrete symmetry groups fed to the curved Haag-Kastler axioms. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 13d47222-6d29-4e0b-a0b6-a4d13b47c7c1 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
This reverts commit fdf5ff1.
…s through… - Introduce `SmoothPath.tangent` as a named accessor for the `mfderivWithin … (1 : ℝ)` expression, with an unfolding lemma and a `tangent_ne_zero` convenience theorem. - Simplify all causal and orientation predicates (`IsTimelikeAt`, `IsTimelike`, `IsCausal`, `IsFutureOriented`, `IsPastOriented`) to reference `μ.tangent s` instead of the raw `mfderivWithin` term. - Update `pushforwardPath_tangent` in `IsometryCausality` to use the new accessor on both sides. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 1ab0fdd0-ada5-4707-a02b-e9ad9be80116 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…in rule - Add `val_smul_smul` showing the metric scales quadratically under `c • v`, then derive `isTimelike_smul_iff`, `isNull_smul_iff`, and `isSpacelike_smul_iff` for nonzero scalars, covering Gap 2's classification-invariance requirement. - Add `SmoothPath.mfderivWithin_comp_reparam` proving that the tangent vector of a reparametrised path equals the scalar derivative of the reparametrisation times the original tangent, via the manifold chain rule and `mfderivWithin_eq_fderivWithin`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 1ab0fdd0-ada5-4707-a02b-e9ad9be80116 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Introduce `SmoothPath.tangent_reparam_eq` to express the tangent vector of `μ₁` as a scalar multiple of `μ₂`'s tangent after reparametrisation `φ`, using the chain rule (`mfderivWithin_comp_reparam`) and `mfderivWithin_congr` to handle pointwise equality. - Use this to prove `SmoothPath.isTimelikeAt_reparam`: under a reparametrisation with nonzero derivative, `μ₁` is timelike at `s` iff `μ₂` is timelike at `φ s`, via `isTimelike_smul_iff`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 1ab0fdd0-ada5-4707-a02b-e9ad9be80116 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…sal paths - Prove `derivWithin_ne_zero_of_leftInverse`: differentiating a left-inverse identity via the chain rule shows the reparametrisation derivative is non-zero. - Add `mdifferentiableWithinAt_of_contDiffOn` to bridge `ContDiffOn ℝ ⊤` to `MDifferentiableWithinAt` via `contMDiffWithinAt`. - Prove `causalAt_reparam` (pointwise timelike-or-null invariance under scaling) and use it together with `isTimelikeAt_reparam` in the global `SmoothPathEquiv`-level theorems `isTimelike_iff_of_smoothPathEquiv` and `isCausal_iff_of_smoothPathEquiv`, with surjectivity handled through the inverse diffeomorphism `ψ`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 34fd85b2-00cc-4ef7-8827-ded52fd243a1 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…nder it - Introduce `OrientedSmoothPathEquiv`, extending `SmoothPathEquiv` with a positivity condition on `derivWithin φ`, to capture orientation-preserving reparametrisations. - Prove `isFuturePointing_smul_iff` and `isPastPointing_smul_iff` (positive-scaling invariance of time orientation) in `CausalStructure.lean`. - Use these to prove pointwise `isFuturePointing_reparam` / `isPastPointing_reparam` and the global `isFutureOriented_iff_of_orientedSmoothPathEquiv` / `isPastOriented_iff_of_orientedSmoothPathEquiv` in `Curves.lean`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 34fd85b2-00cc-4ef7-8827-ded52fd243a1 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…SmoothCur… - Add `eqvGen` iff lemmas for timelikeness, causality, future- and past-orientedness, threading invariance through the full equivalence closure of the respective path-equivalence relations. - Prove `isTimelikeSmoothCurve_ofPath_iff` and `isCausalSmoothCurve_ofPath_iff`, establishing that these predicates on `SmoothCurve` are independent of the chosen representative. - Introduce `OrientedSmoothCurve` (quotient by `OrientedSmoothPathEquiv`), `IsFutureOrientedCurve`, and `IsPastOrientedCurve`, with corresponding well-definedness iffs via `Quot.eqvGen_exact`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 34fd85b2-00cc-4ef7-8827-ded52fd243a1 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…ompatibil… - Define `OrientedSmoothCurve.toSmoothCurve` as the canonical forgetful map induced on the quotient, using the fact that `OrientedSmoothPathEquiv` refines `SmoothPathEquiv`. - Prove it is surjective and commutes with `ofPath` (simp lemma). - Show the timelike and causal predicates factor through the projection via `isTimelikeSmoothCurve_toSmoothCurve_ofPath` and `isCausalSmoothCurve_toSmoothCurve_ofPath`. - Derive that future- and past-oriented curves project to causal smooth curves. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 34fd85b2-00cc-4ef7-8827-ded52fd243a1 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…valence r… - Define `UnitaryEquiv π₁ π₂` as the existence of a `LinearIsometryEquiv` intertwining two `*`-representations, and prove reflexivity, symmetry, and transitivity. - Introduce `conjMulEquiv U : (H₁ →L H₁) ≃* (H₂ →L H₂)` (conjugation by a unitary) and show it carries `π₁(A)` onto `π₂(A)`, centralizers onto centralizers, and scalar operators onto scalar operators. - Derive that irreducibility (`IsIrreducible`) and factoriality (`IsFactor`) are unitary invariants, each in both one-directional and iff forms. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 004aacf7-1221-49f5-8ccb-3ae0981dfb22 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Introduce `Intertwines`, `AreDisjoint`, and `QuasiEquiv` for `*`-representations on Hilbert spaces, along with the algebra of intertwiners (zero, sum, scalar multiple, composition, adjoint). - Prove disjointness is symmetric and irreflexive, and that unitarily equivalent representations are never disjoint. - Build `conjStarAlgEquiv` (conjugation by a unitary as a `*`-algebra isomorphism) and show unitary equivalence implies quasi-equivalence; prove quasi-equivalence is an equivalence relation. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 004aacf7-1221-49f5-8ccb-3ae0981dfb22 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…s, and qu… - Define unitary equivalence of *-representations with the intertwining unitary condition - Add theorem that irreducibility and factoriality are preserved under unitary equivalence - Define disjoint representations via trivial intertwiner space and note symmetry properties - Define quasi-equivalence via *-isomorphism of generated von Neumann algebras, noting it is coarser than unitary equivalence Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 507f2b66-5bb1-4fe7-8afe-dd125a4c0c15 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
Introduce `Physicslib4.Operators.LpDiagonal`, defining a reusable `lpDiag` operator that acts coordinatewise on `lp E 2` from a uniformly bounded family `T i : E i →L[𝕜] E i`. The file proves the full suite of structural laws needed to assemble direct-sum *-representations: - `lpDiag_apply_coe` (coordinate action), `lpDiag_congr` (bound-independence) - `lpDiag_one`, `lpDiag_mul`, `lpDiag_add`, `lpDiag_smul` (unital ring + module structure) - `lpDiag_star` (adjoint of diagonal = diagonal of adjoints, requiring `CompleteSpace`) Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 507f2b66-5bb1-4fe7-8afe-dd125a4c0c15 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…sults Introduces `GNS.DirectSum`, a new file building `directSum π : A →⋆ₐ[ℂ] (lp H 2 →L[ℂ] lp H 2)` from a family of *-representations via the diagonal operator on the ℓ²-direct sum. Also proves `intertwines_single` (each summand embeds as a subrepresentation via the isometric inclusion) and `summandProj_mem_commutant` (the orthogonal projection onto each summand lies in the commutant, showing the direct sum is reducible whenever more than one summand is nonzero). Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 507f2b66-5bb1-4fe7-8afe-dd125a4c0c15 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Introduce `amplification` as the ι-fold direct sum `⊕_{i:ι} π` with the embedding intertwining lemma `amplification_intertwines_single`.
- Derive `summandProj_isScalar_of_isIrreducible` from `summandProj_mem_commutant` and irreducibility, then use it in `not_isIrreducible_directSum` to show any direct sum with two nonzero summands is reducible.
- Document the deferred quasi-equivalence `π ~ ι · π`, noting the missing amplification commutant theorem `(π ⊗ 1)' = π' ⊗ B(K)` as the obstruction.
Blueprint: aqft-in-lean
Repository: physicslib/physicslib4
Agent job: 507f2b66-5bb1-4fe7-8afe-dd125a4c0c15
Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…ibility - Define the direct-sum representation and amplification constructions, referencing the corresponding Lean declarations in `DirectSum.lean` and `Amplification.lean`. - State the subrepresentation/commutant theorem (`intertwines_single`, `summandProj_mem_commutant`) and the reducibility result (`not_isIrreducible_directSum`) as blueprint theorems with full `\uses` dependency chains. - Insert the new subsection before "Covariant States" to keep the superselection section logically ordered. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 507f2b66-5bb1-4fe7-8afe-dd125a4c0c15 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…heorems - Add theorem on reparametrisation-invariance of causal type (timelike/causal predicates are independent of path representative) - Add definition and theorem for oriented smooth curves (equivalence under orientation-preserving reparametrisations) - Add theorem on the forgetful projection from oriented curves to smooth curves, with factoring of causal predicates Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 507f2b66-5bb1-4fe7-8afe-dd125a4c0c15 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…represent… - Add `UnitaryEquiv.of_intertwines_of_isIrreducible`: a nonzero intertwiner between two irreducible representations yields a unitary equivalence, by showing `T⋆T` and `TT⋆` are positive scalars (via Schur), normalising `T` to a linear isometry, and proving surjectivity from the scalar identity for `TT⋆`. - Add `areDisjoint_or_unitaryEquiv_of_isIrreducible`: two irreducible representations are either disjoint or unitarily equivalent, as an immediate corollary. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 507f2b66-5bb1-4fe7-8afe-dd125a4c0c15 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…section Documents Schur's Lemma and the irreducible dichotomy as a blueprinted theorem, linking to the two Lean declarations `UnitaryEquiv.of_intertwines_of_isIrreducible` and `areDisjoint_or_unitaryEquiv_of_isIrreducible`. The entry explains the scalar argument for intertwiners between irreducible representations and records the corollary that irreducible representations are either disjoint or unitarily equivalent. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 9971521e-c8d9-49d5-813e-124738560153 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…cibles is… Proves `eq_smul_of_intertwines_of_isIrreducible`: given irreducible π₁, π₂ and intertwiners S ≠ 0, T, there exists λ : ℂ with T = λ • S. The argument uses Schur's lemma to write S*S = a·1, S*T = b·1, SS* = c·1, shows a ≠ 0 and c ≠ 0 (hence S* is injective), then deduces T − (b/a)·S = 0 from S*(T − (b/a)S) = 0. The corresponding blueprint lemma is added with `\leanok` and proof sketch. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 9971521e-c8d9-49d5-813e-124738560153 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…omy corol… - Prove `intertwines_self_iff_isScalar`: every self-intertwiner of an irreducible representation is a scalar multiple of the identity, via a new `intertwines_self_iff_mem_centralizer` bridge lemma. - Register `areDisjoint_or_unitaryEquiv_of_isIrreducible` in the curved-spacetime purity module, delegating to the abstract GNS result. - Add corresponding blueprint lemma and theorem nodes with `\leanok` tags and `\uses` dependencies in both the flat and curved sections. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 9971521e-c8d9-49d5-813e-124738560153 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…zation Proves that the GNS representations of two pure states are either disjoint or unitarily equivalent, by reducing to the irreducible-dichotomy result via the equivalence of purity and irreducibility of the GNS representation. Adds the corresponding blueprint theorem node with `\leanok` and appropriate `\uses` dependencies. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 9971521e-c8d9-49d5-813e-124738560153 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.