Unique Descent on the Final Orthogonal Residual

Abstract

The orthogonal residual of an iterated observable closure is invariant and has a unique quotient descent.

Theorem 1.1 (The final orthogonal residual is invariant and has a unique quotient descent).

$$\begin{gathered} \forall V:\mathrm{Type},[\mathrm{NormedAddCommGroup}(V)],[{\mathrm{InnerProductSpace}}_{\mathbb{R}}(V)],[{\mathrm{FiniteDimensional}}_{\mathbb{R}}(V)],K:{\mathrm{LinearMap}}_{\mathbb{R}}(V\to V),Phi:{\mathrm{LinearMap}}_{\mathbb{R}}(V\to V),W:\mathrm{Submodule}(\mathbb{R},V),\forall x,a,\mathrm{inner}(\mathbb{R},Phi(x),a)=\mathrm{inner}(\mathbb{R},x,K(a))\Rightarrow (\forall x,x\in \mathrm{observableClosureUnique}(K,W{)}^{\perp },Phi(x)\in \mathrm{observableClosureUnique}(K,W{)}^{\perp })\wedge \\ \exists induced:{\mathrm{LinearMap}}_{\mathbb{R}}(\mathrm{Quotient}(\mathrm{observableClosureUnique}(K,W{)}^{\perp })\to \mathrm{Quotient}(\mathrm{observableClosureUnique}(K,W{)}^{\perp })),(\forall x,induced(\mathrm{mkQ}(\mathrm{observableClosureUnique}(K,W{)}^{\perp },x))=\mathrm{mkQ}(\mathrm{observableClosureUnique}(K,W{)}^{\perp },Phi(x))\wedge \forall other:{\mathrm{LinearMap}}_{\mathbb{R}}(\mathrm{Quotient}(\mathrm{observableClosureUnique}(K,W{)}^{\perp })\to \mathrm{Quotient}(\mathrm{observableClosureUnique}(K,W{)}^{\perp })),\forall x,other(\mathrm{mkQ}(\mathrm{observableClosureUnique}(K,W{)}^{\perp },x))=\mathrm{mkQ}(\mathrm{observableClosureUnique}(K,W{)}^{\perp },Phi(x))\Rightarrow other=induced). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/QuantumStates/DynamicsResidualQuotientUnique.dynamics_residual_invariant_and_unique_quotient (✓ std3). ∎

Source. Repository-derived.

Commentary.

The visible space is constructed from every forward iterate of the adjoint observable map K applied to the source visible subspace W. The residual is its orthogonal complement.

The adjoint pairing transfers orthogonality through Phi, and the public existence-unique clause states that exactly one linear map on the quotient satisfies the projection law.

Repository search found no exact theorem packaging the invariant residual with unique quotient descent. Pinned Mathlib supplies and is applied through Submodule.mem_orthogonal’, Submodule.liftQ, Submodule.liftQ_apply, Submodule.Quotient.mk_eq_zero, and Submodule.mkQ_surjective.

References

• Truth anchor: D5/S3/QuantumStates/DynamicsResidualQuotientUnique.dynamics_residual_invariant_and_unique_quotient