Activity and attainable threshold transcripts

The number of attainable input-reading transcripts is bounded by a Hamming ball at the worst-case input-reading activity, or at the worst-case Hamming distance from any fixed baseline activation pattern. Projecting the full gate valuations gives a second bound using the total gate count and maximum activity (or distance from a baseline) across all gates. Both bounds use the same finite-image counting lemma.

The resulting exact binomial sum is an upper bound on the number of patterns. Lower bounds for a computed function also require a representation theorem, such as the comparison-tree compiler.

Main definitions

• Cslib.Circuits.Boolean.WeightedThreshold.attainableTranscripts: the realized transcripts.
• Cslib.Circuits.Boolean.WeightedThreshold.inputActivity: maximum input-reading activity.
• Cslib.Circuits.Boolean.WeightedThreshold.gateActivity: maximum activity across all gates.
• Cslib.Circuits.Boolean.WeightedThreshold.inputActivityFrom: maximum Hamming distance of the restricted transcript from a fixed baseline pattern.
• Cslib.Circuits.Boolean.WeightedThreshold.gateActivityFrom: maximum Hamming distance of the full gate valuation from a fixed baseline pattern.

Main results

• Cslib.Circuits.Boolean.WeightedThreshold.card_attainableTranscripts_le_sum_choose: the exact Hamming-ball bound for attainable patterns.
• Cslib.Circuits.Boolean.WeightedThreshold.card_attainableTranscripts_le_sum_choose_gateActivity: the bound using activity across all gates.
• card_attainableTranscripts_le_sum_choose_inputActivityFrom: the shifted-baseline Hamming-ball bound on input-reading gates.
• card_attainableTranscripts_le_sum_choose_gateActivityFrom: the shifted-baseline Hamming-ball bound across all gates.

References

• [Threshold Circuits as Decision Trees and Finite-State Programs, Theorem 3.2 and Section 3.1] [26]

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.attainableTranscripts {n g : ℕ} (p : Program signature n g) : Finset (↥(inputGates p) → Bool)

The restricted activation transcripts realized by Boolean inputs.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.inputActivity {n g : ℕ} (p : Program signature n g) : ℕ

The maximum number of active input-reading gates on one input.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.gateActivity {n g : ℕ} (p : Program signature n g) : ℕ

The maximum number of active gates on one input, including gates without direct inputs.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.inputActivityFrom {n g : ℕ} (p : Program signature n g) (v : ↥(inputGates p) → Bool) : ℕ

The maximum Hamming distance of the restricted activation transcript from a fixed baseline pattern v.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.gateActivityFrom {n g : ℕ} (p : Program signature n g) (v : Fin g → Bool) : ℕ

The maximum Hamming distance of the full gate valuation from a fixed baseline pattern v.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.mem_attainableTranscripts {n g : ℕ} (p : Program signature n g) (z : ↥(inputGates p) → Bool) : z ∈ attainableTranscripts p ↔ ∃ (x : Fin n → Bool), transcript p x = z

theorem Cslib.Circuits.Boolean.WeightedThreshold.inputActivity_le_iff {n g : ℕ} (p : Program signature n g) {e : ℕ} : inputActivity p ≤ e ↔ ∀ (x : Fin n → Bool), BitString.weight (transcript p x) ≤ e

An activity bound is exactly a uniform bound on the weight of the restricted transcripts.

theorem Cslib.Circuits.Boolean.WeightedThreshold.gateActivity_le_iff {n g : ℕ} (p : Program signature n g) {e : ℕ} : gateActivity p ≤ e ↔ ∀ (x : Fin n → Bool), BitString.weight (p.eval interpretation x) ≤ e

A bound on total activity is exactly a uniform bound on complete gate valuations.

theorem Cslib.Circuits.Boolean.WeightedThreshold.inputActivityFrom_le_iff {n g : ℕ} (p : Program signature n g) (v : ↥(inputGates p) → Bool) {e : ℕ} : inputActivityFrom p v ≤ e ↔ ∀ (x : Fin n → Bool), hammingDist (transcript p x) v ≤ e

