Definitions for Observables I: Stone Spectra

QAlgorithms.Papers.Independent.Intakethird100.P20.BorelSets

For any type $M$ equipped with a topology, $\mathrm{BorelSets}(M)$ is the type of subsets of $M$ that are measurable for the Borel $\sigma$-algebra generated by that topology. Each element consists of a subset together with evidence that it is Borel measurable. No nonemptiness or separation assumption is imposed on $M$.

QAlgorithms.Papers.Independent.Intakethird100.P20.CofiniteSubspaces

For any type $H$ equipped with a normed additive commutative group structure and a compatible complex inner product space structure, this defines the type of closed complex linear subspaces $U\subseteq H$ satisfying $U=\{0\}$ or $\dim_{\mathbb C}(U^\perp)<\infty$, where $U^\perp$ is the orthogonal complement, regarded as a complex linear subspace. The zero subspace is included regardless of the dimension of its orthogonal complement, and the whole space is included because its orthogonal complement is zero-dimensional. Completeness of $H$ is not assumed.

QAlgorithms.Papers.Independent.Intakethird100.P20.DualIdeal

For any bounded lattice $L$, this defines the type of subsets $J\subseteq L$ that are nonempty, exclude $\bot$, are upward closed, and are closed under binary meets: if $a\in J$ and $a\le b$, then $b\in J$, and if $a,b\in J$, then $a\wedge b\in J$. If $\bot=\top$, there are no such subsets, so this type is empty.

QAlgorithms.Papers.Independent.Intakethird100.P20.HasDirectedMeetLaw

For any complete lattice $L$, this property means that every $a\in L$ and every nonempty subset $s\subseteq L$ directed upwards within itself satisfy $a\wedge\sup s=\sup\{a\wedge b\mid b\in s\}$. Here directedness means that for every $b,c\in s$ there is $d\in s$ with $b\le d$ and $c\le d$. No condition is imposed for empty $s$.

QAlgorithms.Papers.Independent.Intakethird100.P20.HasFrameLaw

For any complete lattice $L$, this property means that for every $a\in L$ and every subset $s\subseteq L$, $a\wedge\sup s=\sup\{a\wedge b\mid b\in s\}$. The subset $s$ may be empty, in which case the asserted equality is $a\wedge\bot=\bot$.

QAlgorithms.Papers.Independent.Intakethird100.P20.HasIntersectionProperty

For any bounded lattice $L$ and any real-valued function $f$ on the nonempty, upward-closed, binary-meet-closed subsets of $L$ that exclude $\bot$, this property means the following: for every nonempty family $\mathcal F$ of such subsets and every such subset $J$, if $J=\bigcap_{K\in\mathcal F}K$, then $f(J)=\sup\{f(K)\mid K\in\mathcal F\}$. No upper bound on the displayed set of real values is assumed; if it is unbounded above, the total real supremum used here equals $0$. Empty families are excluded.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsAbstractObservable

For any bounded lattice $L$, let $\mathcal D$ be the set of all nonempty, upward-closed, binary-meet-closed subsets of $L$ that exclude $\bot$, equipped with the topology generated by the sets $\{J\in\mathcal D\mid a\in J\}$ for $a\in L$. For a function $f:\mathcal D\to\mathbb R$, this property means that $f$ is upper semicontinuous—equivalently, $\{J\in\mathcal D\mid f(J)<c\}$ is open for every real $c$—and that, for every nonempty family $\mathcal F\subseteq\mathcal D$ and every $J\in\mathcal D$ equal to $\bigcap_{K\in\mathcal F}K$, one has $f(J)=\sup\{f(K)\mid K\in\mathcal F\}$. The supremum is the total real supremum, which equals $0$ for a set unbounded above.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsBooleanFilterBase

For any bounded lattice $L$, any function $\perp:L\to L$, and any subset $B\subseteq L$, this property means that $B$ is nonempty, $\bot\notin B$, every $a,b\in B$ admit some $c\in B$ with $c\le a$ and $c\le b$, and every ordered pair $a,b\in B$ satisfies $a=(a\wedge b)\vee(a\wedge\perp(b))$. The last condition includes $a=b$. No upward closure of $B$ or orthocomplementation laws for $\perp$ are assumed; if $\bot=\top$, no such $B$ exists.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsBooleanQuasipoint

