Hashing circuits for anti-checker counters -- proof internals #
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.hashingEstimate_lt_counterRange_internal
{arity prefixLength : ℕ}
(beta : PositiveRationalScale)
(harity : arity ≠ 0)
(input : BitString (counterInputWidth arity prefixLength))
(seed : BitString (hashingCounterSeedWidth beta arity prefixLength))
:
ApproximateCounting.Relative.hashingEstimate (roundPrecision arity) (counterInputWidth arity prefixLength + 1)
(encodedSurvivorSet arity (smallThreshold beta arity) input) seed < 2 ^ counterOutputWidth beta arity
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.exists_correct_counter_of_hashingCircuit_internal
{overhead arity prefixLength internalGates : ℕ}
(beta : PositiveRationalScale)
(harity : arity ≠ 0)
{circuit :
Circuit Basis.andOr2 (hashingCounterSeedWidth beta arity prefixLength + counterInputWidth arity prefixLength)
(counterOutputWidth beta arity) internalGates}
(himplements : HashingCircuitImplements beta circuit)
(hsize : circuit.size ≤ counterSizeBound overhead beta arity)
:
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.exists_correct_counter_of_oracleProgram_internal
{language : Language}
{overhead arity prefixLength rounds : ℕ}
(beta : PositiveRationalScale)
(harity : arity ≠ 0)
(program :
AdaptiveOracleProgram (hashingCounterSeedWidth beta arity prefixLength + counterInputWidth arity prefixLength)
(counterOutputWidth beta arity) rounds)
(circuitOracle : PolynomialCircuitOracle language)
(hprogram :
ApproximateCounting.Relative.OracleProgramImplements (roundPrecision arity) (counterInputWidth arity prefixLength + 1)
(encodedSurvivorSet arity (smallThreshold beta arity)) program circuitOracle.oracle)
(hsize : (program.inlineCircuitOracle circuitOracle).snd.size ≤ counterSizeBound overhead beta arity)
:
∃ (counter : ApproximateCounterCircuit overhead beta arity prefixLength),
counter.IsCorrect ∧ counter.circuit.size = (program.inlineCircuitOracle circuitOracle).snd.size