Many new standard AQFT constructs#19
Merged
Merged
Conversation
…heorem - Define `localOperators π B` as the image `π(𝔘(B))` inside `H →L[ℂ] H`. - Define `localVonNeumann π B` as the bicommutant `π(𝔘(B))''` via `Set.centralizer`. - Prove `localVonNeumann_subset_centralizer`: for completely spacelike-separated basis regions B₁, B₂, the von Neumann algebras satisfy R(B₁) ⊆ R(B₂)′, by lifting `einstein_causality` through the triple-centralizer identity. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 0a8f6e89-d8cb-4813-aa8c-645a7fdeb219 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…or curved… - Introduce `localOperators` (image π(𝔘(B'))) and `localVonNeumann` (bicommutant R(B') = π(𝔘(B'))'') for curved Haag–Kastler nets, mirroring the existing Minkowski construction. - Prove `localVonNeumann_subset_centralizer`: for completely spacelike-separated basis regions B₁, B₂ ⊆ B, R(B₁) ⊆ R(B₂)', lifting curved Einstein causality to the von Neumann level via `Set.centralizer_centralizer_centralizer`. - Fix a `show` → `change` tactic in the Minkowski counterpart to handle the goal rewrite correctly. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 03318cb2-1ba7-4e72-a53f-785455f3bde1 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…mann resu… - Prove `localVonNeumann_mono` in both the flat (Minkowski) and curved spacetime settings: for nested basis regions B₁ ⊆ B₂, the double commutant satisfies R(B₁) ⊆ R(B₂), using monotonicity of the centralizer operation. - In the curved case, coherence of the Axiom 3 isotony witnesses (B₁↪B factors through B₂) is taken as an explicit hypothesis, reflecting that the curved net has no canonical composition law. - Add corresponding blueprint definitions and theorems for local von Neumann algebras, von Neumann-level microcausality, and isotony in both the flat and curved sections, with full `\lean`/`\leanfile`/`\leanok`/`\uses` annotations. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 03318cb2-1ba7-4e72-a53f-785455f3bde1 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
…layer - Introduce `IsIrreducible` (von Neumann commutant definition), the topological Schur lemma `eq_smul_one_of_commute_of_cyclic` (off-diagonal coefficients vanish by density of the cyclic orbit), and `isScalar_iff_coeff_proportional` as the precise bridge between commutant scalars and proportionality of the GNS diagonal coefficient to the state. - Add `IsPure` as the order-theoretic (dominated-functional) definition of a pure state, avoiding convex-combination bookkeeping; the blueprint notes the remaining GNS Radon-Nikodym step needed to close the full equivalence. - Mirror all four items in the blueprint with `\lean`/`\leanok` tags and a prose explanation of the proof strategy. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 03318cb2-1ba7-4e72-a53f-785455f3bde1 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Add `isIrreducible_of_isPure` and the supporting lemma `scalar_of_isSelfAdjoint_of_isPure`: a self-adjoint commutant element is scaled into a positive operator `T` with `0 ≤ T ≤ 1`; its coefficient functional is positive and dominated by `ω`; purity forces proportionality to `ω`; Schur's lemma (`eq_smul_one_of_commute_of_cyclic`) then makes `T` (and `S`) a scalar. The general case reduces to the self-adjoint case by decomposing any commuting operator into its `*`-symmetric real and imaginary parts. - Add `coeffFunctional` (continuous linear functional `a ↦ ⟪Ω, T(πa Ω)⟫`) and auxiliary lemmas for its evaluation on `star a * a` and for positivity of diagonal inner products against positive operators. - Update the blueprint with a `Pure Implies Irreducible` theorem node (`\leanok`), noting that the converse requires the full GNS Radon–Nikodym surjectivity and is left for future work. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 03318cb2-1ba7-4e72-a53f-785455f3bde1 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf
- Introduce `RadonNikodym.lean` with the bounded-form estimate `gns_form_norm_le` (Cauchy-Schwarz + domination + reproducing identity), well-definedness on GNS vectors, and the Riesz-based construction of the commutant operator `rnOp` with its reproducing identity and commutativity. - Use `rnOp` to prove `isPure_of_isIrreducible`: the Radon-Nikodym operator lies in the commutant, is therefore scalar by irreducibility, and the reproducing identity makes every dominated functional proportional to `ω`. - Combine with the existing `isIrreducible_of_isPure` to close `isPure_iff_isIrreducible`, the full biconditional. - Add corresponding blueprint theorems (`thrm:gns-form-bound`, `thrm:gns-radon-nikodym-operator`, `thrm:pure-iff-irreducible`) with `\leanok` tags and dependency edges. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 03318cb2-1ba7-4e72-a53f-785455f3bde1 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.