Circuit predicates for anti-checker hash cells -- proof internals

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellPredicateCircuit.ruler_length_internal (beta : PositiveRationalScale) (arity : ℕ) : (ruler beta arity).length = counterSurvivorPowerWidth beta arity

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellPredicateCircuit.evalFamilyCode_code_internal {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))

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellPredicateCircuit.query_mem_extensionLanguage_iff_internal {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