For any bounded lattice $L$, any function $\perp:L\to L$, and any subset $B\subseteq L$, this property means that $B$ is nonempty, excludes $\bot$, admits for every $a,b\in B$ an element $c\in B$ with $c\le a,b$, and satisfies $a=(a\wedge b)\vee(a\wedge\perp(b))$ for every ordered pair $a,b\in B$; furthermore, every subset $C\subseteq L$ satisfying these same conditions and containing $B$ must equal $B$. No orthocomplementation laws are assumed for $\perp$; if $\bot=\top$, no such $B$ exists.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsBooleanSector

For any bounded lattice $L$, any function $\perp:L\to L$, and any subset $S\subseteq L$, this property means that $S$ contains $\bot$ and $\top$, is closed under $\perp$, binary meets, and binary joins, and satisfies both distributive identities $a\wedge(b\vee c)=(a\wedge b)\vee(a\wedge c)$ and $a\vee(b\wedge c)=(a\vee b)\wedge(a\vee c)$ for all $a,b,c\in S$; moreover, every subset $T\subseteq L$ with these same containment, closure, and distributivity properties and with $S\subseteq T$ must equal $S$. No orthocomplementation laws are assumed for $\perp$.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsBoundedSpectralFamily

For any complete lattice $L$ and function $E:\mathbb R\to L$, this property means that $E(t)\le E(s)$ whenever $t\le s$, that $E(t)=\inf\{E(s)\mid s>t\}$ for every real $t$, that the infimum and supremum of its entire range are respectively $\bot$ and $\top$, and that there exist real numbers $a,b$ such that $E(t)=\bot$ for every $t<a$ and $E(t)=\top$ for every $t>b$. No ordering between $a$ and $b$ is explicitly required, and these last two conditions use strict inequalities.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsCompletePresheaf

Let $L$ be a complete lattice, and let $S$ assign a type $S(a)$ to each $a\in L$, with restriction maps $\rho_{a,b}:S(b)\to S(a)$ for $a\leq b$ that preserve identities and composition. The predicate $\mathrm{IsCompletePresheaf}(S)$ means that for every $a\in L$, every subset $C\subseteq L$ with $\sup C=a$, and every choice of sections $s_b\in S(b)$ for $b\in C$, if $\rho_{b\wedge c,b}(s_b)=\rho_{b\wedge c,c}(s_c)$ for every $b,c\in C$ with $b\wedge c\neq\bot$, then there exists exactly one $s\in S(a)$ such that $\rho_{b,a}(s)=s_b$ for every $b\in C$. No compatibility condition is required when $b\wedge c=\bot$. The subset $C$ may be empty; that case has $a=\bot$ and requires $S(\bot)$ to have exactly one element.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsCompletelyIncreasing

For any complete lattice $L$ and any function $r:L\setminus\{\bot\}\to\mathbb R$, this property means that for every nonempty subset $S\subseteq L\setminus\{\bot\}$ and every $a\in L\setminus\{\bot\}$, if $a$ is the least upper bound in $L$ of the elements of $S$, then $r(a)=\sup\{r(b)\mid b\in S\}$. No boundedness assumption is imposed on these real values; if they are unbounded above, their total real supremum is $0$. Empty subsets impose no condition, and if $L$ consists only of $\bot$, the property holds vacuously.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsDistributive

For any lattice $L$, with meet $\wedge$ and join $\vee$, this predicate means that both identities $a\wedge(b\vee c)=(a\wedge b)\vee(a\wedge c)$ and $a\vee(b\wedge c)=(a\vee b)\wedge(a\vee c)$ hold for every $a,b,c\in L$. No least or greatest element is assumed.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsDistributiveOn

For any lattice $L$ and subset $S\subseteq L$, this property means that every $a,b,c\in S$ satisfies both $a\wedge(b\vee c)=(a\wedge b)\vee(a\wedge c)$ and $a\vee(b\wedge c)=(a\vee b)\wedge(a\vee c)$. Closure of $S$ under lattice operations is not required; when $S=\varnothing$, both conditions hold vacuously.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsDualIdeal

For any bounded lattice $L$, with least element $\bot$, greatest element $\top$, and meet operation $\wedge$, and any subset $J\subseteq L$, this predicate means that $J$ is nonempty, $\bot\notin J$, every $a\in J$ and $b\in L$ with $a\le b$ satisfy $b\in J$, and every $a,b\in J$ satisfy $a\wedge b\in J$. There is no nontriviality assumption on $L$; if $\bot=\top$, no subset satisfies these conditions.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsFilterBase

