Product Dynamics Local Support

Abstract

Product pullbacks preserve exact local support or lower it within the active factors.

Theorem 1.1 (Product pullbacks cannot create support outside the active set).

$$\begin{array}{c}\forall \iota :\mathrm{Type}(),\mathrm{DecidableEq}(\iota ),\\ M:\iota \to \mathrm{Type}(),\\ (\forall i:\iota ,\mathrm{AddCommGroup}(M\left(i\right))\wedge \mathrm{Module}(\mathbb{R},M\left(i\right))),\\ I:\prod _{i:\iota }M\left(i\right),tr:\prod _{i:\iota }\mathrm{LinearMap}(\mathbb{R},M\left(i\right),\mathbb{R}),\\ (\forall i:\iota ,tr\left(i\right)\left(I\left(i\right)\right)=1),\\ phi:\prod _{i:\iota }\mathrm{LinearMap}(\mathbb{R},M\left(i\right),M\left(i\right)),\\ (\forall i:\iota ,phi\left(i\right)\left(I\left(i\right)\right)=I\left(i\right)),\\ S:\mathrm{Finset}(\iota ),\\ \text{let }U:\prod _{i:\iota }\mathrm{Submodule}(\mathbb{R},M\left(i\right)):=i\mapsto \mathrm{span}(\mathbb{R},\{I\left(i\right)\});\\ Z:\prod _{i:\iota }\mathrm{Submodule}(\mathbb{R},M\left(i\right)):=i\mapsto \ker (tr\left(i\right));\\ V:\mathrm{Finset}(\iota )\to \mathrm{Submodule}(\mathbb{R},\mathrm{PiTensorProduct}(\mathbb{R},M)):=R\mapsto \mathrm{range}(\mathrm{PiTensorMapIncl}(\mathbb{R},\mathrm{factorFamily}(i\mapsto \mathrm{ifMem}(i,R,Z\left(i\right),U\left(i\right)))));\\ pullback:\mathrm{LinearMap}(\mathbb{R},\mathrm{PiTensorProduct}(\mathbb{R},M),\mathrm{PiTensorProduct}(\mathbb{R},M)):=\mathrm{PiTensorMap}(\mathbb{R},phi);\\ (\forall A:\mathrm{PiTensorProduct}(\mathbb{R},M),A\in V\left(S\right)\Rightarrow pullback\left(A\right)\in \mathrm{iSup}(\{T:\mathrm{Finset}(\iota )\mid T\subseteq S\},T\mapsto V\left(T\right)))\wedge \\ ((\forall i:\iota ,\mathrm{map}(phi\left(i\right),Z\left(i\right))\subseteq Z\left(i\right))\Rightarrow \\ \forall A:\mathrm{PiTensorProduct}(\mathbb{R},M),A\in V\left(S\right)\Rightarrow pullback\left(A\right)\in V\left(S\right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/ProductDynamicsLocalSupport.product_pullback_local_support (✓ std3). ∎

Source. Repository-derived.

Commentary.

A normalized identity direction and a local trace map construct the scalar sector U as its real span and the trace-zero sector Z as the trace kernel. No abstract sector decomposition is assumed.

The dynamics is the canonical tensor map induced by the local linear pullbacks. Scalar-sector invariance prevents a new active factor; multilinearity expands every active local sum over subsets of S.

If the local pullbacks also preserve every Z sector, the same restriction map factors the product pullback through the original sector V(S).

References

• Truth anchor: D5/S3/Quantum/Dynamics/ProductDynamicsLocalSupport.product_pullback_local_support