Future Words and Orthogonal Residuals

Abstract

Finite expectation words characterize residuals and visible projections.

Theorem 1.1 (Finite-word equality is orthogonal-residual equivalence).

$$\forall k,E,S:\mathrm{Type},[\mathrm{RCLike}(k)],[\mathrm{NormedAddCommGroup}(E)],[{\mathrm{InnerProductSpace}}_k(E)],[{\mathrm{FiniteDimensional}}_k(E)],m\in \mathbb{N},e:\mathrm{Fin}(m+1)\to E,X:S\to E,\rho ,\sigma \in S,((W_m^{e,X}(\rho )=W_m^{e,X}(\sigma ))\iff (X(\rho )-X(\sigma )\in {\mathrm{span}}_k(\mathrm{range}(e){)}^{\perp }))\wedge ((X(\rho )-X(\sigma )\in {\mathrm{span}}_k(\mathrm{range}(e){)}^{\perp })\iff (P_{{\mathrm{span}}_k(\mathrm{range}(e))}(X(\rho ))=P_{{\mathrm{span}}_k(\mathrm{range}(e))}(X(\sigma )))).$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/FutureWordOrthogonalResidual.future_word_orthogonal_residual (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let a finite family of effects generate the visible subspace. The expectation word of a represented state records its inner product with each effect. Equality of two such words is equivalent to the difference of the represented states lying in the orthogonal complement of the visible span.

The same residual condition is equivalent to equality of the two canonical orthogonal projections onto the visible span. Both equivalences appear as explicit conjuncts in the named theorem.

Repository search found the existing complementary-projection machinery but no theorem with this complete finite-word characterization. Loogle returned exact single hits for the span-induction, orthogonality, and zero-projection declarations applied by the proof. The attempted shaped LeanSearch API query returned HTTP 404.

References

• Truth anchor: D5/S3/Quantum/Algebra/FutureWordOrthogonalResidual.future_word_orthogonal_residual
• Dependency: D5/S3/Quantum/Algebra/OrthogonalProjectionComplement