Hash-cell occupancy amplification -- proof internals

theorem Complexity.PairwiseIndependentHash.mem_majorityNonemptyEvent_iff_internal {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (errorBits : ℕ) (seed : BitString (majoritySeedWidth seedWidth errorBits)) : seed ∈ hash.majorityNonemptyEvent set target errorBits ↔ hash.majorityNonempty set target errorBits seed = true

Internal membership characterization for an amplified positive answer.

theorem Complexity.PairwiseIndependentHash.mem_majorityEmptyEvent_iff_internal {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (errorBits : ℕ) (seed : BitString (majoritySeedWidth seedWidth errorBits)) : seed ∈ hash.majorityEmptyEvent set target errorBits ↔ hash.majorityNonempty set target errorBits seed = false

Internal membership characterization for an amplified negative answer.

theorem Complexity.PairwiseIndependentHash.majorityEmptyEvent_eq_compl_majorityNonemptyEvent_internal {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (errorBits : ℕ) : hash.majorityEmptyEvent set target errorBits = (hash.majorityNonemptyEvent set target errorBits)ᶜ

Internal complement identity for the two amplified occupancy outcomes.

theorem Complexity.PairwiseIndependentHash.one_sub_two_pow_le_eventProb_majorityNonemptyEvent_internal {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (errorBits : ℕ) (hmean : 8 ≤ hash.averageCellSize set target) : 1 - 1 / 2 ^ errorBits ≤ eventProb (hash.majorityNonemptyEvent set target errorBits)

Internal high-mean amplification theorem.

theorem Complexity.PairwiseIndependentHash.eventProb_majorityEmptyEvent_le_two_pow_internal {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (errorBits : ℕ) (hmean : 8 ≤ hash.averageCellSize set target) : eventProb (hash.majorityEmptyEvent set target errorBits) ≤ 1 / 2 ^ errorBits

Internal high-mean failure-probability theorem.

theorem Complexity.PairwiseIndependentHash.eventProb_majorityNonemptyEvent_le_two_pow_internal {domainWidth rangeWidth seedWidth : ℕ} (hash : PairwiseIndependentHash domainWidth rangeWidth seedWidth) (set : Finset (BitString domainWidth)) (target : BitString rangeWidth) (errorBits : ℕ) (hmean : hash.averageCellSize set target ≤ 1 / 8) : eventProb (hash.majorityNonemptyEvent set target errorBits) ≤ 1 / 2 ^ errorBits

Internal low-mean amplification theorem.