A shifted-baseline input-reading activity bound is a uniform Hamming-distance bound on restricted transcripts.

theorem Cslib.Circuits.Boolean.WeightedThreshold.gateActivityFrom_le_iff {n g : ℕ} (p : Program signature n g) (v : Fin g → Bool) {e : ℕ} : gateActivityFrom p v ≤ e ↔ ∀ (x : Fin n → Bool), hammingDist (p.eval interpretation x) v ≤ e

A shifted-baseline total activity bound is a uniform Hamming-distance bound on complete gate valuations.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.inputActivityFrom_zero {n g : ℕ} (p : Program signature n g) : inputActivityFrom p 0 = inputActivity p

At the all-false baseline, shifted-baseline input-reading activity equals inputActivity.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.gateActivityFrom_zero {n g : ℕ} (p : Program signature n g) : gateActivityFrom p 0 = gateActivity p

At the all-false baseline, shifted-baseline total activity equals gateActivity.

theorem Cslib.Circuits.Boolean.WeightedThreshold.gateActivity_le {n g : ℕ} (p : Program signature n g) : gateActivity p ≤ g

Total gate activity never exceeds the number of gates.

theorem Cslib.Circuits.Boolean.WeightedThreshold.inputActivity_le_gateActivity {n g : ℕ} (p : Program signature n g) : inputActivity p ≤ gateActivity p

Restricting to the input-reading gates cannot increase activity.

theorem Cslib.Circuits.Boolean.WeightedThreshold.inputActivity_le_card {n g : ℕ} (p : Program signature n g) : inputActivity p ≤ (inputGates p).card

Input-reading activity never exceeds the number of input-reading gates.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_attainableTranscripts_le_sum_choose_of_le {n g : ℕ} (p : Program signature n g) {e : ℕ} (he : inputActivity p ≤ e) : (attainableTranscripts p).card ≤ ∑ j ∈ Finset.range (e + 1), (inputGates p).card.choose j

Every realized transcript lies in the Hamming ball specified by any uniform activity bound. The bound also permits a radius larger than the number of input-reading gates.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_attainableTranscripts_le_sum_choose {n g : ℕ} (p : Program signature n g) : (attainableTranscripts p).card ≤ ∑ j ∈ Finset.range (inputActivity p + 1), (inputGates p).card.choose j

Attainable patterns are bounded by the exact binomial sum at worst-case activity.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_attainableTranscripts_le_sum_choose_gateActivity {n g : ℕ} (p : Program signature n g) : (attainableTranscripts p).card ≤ ∑ j ∈ Finset.range (gateActivity p + 1), g.choose j

Projecting full gate valuations cannot create additional restricted transcripts, so total gate activity gives a Hamming-ball bound using the total number of gates.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_attainableTranscripts_le_sum_choose_of_inputActivityFrom_le {n g : ℕ} (p : Program signature n g) (v : ↥(inputGates p) → Bool) {e : ℕ} (he : inputActivityFrom p v ≤ e) : (attainableTranscripts p).card ≤ ∑ j ∈ Finset.range (e + 1), (inputGates p).card.choose j

Every realized transcript lies in the Hamming ball of radius e around any fixed baseline v whenever inputActivityFrom p v ≤ e.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_attainableTranscripts_le_sum_choose_inputActivityFrom {n g : ℕ} (p : Program signature n g) (v : ↥(inputGates p) → Bool) : (attainableTranscripts p).card ≤ ∑ j ∈ Finset.range (inputActivityFrom p v + 1), (inputGates p).card.choose j

Attainable patterns are bounded by the exact binomial sum at the worst-case distance from any fixed baseline on input-reading gates.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_attainableTranscripts_le_sum_choose_gateActivityFrom {n g : ℕ} (p : Program signature n g) (v : Fin g → Bool) : (attainableTranscripts p).card ≤ ∑ j ∈ Finset.range (gateActivityFrom p v + 1), g.choose j

Projecting shifted gate valuations bounds attainable patterns by the binomial sum at the worst-case distance from any fixed baseline across all gates.