The represented corner lies in the weighted Gaussian algebra

Fix real numbers $0<v<u$. Consider the full two-vertex path Fock space with edge labels in $\mathbb N$, the operators $S_i=uc_{i,\mathrm{true}}+vc_{i,\mathrm{false}}+\text{h.c.}$ built from creation operators, the coordinate projection $P$ onto paths starting at the vertex $\mathrm{true}$, and the ambient von Neumann algebra $\{P,S_i\}''$. Let $\mathrm{PRange}$ be the range of $P$, and let $\mathrm{representedAmbient}(u,v)$ be the corner of the ambient algebra by $P$, represented on $\mathrm{PRange}$. Let $\mathcal X$ be the weighted Gaussian system on $\mathrm{PRange}$ with the restricted vacuum as root, and let $\sigma$ be the scalar flip of its index set. Then

where $W^*(\mathcal X,\sigma)$ is the double commutant of the generators of $\mathcal X$. This is one inclusion in the recognition of the corner as a Gaussian algebra.

Formalization Note The statement is verbatim from OpenAI's Lean development, with the listed Definitions imported in place of the upstream modules; the definitions are supporting code for this statement.