Sector Schmidt Encodings

Abstract

Dependent sector coordinates and the normalized source and flat target encoding matrices.

Sector and Coord are finite types with decidable equality. The natural number d(s) is the target rank of sector s. sourceFiber(d,Coord,s) is Fin(d(s)) times Coord, while targetFiber(d,s) is Fin(d(s)). Sigma forms the dependent sum over Sector. Each such coordinate x has sector(x); a source coordinate also has residual(x) in Coord. ofNat and ofReal denote the real and complex scalar embeddings.

Definition 1.1 (Source coordinates).

$$\forall Sector\in FiniteType,Coord\in FiniteType,d\in \mathrm{Function}\left(Sector,\mathbb{N}\right),\mathrm{SourceLocal}\left(d,Coord\right)=\mathrm{Sigma}\left(Sector,\mathrm{sourceFiber}\left(d,Coord\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/SectorSchmidtEncoding.SourceLocal (✓ std3).

Source. Repository-derived.

Commentary.

A source coordinate contains its sector, one target coordinate, and one residual spectral coordinate.

Definition 1.2 (Target coordinates).

$$\forall Sector\in FiniteType,d\in \mathrm{Function}\left(Sector,\mathbb{N}\right),\mathrm{TargetLocal}\left(d\right)=\mathrm{Sigma}\left(Sector,\mathrm{targetFiber}\left(d\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/SectorSchmidtEncoding.TargetLocal (✓ std3).

Source. Repository-derived.

Commentary.

A target coordinate contains its sector and one coordinate within the sector rank.

Definition 1.3 (Source encoding matrix).

$$\forall Sector\in FiniteType,Coord\in FiniteType,d\in \mathrm{Function}\left(Sector,\mathbb{N}\right),\forall spectrum\in \mathrm{Function}\left(Sector,\mathrm{Function}\left(Coord,\mathbb{R}\right)\right),x\in \mathrm{SourceLocal}\left(d,Coord\right),y\in \mathrm{SourceLocal}\left(d,Coord\right),s\in Sector,\mathrm{entry}\left(\mathrm{sourceEncoding}\left(d,spectrum\right),\mathrm{pair}\left(x,y\right),s\right)=\mathrm{ite}\left(x=y\wedge \mathrm{sector}\left(x\right)=s,\mathrm{ofReal}\left(\mathrm{sqrt}\left(\frac{\mathrm{apply}\left(spectrum,\mathrm{sector}\left(x\right),\mathrm{residual}\left(x\right)\right)}{\mathrm{ofNat}\left(\mathrm{apply}\left(d,\mathrm{sector}\left(x\right)\right)\right)}\right)\right),0\right)$$

Formalization. D5/S3/Quantum/Entanglement/SectorSchmidtEncoding.sourceEncoding (✓ std3).

Source. Repository-derived.

Commentary.

The source matrix is diagonal across the two physical sides. In sector s each residual value is repeated d(s) times, with amplitude sqrt(spectrum(s,j)/d(s)). Positive ranks and normalized nonnegative spectra make these columns unit vectors; distinct sector columns have disjoint support.

Definition 1.4 (Flat target encoding matrix).

$$\forall Sector\in FiniteType,d\in \mathrm{Function}\left(Sector,\mathbb{N}\right),\forall x\in \mathrm{TargetLocal}\left(d\right),y\in \mathrm{TargetLocal}\left(d\right),s\in Sector,\mathrm{entry}\left(\mathrm{targetEncoding}\left(d\right),\mathrm{pair}\left(x,y\right),s\right)=\mathrm{ite}\left(x=y\wedge \mathrm{sector}\left(x\right)=s,\mathrm{ofReal}\left(\mathrm{sqrt}\left(\mathrm{inv}\left(\mathrm{ofNat}\left(\mathrm{apply}\left(d,\mathrm{sector}\left(x\right)\right)\right)\right)\right)\right),0\right)$$

Formalization. D5/S3/Quantum/Entanglement/SectorSchmidtEncoding.targetEncoding (✓ std3).

Source. Repository-derived.

Commentary.

The target matrix has equal amplitude sqrt(1/d(s)) on the diagonal coordinates of sector s. Positive sector ranks make its columns unit vectors with disjoint sector supports.

References

• Truth anchor: D5/S3/Quantum/Entanglement/SectorSchmidtEncoding.SourceLocal
• Truth anchor: D5/S3/Quantum/Entanglement/SectorSchmidtEncoding.TargetLocal
• Truth anchor: D5/S3/Quantum/Entanglement/SectorSchmidtEncoding.sourceEncoding
• Truth anchor: D5/S3/Quantum/Entanglement/SectorSchmidtEncoding.targetEncoding
• Dependency: D5/S3/Quantum/Foundation/FiniteStateChannel