Resolved-count weak values

Abstract

Every resolved coherent-state weak value differs from the no-click value by the count times the single-photon weak value.

Theorem 1.1 (The first factorial moment of the exponential series).

$$\forall (t:\mathbb{C}),(\mathrm{HasSum}\left(n:\mathbb{N}\mapsto \frac{((n:\mathbb{C}))\cdot ((t{)}^n)}{Nat.factorial\left(n\right)},(t)\cdot (Complex.exp\left(t\right))\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/ResolvedCountWeakValue.weighted_exp_hasSum (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every complex t, the sum of n t^n/n! is t exp(t). A shift by one in the exponential series and the factorial recurrence give the identity. Number insertion in a coherent state uses this weighted series; the second factorial moment of an exponential series also follows by a shift.

Definition 1.2 (The all-count proposition).

$$\mathrm{claim}=\forall (k:\mathbb{N}),(\forall (A:\mathrm{LinearIsometryEquiv}\left(\mathbb{C},\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(k+1\right)\right),\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(k+1\right)\right)\right)),(\forall (B:\mathrm{LinearIsometryEquiv}\left(\mathbb{C},\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(k+1\right)\right),\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(k+1\right)\right)\right)),(\forall (alpha:\mathbb{C}),((alpha\ne 0)\Rightarrow (\forall (m:\mathbb{N}),(\forall (hM:\mathrm{coherentProbability}\left(A,B,alpha,m\right)\ne 0),(\exists (hZero:\mathrm{coherentProbability}\left(A,B,alpha,0\right)\ne 0),(\mathrm{ite}\left(m=0,\mathrm{coherentWeakValue}\left(A,B,alpha,m,hM\right)-\mathrm{coherentWeakValue}\left(A,B,alpha,0,hZero\right)=0,\exists (hOne:\mathrm{singleProbability}\left(A,B,(1:\mathrm{Fin}\left(2\right))\right)\ne 0),(\mathrm{coherentWeakValue}\left(A,B,alpha,m,hM\right)-\mathrm{coherentWeakValue}\left(A,B,alpha,0,hZero\right)=((m:\mathbb{C}))\cdot (\mathrm{singleWeakValue}\left(A,B,(1:\mathrm{Fin}\left(2\right)),hOne\right)))\right)))))))))$$

Formalization. D5/S3/Quantum/ResolvedCountWeakValue.claim (✓ std3).

Citation. H. M. Wiseman, A. M. Steinberg, M. Hallaji (2023). Obtaining a single-photon weak value from experiments using a strong (many-photon) coherent state. DOI: 10.1116/5.0137579. URL: https://arxiv.org/abs/2211.15761v2.

Commentary.

Section V, page 6: “This supports earlier approximate results which suggested that if a photon-number resolving detector were used, the weak value post-selected on detecting m photons would exceed the no-click weak value by precisely m times the single-photon number. We leave a rigorous proof of this conjecture for future work.” The encoding has k+1 modes, with mode 0 probed and detected; A and B are arbitrary passive evolutions. Alpha is nonzero, m is a natural count, and all conditional values require nonzero probabilities. For m=0 the difference is zero without a single-photon denominator.

Theorem 1.3 (The resolved-count identity).

$$\forall (k:\mathbb{N}),(\forall (A:\mathrm{LinearIsometryEquiv}\left(\mathbb{C},\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(k+1\right)\right),\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(k+1\right)\right)\right)),(\forall (B:\mathrm{LinearIsometryEquiv}\left(\mathbb{C},\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(k+1\right)\right),\mathrm{EuclideanSpace}\left(\mathbb{C},\mathrm{Fin}\left(k+1\right)\right)\right)),(\forall (alpha:\mathbb{C}),((alpha\ne 0)\Rightarrow (\forall (m:\mathbb{N}),(\forall (hM:\mathrm{coherentProbability}\left(A,B,alpha,m\right)\ne 0),(\exists (hZero:\mathrm{coherentProbability}\left(A,B,alpha,0\right)\ne 0),(\mathrm{ite}\left(m=0,\mathrm{coherentWeakValue}\left(A,B,alpha,m,hM\right)-\mathrm{coherentWeakValue}\left(A,B,alpha,0,hZero\right)=0,\exists (hOne:\mathrm{singleProbability}\left(A,B,(1:\mathrm{Fin}\left(2\right))\right)\ne 0),(\mathrm{coherentWeakValue}\left(A,B,alpha,m,hM\right)-\mathrm{coherentWeakValue}\left(A,B,alpha,0,hZero\right)=((m:\mathbb{C}))\cdot (\mathrm{singleWeakValue}\left(A,B,(1:\mathrm{Fin}\left(2\right)),hOne\right)))\right)))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/ResolvedCountWeakValue.result (✓ std3). ∎

Resolves. Problems/wiseman-steinberg-hallaji-2023-resolved-count-weak-values (proved) by D5/S3/Quantum/ResolvedCountWeakValue.result.

Source. Repository-derived.

Acknowledgement. H. M. Wiseman, A. M. Steinberg, M. Hallaji (2023). Obtaining a single-photon weak value from experiments using a strong (many-photon) coherent state. DOI: 10.1116/5.0137579. URL: https://arxiv.org/abs/2211.15761v2.

Commentary.

Number insertion creates one excitation in the coherent field. Its detected-mode contribution is proportional to m, while the ignored modes contribute a term independent of m. Subtracting the zero-count value cancels that term; scaling the input amplitude cancels from the remaining ratio. A positive count with nonzero probability also guarantees a nonzero single-photon probability.

References

• Truth anchor: D5/S3/Quantum/ResolvedCountWeakValue.claim
• Truth anchor: D5/S3/Quantum/ResolvedCountWeakValue.result
• Truth anchor: D5/S3/Quantum/ResolvedCountWeakValue.weighted_exp_hasSum
• Dependency: D5/S3/Quantum/PassiveFockModel