For any type $L$ equipped with a binary relation $\le$ and a distinguished element $\bot$, and any subset $B\subseteq L$, this predicate means that $B$ is nonempty, $\bot\notin B$, and for every $a,b\in B$ there exists $c\in B$ satisfying $c\le a$ and $c\le b$. No order axioms for $\le$, or requirement that $\bot$ be a least element, are assumed. In particular, the empty set does not satisfy the predicate.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsFiniteType

For any complete lattice $L$, let $Q$ be the set of all subsets $B\subseteq L$ maximal under inclusion among subsets that are nonempty, exclude $\bot$, and have, for every $a,b\in B$, some $c\in B$ with $c\le a$ and $c\le b$. For $a\in L$, put $Q_a=\{B\in Q\mid a\in B\}$, and equip $Q$ with the topology generated by all the sets $Q_a$. This property means that every nonempty subset $s\subseteq L$ directed upwards within itself—that is, every $a,b\in s$ have some $c\in s$ with $a\le c$ and $b\le c$—satisfies $\overline{\bigcup_{a\in s}Q_a}=Q_{\sup s}$, where closure is taken in that topology. No condition is imposed for empty $s$.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsLatticePoint

For any complete lattice $L$ and any subset $p\subseteq L$, this predicate means that $p$ is nonempty, excludes $\bot$, is upward closed, and is closed under binary meets, and that for every subset $s\subseteq L$, if $\sup s\in p$, then there exists $a\in s$ with $a\in p$. The quantification includes the empty subset, whose supremum is $\bot$, so its antecedent is false because $\bot\notin p$. No nontriviality assumption on $L$ is imposed; if $\bot=\top$, no such $p$ exists.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsMeasurableSpectralFamily

For any type $M$ equipped with a measurable space and any function $E:\mathbb R\to\mathcal P(M)$, this property means that $E(t)$ is measurable for every real $t$, that $E(t)\subseteq E(s)$ whenever $t\le s$, that $E(t)=\bigcap_{s>t}E(s)$ for every real $t$, and that $\bigcap_{t\in\mathbb R}E(t)=\varnothing$ and $\bigcup_{t\in\mathbb R}E(t)=M$. The type $M$ may be empty; no value of $E$ is required to equal either $\varnothing$ or $M$.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsOrthocomplement

For any bounded lattice $L$ and any function $a\mapsto a^\perp$ from $L$ to itself, this predicate means that $a\wedge a^\perp=\bot$ and $a\vee a^\perp=\top$ for every $a\in L$, that $(a\wedge b)^\perp=a^\perp\vee b^\perp$ and $(a\vee b)^\perp=a^\perp\wedge b^\perp$ for every $a,b\in L$, and that $(a^\perp)^\perp=a$ for every $a\in L$. The lattice is not required to be nontrivial.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsOrthogonalRepresentation

Let $H$ be a complete complex inner product space with its normed additive commutative group structure, let $R$ be a von Neumann algebra of continuous complex-linear operators on $H$, let $n\in\mathbb N$, let $x$ be an element of the complex star subalgebra underlying $R$, and let $c_i\in\mathbb C$ and $p_i\in R$ be indexed by $i\in\{0,\ldots,n-1\}$, with each $p_i$ self-adjoint and idempotent. The predicate $\mathrm{IsOrthogonalRepresentation}(x,c,p)$ means that every $p_i$ is nonzero, that $p_ip_j=0$ for every pair of distinct indices $i,j$, and that the underlying operator of $x$ equals $\sum_{i=0}^{n-1}c_ip_i$. The coefficients may be zero or repeated. The case $n=0$ is included: both projection conditions are then vacuous, and the equality requires $x=0$.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsOrthomodular

For any bounded lattice $L$ and any function $a\mapsto a^\perp$ from $L$ to itself, this predicate means that $a\wedge a^\perp=\bot$, $a\vee a^\perp=\top$, and $(a^\perp)^\perp=a$ for every $a\in L$, that $(a\wedge b)^\perp=a^\perp\vee b^\perp$ and $(a\vee b)^\perp=a^\perp\wedge b^\perp$ for every $a,b\in L$, and additionally that for every $a,b,c\in L$ satisfying $b\le a$ and $c\le a^\perp$, one has $a\wedge(b\vee c)=(a\wedge b)\vee(a\wedge c)$. The lattice is not required to be nontrivial.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsQuasipoint

For any type $L$ equipped with a binary relation $\le$ and a distinguished element $\bot$, and any subset $B\subseteq L$, this predicate means that $B$ is nonempty, excludes $\bot$, and contains, for every $a,b\in B$, some $c\in B$ with $c\le a$ and $c\le b$; moreover, for every subset $C\subseteq L$ having these same three properties, $B\subseteq C$ implies $C=B$. Thus maximality is with respect to inclusion among subsets satisfying precisely these properties. No order axioms or least-element property of $\bot$ are assumed.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsRegularSpectralFamily

For any topological space $M$, possibly empty, and any family $E:\mathbb R\to\operatorname{Opens}(M)$, this is the conjunction of the following conditions, viewing each $E(t)$ as a subset of $M$: $E(t)\subseteq E(s)$ whenever $t\le s$; for every real $t$,

$$E(t)=\operatorname{int}\!\left(\bigcap_{s>t}E(s)\right);$$

the family satisfies

$$\operatorname{int}\!\left(\bigcap_{t\in\mathbb R}E(t)\right)=\varnothing, \qquad \bigcup_{t\in\mathbb R}E(t)=M;$$

and, for every pair of real numbers $t<s$, one has $\overline{E(t)}\subseteq E(s)$. The interiors in these formulas arise because the infima are taken in the lattice of open subsets of $M$.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsSigmaComplete

For any partially ordered type $L$, the predicate $\mathrm{IsSigmaComplete}(L)$ means that every sequence $(a_n)_{n\in\mathbb N}$ in $L$ has an element $b\in L$ that is a least upper bound of its range: $a_n\leq b$ for every $n$, and $b\leq c$ for every $c\in L$ satisfying $a_n\leq c$ for every $n$. The sequences need not be increasing or bounded in advance. This condition does not explicitly require a supremum of the empty set; if $L$ is empty, there are no such sequences and the predicate holds vacuously.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsSigmaIdeal

Let $L$ be a lattice with a least element $\bot$ and a greatest element $\top$, and let $I\subseteq L$. The predicate $\mathrm{IsSigmaIdeal}(I)$ means that $I$ is nonempty, that $a\in I$ and $b\leq a$ imply $b\in I$ for every $a,b\in L$, and that for every sequence $(a_n)_{n\in\mathbb N}$ of elements of $I$, every element $b\in L$ that is a least upper bound of $\{a_n:n\in\mathbb N\}$ belongs to $I$. This does not require such a least upper bound to exist; for a sequence without one, the final condition imposes no requirement. Nonemptiness and downward closure imply $\bot\in I$, and $I=L$ is allowed.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsSigmaPoint

For any bounded lattice $L$ and any subset $p\subseteq L$, this predicate means that $p$ is nonempty, excludes $\bot$, is upward closed, and is closed under binary meets, and that for every sequence $(a_n)_{n\in\mathbb N}$ in $L$ and every $b\in L$, if $b$ is a least upper bound of $\{a_n:n\in\mathbb N\}$ and $b\in p$, then $a_n\in p$ for some $n\in\mathbb N$. The lattice is not assumed to have least upper bounds for all sequences; a sequence with no least upper bound imposes no condition through this clause. If $\bot=\top$, no such $p$ exists.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsSpectralFamily

For any complete lattice $L$ and function $E:\mathbb R\to L$, this property means that $E(t)\le E(s)$ whenever $t\le s$, that $E(t)=\inf\{E(s)\mid s>t\}$ for every real $t$, and that $\inf\{E(t)\mid t\in\mathbb R\}=\bot$ and $\sup\{E(t)\mid t\in\mathbb R\}=\top$. The endpoint conditions concern the infimum and supremum of the entire range and do not require either endpoint to be attained.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsSubOrtholattice

For any bounded lattice $L$, any function $\perp:L\to L$, and any subset $S\subseteq L$, this property means that $\bot,\top\in S$, that $\perp(a)\in S$ for every $a\in S$, and that $a\wedge b,a\vee b\in S$ for every $a,b\in S$. No orthocomplementation laws are assumed for $\perp$.

QAlgorithms.Papers.Independent.Intakethird100.P20.IsUnboundedQuasipoint

For every topological space $M$ and every quasipoint $B$ of its open-set lattice, the proposition $\operatorname{IsUnboundedQuasipoint}(B)$ means that for every compact subset $K\subseteq M$, there is a member $U\in B$ whose underlying set is exactly $M\setminus K$. Here $B$ is a nonempty family of open subsets, excludes $\varnothing$, contains a common smaller member for each pair of members, and is maximal under inclusion among families with these properties. Thus the condition requires the complement of every compact set to be open and to belong to $B$. The quantifier includes $K=\varnothing$, requiring $M\in B$; if $M$ itself is compact, it also includes $K=M$, which would require $\varnothing\in B$, so the proposition cannot hold in that case.

