Empirical/CSD/Crypto: BB84 intercept-resend with a dynamical collapse step

Category: CSD bridge (dynamical). The second empirical entry consuming the measurement dynamics, and the first with a cross-basis sequential read.

The dissolved gate

Empirical/QM/Crypto/BB84.lean proves the intercept-resend QBER ¼ with an explicit scope note: Eve's measurement is a classical marginal over her outcomes, because a measurement-update (collapse) operator "remains out of scope — the same LF5 gate". That gate predates the dynamical measurement layer. This module replaces the posited marginal with the calibrated-swap dynamics: Eve's measure-and-resend step is csd_sequential_born — the collapse is a pushforward theorem, not a modelling assumption.

The round, and why it is the dual of the QM module's

The QM module's canonical sifted round is Alice Z, Bob Z, Eve X. Here we take the dual round Alice X (|+⟩), Bob X, Eve Z — so that Eve's measurement is in the computational basis, the calibrated-swap witness's native scope, and Bob's follow-up is the rotated (X-basis) context basisContext xBasisON from SigmaLayer/RotatedContext.lean. The two rounds have the same per-basis error values by the Z/X symmetry of the four states; bb84_dynamical_matches_marginal records that the dynamically derived numbers coincide with the QM module's classical-marginal ones.

Addendum 2026-08-02 — the dual-round caveat is retired: with the unitary-covariance law (SigmaLayer/RotatedSwap.lean, measurement_covariance), the primal round is now directly formalised too: bb84_primal_wrong_basis — Eve X-measures the Z-carrier |a⟩ (rotated selector, rotated bank), and whatever she records, Bob's Z-basin has probability exactly ½. Both rounds now run natively; neither needs the other's symmetry.

Unlike the eraser twin (QuantumEraserVolume.lean), where the cross-basis step was realised kinematically, both measurements here are context-field reads of the dynamical layer: Eve's via momentContext, Bob's via the rotated context — the sequential composition is end-to-end.

What this file proves

• bb84_eve_selector_born — Eve's Z-outcome weights on |+⟩ are ½, ½: she learns a fair coin, uncorrelated with Alice's X-bit (the information side of the tradeoff).
• bb84_eve_sector_pos — the conditioning is licensed: each Eve outcome has nonzero sector measure, proved from the preparation (prep_outcome_pos), not carried as a hypothesis.
• ★ bb84_wrong_basis_bob — after Eve's Z-measurement outcome i, Bob's X-basin j has probability ½, whatever i and j: the resent eigenstate is unbiased in the sifted basis, so Bob errs with probability ½ (bb84_wrong_basis_error). The disturbance side of the tradeoff, with the collapse a theorem.
• ★ bb84_right_basis_no_disturbance / bb84_right_basis_faithful — Eve in the matching basis is exactly repeatability: Bob's error basin is null, his correct basin has probability 1. Eve learns the bit and disturbs nothing.
• bb84_dynamical_matches_marginal — the per-basis values 0 and ½ and the assembled QBER ¼ agree with the QM module's irErrorZ0 marginal model (bb84_qber).

⚠️ Honest scope

One sifted round of the intercept-resend model, inheriting the calibrated-swap witness's scope notes (calibration posit; Hamiltonian origin §2a-scoped). Eve's basis choice and the ¼ average over it are classical bookkeeping, taken from the QM side. Full composable finite-key security remains the recorded QKD tranche (specs/future-work.md) — nothing beyond intercept-resend is claimed, matching the QM module's own boundary.

References

Empirical/QM/Crypto/BB84.lean (states, inner products, irErrorZ0, bb84_qber); Empirical/QM/Crypto/B92.lean (ketPlus_inner_self, ketPlus_unit, ketMinus_inner_ketPlus, half — reused, not re-proved); Empirical/CSD/SequentialMeasurement.lean (csd_sequential_born, csd_repeatability_*, readyPrep, prep_outcome_pos); SigmaLayer/RotatedContext.lean (basisContext, basisContext_rate_mk); SigmaLayer/SwapLuders.lean (swap_luders_born — the engine); SigmaLayer/DegenerateLuders.lean (vertexPoint, momentMap_vertex); Bennett–Brassard 1984; specs/BACKLOG.md; specs/future-work.md.

The X basis as an orthonormal basis

theorem CSD.Empirical.CSDBridge.BB84Sequential.ketPlus_inner_ket1 : inner ℂ BB84.ketPlus BB84.ket1 = (↑√2)⁻¹

The missing conjugate-order inner products: ⟨+|1⟩ = (√2)⁻¹.

