Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized
Dark green border: this is in Mathlib

Definition 141The Involution on a Completion

Let $A$ be as in 140. Define the involution on $\widehat{A}$ by

\begin{align} \star _{\widehat{A}} := \texttt{UniformSpace.Completion.map } \star _{A}. \end{align}

This is legitimate because $\star _A$ is an isometry — which is not assumed but obtained from the C*-inequality on $A$ via CStarRing.to_normedStarGroup — hence uniformly continuous by Isometry.uniformContinuous, and UniformSpace.Completion.map lifts any uniformly continuous map to the completions. It is uniformly continuous, satisfies $\eta (a)^{*} = \eta (a^{*})$ by UniformSpace.Completion.map_coe, and is the unique continuous map with that property by UniformSpace.Completion.map_unique.

Why this is by hand, and only here. For the completion the involution really does have to be written down, and Mathlib supplies nothing to start from. An audit against the local Mathlib clone found zero occurrences of Star, InvolutiveStar or StarRing on UniformSpace.Completion: the files checked were Topology/Algebra/UniformRing.lean, Topology/UniformSpace/Completion.lean, Topology/Algebra/GroupCompletion.lean, Analysis/Normed/Group/Completion.lean and all of Algebra/Star/. The ring and norm structure, by contrast, is free: the instance is UniformSpace.Completion.instNormedRing, an auto-generated but perfectly citable name for the anonymous instance [SeminormedRing A] : NormedRing (Completion A) of Analysis/Normed/Module/Completion.lean:75. Note its hypothesis: SeminormedRing, with no commutativity. That is worth holding next to the trap recorded in 145, where the analogous NormedAlgebra instance in the same file is commutativity-gated and therefore does not fire. So the involution and its axioms are the whole of what this node and 142 have to build. This is in contrast to the colimit, where Mathlib’s DirectLimit does supply Star and StarRing instances — recorded at the start of this subsection — and nothing has to be built at all.

The right tool, and the wrong one. The tool to use is UniformSpace.Completion.map, characterised on the canonical image by UniformSpace.Completion.map_coe as above. What must not be used is UniformSpace.Completion.mapRingHom, even though it looks like the natural fit: it transports a ring homomorphism to the completions, and $\star $ is anti-multiplicative, not multiplicative, so it is not a ring homomorphism $A \to A$ and does not typecheck as input. If a bundled-morphism formulation is wanted anyway, the opposite-algebra dodge is available — read $\star $ as a ring homomorphism $A \to A^{\mathrm{op}}$ — and it is supported, since MulOpposite carries a CStarAlgebra instance (MulOpposite.instCStarAlgebra). That is an optional convenience, not a requirement: the unbundled map route above suffices.

Why the continuity side goals are free, recorded once for the whole block. UniformSpace.Completion.uniformContinuous_map, UniformContinuous (Completion.map f), is unconditional — it needs no hypothesis on $f$ whatsoever, not even uniform continuity — and it is tagged @[fun_prop], as is its corollary UniformSpace.Completion.continuous_map (both in Topology/UniformSpace/Completion.lean, lines 480–486). Consequently every continuity side goal raised by an isClosed_eq or isClosed_le in this subsection — and each of 142 and 144 raises at least one — is discharged by fun_prop in a single line. This is the fact that makes the four-lines-per-obligation estimate quoted throughout this block real rather than optimistic; Mathlib’s own norm_mul_le field for the completion is written in exactly that style and is four lines long.

LaTeX

Definition 132Axiom 2: Isotony

Let $\mathbf{B}_1$ and $\mathbf{B}_2$ be any two basis elements of the Alexandrov topology on Minkowski spacetime, i.e. any two sets of the form $I^+(p_1) \cap I^-(q_1)$ and $I^+(p_2) \cap I^-(q_2)$.

The axiom supplies, as data, a family of unital $*$-monomorphisms

\begin{align} i_{\mathbf{B}_1\mathbf{B}_2} : \mathfrak {U}(\mathbf{B}_1) \hookrightarrow \mathfrak {U}(\mathbf{B}_2), \end{align}

one for every pair of basis sets with $\mathbf{B}_1 \subseteq \mathbf{B}_2$, subject to three conditions:

