Hashed anti-checker survivor cells -- proof internals #
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.hashCellWitness_iff_blocks_internal
{count arity threshold precision rangeWidth : ℕ}
(input : BitString (count * (arity + 1)))
(seed : BitString (PairwiseIndependentHash.affineSeedWidth (survivorPowerWidth arity threshold precision) rangeWidth))
(witness : BitString (survivorPowerWidth arity threshold precision))
:
HashCellWitness arity threshold precision rangeWidth input seed witness ↔ (∀ (copy : Fin (ApproximateCounting.relativeCopies precision)),
(blocksEquiv (ApproximateCounting.relativeCopies precision) (candidateCodeWidth arity threshold)) witness copy ∈ encodedSurvivorSet arity threshold input) ∧ (PairwiseIndependentHash.affine (survivorPowerWidth arity threshold precision) rangeWidth).eval seed witness = fun (x : Fin rangeWidth) => false
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.hashCellNonempty_iff_cellNonempty_internal
{count arity threshold precision rangeWidth : ℕ}
(input : BitString (count * (arity + 1)))
(seed : BitString (PairwiseIndependentHash.affineSeedWidth (survivorPowerWidth arity threshold precision) rangeWidth))
:
HashCellNonempty arity threshold precision rangeWidth input seed ↔ ((PairwiseIndependentHash.affine (survivorPowerWidth arity threshold precision) rangeWidth).cell
(ApproximateCounting.cartesianPower (encodedSurvivorSet arity threshold input)
(ApproximateCounting.relativeCopies precision))
(fun (x : Fin rangeWidth) => false) seed).Nonempty
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.hashCellNonempty_iff_cellSize_pos_internal
{count arity threshold precision rangeWidth : ℕ}
(input : BitString (count * (arity + 1)))
(seed : BitString (PairwiseIndependentHash.affineSeedWidth (survivorPowerWidth arity threshold precision) rangeWidth))
:
HashCellNonempty arity threshold precision rangeWidth input seed ↔ 0 < (PairwiseIndependentHash.affine (survivorPowerWidth arity threshold precision) rangeWidth).cellSize
(ApproximateCounting.cartesianPower (encodedSurvivorSet arity threshold input)
(ApproximateCounting.relativeCopies precision))
(fun (x : Fin rangeWidth) => false) seed