Circuit predicates for anti-checker hash cells #
The canonical fixed-prefix circuit-satisfiability query associated with an implementing predicate circuit is accepted exactly when its semantic affine zero cell contains a powered survivor tuple.
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellPredicateCircuit.ruler_length
(beta : PositiveRationalScale)
(arity : ℕ)
:
The existential-witness ruler has exactly the powered-survivor width.
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellPredicateCircuit.evalFamilyCode_code
{beta : PositiveRationalScale}
{arity prefixLength rangeWidth : ℕ}
(predicate : HashCellPredicateCircuit beta arity prefixLength rangeWidth)
(input : BitString (counterInputWidth arity prefixLength))
(seed : BitString (PairwiseIndependentHash.affineSeedWidth (counterSurvivorPowerWidth beta arity) rangeWidth))
(witness : BitString (counterSurvivorPowerWidth beta arity))
:
CircuitCode.evalFamilyCode predicate.code ((hashCellPublicInput beta input seed).toList ++ witness.toList) = some (decide (HashCellWitness arity (smallThreshold beta arity) (roundPrecision arity) rangeWidth input seed witness))
Evaluating a predicate's tagged code on its public prefix followed by a witness returns the semantic hash-cell predicate.
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellPredicateCircuit.query_mem_extensionLanguage_iff
{beta : PositiveRationalScale}
{arity prefixLength rangeWidth : ℕ}
(predicate : HashCellPredicateCircuit beta arity prefixLength rangeWidth)
(input : BitString (counterInputWidth arity prefixLength))
(seed : BitString (PairwiseIndependentHash.affineSeedWidth (counterSurvivorPowerWidth beta arity) rangeWidth))
:
predicate.query input seed ∈ CircuitSAT.extensionLanguage ↔ HashCellNonempty arity (smallThreshold beta arity) (roundPrecision arity) rangeWidth input seed
The canonical extension-language query is accepted exactly when the selected affine zero cell contains a powered survivor witness.