injectivity: each $i_{\mathbf{B}_1\mathbf{B}_2}$ is injective;
identity: $i_{\mathbf{B}\mathbf{B}} = \mathrm{id}_{\mathfrak {U}(\mathbf{B})}$ for every basis set $\mathbf{B}$;
composition: $i_{\mathbf{B}_2\mathbf{B}_3} \circ i_{\mathbf{B}_1\mathbf{B}_2} = i_{\mathbf{B}_1\mathbf{B}_3}$ whenever $\mathbf{B}_1 \subseteq \mathbf{B}_2 \subseteq \mathbf{B}_3$.

Conditions (b) and (c) say exactly that $\mathbf{B} \mapsto \mathfrak {U}(\mathbf{B})$ is a functor on the inclusion order of basis sets, with the $i_{\mathbf{B}_1\mathbf{B}_2}$ as its action on morphisms.

Two points about the shape of this axiom. First, the family must be chosen data and not an existence statement: (b) and (c) are equations between the maps themselves, so there is nothing to state unless the maps are fixed. An axiom of the form “for each inclusion there exists some monomorphism” cannot express functoriality at all.

Second, the hypothesis is the non-strict inclusion $\mathbf{B}_1 \subseteq \mathbf{B}_2$, matching the formalisation, which quantifies over B$_1$ $\subseteq $ B$_2$. Earlier versions of this statement wrote $\subset $; that was a divergence from the Lean, and the non-strict form is the correct one. It also matters mathematically: the reflexive case $\mathbf{B}_1 = \mathbf{B}_2$ is what makes (b) expressible, and the strict reading would leave the diagonal of the inclusion order outside the axiom altogether.

Conditions (b) and (c) are required rather than derived because they are properties of the net’s chosen embeddings, not of the spacetime: no geometric fact about Alexandrov diamonds constrains which monomorphism a net picks for a given inclusion, so coherence cannot be discharged after the fact and must be part of the axiom. Their payoff is that the assignment becomes a genuine directed system, which is what gives 148 its algebra structure, and that consumers no longer have to carry coherence as a side hypothesis.

LaTeX Lean

Definition 320Equivalence of Haag-Kastler Nets

Let $M_1$ and $M_2$ be Lorentzian spacetimes (78) and let $e : M_1.\mathrm{Carrier} \simeq M_2.\mathrm{Carrier}$ be a bijection of their carriers which maps basis sets to basis sets: $M_2.\mathrm{IsBasisSet}\, (e(\mathbf{B}))$ holds whenever $M_1.\mathrm{IsBasisSet}\, \mathbf{B}$ does. Let $\mathfrak {U}_1$ and $\mathfrak {U}_2$ be Haag-Kastler nets (277) over $M_1$ and $M_2$ respectively. An equivalence of nets along $e$ is a chosen family of unital $*$-isomorphisms

\begin{align} \Theta _{\mathbf{B}} : \mathfrak {U}_1(\mathbf{B}) \longrightarrow \mathfrak {U}_2(e(\mathbf{B})), \end{align}

one for each basis set $\mathbf{B}$ of $M_1$ — well-typed precisely because of the basis-set hypothesis on $e$ — such that for all basis sets $\mathbf{B}_1 \subseteq \mathbf{B}_2$ of $M_1$ the diagram

$\begin{tikzcd} \mathfrak{U}_1(\mathbf{B}_2) \arrow[r, "\Theta_{\mathbf{B}_2}"] & \mathfrak{U}_2(e(\mathbf{B}_2)) \\ \mathfrak{U}_1(\mathbf{B}_1) \arrow[r, "\Theta_{\mathbf{B}_1}"] \arrow[u, "\iota_1"] & \mathfrak{U}_2(e(\mathbf{B}_1)) \arrow[u, "\iota_2"] \end{tikzcd}$

commutes, where $\iota _1$ and $\iota _2$ are the canonical isotony embeddings $\mathtt{commIsotony}$ of the two nets.

Three points on the encoding.

