Finite Shifted Record Realization

Abstract

Concrete finite shifted records realize the normalized coefficient coherence channel.

Theorem 1.1 (Concrete normalized records and their signed overlaps).

$$\forall S\in FiniteType,N\in Nat,c\in \mathbb{Z}\to \mathbb{C},q\in S\to \mathbb{Z},\left(\left(\forall n\in \mathbb{Z},\left(n<0\vee N<n\right)\Rightarrow c\left(n\right)=0\right)\wedge \sum _{n\in \mathrm{Icc}\left(0,N\right)}\mathrm{norm}{\left(c\left(n\right)\right)}^2=1\right)\Rightarrow \mathrm{let}Q=\sum _{i\in S}\mathrm{natAbs}\left(q\left(i\right)\right);\mathrm{let}L=N+2\cdot Q+1;\mathrm{let}D=\mathrm{Icc}\left(-Q,N+Q\right);\mathrm{let}\forall a\in \mathrm{Fin}\left(L\right),coord\left(a\right)=\mathrm{int}\left(a\right)-Q;\mathrm{let}\forall i\in S,a\in \mathrm{Fin}\left(L\right),E\left(i\right)\left(a\right)=c\left(coord\left(a\right)+q\left(i\right)\right);\mathrm{let}\forall ell\in \mathbb{Z},\gamma \left(ell\right)=\sum _{n\in \mathrm{Icc}\left(0,N\right)}c\left(n+ell\right)\cdot \mathrm{conj}\left(c\left(n\right)\right);\left(\left(\left(\mathrm{range}\left(coord\right)=D\wedge \mathrm{Injective}\left(coord\right)\right)\wedge \left(\forall i\in S,m\in \mathbb{Z},c\left(m+q\left(i\right)\right)\ne 0\Rightarrow m\in D\right)\right)\wedge \left(\forall i\in S,\sum _{a\in \mathrm{Fin}\left(L\right)}\mathrm{norm}{\left(E\left(i\right)\left(a\right)\right)}^2=1\right)\right)\wedge \left(\forall i\in S,j\in S,\sum _{a\in \mathrm{Fin}\left(L\right)}\mathrm{conj}\left(E\left(j\right)\left(a\right)\right)\cdot E\left(i\right)\left(a\right)=\gamma \left(q\left(i\right)-q\left(j\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Decoherence/FiniteShiftedRecordChannel.shifted_coefficient_records (✓ std3). ∎

Source. Repository-derived.

Commentary.

S is an arbitrary finite system basis. Integer labels q may repeat or be negative, and S may be empty. The coefficient function is zero outside the integer interval from zero to N and its squared norms sum to one. Q is the sum of absolute labels, so the explicit interval D contains every shifted support. Its coordinate enumeration is both onto D and injective. The record norms and overlaps follow from the coefficient hypotheses by finite reindexing; they are conclusions, not additional hypotheses.

Theorem 1.2 (Finite unit-norm records give a complete diagonal Kraus family).

$$\forall I\in Type,[\mathrm{Fintype}\left(I\right)][\mathrm{DecidableEq}\left(I\right)]\forall E\in Type,[\mathrm{Fintype}\left(E\right)]\forall record\in I\to \left(E\to \mathbb{C}\right),\left(\forall i\in I,\sum _{a:E}\mathrm{norm}{\left(record\left(i\right)\left(a\right)\right)}^2=1\right)\Rightarrow \sum _{a:E}Matrix.diagonal{\left((fun(i:I)\mapsto record\left(i\right)\left(a\right))\right)}^{\ast }\cdot Matrix.diagonal\left((fun(i:I)\mapsto record\left(i\right)\left(a\right))\right)=1$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Decoherence/FiniteShiftedRecordChannel.diagonal_kraus_complete (✓ std3). ∎

Source. Repository-derived.

Commentary.

For finite index types ι and ε, any complex record whose rows have squared norm one yields diagonal Kraus operators whose adjoint products sum to the identity matrix. The theorem is uniform in both finite carriers and the record values.

Theorem 1.3 (The diagonal Kraus action entry).

$$\forall I\in Type,\forall E\in Type,[\mathrm{Fintype}\left(I\right)][\mathrm{DecidableEq}\left(I\right)][\mathrm{Fintype}\left(E\right)]\forall record\in I\to \left(E\to \mathbb{C}\right),rho\in \mathrm{Matrix}\left(I,I,\mathbb{C}\right),i\in I,j\in I,(\sum _{a:E}(Matrix.diagonal\left((fun(i:I)\mapsto record\left(i\right)\left(a\right))\right)\cdot rho\cdot Matrix.diagonal{\left((fun(i:I)\mapsto record\left(i\right)\left(a\right))\right)}^{\ast }))\left(i\right)\left(j\right)=(\sum _{a:E}\mathrm{star}\left(record\left(j\right)\left(a\right)\right)\cdot record\left(i\right)\left(a\right))\cdot rho\left(i\right)\left(j\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Decoherence/FiniteShiftedRecordChannel.diagonal_kraus_entry (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a finite record family, the (i,j) entry of the sum of diagonal Kraus actions on rho is the record Gram coefficient at (i,j) multiplied by rho(i,j). The displayed left side is the literal Kraus-sum entry; the right side computes its value.

Theorem 1.4 (The actual finite marginal is a completely positive trace-preserving channel).

$$\forall S\in FiniteType,N\in Nat,c\in \mathbb{Z}\to \mathbb{C},q\in S\to \mathbb{Z},\left(\left(\forall n\in \mathbb{Z},\left(n<0\vee N<n\right)\Rightarrow c\left(n\right)=0\right)\wedge \sum _{n\in \mathrm{Icc}\left(0,N\right)}\mathrm{norm}{\left(c\left(n\right)\right)}^2=1\right)\Rightarrow \mathrm{let}Q=\sum _{i\in S}\mathrm{natAbs}\left(q\left(i\right)\right);\mathrm{let}L=N+2\cdot Q+1;\mathrm{let}D=\mathrm{Icc}\left(-Q,N+Q\right);\mathrm{let}\forall a\in \mathrm{Fin}\left(L\right),coord\left(a\right)=\mathrm{int}\left(a\right)-Q;\mathrm{let}\forall i\in S,a\in \mathrm{Fin}\left(L\right),E\left(i\right)\left(a\right)=c\left(coord\left(a\right)+q\left(i\right)\right);\mathrm{let}\forall ell\in \mathbb{Z},\gamma \left(ell\right)=\sum _{n\in \mathrm{Icc}\left(0,N\right)}c\left(n+ell\right)\cdot \mathrm{conj}\left(c\left(n\right)\right);\mathrm{let}\forall i\in S,a\in \mathrm{Fin}\left(L\right),j\in S,\mathrm{entry}\left(V,\mathrm{pair}\left(i,a\right),j\right)=\mathrm{ite}\left(j=i,E\left(i\right)\left(a\right),0\right);\mathrm{let}\forall X\in \mathrm{Matrix}\left(S\times \mathrm{Fin}\left(L\right),S\times \mathrm{Fin}\left(L\right),\mathbb{C}\right),i\in S,j\in S,\mathrm{entry}\left(T\left(X\right),i,j\right)=\sum _{a\in \mathrm{Fin}\left(L\right)}\mathrm{entry}\left(X,\mathrm{pair}\left(i,a\right),\mathrm{pair}\left(j,a\right)\right);\mathrm{let}\forall rho\in \mathrm{Matrix}\left(S,S,\mathbb{C}\right),\Lambda \left(rho\right)=T\left(V\cdot rho\cdot V^{\ast }\right);\left(\left(\left(\left(\left(\left(\left(\left(\mathrm{range}\left(coord\right)=D\wedge \mathrm{Injective}\left(coord\right)\right)\wedge \left(\forall i\in S,m\in \mathbb{Z},c\left(m+q\left(i\right)\right)\ne 0\Rightarrow m\in D\right)\right)\wedge \left(\forall i\in S,\sum _{a\in \mathrm{Fin}\left(L\right)}\mathrm{norm}{\left(E\left(i\right)\left(a\right)\right)}^2=1\right)\right)\wedge \left(\forall i\in S,j\in S,\sum _{a\in \mathrm{Fin}\left(L\right)}\mathrm{conj}\left(E\left(j\right)\left(a\right)\right)\cdot E\left(i\right)\left(a\right)=\gamma \left(q\left(i\right)-q\left(j\right)\right)\right)\right)\wedge \left(\forall ell\in \mathbb{Z},\gamma \left(ell\right)=\sum _{n\in \mathbb{Z}}c\left(n+ell\right)\cdot \mathrm{conj}\left(c\left(n\right)\right)\right)\right)\wedge V^{\ast }\cdot V=1\right)\wedge \left(\exists C\in \mathrm{QuantumChannel}\left(S,S\right),\forall rho\in \mathrm{Matrix}\left(S,S,\mathbb{C}\right),\mathrm{fromCstar}\left(\mathrm{apply}\left(C,\mathrm{toCstar}\left(rho\right)\right)\right)=\Lambda \left(rho\right)\right)\right)\wedge \left(\forall rho\in \mathrm{Matrix}\left(S,S,\mathbb{C}\right),i\in S,j\in S,\mathrm{entry}\left(\Lambda \left(rho\right),i,j\right)=\gamma \left(q\left(i\right)-q\left(j\right)\right)\cdot \mathrm{entry}\left(rho,i,j\right)\right)\right)\wedge \left(\forall rho\in \mathrm{Matrix}\left(S,S,\mathbb{C}\right),\mathrm{trace}\left(\Lambda \left(rho\right)\right)=\mathrm{trace}\left(rho\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Decoherence/FiniteShiftedRecordChannel.finite_shifted_record_channel (✓ std3). ∎

Source. Repository-derived.

Commentary.

The actual recording V sends basis vector i to i tensored with E(i). T sums equal environment coordinates and Lambda is defined by applying T to V rho V adjoint. The channel is never defined by the desired entry formula. The frozen environment marginal theorem supplies that formula after finite-coordinate transport and substitution of the proved overlap.

QuantumChannel is the canonical FiniteStateChannel bundle of Mathlib CompletelyPositiveMap on CStarMatrix and trace preservation. Its positivity holds at every finite amplification, and both its equality with Lambda and the entry identity hold for every complex matrix. toCstar and fromCstar denote CStarMatrix.ofMatrix and its inverse; adjoint means conjugate transpose. The integer gamma sum is the tsum of the zero-extended coefficients.

This is one finite isometric realization. It makes no claim of energy conservation for a specified Hamiltonian, spatial locality, zero operation cost, or universality over all reference devices. QUANTUM-REALITY definition74.1 and theorem74.1 supply the source provenance; commentary there about existing repository code is not an extra mathematical claim.

References

• Truth anchor: D5/S3/Quantum/Decoherence/FiniteShiftedRecordChannel.diagonal_kraus_complete
• Truth anchor: D5/S3/Quantum/Decoherence/FiniteShiftedRecordChannel.diagonal_kraus_entry
• Truth anchor: D5/S3/Quantum/Decoherence/FiniteShiftedRecordChannel.finite_shifted_record_channel
• Truth anchor: D5/S3/Quantum/Decoherence/FiniteShiftedRecordChannel.shifted_coefficient_records
• Dependency: D5/S3/Quantum/Decoherence/EnvironmentMarginalChannel
• Dependency: D5/S3/Quantum/Foundation/FiniteKrausChannel