Good-string combinatorics -- definitions

The good-string argument studies tuples drawn from the circuit descriptions surviving a sample prefix. An input catches a tuple when at least half of its entries disagree with the target there.

@[reducible, inline]

abbrev Complexity.AntiChecker.SurvivorCode {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) : Finset (List Bool)

Circuit codes surviving the canonical sample prefix, regarded as a finite type.

Equations

• Complexity.AntiChecker.SurvivorCode target threshold inputs = Complexity.AntiChecker.ConsistentCodes target inputs (Complexity.AntiChecker.candidateCodes arity threshold)

def Complexity.AntiChecker.survivorCodeOutput {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (code : ↥(SurvivorCode target threshold inputs)) (input : BitString arity) : Bool

The Boolean output of a surviving circuit code on one input. The default branch is unreachable for survivor codes: candidate membership guarantees a canonical well-formed circuit at the declared arity.

Equations

• Complexity.AntiChecker.survivorCodeOutput target threshold inputs code input = (Complexity.CircuitCode.evalCode arity (↑code) input.toList).getD false

def Complexity.AntiChecker.SurvivorTupleMajorityComputes {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (tuple : Fin arity → ↥(SurvivorCode target threshold inputs)) : Prop

A survivor tuple computes the target by taking the strict majority of its pointwise circuit outputs.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.AntiChecker.disagreeingSurvivors {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (input : BitString arity) : Finset ↥(SurvivorCode target threshold inputs)

Current survivors that disagree with the target at one possible next input.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.AntiChecker.survivorTupleAgreementCount {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (input : BitString arity) (tuple : Fin arity → ↥(SurvivorCode target threshold inputs)) : ℕ

Number of positions in a survivor tuple whose circuits agree with the target at one input.

Equations

• Complexity.AntiChecker.survivorTupleAgreementCount target threshold inputs input tuple = {i : Fin arity | Complexity.AntiChecker.CodeAgreesAt target (↑(tuple i)) input}.card

def Complexity.AntiChecker.IsSurvivorTupleCaughtAt {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (input : BitString arity) (tuple : Fin arity → ↥(SurvivorCode target threshold inputs)) : Prop

An input catches a survivor tuple when at least the ceiling of half of its entries disagree with the target.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Complexity.AntiChecker.instDecidableIsSurvivorTupleCaughtAt {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (input : BitString arity) (tuple : Fin arity → ↥(SurvivorCode target threshold inputs)) : Decidable (IsSurvivorTupleCaughtAt target threshold inputs input tuple)

Equations

• Complexity.AntiChecker.instDecidableIsSurvivorTupleCaughtAt target threshold inputs input tuple = id inferInstance

def Complexity.AntiChecker.caughtSurvivorTuples {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) (input : BitString arity) : Finset (Fin arity → ↥(SurvivorCode target threshold inputs))

Survivor tuples caught by one possible next input.

Equations

• Complexity.AntiChecker.caughtSurvivorTuples target threshold inputs input = Finset.filter (Complexity.AntiChecker.IsSurvivorTupleCaughtAt target threshold inputs input) Finset.univ

def Complexity.AntiChecker.EverySurvivorTupleCaught {arity : ℕ} (target : BitString arity → Bool) (threshold : ℕ) (inputs : List (BitString arity)) : Prop

Every survivor tuple is caught by some input. Circuit hardness will supply this premise by ruling out a majority circuit for the tuple.

Equations

• One or more equations did not get rendered due to their size.