The carriers are related by data, not by an equality. A Lorentzian spacetime (78) carries its point set as a field, so “two spacetimes on a common carrier” would be an assertion of type equality between $M_1.\mathrm{Carrier}$ and $M_2.\mathrm{Carrier}$. That is not a usable hypothesis: it cannot be transported along, and it forces the regions, basis-set predicates and algebras of the two nets to be compared across a type cast. Supplying a bijection $e$ instead makes every comparison take place at a definite type, and it is exactly what the geometric case provides, the relabelling diffeomorphism being a bijection of the carrier with itself.

Only the basis-set condition on $e$ is needed here. The definition mentions neither metrics nor isometries. All it requires of $e$ is that it carry basis sets to basis sets, which is what makes $\Theta _{\mathbf{B}}$ typecheck. The geometric input — that a cross-metric isometry satisfying the two-sided orientation hypothesis does carry basis sets to basis sets — is supplied at the point of use, in 321.

$\Theta $ must be data, and the $\iota _i$ come for free. The family $\Theta $ has to be data rather than a bare existence statement, since the commuting square refers to the chosen maps. The vertical arrows must likewise be chosen embeddings and not mere existence witnesses — but no extra hypothesis is needed to obtain them: Axiom 2 (272) supplies the isotony family as chosen data, together with its injectivity, for every inclusion of basis sets, and we adopt that convention rather than have the equivalence carry a supplied family of embeddings in the style of Axiom 5 (276).

Note also that naturality needs no composition or compatibility hypothesis: it is one square attached to a single inclusion $\mathbf{B}_1 \subseteq \mathbf{B}_2$ and never composes two embeddings. That observation still stands, but its justification has changed. It previously mattered because the embeddings were witnesses chosen inside Axiom 3, which carried no composition law, so coherence had to be assumed wherever a three-fold inclusion was factored — as in 282. Axiom 2 now carries the identity and composition laws itself, so that coherence holds for every net and nothing has to be assumed anywhere; the point here is simply that this square would not have needed it in any case.

LaTeX Lean

Definition 148Quasilocal Algebra

Consider the union of all $\mathfrak {U}(\mathbf{B})$, taken along the isotony family of Axiom 2 (132). This union is a normed *-algebra; taking its completion one obtains a C*-algebra denoted $\mathfrak {U}$, called the quasilocal algebra.

The union is to be read as a directed colimit, not as a set-theoretic union. This is what Axiom 2’s identity and composition laws buy: with $\mathbf{B} \mapsto \mathfrak {U}(\mathbf{B})$ a functor on the inclusion order, and the Alexandrov diamonds upward directed, the local algebras form a directed system and the colimit carries a well-defined $*$-algebra structure — the product of $a_1 \in \mathfrak {U}(\mathbf{B}_1)$ and $a_2 \in \mathfrak {U}(\mathbf{B}_2)$ is computed in any $\mathfrak {U}(\mathbf{B})$ containing both, and functoriality is exactly what makes the answer independent of that choice. Without the two laws there is no such structure: a bare set-theoretic union of the $\mathfrak {U}(\mathbf{B})$ has no multiplication at all, since elements of different local algebras live in unrelated carriers.

The three supporting results this definition rests on are now declarations of this blueprint rather than appeals to the informal discussion of Chapters 6.1 and 6.2: (i) upward directedness of the Alexandrov diamonds (88), which supplies the containing diamond $\mathbf{B}$ in the description above; (ii) that the colimit of the directed system is a normed $*$-algebra (138); and (iii) that its completion is a C*-algebra (147). All three are formalized. What would pin $\mathfrak {U}$ down up to isomorphism rather than merely produce it is uniqueness of the complete C*-norm; that is discussed as prose in the passage following 147 and is deliberately not claimed by any declaration here, for the reasons given there.

The colimit-and-completion construction of $\mathfrak {U}$ is therefore formalized, while the Lean structure continues to take $\mathfrak {U}$ as given — an ambient C*-algebra together with the canonical embeddings $\iota _{\mathbf{B}}$ and their cocone condition, as recorded in 149. There is no longer any discrepancy between this blueprint’s formalization markings and the Lean, and the construction and the structure are now connected: that connection is made by 152, which produces a quasilocal algebra for the net out of the colimit-and-completion construction, and it is from that theorem that a Haag–Kastler net (160) obtains its canonical $\mathfrak {U}$. See the formalization note following 147 on the two available construction routes.

