Finite additive readouts of one coherent source determine quotient blocks and flat marginals.
All notation uses the Lean definitions in FiniteAdditiveReadoutBlocks: BlockQuotient is G modulo kernelSum(alpha,beta), which is alpha.ker sup beta.ker; actualCoefficient is the normalized source sum; actualJoint is its outer product; actualReducedA and actualReducedB are partialTraceRight and partialTraceLeft of that joint matrix. leftVectors and rightVectors are the normalized block columns; blockWeight is card(alpha.ker) times card(beta.ker) divided by card(G). The formula names refer to those definitions, with real weights coerced to complex scalars for matrix and vector operations, and natural cardinalities coerced to reals in Real.log and Real.sqrt.
For finite additive commutative groups G, A and B, the two additive readouts alpha and beta have a jointly injective paired map. Every matrix here is computed from the source sum normalized by the square root of the source cardinality. The quotient is G modulo the sum of the readout kernels. The positive block weight is the product of their cardinalities divided by the source cardinality. Logarithms are natural logarithms.
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/FiniteAdditiveReadoutSpectrum.actual_eigenspaces (✓ std3). ∎
Source. Repository-derived.
Commentary.
On either side, a vector has eigenvalue equal to the positive block weight exactly when it lies in the range of that side’s block-column matrix. The zero eigenspace is the kernel of its conjugate transpose. The positive eigenspaces have dimension equal to the quotient cardinality; the zero eigenspaces have the ambient dimension minus that cardinality.
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/FiniteAdditiveReadoutSpectrum.actual_flat_reductions (✓ std3). ∎
Source. Repository-derived.
Commentary.
The kernels intersect only at zero, their sum has the product cardinality, and the source cardinality is that product times the quotient cardinality. The block weight is the reciprocal quotient cardinality. Both actual marginals have trace one and rank equal to the quotient cardinality, as does the actual coefficient matrix. Their positive eigenvalues equal the block weight with that multiplicity; all remaining eigenvalues are zero. The von Neumann entropy of either actual marginal is the logarithm of the quotient cardinality, equal to the source-cardinality logarithm minus the two kernel-cardinality logarithms. The actual coefficient map between Euclidean spaces has the square root of the block weight as each positive singular value, repeated the quotient cardinality times, with every subsequent singular value zero.
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/FiniteAdditiveReadoutSpectrum.actual_joint_state (✓ std3). ∎
Source. Repository-derived.
Commentary.
The outer product of the actual coefficients is positive semidefinite and Hermitian, has trace and rank one, and is idempotent. The coefficient norm square is one. The sum of the actual source basis kets equals the coefficient vector coordinate by coordinate, and equals the sum of the products of the normalized block vectors scaled by the square root of the block weight.