Affine hash-cell circuit fragments #
The specialized raw fragment reads affine coefficients and a powered-survivor witness directly from the canonical hash-cell input layout, and accepts exactly when the affine hash of that witness is zero.
@[simp]
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellAffineCircuit.length_compileRaw
(beta : PositiveRationalScale)
(arity prefixLength rangeWidth : ℕ)
:
The specialized affine-zero fragment has its advertised exact size.
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellAffineCircuit.outputWire_eq
(beta : PositiveRationalScale)
(arity prefixLength rangeWidth : ℕ)
:
outputWire beta arity prefixLength rangeWidth = hashCellPredicateInputWidth beta arity prefixLength rangeWidth + List.length (compileRaw beta arity prefixLength rangeWidth) - 1
The last emitted gate carries the specialized affine-zero decision.
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellAffineCircuit.compileRaw_wellFormed
(beta : PositiveRationalScale)
(arity prefixLength rangeWidth : ℕ)
:
CircuitCode.RawCircuit.WellFormed (hashCellPredicateInputWidth beta arity prefixLength rangeWidth)
(compileRaw beta arity prefixLength rangeWidth)
Every specialized affine-zero fragment is a valid raw circuit extension.
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellAffineCircuit.eval?_compileRaw
(beta : PositiveRationalScale)
{arity prefixLength rangeWidth : ℕ}
(input : BitString (counterInputWidth arity prefixLength))
(seed : BitString (PairwiseIndependentHash.affineSeedWidth (counterSurvivorPowerWidth beta arity) rangeWidth))
(witness : BitString (counterSurvivorPowerWidth beta arity))
:
(compileRaw beta arity prefixLength rangeWidth).eval?
(BitString.toList (Fin.append (hashCellPublicInput beta input seed) witness)) = some (decide (PairwiseIndependentHash.affineEval seed witness = fun (x : Fin rangeWidth) => false))
The specialized fragment accepts exactly when the packed seed sends the powered-survivor witness to zero.