LaTeX Lean

Definition 151Axiom 4: Quasilocal Completeness

All “observables” are quasilocal observables.

What the quotation marks mean. The quotation marks around “observable” are doing real work and are better explained than left implicit. An “observable” is here a physical primitive: a quantity a physicist can actually measure in the world, an equivalence class of measurement procedures that agree on all outcomes. It is not defined anywhere in this blueprint, and it cannot be, because nothing in the formalism fixes what happens in a laboratory. A quasilocal observable, by contrast, is a mathematical object: by 150 it is an operator $\pi _\omega (a)$ with $a$ a self-adjoint element of the quasilocal algebra $\mathfrak {U}$.

The assertion. This axiom is a bridge principle — the one point in the axiom list at which physical reality is joined to the mathematical formalism. What it asserts is a correspondence between the two sides just distinguished: every physical observable corresponds to a quasilocal observable in the sense of 150.

The direction is the content. The assertion is a one-way inclusion, and which way it runs is precisely what the name “Completeness” records: the formalism is not too small. Nothing a physicist can measure lies outside the quasilocal observables; there is no measurable quantity that the net of local algebras, its quasilocal algebra and their representations fail to account for. The converse — that every quasilocal observable is physically realisable, i.e. that every self-adjoint $\pi _\omega (a)$ is measured by some actual procedure — is a separate and strictly stronger assertion, and it is not asserted here. It is flagged instead as an open modelling question: whether the formalism is also not too large is not settled by this axiom, and the axioms as stated are consistent with $\mathfrak {U}$ containing self-adjoint elements answering to no measurement at all.

This is an interpretive postulate, not a mathematical condition. Axioms 1, 2, 3 and 5 (131, 132, 149, 159) are mathematical conditions on a net: each says something checkable about the assignment $\mathbf{B} \mapsto \mathfrak {U}(\mathbf{B})$ and its structure maps. This axiom is of a different kind. One of its two sides is not a mathematical object, so the statement relates the formalism to the world rather than constraining the formalism internally, and it is therefore not the sort of statement that can be proved or disproved inside the formalism. Consequently it should have no mathematical consumers: a theorem that appears to need Axiom 4 in fact needs the mathematics it was previously conflated with, namely the existence of the quasilocal algebra (152), not the physical correspondence. What keeps the correspondence tenable in the presence of the larger bicommutants of 162 is 158.

Formalization note. This node previously carried Physicslib4.AQFT.HaagKastler.QuasilocalCompleteness. That was withdrawn, because that Lean definition is a mathematical existence claim about the net — an attempt at 152 — and says nothing whatever about physical observables or their correspondence to quasilocal ones. A faithful encoding of this node now exists, as Physicslib4.AQFT.HaagKastler.ObservableCorrespondence. It takes the physical observables as an abstract primitive, exactly as Axiom 1 (131) takes the assignment algebra as abstract data rather than constructing it, and has three fields: Observable, the type of physical observables, uninterpreted; measure, assigning to each physical observable the element of the quasilocal algebra $\mathfrak {U}$ that answers it; and isSelfAdjoint_measure, the axiom itself, that every value of measure is self-adjoint. Nothing is thereby proved about the world, which is as it should be for a bridge principle.

The encoding is representation-independent, deliberately. The correspondence lands in the self-adjoint part of $\mathfrak {U}$ and not in the operators of a fixed GNS representation. Read literally through 150, whose quasilocal observables are operators $\pi _\omega (a)$, the axiom would make its own truth depend on which state $\omega $ was chosen, which is unacceptable for a physical primitive. Landing in the algebra removes that dependence, and being a quasilocal observable in every representation is then a theorem rather than an axiom schema indexed by a choice of state: for any $*$-representation $\pi $ of $\mathfrak {U}$, the operator $\pi (\texttt{measure}\, o)$ is a quasilocal observable in the sense of 150, which is isQuasilocalObservable_measure.

