Finite additive readouts of one coherent source determine quotient blocks and flat marginals.
Notation is the named Lean definition, not an independent block model. Write K = kernelSum(alpha,beta) = alpha.ker sup beta.ker and Q = BlockQuotient(alpha,beta) = G / K. leftBlock(alpha,beta,q,a) means there is x in G with quotient class q and alpha(x) = a; rightBlock uses beta(x) = b. actualCoefficient(alpha,beta)(a,b) is the source sum below; actualJoint(alpha,beta)(p,r) is actualCoefficient at p times the conjugate of actualCoefficient at r. actualReducedA and actualReducedB are respectively partialTraceRight and partialTraceLeft of actualJoint. leftVectors(alpha,beta)(a,q) and rightVectors(alpha,beta)(b,q) are the normalized block indicators shown below; blockWeight is real. All Fintype.card expressions use the displayed type; complex scalar multiplication coerces real weights to complex numbers, and Real.sqrt coerces natural cardinalities to reals. The displayed a, b, p, r, q are arbitrary elements of A, B, A times B, A times B, Q.
The source G and label spaces A and B are finite additive commutative groups. The maps alpha and beta are additive homomorphisms from that same source, and the paired map is injective. Blocks are indexed by G modulo the sum of the two kernels. Source amplitudes are divided by the square root of the source cardinality; labels outside a readout image have zero amplitude.
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/FiniteAdditiveReadoutBlocks.paired_block_iff (✓ std3). ∎
Source. Repository-derived.
Commentary.
A pair of readout labels comes from one source element exactly when the two labels occur in the same quotient block. The kernel sum lets representatives on the two sides be joined into one source. This criterion itself requires neither finiteness nor joint injectivity.
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/FiniteAdditiveReadoutBlocks.actual_coefficient_block (✓ std3). ∎
Source. Repository-derived.
Commentary.
For a jointly injective pair of readouts, each coefficient of the actual source sum is the normalized indicator of its unique quotient block. The assertion comes from the source sum, rather than a prescribed block matrix.
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/FiniteAdditiveReadoutBlocks.source_coset_product (✓ std3). ∎
Source. Repository-derived.
Commentary.
The paired readout restricts to a bijection from each source coset onto the product of its left and right label blocks. Both coordinates of the bijection are the original readout values.
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/FiniteAdditiveReadoutBlocks.actual_block_matrices (✓ std3). ∎
Source. Repository-derived.
Commentary.
Normalized left and right block columns are orthonormal. The actual coefficient matrix factors through these columns with the square-root block weight. Taking its two actual partial traces gives scaled block projections, their column actions, and zero action on the respective conjugate-transpose kernels. Both block projections are Hermitian and idempotent. The blocks on each side are disjoint and their union is precisely that readout’s image. Left and right blocks have the respective opposite kernel cardinalities. For every chosen representative, their labels are its readout translated by the opposite kernel image. Both reductions square to the block weight times themselves. Their entries are the same-block indicators summed over the quotient and scaled by the corresponding kernel cardinality divided by the source cardinality. The quotient cardinality is bounded by both ambient label cardinalities.