Capture Count Coherence

Abstract

The exact finite capture-count distribution is coherent with total mass and its independently computed mean.

Theorem 1.1 (Normalization of the exact capture-count distribution).

$$(\forall b,\sum _y{q}_b(y)=1)\Rightarrow \sum _{0\le j\le |A|}\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)=1.$$

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

Source. Repository-derived.

Commentary.

Rewriting every explicit mass by the frozen exact capture-count theorem reduces the sum to a partition of all samples by their unique realized count.

The count lies between zero and |A|, so exactly one term survives; the frozen total sample-weight identity then gives one.

Theorem 1.2 (Mean 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\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).$$

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

Source. Repository-derived.

Commentary.

The explicit law again selects the unique realized count for each sample, and the cardinality is rewritten as the sum of its capture indicators.

The resulting weighted indicator sum is identified with the independently frozen first-moment calculation from CaptureSecondMoment.

References

• Truth anchor: D5/S0/Asymptotics/WeightedProbability/CaptureCountCoherence.exact_capture_count_probability_mean_agreement
• Truth anchor: D5/S0/Asymptotics/WeightedProbability/CaptureCountCoherence.exact_capture_count_probability_normalizes
• Dependency: D5/S0/Asymptotics/WeightedProbability/ExactCaptureCount
• Dependency: D5/S0/Diagonal/Probability/CaptureSecondMoment