Good-string circuit bridge #
Every canonical survivor code decodes to a typed circuit of the advertised
size. Packing a survivor tuple and composing strict majority therefore gives a
single circuit bounded by survivorTupleMajoritySizeBound. Target hardness
above that bound supplies the every-tuple coverage premise used by the
good-string counting argument.
theorem
Complexity.AntiChecker.exists_survivorCodeCircuit
{arity : ℕ}
[NeZero arity]
(target : BitString arity → Bool)
(threshold : ℕ)
(inputs : List (BitString arity))
(code : ↥(SurvivorCode target threshold inputs))
:
∃ (internalGates : ℕ) (circuit : Circuit Basis.andOr2 arity 1 internalGates),
circuit.size ≤ threshold ∧ ∀ (input : BitString arity), circuit.eval input 0 = survivorCodeOutput target threshold inputs code input
A canonical survivor code has a typed circuit witness of size at most the
survivor threshold, with output equal to survivorCodeOutput.
theorem
Complexity.AntiChecker.exists_survivorTupleMajorityCircuit
{arity : ℕ}
[NeZero arity]
(target : BitString arity → Bool)
(threshold : ℕ)
(inputs : List (BitString arity))
(tuple : Fin arity → ↥(SurvivorCode target threshold inputs))
:
∃ (internalGates : ℕ) (circuit : Circuit Basis.andOr2 arity 1 internalGates),
circuit.size ≤ survivorTupleMajoritySizeBound arity threshold ∧ ∀ (input : BitString arity),
circuit.eval input 0 = majority fun (i : Fin arity) => survivorCodeOutput target threshold inputs (tuple i) input
Pointwise strict majority of a survivor tuple is computed by one circuit within the explicit packing-plus-majority size bound.
theorem
Complexity.AntiChecker.everySurvivorTupleCaught_of_circuitHardness
{arity threshold hardnessThreshold : ℕ}
[NeZero arity]
(target : BitString arity → Bool)
(inputs : List (BitString arity))
(hfits : survivorTupleMajoritySizeBound arity threshold ≤ hardnessThreshold)
(hhard : ¬(MCSP.Instance.ofFunction arity hardnessThreshold target).HasCircuitAtMost)
:
EverySurvivorTupleCaught target threshold inputs
If the target is hard above the packing-plus-majority size bound, every survivor tuple is caught by some input.