theorem CSD.Empirical.CSDBridge.BB84Sequential.ketMinus_inner_ket1 : inner ℂ BB84.ketMinus BB84.ket1 = -(↑√2)⁻¹

⟨−|1⟩ = −(√2)⁻¹.

theorem CSD.Empirical.CSDBridge.BB84Sequential.ketMinus_inner_ketMinus : inner ℂ BB84.ketMinus BB84.ketMinus = 1

theorem CSD.Empirical.CSDBridge.BB84Sequential.ketPlus_inner_ketMinus : inner ℂ BB84.ketPlus BB84.ketMinus = 0

noncomputable def CSD.Empirical.CSDBridge.BB84Sequential.xVec : Fin 2 → EuclideanSpace ℂ (Fin 2)

The X-basis vectors, indexed.

Equations

• CSD.Empirical.CSDBridge.BB84Sequential.xVec 0 = CSD.Empirical.BB84.ketPlus
• CSD.Empirical.CSDBridge.BB84Sequential.xVec 1 = CSD.Empirical.BB84.ketMinus

theorem CSD.Empirical.CSDBridge.BB84Sequential.xVec_orthonormal : Orthonormal ℂ xVec

noncomputable def CSD.Empirical.CSDBridge.BB84Sequential.xBasisON : OrthonormalBasis (Fin 2) ℂ (EuclideanSpace ℂ (Fin 2))

The X basis as an OrthonormalBasis — Bob's sifted-basis apparatus.

Equations

• CSD.Empirical.CSDBridge.BB84Sequential.xBasisON = OrthonormalBasis.mk CSD.Empirical.CSDBridge.BB84Sequential.xVec_orthonormal CSD.Empirical.CSDBridge.BB84Sequential.xBasisON._proof_1

theorem CSD.Empirical.CSDBridge.BB84Sequential.xBasisON_apply (j : Fin 2) : xBasisON j = xVec j

The preparation |+⟩

theorem CSD.Empirical.CSDBridge.BB84Sequential.ketPlus_ne_zero : BB84.ketPlus ≠ 0

theorem CSD.Empirical.CSDBridge.BB84Sequential.momentMap_ketPlus (i : Fin 2) : LF4.momentMap (Projectivization.mk ℂ BB84.ketPlus ketPlus_ne_zero) i = 1 / 2

The Born weights of |+⟩ in the computational basis are ½, ½ — the states are mutually unbiased, transported from the QM module's inner products.

Bob's rotated context

theorem CSD.Empirical.CSDBridge.BB84Sequential.xContext_rate_vertex (i j : Fin 2) : (RecordLayer.basisContext xBasisON).rate (RecordLayer.vertexPoint i) j = 1 / 2

Bob's X-basis rate at Eve's resent eigenstate is ½, all four ways. The rotated context's rate at a computational vertex is the cross-basis Born weight — mutual unbiasedness, now as a context-field fact.

The wrong-basis round: Alice X, Eve Z, Bob X

theorem CSD.Empirical.CSDBridge.BB84Sequential.bb84_eve_selector_born (i : Fin 2) : (RecordLayer.epistemicMeasure (Projectivization.mk ℂ BB84.ketPlus ketPlus_ne_zero)) (RecordLayer.basinIndex (RecordLayer.momentContext 2) ⁻¹' {i}) = ENNReal.ofReal (1 / 2)

Eve's outcome weights are a fair coin. Measuring |+⟩ in the computational basis, each outcome carries weight ½ — Eve's record is uncorrelated with Alice's X-bit. The information side of the information–disturbance tradeoff, as basin measures.

theorem CSD.Empirical.CSDBridge.BB84Sequential.bb84_eve_sector_pos (i : Fin 2) : (RecordLayer.readyPrep (Projectivization.mk ℂ BB84.ketPlus ketPlus_ne_zero)) ((RecordLayer.shearProtocol (RecordLayer.basinIndex (RecordLayer.momentContext 2)) ⋯).outcomeSector i) ≠ 0

The conditioning is licensed by the preparation: each of Eve's outcome sectors has nonzero measure — a theorem (prep_outcome_pos), not a hypothesis.

theorem CSD.Empirical.CSDBridge.BB84Sequential.bb84_wrong_basis_bob (i j : Fin 2) : (SequentialMeasurement.postEnsemble (RecordLayer.readyPrep (Projectivization.mk ℂ BB84.ketPlus ketPlus_ne_zero)) i) ((fun (y : RecordLayer.SwapArena (LF4.KSigma 2) 2) => y.1.1) ⁻¹' RecordLayer.globalBasin (RecordLayer.basisContext xBasisON) j) = ENNReal.ofReal (1 / 2)

★ The disturbance, end-to-end dynamical. Alice sends |+⟩; Eve measures in the computational basis and the calibrated-swap dynamics resends her eigenstate; Bob reads the rotated X-context. Whatever Eve's outcome i, each of Bob's basins has probability exactly ½: the resent state is unbiased in the sifted basis. Both measurements are context-field reads of the dynamical layer — the collapse step is csd_sequential_born, not a classical marginal.

theorem CSD.Empirical.CSDBridge.BB84Sequential.bb84_wrong_basis_error (i : Fin 2) : (SequentialMeasurement.postEnsemble (RecordLayer.readyPrep (Projectivization.mk ℂ BB84.ketPlus ketPlus_ne_zero)) i) ((fun (y : RecordLayer.SwapArena (LF4.KSigma 2) 2) => y.1.1) ⁻¹' RecordLayer.globalBasin (RecordLayer.basisContext xBasisON) 1) = ENNReal.ofReal (1 / 2)

★ The wrong-basis error is ½: Alice's bit was + (X-outcome 0), and Bob's − basin has probability ½ after Eve's intercept — whichever outcome Eve recorded.

The right-basis round: repeatability = zero disturbance

theorem CSD.Empirical.CSDBridge.BB84Sequential.bb84_right_basis_no_disturbance (a : Fin 2) {j : Fin 2} (hj : j ≠ a) : (SequentialMeasurement.postEnsemble (RecordLayer.readyPrep (RecordLayer.vertexPoint a)) a) ((fun (y : RecordLayer.SwapArena (LF4.KSigma 2) 2) => y.1.1) ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 2) j) = 0

★ Eve in the matching basis disturbs nothing. Alice sends the computational vertex a; Eve measures in the same basis; Bob's error basin j ≠ a is null. This is exactly csd_repeatability_other, with hpos again a theorem.

theorem CSD.Empirical.CSDBridge.BB84Sequential.bb84_right_basis_faithful (a : Fin 2) : (SequentialMeasurement.postEnsemble (RecordLayer.readyPrep (RecordLayer.vertexPoint a)) a) ((fun (y : RecordLayer.SwapArena (LF4.KSigma 2) 2) => y.1.1) ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 2) a) = 1

…and Bob's correct basin has probability 1: Eve learned the bit for free.

The bridge to the QM module's marginal model

theorem CSD.Empirical.CSDBridge.BB84Sequential.bb84_dynamical_matches_marginal : BB84.irErrorZ0 BB84.zBasis = 0 ∧ BB84.irErrorZ0 BB84.xBasis = 1 / 2 ∧ 1 / 2 * BB84.irErrorZ0 BB84.zBasis + 1 / 2 * BB84.irErrorZ0 BB84.xBasis = 1 / 4

The dynamical values reproduce the classical-marginal ones. The QM module's intercept-resend model posits Eve's collapse as a marginal; its per-basis error values — 0 matching, ½ wrong — are the numbers derived dynamically above (in the dual round), and they assemble to the same QBER ¼.

The primal round, via the covariance law

theorem CSD.Empirical.CSDBridge.BB84Sequential.normsq_inner_single_xVec (j i : Fin 2) : ‖inner ℂ (EuclideanSpace.single j 1) (xVec i)‖ ^ 2 = 1 / 2

⟨eⱼ, xᵢ⟩ has squared norm ½, all four ways.

theorem CSD.Empirical.CSDBridge.BB84Sequential.normsq_inner_xVec_single (i a : Fin 2) : ‖inner ℂ (xVec i) (EuclideanSpace.single a 1)‖ ^ 2 = 1 / 2

⟨xᵢ, eₐ⟩ has squared norm ½, all four ways.

theorem CSD.Empirical.CSDBridge.BB84Sequential.bb84_primal_wrong_basis (a i j : Fin 2) : ((RecordLayer.swapProtocol (RecordLayer.basinIndex (RecordLayer.basisContext xBasisON)) ⋯).postMeasure ((RecordLayer.readyPrep (RecordLayer.vertexPoint a)).prod (RecordLayer.rotatedBank xBasisON)) i) ((fun (y : RecordLayer.SwapArena (LF4.KSigma 2) 2) => y.1.1) ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 2) j) = ENNReal.ofReal (1 / 2)

★ The primal round (Alice Z, Eve X, Bob Z) — the dual-round caveat retired. Eve measures the Z-carrier |a⟩ in the X basis (rotated selector, rotated bank, via the unitary-covariance law); whatever she records and the dynamics resends, Bob's Z-basin j has probability exactly ½. This is the QM module's own round, now end-to-end dynamical.