Manuscript IX-E@1 · IX-E.tex · proposition · 8f8d5e7f

Proposition: Domain stability

E0: a fixed comparison domain · lines 456–485 · proof included or linked

IX-E@1#prop:domain

Under (eq:free-star), the domain (eq:fixed-domain) satisfies

D_{2} \subset D_{cmp}, σ (D_{2}) = D_{2}, γ (D_{2}) = D_{2}, D_{2}^{†} = D_{2} .

It contains every tensor in $D_{first}$ .

Proof. By definition, $σ (D_{first}) = D_{first}$ . Since $D_{first} \subset D_{decl}$ , this implies $D_{first} \subset D_{cmp}$ . Also

σ (D_{cmp}) = σ (D_{decl}) \cap D_{decl} = D_{cmp} .

Because dagger commutes with flip and preserves $D_{decl}$ ,

D_{cmp}^{†} = D_{decl} \cap σ (D_{decl}) = D_{cmp} .

Consequently $γ = σ †$ preserves $D_{cmp}$ . Every generator in (eq:fixed-domain) therefore belongs to $D_{cmp}$ . Applying either involution permutes these generators; antilinearity of $γ$ preserves their complex span.

Displayed formulas in this passage

unlabeled · line 459
$D_{2} \subset D_{cmp}, σ (D_{2}) = D_{2}, γ (D_{2}) = D_{2}, D_{2}^{†} = D_{2} .$
unlabeled · line 472
$σ (D_{cmp}) = σ (D_{decl}) \cap D_{decl} = D_{cmp} .$
unlabeled · line 477
$D_{cmp}^{†} = D_{decl} \cap σ (D_{decl}) = D_{cmp} .$

Proposition: Domain stability

Displayed formulas in this passage

Nearby in this section