What the encoding does not assert. Only the one-way inclusion is asserted, consistently with the paragraph above declining the converse as separate and strictly stronger: measure is a bare map and is deliberately not strengthened to an equivalence. Consequently the structure is cheaply inhabited — ObservableCorrespondence.maximal exhibits one instance, taking the self-adjoint elements of $\mathfrak {U}$ as the observables and the inclusion as measure — and that is correct behaviour for a bridge principle rather than a defect of the encoding, since it is not a surjectivity claim and no such claim is intended. In the same spirit this node should have no mathematical consumers, and that is why 160 does not bundle it: what appeared to need Axiom 4 needed 152 instead.

LaTeX Lean

Definition 19Spacetime

A spacetime is a real, four-dimensional, connected, smooth, Hausdorff manifold $M$ with a globally defined smooth tensor field $g$ of type $(0,2)$ which is non-degenerate and “Lorentzian”. By Lorentzian we mean that for any $p \in M$ there is a basis of the tangent space $TM|_p$ to $M$ at $p$ relative to which $g|_p$ is zero in its non-diagonal entries and on the diagonal takes the form $\text{diag}(-1,1,1,1)$.

The smoothness clause, precisely. The metric field is a family of continuous bilinear forms $g_x : TM|_x \to _L[\mathbb {R}] TM|_x \to _L[\mathbb {R}] \mathbb {R}$, and “smooth” is the field contMDiff, which asserts that $g$ is a $C^\infty $ section of the bundle of continuous bilinear forms on the tangent bundle — the regularity index being $\infty $, on which see the remark on the index below. Writing $E$ for the model space and $I$ for the model with corners of $M$, it reads

