Anti-checker counter relation -- definitions

The approximate counter estimates the number of canonical small-circuit codes consistent with an arbitrary fixed-width vector of labeled samples. Defining this relation independently of a target function also gives contradictory labels their intended zero-survivor semantics.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.CodeMatchesLabeledSample {arity : ℕ} (code : List Bool) (sample : SuccinctMCSP.Sample arity) : Prop

One encoded circuit agrees with one explicitly labeled sample. Malformed or non-evaluating codes do not agree.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.CodeMatchesLabeledSample code sample = (Complexity.CircuitCode.evalCode arity code sample.input.toList = some sample.output)

@[instance_reducible]

instance Complexity.GapMCSP.Magnification.AntiCheckerLemma.instDecidableCodeMatchesLabeledSample {arity : ℕ} (code : List Bool) (sample : SuccinctMCSP.Sample arity) : Decidable (CodeMatchesLabeledSample code sample)

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.instDecidableCodeMatchesLabeledSample code sample = id inferInstance

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.CodeMatchesLabeledSamples {count arity : ℕ} (samples : Fin count → SuccinctMCSP.Sample arity) (code : List Bool) : Prop

One encoded circuit agrees with every sample in a fixed-width vector.

Equations

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

@[instance_reducible]

instance Complexity.GapMCSP.Magnification.AntiCheckerLemma.instDecidableCodeMatchesLabeledSamples {count arity : ℕ} (samples : Fin count → SuccinctMCSP.Sample arity) (code : List Bool) : Decidable (CodeMatchesLabeledSamples samples code)

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.instDecidableCodeMatchesLabeledSamples samples code = id inferInstance

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateLabeledSurvivorCodes {count : ℕ} (arity threshold : ℕ) (samples : Fin count → SuccinctMCSP.Sample arity) : Finset (List Bool)

Canonical small-circuit codes surviving an arbitrary labeled-sample vector.

Equations

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

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateLabeledSurvivorCount {count : ℕ} (arity threshold : ℕ) (samples : Fin count → SuccinctMCSP.Sample arity) : ℕ

Number of canonical small-circuit codes surviving an arbitrary labeled-sample vector.

Equations

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

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.DescriptionMatchesLabeledSample {arity threshold : ℕ} (description : CircuitCode.FixedWidth.ValidDescription arity threshold) (sample : SuccinctMCSP.Sample arity) : Prop

One valid fixed-width description agrees with one explicitly labeled sample through its parser-free raw-circuit view.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.DescriptionMatchesLabeledSample description sample = ((↑description).toRawCircuit.eval? sample.input.toList = some sample.output)

@[instance_reducible]

instance Complexity.GapMCSP.Magnification.AntiCheckerLemma.instDecidableDescriptionMatchesLabeledSample {arity threshold : ℕ} (description : CircuitCode.FixedWidth.ValidDescription arity threshold) (sample : SuccinctMCSP.Sample arity) : Decidable (DescriptionMatchesLabeledSample description sample)

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.instDecidableDescriptionMatchesLabeledSample description sample = id inferInstance

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.DescriptionMatchesLabeledSamples {count arity threshold : ℕ} (samples : Fin count → SuccinctMCSP.Sample arity) (description : CircuitCode.FixedWidth.ValidDescription arity threshold) : Prop

One valid fixed-width description agrees with every sample in a vector.

Equations

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

@[instance_reducible]

instance Complexity.GapMCSP.Magnification.AntiCheckerLemma.instDecidableDescriptionMatchesLabeledSamples {count arity threshold : ℕ} (samples : Fin count → SuccinctMCSP.Sample arity) (description : CircuitCode.FixedWidth.ValidDescription arity threshold) : Decidable (DescriptionMatchesLabeledSamples samples description)

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.instDecidableDescriptionMatchesLabeledSamples samples description = id inferInstance

noncomputable def Complexity.GapMCSP.Magnification.AntiCheckerLemma.candidateLabeledSurvivorDescriptions {count : ℕ} (arity threshold : ℕ) (samples : Fin count → SuccinctMCSP.Sample arity) : Finset (CircuitCode.FixedWidth.ValidDescription arity threshold)

Valid fixed-width descriptions surviving an arbitrary labeled-sample vector.

Equations

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