Permanent Stability of Sequential Visible Spaces

Abstract

A stable sequential word-effect span remains stable at every later depth.

Theorem 1.1 (One stable sequential stage is permanently stable).

$$\begin{array}{c}\forall d:Nat,A:\mathrm{Type},\\ J:A\to \mathrm{LinearMap}(\mathbb{R},\mathrm{HermitianSpace}(d),\mathrm{HermitianSpace}(d)),n:Nat,\\ \mathrm{span}(\mathbb{R},\{\mathrm{sequentialWordEffect}(J,w)\mid w:\mathrm{List}(A),\mathrm{length}(w)\le n+1\})=\mathrm{span}(\mathbb{R},\{\mathrm{sequentialWordEffect}(J,w)\mid w:\mathrm{List}(A),\mathrm{length}(w)\le n\})\Rightarrow \\ \forall m:Nat,n\le m\Rightarrow \mathrm{span}(\mathbb{R},\{\mathrm{sequentialWordEffect}(J,w)\mid w:\mathrm{List}(A),\mathrm{length}(w)\le m\})=\mathrm{span}(\mathbb{R},\{\mathrm{sequentialWordEffect}(J,w)\mid w:\mathrm{List}(A),\mathrm{length}(w)\le n\}).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/SequentialVisibleSpaceStability.sequential_visible_space_once_stable_permanently (✓ std3). ∎

Source. Repository-derived.

Commentary.

The branch alphabet indexes real-linear Heisenberg dual maps on the full Hermitian matrix carrier. Each finite word effect is the existing source-order fold of those maps applied to identity.

At depth k the visible space is stated directly as the real span of all word effects of length at most k. No parallel visible-space definition is introduced.

Consecutive-stage equality makes the stable span invariant under every branch dual. Word induction then puts every longer effect in that span, while the depth inequality supplies the reverse inclusion.

References

• Truth anchor: D5/S3/Quantum/Tomography/SequentialVisibleSpaceStability.sequential_visible_space_once_stable_permanently
• Dependency: D5/S3/Quantum/Completion/SequentialWordObservationResidual