QAlgorithms.Papers.Independent.Intakethird100.P20.LatticeCommutes

For any lattice $L$, any function $a\mapsto a^\perp$ from $L$ to itself, and any $a,b\in L$, this predicate means exactly that $a=(a\wedge b)\vee(a\wedge b^\perp)$. No bounds on the lattice, identities for the function $a\mapsto a^\perp$, or corresponding identity with $a$ and $b$ exchanged are assumed or included in the predicate.

QAlgorithms.Papers.Independent.Intakethird100.P20.LatticePresheaf

For any partially ordered type $L$, a $\mathrm{LatticePresheaf}$ consists of a type $F(a)$ for every $a\in L$ and, for every inequality $a\leq b$, a restriction map $\rho_{a,b}:F(b)\to F(a)$. These maps satisfy $\rho_{a,a}(s)=s$ for every $a\in L$ and $s\in F(a)$, and $\rho_{a,b}(\rho_{b,c}(s))=\rho_{a,c}(s)$ for every $a\leq b\leq c$ and $s\in F(c)$, where the last restriction uses the composite inequality $a\leq c$. The fibers are arbitrary types and need not be nonempty; no lattice operations on $L$ are assumed.

QAlgorithms.Papers.Independent.Intakethird100.P20.LiesOver

For any topological space $M$, any $B\in\operatorname{StoneSpectrum}(\operatorname{Opens}(M))$, and any $x\in M$, this says that

$$\bigcap_{U\in B}\overline U=\{x\}.$$

Here $B$ is a collection of open subsets of $M$ that is nonempty, excludes $\varnothing$, and has the property that for every $U,V\in B$ there exists $W\in B$ with $W\subseteq U$ and $W\subseteq V$; moreover, $B$ is maximal under inclusion among collections having these properties. Thus the intersection of the closures is required to contain exactly $x$.

QAlgorithms.Papers.Independent.Intakethird100.P20.RegularOpens

For any topological space $M$, possibly empty, this defines the type of open subsets $U\subseteq M$ satisfying $\operatorname{int}(\overline U)=U$, with each such open set accompanied by a proof of this equality. Both $\varnothing$ and $M$ satisfy the defining condition.

QAlgorithms.Papers.Independent.Intakethird100.P20.StoneSpectrum

For any type $L$ equipped with a binary relation $\le$ and a distinguished element $\bot$, this defines the type whose elements are subsets $B\subseteq L$, together with evidence that $B$ is nonempty, excludes $\bot$, contains a common lower bound within $B$ for every pair of its elements, and is maximal under inclusion among subsets with these properties. Here a common lower bound of $a,b$ means an element $c$ satisfying $c\le a$ and $c\le b$. No order axioms, least-element property of $\bot$, or existence of such a maximal subset are assumed; this type may be empty.

QAlgorithms.Papers.Independent.Intakethird100.P20.admissibleDomain

For any topological space $M$, possibly empty, and any family $E:\mathbb R\to\operatorname{Opens}(M)$, this defines the set $\{x\in M\mid \exists t\in\mathbb R,\ x\notin E(t)\}$, equivalently $M\setminus\bigcap_{t\in\mathbb R}E(t)$. No spectral-family conditions on $E$ are assumed.

QAlgorithms.Papers.Independent.Intakethird100.P20.borelSaturation

Let $M$ be any topological space, and let $B$ be a family of open subsets of $M$ that is nonempty, excludes $\varnothing$, and has the property that any two members contain a common member of $B$; assume also that $B$ is maximal under inclusion among families with these properties. The set $\mathrm{borelSaturation}(B)$ consists precisely of the Borel measurable subsets $A\subseteq M$ for which there is an open set $U\in B$ such that the symmetric difference $(A\setminus U)\cup(U\setminus A)$ is meagre, meaning that it is contained in a countable union of nowhere dense subsets of $M$. If no such maximal family $B$ exists, there is no admissible argument $B$ for this definition.

QAlgorithms.Papers.Independent.Intakethird100.P20.borelSetsBoundedOrder

For any topological space $M$, the Borel measurable subsets of $M$, ordered by inclusion, have least element $\varnothing$ and greatest element $M$: every Borel measurable subset contains $\varnothing$ and is contained in $M$. If $M$ is empty, these two distinguished elements coincide.

QAlgorithms.Papers.Independent.Intakethird100.P20.borelSetsLattice

