Circuit interface for relative approximate counting #
Any circuit computing the amplified hashing estimator inherits its exact finite failure bound. This is the bridge used before nonuniform seed fixing.
theorem
Complexity.ApproximateCounting.Relative.badSeedEvent_eq_failureEvent
{inputWidth outputWidth domainWidth internalGates precision failureBits : ℕ}
[NeZero inputWidth]
[NeZero outputWidth]
{setOfInput : BitString inputWidth → Finset (BitString domainWidth)}
{circuit : Circuit Basis.andOr2 (seedWidth domainWidth precision failureBits + inputWidth) outputWidth internalGates}
(himplements : CircuitImplements precision failureBits setOfInput circuit)
(input : BitString inputWidth)
:
circuit.badSeedEvent (OutputIsAccurate precision setOfInput) input = failureEvent precision failureBits (setOfInput input)
Circuit failure seeds coincide exactly with the estimator's semantic failure event.
theorem
Complexity.ApproximateCounting.Relative.eventProb_badSeedEvent_le_two_pow
{inputWidth outputWidth domainWidth internalGates precision failureBits : ℕ}
[NeZero inputWidth]
[NeZero outputWidth]
{setOfInput : BitString inputWidth → Finset (BitString domainWidth)}
{circuit : Circuit Basis.andOr2 (seedWidth domainWidth precision failureBits + inputWidth) outputWidth internalGates}
(hprecision : 0 < precision)
(himplements : CircuitImplements precision failureBits setOfInput circuit)
(input : BitString inputWidth)
:
eventProb (circuit.badSeedEvent (OutputIsAccurate precision setOfInput) input) ≤ 1 / 2 ^ failureBits
Every fixed ordinary input inherits failure probability at most
2^-failureBits from the semantic hashing estimator.
theorem
Complexity.ApproximateCounting.Relative.exists_hardwired_accurate_circuit
{inputWidth outputWidth domainWidth internalGates precision : ℕ}
[NeZero inputWidth]
[NeZero outputWidth]
{setOfInput : BitString inputWidth → Finset (BitString domainWidth)}
{circuit :
Circuit Basis.andOr2 (seedWidth domainWidth precision (inputWidth + 1) + inputWidth) outputWidth internalGates}
(hprecision : 0 < precision)
(himplements : CircuitImplements precision (inputWidth + 1) setOfInput circuit)
:
∃ (fixed : Circuit Basis.andOr2 inputWidth outputWidth internalGates),
(∀ (input : BitString inputWidth), OutputIsAccurate precision setOfInput input (fixed.eval input)) ∧ fixed.size = circuit.size
Choosing failure exponent inputWidth + 1 leaves one seed that is
accurate for every ordinary input; hardwiring it preserves exact circuit
size.