Empirical/CSD: superdense coding (CSD-side reading) #
Category: 3-Local (CSD-side companion to
Empirical/QM/Resources/SuperdenseCoding.lean).
Pairs with the QM-side file (Bennett-Wiesner 1992). The QM file proves
the four encoding identities (I⊗I)|Φ⁺⟩ = |Φ⁺⟩, (X⊗I)|Φ⁺⟩ = |Ψ⁺⟩,
(Z⊗I)|Φ⁺⟩ = |Φ⁻⟩, (XZ⊗I)|Φ⁺⟩ = −|Ψ⁻⟩ and the ten-conjunct
bell_basis_orthonormal. Together these give the two-classical-bits
content: the four single-qubit operations on Alice's half of a Bell
pair carry |Φ⁺⟩ to four orthonormal Bell states, perfectly
distinguishable by a Bell-basis measurement on Bob's side.
This file states the CSD volume-ratio reading: under CSD's ontic
substrate, each two-qubit encoding unitary is realised as a
measure-preserving π-equivariant flow on Σ² (LF4-todo §13.2), and
the Bell-basis measurement is realised through the §14 observable
correspondence on the four Bell projectors. The protocol's two-bit
content lifts to the ontic level.
Polarity (transport, tag bundle) #
Parameter-free numerical content (specific encoding identities + the
orthonormality theorem). The bundle is a tag bundle like
SternGerlach: extends CSDBridge.Context D with no new fields; its
existence is the load-bearing realisability assertion.
LF4 obligations carried #
- §13.2 (general N-qubit unitary realised as Σ-flow): for the
three encoding unitaries
X⊗I,Z⊗I,XZ⊗I(acting on the 2-qubit tensor space). - §14 (observable correspondence): for the four Bell-state projectors used in Bob's measurement.
Both are extant LF4-todo obligations; the bundle does not introduce new ones.
Schema-mismatch acknowledgement #
Bundle fields are Hilbert-side only (in fact, no fields beyond
Context D). The CSD-realisability claim is prose-only; Lean does
not check it. See PLACEHOLDERS.md §7.
Experimental verification #
Mattle, Weinfurter, Kwiat, Zeilinger 1996 Phys. Rev. Lett. 76, 4656 (first experimental superdense coding with polarisation-entangled photons).
Source #
Bennett and Wiesner 1992, Phys. Rev. Lett. 69, 2881.
SCHEMA-MISMATCH: tag bundle; no fields beyond Context D.
See module docstring + PLACEHOLDERS.md §7.
CSD superdense-coding bundle. Extends CSDBridge.Context D with
no additional fields. Its existence is the load-bearing assertion
that:
- The three encoding unitaries
X⊗I,Z⊗I,XZ⊗Ion the 2-qubit tensor space are realised as measure-preserving π-equivariant flows onΣ²(LF4-todo §13.2); - The four Bell-state projectors are realised as ontic observables through the §14 observable correspondence.
Together these underwrite the protocol's two-classical-bits-per-qubit content at the ontic level.
Status: load-bearing, externally supplied, undischarged. LF4-todo §13.2 + §14.
- bridge : LF2.MeasureBridgeData D self.μFS
Instances For
Transport-only encoding identities (CSD reading) #
Each theorem below transports a QM-side superdense-coding encoding identity through the bundle. Foundational triple only.
CSD (I⊗I)|Φ⁺⟩ = |Φ⁺⟩ (trivial encoding, two-bit message 00).
Transported from Empirical.QM.SuperdenseCoding.encode_I.
CSD (X⊗I)|Φ⁺⟩ = |Ψ⁺⟩ (encoding two-bit message 01).
Transported from Empirical.QM.SuperdenseCoding.encode_X.
CSD (Z⊗I)|Φ⁺⟩ = |Φ⁻⟩ (encoding two-bit message 10).
Transported from Empirical.QM.SuperdenseCoding.encode_Z.
CSD (XZ⊗I)|Φ⁺⟩ = −|Ψ⁻⟩ (encoding two-bit message 11; phase
−1 does not affect orthogonality). Transported from
Empirical.QM.SuperdenseCoding.encode_XZ.
CSD Bell-basis orthonormality (perfect distinguishability).
The ten-conjunct theorem: six pairwise-orthogonality identities + four
unit-norm identities. Transported from
Empirical.QM.SuperdenseCoding.bell_basis_orthonormal.