For any topological space $M$, the Borel measurable subsets of $M$, ordered by inclusion, form a lattice in which $A\vee B=A\cup B$ and $A\wedge B=A\cap B$. Thus each of $A$ and $B$ is contained in their union, and their union is contained in every common upper bound; their intersection is contained in each of them, and contains every common lower bound. These operations again produce Borel measurable sets, including when $M$ is empty.

QAlgorithms.Papers.Independent.Intakethird100.P20.closedLine

For any complex inner product space $H$ with its normed additive commutative group structure, and any $x\in H$, $\mathrm{closedLine}(x)$ is the infimum, in the lattice of closed complex-linear subspaces of $H$, of all such subspaces containing $x$; equivalently, it is their intersection. This family is nonempty because it contains $H$. No completeness assumption on $H$ is required, and when $x=0$ the resulting subspace is $\{0\}$.

QAlgorithms.Papers.Independent.Intakethird100.P20.cofiniteBasic

For every complex inner product space $H$, equipped with its normed additive commutative group structure and without any completeness assumption, and every closed complex linear subspace $U\subseteq H$, let $\mathcal C(H)$ be the collection of closed complex linear subspaces $V$ such that $V=\{0\}$ or $V^\perp$ is finite-dimensional, ordered by inclusion. A quasipoint of $\mathcal C(H)$ is a family $B\subseteq\mathcal C(H)$ that is nonempty, excludes the zero subspace, contains for every $V,W\in B$ some $Z\in B$ with $Z\subseteq V\cap W$, and is maximal under inclusion among families with these properties. The set $\operatorname{cofiniteBasic}(U)$ consists of precisely those quasipoints $B$ for which some member $V\in B$ has underlying closed subspace equal to $U$. The argument $U$ need not itself satisfy the defining condition for $\mathcal C(H)$; the resulting set is empty if $U$ does not satisfy that condition, and it is also empty when $U=\{0\}$.

QAlgorithms.Papers.Independent.Intakethird100.P20.cofiniteSubspacesBot

For every complex inner product space $H$, equipped with its normed additive commutative group structure and without any completeness assumption, consider the collection of closed complex linear subspaces $U\subseteq H$ satisfying either $U=\{0\}$ or $U^\perp$ is finite-dimensional over $\mathbb C$. This instance chooses the zero subspace as the distinguished bottom element of that collection. Its membership is justified by the alternative $U=\{0\}$, so no finite-dimensionality assumption on $H$ or on the orthogonal complement of the zero subspace is required.

QAlgorithms.Papers.Independent.Intakethird100.P20.cofiniteSubspacesLE

For any type $H$ equipped with a normed additive commutative group structure and a compatible complex inner product space structure, consider the closed complex linear subspaces $U\subseteq H$ satisfying $U=\{0\}$ or $\dim_{\mathbb C}(U^\perp)<\infty$. This defines the relation $U\le V$ on these subspaces to mean inclusion of their underlying subspaces, $U\subseteq V$. Completeness of $H$ is not assumed.

QAlgorithms.Papers.Independent.Intakethird100.P20.compactificationBase

For every topological space $M$ and every quasipoint $B$ of its open-set lattice, define $\operatorname{compactificationBase}(B)$ to be the family of open subsets $V$ of the one-point space $M\cup\{\infty\}$ whose inverse image under the canonical inclusion $i:M\to M\cup\{\infty\}$ equals some member of $B$: $\exists U\in B,\ U=i^{-1}(V)$. Here a quasipoint $B$ is a nonempty family of open subsets of $M$, excluding $\varnothing$, such that any two members contain a common member of $B$, and maximal under inclusion among families with these properties. The definition places no additional condition on whether $\infty$ belongs to $V$, and assumes neither compactness nor local compactness nor any separation property of $M$.

QAlgorithms.Papers.Independent.Intakethird100.P20.dualIdealTopology

For any bounded lattice $L$, consider the type of all nonempty subsets $J\subseteq L$ that exclude $\bot$, are upward closed, and are closed under binary meets. This defines its topology to be the smallest topology in which, for every $a\in L$, the set $\{J\mid a\in J\}$ is open. Thus these sets form a subbasis for the topology; if $\bot=\top$, the underlying space is empty.

QAlgorithms.Papers.Independent.Intakethird100.P20.dualSpectralValue