\begin{align} \mathtt{ContMDiff}\; I\; \Big(I.\mathtt{prod}\; \mathcal{I}\big(\mathbb {R},\, E \to _L[\mathbb {R}] E \to _L[\mathbb {R}] \mathbb {R}\big)\Big)\; \infty \; \Big(x \mapsto \mathtt{Bundle.TotalSpace.mk'}\; \big(E \to _L[\mathbb {R}] E \to _L[\mathbb {R}] \mathbb {R}\big)\; x\; (g_x)\Big), \end{align}

the fibre over $x$ being $TM|_x \to _L[\mathbb {R}] TM|_x \to _L[\mathbb {R}] \mathbb {R}$ and the index being $\infty $.

The index. Mathlib’s $\mathtt{ContMDiff}$ takes its regularity index $n$ in $\mathbb {N}_{\infty \omega } = \mathtt{WithTop}\; \mathbb {N}_\infty $, in which $\top = \omega $ means real-analytic and $\infty = ((\top : \mathbb {N}_\infty ) : \mathtt{WithTop}\; \mathbb {N}_\infty )$ is strictly smaller. The index to ask for is therefore $\infty $, not $\top $: it is $\infty $ that means $C^\infty $, while $\top $ would demand the strictly stronger condition of analyticity. The Lean definition uses $\infty $, so the field agrees exactly with the informal word “smooth” in the statement above.

Three further points about this formulation.

It is Mathlib’s idiom. The clause is deliberately the shape of the contMDiff field of Mathlib’s Bundle.ContMDiffRiemannianMetric, whose own field is

\begin{align} \mathtt{ContMDiff}\; I_B\; \big(I_B.\mathtt{prod}\; \mathcal{I}(\mathbb {R}, F \to _L[\mathbb {R}] F \to _L[\mathbb {R}] \mathbb {R})\big)\; n\; \big(b \mapsto \mathtt{TotalSpace.mk'}\; (F \to _L[\mathbb {R}] F \to _L[\mathbb {R}] \mathbb {R})\; b\; (\mathtt{inner}\; b)\big), \end{align}

read with $\mathtt{inner}$ replaced by $g$. Matching it verbatim is what makes the whole bundle-section API of Mathlib/Geometry/Manifold/VectorBundle/ apply to $g$ without translation.

The Riemannian class itself is deliberately not instantiated. Mathlib has no pseudo-Riemannian class, and Bundle.ContMDiffRiemannianMetric carries two further fields beyond contMDiff that a Lorentzian form cannot satisfy: pos, which demands $0 {\lt} g_x(v,v)$ for $v \neq 0$ and is contradicted by any timelike vector, and isVonNBounded, which demands that $\{ v \in TM|_x \mid g_x(v,v) {\lt} 1\} $ be von Neumann bounded. The latter is not merely unproven but outright false here: that set contains the entire light cone at $x$, since $g_x(v,v) = 0 \le 0 {\lt} 1$ for every null $v$, and the light cone is unbounded (it is closed under positive scaling). So only the shape of the one field contMDiff is reused; the class is never instantiated and no instance of it may be sought.

The payoff. From a section-level contMDiff one gets, by ContMDiff.clm_bundle_apply$_2$, that for any vector fields $V, W$ that are themselves $C^\infty $ sections of the tangent bundle the scalar function

\begin{align} x \longmapsto g_x\big(V_x,\, W_x\big) \end{align}

is $C^\infty $ on $M$. One identification step is needed to say it in quite that form: clm_bundle_apply$_2$ concludes with a section, of the trivial $\mathbb {R}$-bundle over $M$, so its output is a $\mathtt{Bundle.TotalSpace.mk'}$ term and reaching the plain scalar statement $\mathtt{ContMDiff}\; I\; \mathcal{I}(\mathbb {R},\mathbb {R})\; \infty \; \big(x \mapsto g_x(V_x, W_x)\big)$ means identifying that trivial-bundle section with the function itself. This is exactly what causal and geodesic arguments need — causal type along a curve, the sign of $g(t,\dot\mu )$, and every variational computation are statements about such scalars — and a chart-local formulation quantifying over constant model vectors had no route to it at all, since $V_x$ and $W_x$ vary with the point.

LaTeX Lean

Theorem 152Existence of a Quasilocal Algebra

Every local net (131) satisfying Axiom 2 (132) admits a quasilocal algebra: there exist a C*-algebra $\mathfrak {U}$ and a family of unital $*$-homomorphisms $\iota _{\mathbf{B}} : \mathfrak {U}(\mathbf{B}) \to \mathfrak {U}$, indexed by the Alexandrov-basis sets, such that each $\iota _{\mathbf{B}}$ is injective, the family satisfies the cocone condition $\iota _{\mathbf{B}_2} \circ i_{\mathbf{B}_1 \mathbf{B}_2} = \iota _{\mathbf{B}_1}$ for $\mathbf{B}_1 \subseteq \mathbf{B}_2$, and the union of the images of the $\iota _{\mathbf{B}}$ is dense in $\mathfrak {U}$.

The indexing is essential to the statement and is not a stylistic choice: the family runs over the Alexandrov-basis sets only. Axiom 1 (131) assigns an abstract unital C*-algebra to every subset of spacetime, constrained only at $\emptyset $, so the algebras attached to non-basis subsets are junk fibres about which the axioms say nothing whatever; no claim is made about them here, and none can be.

It is a theorem, not an axiom. Nothing needs to be assumed here: this existence claim is what the colimit-then-completion chain of this subsection establishes, running from 133 through 147. It is stated as its own node because it is the mathematical content that was previously bundled into Axiom 4 (151) and is what the consumers of that axiom actually needed.

Why this node once pointed at no Lean declaration. It now does, and the history of how it came to is kept here because it is the reason the repairs behind that tag were needed. An earlier version of this node claimed that the statement above is exactly what Physicslib4.AQFT.HaagKastler.QuasilocalCompleteness, namely Nonempty (QuasilocalAlgebra U i), asserts, and withdrew the lean and leanfile tags on the ground that the existing Lean stated something else and that something was false. Two independent mismatches in QuasilocalAlgebra.lean were diagnosed here, and both have since been repaired; a third pin, diagnosed nowhere in this blueprint, was found and repaired in the same work. What was wrong and what was done about it are recorded in turn below; none of it is a live obstacle any longer.

The embedding family, fixed as prescribed. The first mismatch was that the family was indexed over all subsets. The field read $\iota $ : $\forall $ B : Set StandardMinkowskiSpacetime.Carrier, StarAlgHom $\mathbb {C}$ (U.algebra B) carrier — total over every subset of spacetime — whereas $\iota $_injective and $\iota $_inclusion were restricted to the Alexandrov-basis sets. Since LocalNet.algebra is likewise total, the structure demanded a unital $*$-homomorphism out of every junk fibre, which the statement above pointedly does not. The field now takes a strict-implicit region argument together with an IsAlexandrovBasisSet hypothesis before returning StarAlgHom $\mathbb {C}$ (U.algebra B) carrier — the binder shape that $\iota $_injective and $\iota $_inclusion already used — so all three fields agree on their domain, exactly as this node prescribed.

That over-generality was not harmless: it made the Prop refutable, and the following net is why the restriction was necessary. Take $\mathfrak {U}(\mathbf{B}) = \mathbb {C}$ for every Alexandrov-basis set and for $\emptyset $, with all transition maps the identity, so that Axiom 2(a), (b) and (c) hold; and put $\mathfrak {U}(\mathbf{B}_0) = M_2(\mathbb {C})$ for a single non-basis subset $\mathbf{B}_0$, say a singleton, which is not of the form $I^+(p) \cap I^-(q)$. For any candidate structure, each $\iota _{\mathbf{B}}$ on a basis set is a $\mathbb {C}$-algebra homomorphism out of $\mathbb {C}$, so its range is $\mathbb {C}\cdot 1$; the density clause then forces the carrier to be $\overline{\mathbb {C}\cdot 1} = \mathbb {C}\cdot 1$, while injectivity on basis sets forces it to be nontrivial, so the carrier is $\mathbb {C}$. But $\iota _{\mathbf{B}_0} : M_2(\mathbb {C}) \to \mathbb {C}$ is unital and $M_2(\mathbb {C})$ is simple, so its kernel is $0$ and it is injective — giving $4 \le 1$, a contradiction. Hence Nonempty (QuasilocalAlgebra U i) was false for that net. With $\iota $ now restricted to the basis sets, no embedding of $\mathfrak {U}(\mathbf{B}_0)$ is demanded of a candidate structure and the refutation no longer applies; the net is kept on record because it is the reason the restriction was needed, not because it refutes the present Lean.

The carrier universe, fixed — but not by the means this node prescribed. The second mismatch was that the carrier was pinned to Type 0. The field read carrier : Type, while LocalNet.algebra : Set $\_ $ $\rightarrow $ Type* is universe polymorphic, so for a net whose local algebras genuinely live in Type 1 no Type 0 carrier could hold injective copies of them and the existence claim failed for size reasons alone. What this node prescribed was carrier : Type*, a free universe, and that prescription does not work: a free carrier universe is constrained by no field of the structure, so it cannot be inferred, and LocalCommutativity fails to elaborate with “failed to infer universe levels”. The only escape would be to give Axioms 3 and 4 an explicit universe parameter, which would make the content of those axioms depend on that index — a family of Props rather than a Prop. What was done instead is to tie the carrier to the net’s universe: the structure now reads QuasilocalAlgebra (U : LocalNet.{u}) with carrier : Type u. That costs no generality, because the density clause forces $\mathfrak {U}$ to be the closure of the union of the images of the local algebras, so any quasilocal algebra already lives in the universe of those algebras, and a free universe could only add copies of the same algebra higher up.

A third pin, one level up. Fixing the carrier alone would not have lifted the size restriction, and this was found while making the change just described. HaagKastlerNet carried no universe parameter at all, so it pinned the universe of LocalNet outright, and CovariantQuasilocalAlgebra inherited that pin through its net field; repairing only the carrier would therefore have left the very same size restriction one level up, with every net in the development confined to a single fixed universe. Both structures now carry the net’s universe. One consequence is that the two satisfiability witnesses, nonempty_haagKastlerNet and nonempty_covariantQuasilocalAlgebra, are now stated explicitly at universe 0, since they are built from $\mathbb {C}$; consistency of the axioms needs only one model, so nothing is lost. No pin remains in the construction itself: QuasilocalColimit and QuasilocalCompletion are declared over LocalNet.{u} with result type Type u, so the colimit-and-completion development — colimitNorm, colimitRingNorm, colimitNormedAlgebra, colimitCStarRing and quasilocalCompletionCStarAlgebra, that is, the $\mathfrak {U}$ that 147 supplies — is available at every universe.

The node is now formalized, as Physicslib4.AQFT.HaagKastler.exists_quasilocalAlgebra, the assembly together with all six supporting results — 143 above and the five embedding lemmas stated immediately below this node, 153, 154, 155, 156 and 157 — having been completed.

One consequence reaches beyond this node and is recorded because this is where it was found. 160 used to bundle QuasilocalCompleteness as a field — a mathematical existence claim about the net, carrying Axiom 4’s name rather than stating the bridge principle of 151. That re-pointing has been carried out: the field is gone, and the net’s canonical quasilocal algebra is built from this theorem instead.

LaTeX Lean

Theorem 158Quasilocal Observables are Strongly Dense in the Bicommutant

Let $\pi $ be a unital $*$-representation of the quasilocal algebra $\mathfrak {U}$ on a Hilbert space $H$. Then the image $\pi (\mathfrak {U})$ is dense in its bicommutant $\pi (\mathfrak {U})''$ in the strong operator topology.

Unitality is the hypothesis that does the work and it is stated directly rather than derived from a stronger one. It is essential, not decorative: for the zero representation $\pi = 0$ on a nonzero $H$ the image $\pi (\mathfrak {U}) = \{ 0\} $ is already strongly closed while $\pi (\mathfrak {U})'' = \mathbb {C}\cdot 1$, so density fails outright. The case of interest here is the GNS representation $\pi _\omega $ attached to a state $\omega $ (13, 15), which is unital because $\mathfrak {U}$ is a unital C*-algebra and $\omega $ a state; but the theorem holds for any unital $*$-representation, and stating it for the GNS one only would be assuming more than the density theorem needs. Below, $\pi _\omega $ is written wherever the GNS case is the one being discussed.

Its role: this is what makes the bridge principle tenable. The observables of a region are read off from the local von Neumann algebra $R(\mathbf{B}) = \pi _\omega (\mathfrak {U}(\mathbf{B}))''$ of 162, and a bicommutant is in general strictly larger than the image it is formed from. The statement above is about the global bicommutant $\pi _\omega (\mathfrak {U})''$, and it covers the local ones because $\pi _\omega (\mathfrak {U}(\mathbf{B})) \subseteq \pi _\omega (\mathfrak {U})$ and taking commutants reverses inclusions twice over, so $R(\mathbf{B}) \subseteq \pi _\omega (\mathfrak {U})''$ for every $\mathbf{B}$. Taken naively, the strictness looks like a refutation of Axiom 4 (151): the bicommutant would contain self-adjoint operators that are not quasilocal observables, hence physical observables outside the quasilocal ones. This node is what blocks that reading. Every element of the bicommutant is approximated in the strong topology by elements of $\pi _\omega (\mathfrak {U})$, and strong convergence implies convergence of all the expectation values $\langle \psi , T \psi \rangle $ that a measurement can return — the implication runs this way and not the other, since the strong topology is strictly finer than the weak one in which those expectation values converge — so no measurement of finite precision can distinguish an element of the bicommutant from a quasilocal observable close to it. The extra elements are therefore not new measurable quantities, and their existence does not falsify the identification of physical observables with quasilocal ones; it refines it. This is the content that Chapter 6.3 argues informally, citing Murphy Lemma 4.1.4: a unital $*$-subalgebra of $\mathcal{B}(H)$ containing the identity is strongly dense in its bicommutant.

One refinement of the argument is worth recording, since it is easy to overstate. The approximants furnished by the density theorem are elements of $\pi _\omega (\mathfrak {U})$, but they are not guaranteed to be self-adjoint, so the reading “every self-adjoint element of the bicommutant is a strong limit of self-adjoint quasilocal observables” is a strictly stronger claim than the one asserted here. That stronger claim is the Kaplansky density theorem, which additionally preserves self-adjointness and norm bounds. Nothing in the tenability argument above needs it — indistinguishability by expectation values only requires approximants at all — but it is the result to invoke if the self-adjoint form is ever wanted.

LaTeX