Empirical/CSD/Crypto: Wiesner money — the measure-resend counterfeit, dynamically #
Category: CSD bridge (dynamical). An instantiation of the BB84Sequential engine on the
Wiesner mint/verify round — recorded as such: the counterfeit round is a genuine sequential
measurement (the forger's measurement collapses the note, the bank then verifies), and that is
exactly the calibrated-swap composition.
The round #
The mint (Empirical/QM/Crypto/WiesnerProtocol.lean) encodes a bit in one of two conjugate
carriers: mint false = |0⟩, mint true = |+⟩ — the same states as the BB84/B92 layer
(mint_false_eq/mint_true_eq are rfl). Honest verification measures in the mint basis and
accepts with certainty. A counterfeiter who does not know the basis must measure to copy — and
the measurement is a de-isolation that collapses the note:
wiesner_honest_x_pass/wiesner_honest_z_pass— honest verification accepts with probability1, as basin measures: the pass basin is full measure for the untouched note (wiesner_rate_eq_verifyProbties the X-side rate to the QM module'sverifyProb).- ★
wiesner_forge_x_pass_half/wiesner_forge_x_caught_half— the forger Z-measures a|+⟩note (calibrated-swap dynamics) and resends; the bank's pass and reject basins each have probability½, whatever the forger recorded. The collapse that catches the counterfeit is a pushforward theorem. - ★
wiesner_forge_z_invisible— on a matching-basis note the forger is exactly repeatability: the bank's pass basin keeps probability1. Measuring in the right basis copies for free — which is why the mint's secret basis choice is the entire security. wiesner_forge_pass_avg— averaging the two dynamical values over the mint's fair basis coin: the measure-resend counterfeit passes per-position verification with probability¾ = ½·1 + ½·½— the per-qubit value of the(3/4)ⁿcounterfeiting bound.
⚠️ Honest scope #
Per-position analysis of the Z-measure-resend attack; the mint's basis coin and the ¾
average are classical bookkeeping. That ¾ is also the optimal simple-counterfeit value
(Molina–Vidick–Watrous 2012) is not proved here — only that measure-resend attains it. The
unforgeability side (forgery ⟹ cloning) stays wiesner_forge_impossible / no-cloning on the QM
side. Inherits the calibrated-swap witness's scope notes.
References #
Empirical/QM/Crypto/WiesnerProtocol.lean (mint, verifyProb, wiesner_verify_honest,
wiesner_forge_impossible); Empirical/QM/Crypto/QuantumMoney.lean (the states);
Empirical/CSD/Crypto/BB84Sequential.lean (the engine); Empirical/CSD/Crypto/B92Sequential.lean
(xContext_rate_ketPlus_plus); Wiesner 1983; Molina–Vidick–Watrous 2012 (optimality, out of
scope); specs/BACKLOG.md.
The mint's carriers are the BB84/B92 states #
Honest verification: the pass basin is full #
The X-side pass rate equals the QM module's verifyProb for an honest conjugate-basis
note — the ontic rate and the operational acceptance probability are the same number.
Honest verification is certain (conjugate-basis note). The pass basin of an untouched
|+⟩ note has full measure.
Honest verification is certain (computational-basis note).
The counterfeit round #
★ The counterfeit is caught half the time on conjugate-basis notes. The forger
Z-measures a |+⟩ note and resends; the bank's pass basin has probability ½ whatever the
forger recorded — the collapse is the calibrated-swap pushforward, not a posit.
…and the reject basin has the other ½: the detection probability per conjugate
position.
★ On a matching-basis note the forger is invisible — exactly repeatability: the bank's
pass basin keeps probability 1 after the forger's measure-and-resend. The mint's secret basis
choice is the entire security.
The ¾ per-position pass probability. Averaging the two dynamical values
(wiesner_forge_z_invisible: 1; wiesner_forge_x_pass_half: ½) over the mint's fair basis
coin: the measure-resend counterfeit passes each position with probability ¾ — the per-qubit
value of the (3/4)ⁿ counterfeiting bound. Optimality of this value is out of scope (see the
module docstring).