Documentation

CsdLean4.Empirical.CSD.Crypto.B92Sequential

Empirical/CSD/Crypto: B92 — false conclusive clicks from a dynamical intercept #

Category: CSD bridge (dynamical). An instantiation of the BB84Sequential engine on the B92 unambiguous-discrimination round — recorded as such: the dynamical theorem is the same calibrated-swap fact, re-read on B92's conclusive-click semantics.

The round #

B92 encodes bit 0 in |0⟩ and bit 1 in |+⟩. Bob's conclusive detector for bit 0 is the |−⟩ click: honest carriers of bit 1 (|+⟩) can never trigger it (⟨−|+⟩ = 0, b92_unambiguous_zero on the QM side). This module gives that unambiguity its ontic form and then shows what an intercepting Eve does to it:

⚠️ Honest scope #

One sifted round; the dynamical content is bb84_wrong_basis_error re-read (stated, not hidden); Eve's basis choice stays classical bookkeeping. Inherits the calibrated-swap witness's scope notes via SequentialMeasurement.lean. The unambiguous-discrimination optimality (IDP bound) and full key-rate analysis remain on the QM side and the recorded QKD tranche.

References #

Empirical/QM/Crypto/B92.lean (b92_unambiguous_zero, b92_conclusive_rate_one, ketMinus_inner_ketPlus, ketPlus_unit); Empirical/CSD/Crypto/BB84Sequential.lean (the engine: xBasisON, xContext_rate_vertex, bb84_wrong_basis_error); SigmaLayer/RotatedContext.lean (basisContext_rate_mk); Bennett 1992; specs/BACKLOG.md.

The honest X-context rates at the two carriers #

Unambiguity as a null basin #

Unambiguity is an ontic impossibility. For a |+⟩ (bit-1) carrier, the conclusive-bit-0 basin (|−⟩ click) is a null set: the context-fixed fibre arc has width zero at that base point. No microstate of an honest bit-1 carrier produces a false conclusive click — the same shape as the eraser twin's dark fringe.

The Z-side unambiguity: a |0⟩ (bit-0) carrier never triggers the conclusive-bit-1 click (|1⟩ in the computational basis) — momentMap_vertex at the off-index.

The honest conclusive rate: a |0⟩ carrier triggers the conclusive-bit-0 click with basin measure ½ — B92's ½ conclusive rate as a fibre-arc width.

The intercepted round #

★ Eve creates false conclusive clicks. Alice sends |+⟩ (bit 1); Eve measures in the computational basis and the calibrated-swap dynamics resends her eigenstate; Bob's conclusive-bit-0 basin now has probability ½whatever Eve recorded. The dynamical fact is bb84_wrong_basis_error, re-read on B92's click semantics: where honestly no microstate could produce this click, the intercept produces it half the time.