Second Moment Coherence

Abstract

The exact finite capture-count distribution reproduces its independently frozen second moment.

Theorem 1.1 (Second moment agreement for the exact capture-count distribution).

$$(\forall b,y,0\le q_b(y))\wedge (\forall b,\sum _y{q}_b(y)=1)\Rightarrow \sum _{0\le j\le |A|}{j}^2\sum _{S\subseteq A,|S|=j}\sum _{U\subseteq A\setminus S}(-1{)}^{|U|}\prod _{b\in A}\mathrm{if}\left(b\in \mathrm{union}\left(S,U\right),\mathrm{fixedPowerMass}\left(q,f,b,|\mathrm{union}\left(S,U\right)|\right),\mathrm{collisionPowerMass}\left(q,f,b,|\mathrm{union}\left(S,U\right)|\right)\right)=\sum _{a\in A}\mathrm{captureProbability}\left(q,f,a\right)+2\mathrm{pairProbabilitySum}\left(q,f\right).$$

Proof. Machine-checked in Lean as D5/S0/Asymptotics/WeightedProbability/SecondMomentCoherence.exact_capture_count_probability_second_moment_agreement (✓ std3). ∎

Source. Repository-derived.

Commentary.

The explicit alternating-product law selects the unique realized count for each sample, and the squared cardinality is rewritten as the square of its capture-indicator sum.

The resulting weighted sum is identified with the independently frozen indicator-square second moment, which expands as the one-address probability sum plus twice the unordered two-address sum.

References

• Truth anchor: D5/S0/Asymptotics/WeightedProbability/SecondMomentCoherence.exact_capture_count_probability_second_moment_agreement
• Dependency: D5/S0/Asymptotics/WeightedProbability/CaptureCountCoherence
• Dependency: D5/S0/Diagonal/Probability/CaptureCountMoments