Hashed anti-checker survivor cells #
This module identifies the existential query used by every amplified occupancy probe with the generic affine-hash cell semantics.
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.hashCellWitness_iff_blocks
{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
A hash-cell witness is exactly a row-major tuple whose every block is an encoded survivor and whose full tuple hashes to zero.
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.hashCellNonempty_iff_cellNonempty
{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
The anti-checker hash-cell predicate is exactly nonemptiness of the corresponding generic affine zero cell.
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.hashCellNonempty_iff_cellSize_pos
{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
Equivalently, the generic affine zero-cell cardinality is positive.