Quotient-Compatible Residual Transport

Abstract

Isometric quotient transport preserves canonical residual norms and costs.

Theorem 1.1 (Quotient transport preserves residual cost).

$$\begin{array}{c}{M}_k\subset H_k,M_j\subset H_j,T_{kj}:H_k\to H_j,\\ T_{kj}(M_k)\subset M_j,T_{kj}(x_k)-x_j\in M_j,\\ \overline{T_{kj}}([x_k])=[x_j]\wedge \\ (\mathrm{Isometry}\left(\overline{T_{kj}}\right)\Rightarrow \\ \Vert x_k-P_{M_k}(x_k)\Vert =\Vert x_j-P_{M_j}(x_j)\Vert \wedge \\ \frac{1}{2}\Vert x_k-P_{M_k}(x_k){\Vert }^2=\frac{1}{2}\Vert x_j-P_{M_j}(x_j){\Vert }^2)\wedge \\ \exists f,g:\mathrm{ContinuousLinearMap}\left(\mathbb{R},\mathbb{R}\right),z\in \mathbb{R},\\ (\forall x,f(x)=0\iff g(x)=0)\wedge \\ \frac{1}{2}\Vert f(z){\Vert }^2\ne \frac{1}{2}\Vert g(z){\Vert }^2.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/QuotientResidualTransport.quotient_residual_transport_and_zero_set_countermodel (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let the two charts be real-or-complex inner-product spaces with closed subspaces admitting orthogonal projections. A continuous linear transition preserves the subspaces and carries the two selected points to the same target quotient class.

The quotient transition is constructed canonically with the quotient lift. When it is an isometry, the imported canonical quotient-to-orthogonal-complement equivalence identifies quotient norms with the norms of the two projection residuals. Their half-squared costs therefore agree.

The final conjunct gives two explicit continuous linear residual maps on the real line. They have exactly the same zero set, but their costs at the displayed point differ, so zero-set agreement alone cannot supply cost invariance.

References

• Truth anchor: D5/S3/Quantum/Fibers/QuotientResidualTransport.quotient_residual_transport_and_zero_set_countermodel
• Dependency: D5/S3/Quantum/Algebra/QuotientOrthogonalComplement