For any bounded lattice $L$, any function $E:\mathbb R\to L$, and any nonempty subset $J\subseteq L$ that excludes $\bot$, is upward closed, and is closed under binary meets, this defines the real number $\inf\{t\in\mathbb R\mid E(t)\in J\}$. No monotonicity, continuity, boundedness, or spectral-family condition is imposed on $E$. The infimum is the total real infimum: if the set is empty or unbounded below, its value is $0$.

QAlgorithms.Papers.Independent.Intakethird100.P20.extendIncreasing

For any bounded lattice $L$, any function $r:L\setminus\{\bot\}\to\mathbb R$, and any nonempty subset $J\subseteq L$ that excludes $\bot$, is upward closed, and is closed under binary meets, this defines the real number $\inf\{r(a)\mid a\in L\setminus\{\bot\},\ a\in J\}$. No increasingness condition is imposed on $r$. The set of values is nonempty because $J$ is nonempty and excludes $\bot$; if it is unbounded below, the total real infimum used here is $0$.

QAlgorithms.Papers.Independent.Intakethird100.P20.latticeCommutant

For any lattice $L$, any function $\perp:L\to L$, and any subset $S\subseteq L$, the set called the commutant of $S$ is defined by

$$C_\perp(S)=\{b\in L:\ \text{for every }a\in S,\ a=(a\wedge b)\vee(a\wedge\perp b)\}.$$

No properties of the function $\perp$ are assumed. In particular, $C_\perp(\varnothing)=L$, since its membership condition is then vacuous.

QAlgorithms.Papers.Independent.Intakethird100.P20.measurableSublevels

For any type $M$, possibly empty, any function $g:M\to\mathbb R$, and any $t\in\mathbb R$, this defines the set $\{x\in M\mid g(x)\le t\}$. No measurable structure on $M$ or measurability assumption on $g$ is required.

QAlgorithms.Papers.Independent.Intakethird100.P20.openPseudoCompl

For any topological space $M$, possibly empty, and any open subset $U\subseteq M$, this defines the open subset $M\setminus\overline U$, the complement in $M$ of the closure of $U$.

QAlgorithms.Papers.Independent.Intakethird100.P20.openSublevels

For any topological space $M$, possibly empty, any function $f:M\to\mathbb R$, and any $t\in\mathbb R$, this defines the open set $\operatorname{int}\{x\in M\mid f(x)\le t\}$, where the interior is taken in $M$. No continuity or measurability assumption on $f$ is required.

QAlgorithms.Papers.Independent.Intakethird100.P20.operatorProjectionBot

For any complete complex inner product space $H$, with its normed additive commutative group structure, and any von Neumann algebra $R$ of continuous complex-linear operators on $H$, this declaration equips the type of projections in $R$ with a distinguished bottom element given by the zero operator. Here a projection is an operator belonging to $R$ that is self-adjoint and idempotent; the zero operator has both properties. The declared structure specifies this element without itself asserting an order inequality.

QAlgorithms.Papers.Independent.Intakethird100.P20.ortholatticeGenerated

For any bounded lattice $L$, any function $\perp:L\to L$, and any subset $B\subseteq L$, this definition gives the set of all $a\in L$ such that $a\in S$ for every subset $S\subseteq L$ which contains $B$, $\bot$, and $\top$ and is closed under $\perp$, binary meets, and binary joins. Equivalently, it is the intersection of all such subsets $S$. The input $B$ may be empty; the collection being intersected is always nonempty because it contains $L$ itself. No orthocomplementation laws are assumed for $\perp$.

QAlgorithms.Papers.Independent.Intakethird100.P20.principalDualIdeal

For any bounded lattice $L$ and any element $a\in L$ satisfying $a\ne\bot$, this defines the dual ideal $\{b\in L\mid a\le b\}$, regarded as a nonempty subset that excludes $\bot$, is upward closed, and is closed under binary meets. The element $a$ belongs to this subset. If $L$ has no element distinct from $\bot$, there is no admissible input $a$.

QAlgorithms.Papers.Independent.Intakethird100.P20.principalQuasipoint

For any type $L$ equipped with a binary relation $\le$, and any $a\in L$, this defines the subset $\{b\in L\mid a\le b\}$. No reflexivity, transitivity, antisymmetry, bottom element, or other order property is assumed; in particular, the definition does not assert that this subset is a quasipoint.

QAlgorithms.Papers.Independent.Intakethird100.P20.regularOpensBot

For any topological space $M$, possibly empty, this designates the empty open set as the bottom element of the type of open subsets $U\subseteq M$ satisfying $\operatorname{int}(\overline U)=U$, using the equality $\operatorname{int}(\overline\varnothing)=\varnothing$.

