Added various standard AQFT theorems and definitions#21
Merged
Conversation
- Introduce `ExtremeState.lean` proving `IsPure ω ↔ ω.IsExtremePoint` via the Radon-Nikodym operator and Cauchy-Schwarz; includes `norm_eq_re_apply_one_of_positive`, `State.apply_one`, and the forward/backward directions of the equivalence. - Add corresponding blueprint entries for the norm identity, the extreme-point definition, and the pure ↔ extreme theorem with proof sketches for both directions. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 7dba6c6d-311a-4c4c-91b4-140cfc2bc2f7 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…bras - New `Purity.lean` registers two corollaries for each local algebra `𝔘(B)`: pure ↔ extreme point of the state space, and pure ↔ irreducible GNS representation, by applying the abstract `isPure_iff_isExtremePoint` and `isPure_iff_isIrreducible` lemmas. - Corresponding blueprint theorems (`thrm:pure-iff-extreme-in-curved-spacetime` and `thrm:pure-iff-irreducible-in-curved-spacetime`) added with `\leanok` and dependency tags, explaining that these are per-region statements due to the absence of a quasilocal algebra in curved spacetime. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 7dba6c6d-311a-4c4c-91b4-140cfc2bc2f7 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…al algebr… - New `Purity.lean` file specializes the abstract pure ⟺ extreme-point and pure ⟺ irreducible-GNS equivalences to the canonical quasilocal algebra `𝔘` of a Minkowski Haag-Kastler net, registering them as `pure_iff_extreme` and `exists_gns_pure_iff_irreducible`. - Blueprint adds matching `\leanok` theorems (`thrm:pure-iff-extreme-quasilocal`, `thrm:pure-iff-irreducible-quasilocal`) with dependency links to the abstract results and the GNS construction. - Root import list updated to include the new file. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 7dba6c6d-311a-4c4c-91b4-140cfc2bc2f7 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…acetime - Extend `exists_gns_unitary_of_invariant` and its specializations to also return `IsCyclicVector π Ω` as part of the conclusion tuple. - Prove `IsInvariantState.exists_gns_vacuum` (Minkowski) and `exists_gns_vacuum_stabilizer` (curved): a pure invariant state yields a GNS triple that is simultaneously covariant and irreducible, combining the existing unitary construction with `isPure_iff_isIrreducible`. - Add corresponding blueprint theorems with `\leanok` and dependency edges to the pure/irreducible and covariant-GNS results. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 7dba6c6d-311a-4c4c-91b4-140cfc2bc2f7 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…uum claim The previous names implied a full vacuum sector, but no spectrum condition is imposed and curved spacetime admits no global vacuum. Rename the Minkowski theorem to `exists_gns_irreducible_covariant` and the curved-spacetime theorem to `exists_gns_irreducible_covariant_stabilizer`, with matching blueprint labels and docstrings. Each docstring and theorem environment now explicitly notes that the spectrum condition (or its curved analogue, the Hadamard/microlocal spectrum condition) is a separate, unimposed ingredient needed to reach a genuine vacuum representation. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 7dba6c6d-311a-4c4c-91b4-140cfc2bc2f7 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…ializatio… - Introduce `State.precomp`, `isPure_precomp_of_isPure`, and `isPure_precomp_iff` in `GNS/ExtremeState.lean`: pulling back a state along a `*`-automorphism preserves purity in both directions, proved by transporting dominated functionals through `Φ` and `Φ⁻¹`. - Specialize to `isPure_precomp_action_iff` (Minkowski covariance automorphism `β_L`) and `isPure_precomp_stabAut_iff` (curved stabilizer automorphism `α̂_g`). - Add corresponding blueprint theorems in both the flat and curved sections, with `\leanok` tags and dependency edges. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 7dba6c6d-311a-4c4c-91b4-140cfc2bc2f7 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Define `gnsVonNeumann` as the bicommutant `π(A)''` of a representation. - Prove `center_gnsVonNeumann_eq_of_isIrreducible`: for an irreducible `π`, the center `π(A)'' ∩ (π(A)'')'` equals the scalar multiples of the identity, using triple-commutant collapse and Schur's lemma. - Prove `exists_gns_factor_of_isPure`: every pure state admits a cyclic GNS triple whose generated von Neumann algebra is a factor, combining the GNS construction with `isPure_iff_isIrreducible`. - Add corresponding blueprint theorems `thrm:irreducible-factor` and `thrm:pure-factor` with `\leanok` annotations. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 7dba6c6d-311a-4c4c-91b4-140cfc2bc2f7 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Add `vonNeumannOfSelfAdjoint` in `GNS/Irreducibility.lean`: proves the commutant of a self-adjoint set is `*`-closed, packages it as a `StarSubalgebra`, and uses `centralizer_centralizer_centralizer` to satisfy the `VonNeumannAlgebra` axiom. - Expose `localVonNeumannAlgebra` and `coe_localVonNeumannAlgebra` in both the flat (Minkowski) and curved Haag–Kastler files, so `R(B)` is a genuine bundled `VonNeumannAlgebra H` whose coercion to sets equals the existing `localVonNeumann` definition. - Add corresponding blueprint definitions for both spacetime settings, marked `leanok`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 7dba6c6d-311a-4c4c-91b4-140cfc2bc2f7 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…n both ne… - Add `localVonNeumannAlgebra_le_commutant` and `localVonNeumannAlgebra_mono` for both the Minkowski and curved-spacetime Haag–Kastler nets, reducing the bundled `≤` statements to the existing set-level results via `SetLike.coe_subset_coe`. - Document both theorems in the blueprint for Minkowski (§10.3) and curved spacetime (§10.4), noting that proofs reduce through the coercion `↑R(B) = π(𝔘(B))''`. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 7dba6c6d-311a-4c4c-91b4-140cfc2bc2f7 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.