Operational Completeness and Classical Separation

Abstract

Full finite-window operations and state tomography do not yield a multiplicative classical state.

Theorem 1.1 (Operational completeness does not imply classical completeness).

$$\begin{array}{c}\forall M\in {\mathbb{N}}_{>1},\\ \mathrm{Generated}\left(\mathrm{clock}\left(M\right),\mathrm{shift}\left(M\right)\right)=\mathrm{Matrix}\left(M\right)\wedge \\ \mathrm{centralizer}\left(\mathrm{Generated}\left(\mathrm{clock}\left(M\right),\mathrm{shift}\left(M\right)\right)\right)=\mathrm{Scalars}\left(M\right)\wedge \mathrm{Char}\left(\mathrm{Generated}\left(\mathrm{clock}\left(M\right),\mathrm{shift}\left(M\right)\right)\right)=\varnothing \wedge \\ (\forall \rho ,\sigma ,\mathrm{Density}\left(\rho ,M\right)\wedge \mathrm{Density}\left(\sigma ,M\right)\wedge (\forall A,\mathrm{omega}\left(\rho ,A\right)=\mathrm{omega}\left(\sigma ,A\right))\Rightarrow \rho =\sigma )\wedge \\ (\forall \rho ,\mathrm{Density}\left(\rho ,M\right)\Rightarrow \mathrm{Linear}\left(\mathrm{omega}\left(\rho \right)\right)\wedge \mathrm{Positive}\left(\mathrm{omega}\left(\rho \right)\right)\wedge \mathrm{omega}\left(\rho ,I\right)=1)\wedge \\ \exists \rho ,A,B,\mathrm{Density}\left(\rho ,M\right)\wedge \mathrm{omega}\left(\rho ,A\right)=0\wedge \mathrm{omega}\left(\rho ,B\right)=0\wedge \mathrm{omega}\left(\rho ,AB\right)=1.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/WindowAlgebra/OperationalClassicalSeparation.operational_complete_not_classically_complete (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every finite cyclic window with more than one address, the algebra generated by the canonical clock and shift is the full matrix algebra. Its canonical centralizer is exactly the scalar matrices, and the generated algebra has no unital complex character.

The trace functional is imported from the matrix-state family. Trace expectations against all matrices separate positive trace-one density matrices, while each such density gives a normalized complex-linear functional that is nonnegative on adjoint squares.

The final clause constructs the basis density at address zero and the opposite matrix units from zero to one and one to zero. Their individual expectations vanish, but the expectation of their product is one, so the state is explicitly not multiplicative.

The proof applies the existing window generation, scalar commutant, character exclusion, and matrix-state cone results together with Mathlib’s trace-pairing separation and matrix-unit identities. No existing declaration combined all six public clauses.

References

• Truth anchor: D5/S3/Observer/WindowAlgebra/OperationalClassicalSeparation.operational_complete_not_classically_complete
• Dependency: D5/S3/Observer/WindowAlgebra/WindowGeneration
• Dependency: D5/S3/Observer/WindowCharacter
• Dependency: D5/S3/QuantumStates/GNSStateCone
• Dependency: D5/S3/QuantumStates/GNSZeroPropagation