QAlgorithms.Papers.Independent.Intakethird100.P20.regularOpensLE

For any topological space $M$, possibly empty, this equips the type of open subsets $U\subseteq M$ satisfying $\operatorname{int}(\overline U)=U$ with the relation $U\le V$ defined by inclusion of their underlying open sets: $U\le V$ means $U\subseteq V$.

QAlgorithms.Papers.Independent.Intakethird100.P20.regularizeOpen

For any topological space $M$, possibly empty, and any open subset $U\subseteq M$, this defines the open subset $\operatorname{int}(\overline U)$, the interior in $M$ of the closure of $U$.

QAlgorithms.Papers.Independent.Intakethird100.P20.regularizedBase

For any topological space $M$ and any $B\in\operatorname{StoneSpectrum}(\operatorname{Opens}(M))$, this defines the set of regular open subsets $V\subseteq M$ for which there exists $U\in B$ with $\operatorname{int}(\overline U)=V$; here “regular open” means that $V$ is open and $\operatorname{int}(\overline V)=V$. The collection $B$ is nonempty, excludes the empty open set, and contains, for every $U_1,U_2\in B$, some $W\in B$ contained in both $U_1$ and $U_2$; it is maximal under inclusion among collections of open sets having these properties.

QAlgorithms.Papers.Independent.Intakethird100.P20.restrictObservable

For any bounded lattice $L$, any real-valued function $f$ on the nonempty, upward-closed, binary-meet-closed subsets of $L$ that exclude $\bot$, and any $a\in L$ with $a\ne\bot$, this defines the real number $f(\{b\in L\mid a\le b\})$. The argument of $f$ is the dual ideal consisting of all elements above $a$. No semicontinuity or intersection property is assumed of $f$.

QAlgorithms.Papers.Independent.Intakethird100.P20.spectralCutInfimum

For any type $M$, any family of sets $E:\mathbb R\to\mathcal P(M)$, and any $x\in M$, this defines the real number $\inf\{t\in\mathbb R\mid x\in E(t)\}$, using the total real infimum operation. If this set is nonempty and bounded below, this is its usual infimum; if it is empty or unbounded below, the value is $0$. No monotonicity or other condition on $E$ is assumed.

QAlgorithms.Papers.Independent.Intakethird100.P20.spectralSumFunction

Let $H$ be a complete complex inner product space with its normed additive commutative group structure, let $R$ be a von Neumann algebra of continuous complex-linear operators on $H$, let $n\in\mathbb N$, and choose coefficients $c_i\in\mathbb C$ and self-adjoint idempotent operators $p_i\in R$ for $i\in\{0,\ldots,n-1\}$. Let $B$ be a nonempty family of projections in $R$ that excludes the zero projection, such that for any $e,f\in B$ there is $g\in B$ with $g\leq e$ and $g\leq f$, and that is maximal under inclusion among families with these properties. Then $\mathrm{spectralSumFunction}(c,p,B)$ is the complex number $\sum_{i=0}^{n-1}d_i$, where $d_i=c_i$ if $p_i\in B$ and $d_i=0$ otherwise. No nonzero, orthogonality, or representation condition is imposed on the family $(p_i)$. Repeated projections contribute separately at their respective indices, and when $n=0$ the value is $0$.

QAlgorithms.Papers.Independent.Intakethird100.P20.stoneBasic

For any type $L$ equipped with a binary relation $\le$ and a distinguished element $\bot$, and any $a\in L$, this defines the set of all subsets $B\subseteq L$ that contain $a$ and are maximal under inclusion among nonempty subsets excluding $\bot$ and containing, for each pair $x,y$ of their elements, an element $z$ with $z\le x$ and $z\le y$. These $B$ are regarded as elements of the type of such maximal subsets. No order axioms or least-element property of $\bot$ are assumed. When $a=\bot$, the defined set is empty.

QAlgorithms.Papers.Independent.Intakethird100.P20.stoneTopology

For any type $L$ equipped with a binary relation $\le$ and a distinguished element $\bot$, this equips the type of maximal nonempty subsets $B\subseteq L$ excluding $\bot$ and containing a common lower bound within $B$ for each pair of their elements with the smallest topology in which every set $\mathcal U_a=\{B:a\in B\}$, for $a\in L$, is open; here a common lower bound of $x,y$ is an element $z$ satisfying $z\le x$ and $z\le y$, and maximality is under inclusion among subsets with the stated properties. No order axioms or least-element property of $\bot$ are assumed, and the underlying type is allowed to be empty.