Endnote [6]: normalization of the printed nondecoy monitoring count table

Proved

QAlgorithms.Papers.Independent.Intakethird100.P33.printedTableNormalization

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $x,p_d,f\in\mathbb R$ . In the source's printed first-order nondecoy table, give each pattern 00, 01, 10, 11 weight $(1-f)/4$ . Its two signal coefficients are $(x/4,x/4)$ , $(0,0)$ , $(x,0)$ , and $(x/4,x/4)$ , respectively. For a signal coefficient $s$ , the specified table count is $s+(1-s)p_d$ . If $C_{a,r}$ is that count multiplied by the printed pattern weight, then

\sum_{a\in\{00,01,10,11\}}\sum_{r=1}^2 C_{a,r} =\left[{x\over2}+\left(2-{x\over2}\right)p_d\right](1-f).

The identity holds for all real parameters. It checks the algebra of endnote [6], without equating the table to exact coherent click probabilities or resolving the sampling convention in (12). A probability interpretation of individual first-order entries would need additional parameter-domain and detector assumptions.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P33

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P33

open scoped BigOperators ENNReal

open QAlgorithms.RealRegisters (Hilbert)

open QAlgorithms.Papers.Independent.Dependency50.P33 (IsDensity rankOne)

open QAlgorithms.Papers.Independent.Dependency50.P39 (coherentCoefficient)

open QAlgorithms.Papers.Independent.Support50.P48 (vacuumAmplitude)

open QAlgorithms.Papers.Independent.Next46.P32 (FockPOVM realFockTracePair)

open QAlgorithms.Papers.Independent.Dependency50.P34
  (TwoModeFock fockKet photonMean)

open QAlgorithms.Papers.Independent.Frontier18.P14
  (coherentPair coherentPairCoefficients)

attribute [local instance] Classical.propDecidable

attribute [local instance] Classical.decEq

/-- PDF pp.4,7, (13) and endnote [6]: algebraic sum of the printed eight entries.
The statement does not interpret the table weights as an exact sampling law.
No domain guards are needed for a polynomial identity over the reals. -/
theorem printedTableNormalization (x pd f : ℝ) :
    (∑ pattern : Fin 4, ∑ port : Fin 2, printedCount x pd f pattern port) =
      (x / 2 + (2 - x / 2) * pd) * (1 - f) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P33

end

Source

Towards practical and fast Quantum Cryptography, arXiv:quant-ph/0411022v1, PDF p. 7, Endnote [6], with (13)

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For all real numbers $x,p_d,f$ , with no sign or range restrictions, define a signal $S_{a,b}$ for $a\in\{0,1,2,3\}$ , $b\in\{0,1\}$ by $S_{2,0}=x$ , $S_{2,1}=0$ , $S_{1,0}=S_{1,1}=0$ , and $S_{a,b}=x/4$ when $a=0$ or $a=3$ . Define $C_{a,b}=(S_{a,b}+(1-S_{a,b})p_d)(1-f)/4$ . Then the sum of all eight entries is

\sum_{a=0}^{3}\sum_{b=0}^{1}C_{a,b} =\left(\frac{x}{2}+\left(2-\frac{x}{2}\right)p_d\right)(1-f).

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph