Hashing circuits for anti-checker counters

Any bounded circuit implementing the amplified relative hashing estimator on the encoded survivor set yields a deterministic correct anti-checker counter. The random seed is fixed nonuniformly, with exact circuit-size preservation.

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

Every semantic relative-hashing estimate fits in the output width reserved by the anti-checker counter.

theorem Complexity.GapMCSP.Magnification.AntiCheckerLemma.exists_correct_counter_of_hashingCircuit {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) : ∃ (counter : ApproximateCounterCircuit overhead beta arity prefixLength), counter.IsCorrect ∧ counter.circuit.size = circuit.size

A bounded hashing-estimator circuit yields a deterministic counter that is accurate on every packed labeled-sample input, at identical size.

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

A relative-counting oracle program and an exact polynomial circuit oracle produce the required deterministic counter once their inlined size meets the anti-checker bound.