Good-string circuit bridge -- proof internals #
theorem
Complexity.AntiChecker.exists_survivorCodeCircuit_internal
{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
theorem
Complexity.AntiChecker.exists_survivorTupleMajorityCircuit_internal
{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
theorem
Complexity.AntiChecker.everySurvivorTupleCaught_of_circuitHardness_internal
{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