Scalar query-activity run capacity

When every gate of a weighted threshold program p reads the original inputs along a single direction w : Fin n → ℝ (∀ j, ∃ c : ℝ, inputWeight p j = c • w), fixing the restricted input-reading transcript transcript p x turns every gate condition into a half-line condition on the scalar score scalarScore w x = ∑ i, w i * (x i).toNat. Consequently, the fibers of transcript p (and of the full gate evaluation p.eval interpretation) are order-convex along scalarScore w (eval_eq_of_scalarScore_between, transcript_eq_of_scalarScore_between).

Extending the evaluation from the finite set of realized scalar scores to all of ℝ produces a one-dimensional step function scalarEval p w : ℝ → (Fin g → Bool) whose level sets are indexed by the monotone count of transcripts realized up to t. This yields at most (attainableTranscripts p).card pieces (piecesAtMost_scalarEval, piecesAtMost_scalarTranscript, piecesAtMost_scalarReadout) and at most (attainableTranscripts p).card - 1 changes (changesAtMost_scalarReadout), bounding the length of any score-ordered alternating run of outputs by (attainableTranscripts p).card and hence by the Hamming-ball sums at inputActivity p and gateActivity p (Theorem 4.1 of [ThresholdCircuitRepresentations2026]). Combining this one-dimensional representation with the multilevel rectangle-free capacity bound gives the scalar activity lower bounds for two-sided K-rectangle-free functions (Corollary 4.2). Cover's enumerative coding for weight-bounded words (Theorem 4.3) is in Complexity.Foundations.Data.BitString.CoverCoding.

Main definitions

• Cslib.Circuits.Boolean.WeightedThreshold.scalarScore: directional projection ∑ i, w i * (x i).toNat.
• Cslib.Circuits.Boolean.WeightedThreshold.scalarEval, Cslib.Circuits.Boolean.WeightedThreshold.scalarTranscript, Cslib.Circuits.Boolean.WeightedThreshold.scalarReadout: extension of gate evaluation, input-reading transcripts, and readouts to ℝ along scalarScore w.

Main results

• Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_of_scalarScore_between, Cslib.Circuits.Boolean.WeightedThreshold.transcript_eq_of_scalarScore_between: order-convexity of gate evaluations and transcripts along scalarScore w.
• Cslib.Circuits.Boolean.WeightedThreshold.piecesAtMost_scalarTranscript, Cslib.Circuits.Boolean.WeightedThreshold.piecesAtMost_scalarReadout, Cslib.Circuits.Boolean.WeightedThreshold.changesAtMost_scalarReadout: piece and change bounds in terms of (attainableTranscripts p).card (Theorem 4.1).
• Cslib.Circuits.Boolean.WeightedThreshold.length_le_card_attainableTranscripts_of_isChain, Cslib.Circuits.Boolean.WeightedThreshold.length_le_sum_choose_of_isChain, Cslib.Circuits.Boolean.WeightedThreshold.length_le_sum_choose_gateActivity_of_isChain: alternating-run capacity bounds along scalarScore w.
• Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_mul_card_attainableTranscripts_of_direction, Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_mul_sum_choose_of_direction, Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_mul_sum_choose_gateActivity_of_direction: rectangle-free scalar activity bounds (Corollary 4.2).

References

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

Section 4.1: Order-convexity of scalar-direction transcripts and run capacity

def Cslib.Circuits.Boolean.WeightedThreshold.scalarScore {n : ℕ} (w : Fin n → ℝ) (x : Fin n → Bool) : ℝ

The scalar score ∑ i, w i * (x i).toNat of a Boolean input x along direction w.

theorem Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_of_scalarScore_between {n g : ℕ} (p : Program signature n g) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) {x₁ x₂ x₃ : Fin n → Bool} (h₁₂ : scalarScore w x₁ ≤ scalarScore w x₂) (h₂₃ : scalarScore w x₂ ≤ scalarScore w x₃) (htr : transcript p x₁ = transcript p x₃) : p.eval interpretation x₂ = p.eval interpretation x₁

Order-convexity of gate evaluations along a scalar direction: if every gate's input weight vector is a multiple of w, scalarScore w x₁ ≤ scalarScore w x₂ ≤ scalarScore w x₃, and transcript p x₁ = transcript p x₃, then p.eval interpretation x₂ = p.eval interpretation x₁.

theorem Cslib.Circuits.Boolean.WeightedThreshold.transcript_eq_of_scalarScore_between {n g : ℕ} (p : Program signature n g) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) {x₁ x₂ x₃ : Fin n → Bool} (h₁₂ : scalarScore w x₁ ≤ scalarScore w x₂) (h₂₃ : scalarScore w x₂ ≤ scalarScore w x₃) (htr : transcript p x₁ = transcript p x₃) : transcript p x₂ = transcript p x₁

Order-convexity of input-reading transcripts along a scalar direction.

theorem Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_of_scalarScore_eq {n g : ℕ} (p : Program signature n g) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) {x₁ x₂ : Fin n → Bool} (h : scalarScore w x₁ = scalarScore w x₂) : p.eval interpretation x₁ = p.eval interpretation x₂

Inputs with equal scalar score have identical gate evaluations.

theorem Cslib.Circuits.Boolean.WeightedThreshold.transcript_eq_of_scalarScore_eq {n g : ℕ} (p : Program signature n g) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) {x₁ x₂ : Fin n → Bool} (h : scalarScore w x₁ = scalarScore w x₂) : transcript p x₁ = transcript p x₂

Inputs with equal scalar score have identical input-reading transcripts.

theorem Cslib.Circuits.Boolean.WeightedThreshold.attainableTranscripts_nonempty {n g : ℕ} (p : Program signature n g) : (attainableTranscripts p).Nonempty

The set of attainable transcripts is always nonempty.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_attainableTranscripts_pos {n g : ℕ} (p : Program signature n g) : 0 < (attainableTranscripts p).card

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.leInputs {n : ℕ} (w : Fin n → ℝ) (t : ℝ) : Finset (Fin n → Bool)

Boolean inputs with scalar score at most t.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.leTranscripts {n g : ℕ} (p : Program signature n g) (w : Fin n → ℝ) (t : ℝ) : Finset (↥(inputGates p) → Bool)

Input-reading transcripts realized by inputs with scalar score at most t.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.scalarRep {n : ℕ} (w : Fin n → ℝ) (t : ℝ) : Fin n → Bool

Representative input at scalar threshold t: an input in leInputs w t maximizing scalarScore w when leInputs w t is nonempty, and a global minimizer of scalarScore w otherwise.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.scalarEval {n g : ℕ} (p : Program signature n g) (w : Fin n → ℝ) (t : ℝ) : Fin g → Bool

One-dimensional extension of gate evaluation along scalarScore w.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.scalarTranscript {n g : ℕ} (p : Program signature n g) (w : Fin n → ℝ) (t : ℝ) : ↥(inputGates p) → Bool

One-dimensional extension of the input-reading transcript along scalarScore w.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.scalarReadout {n g : ℕ} {β : Type u_1} (p : Program signature n g) (w : Fin n → ℝ) (readout : (Fin g → Bool) → β) (t : ℝ) : β

One-dimensional extension of a gate readout along scalarScore w.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.scalarEval_scalarScore {n g : ℕ} (p : Program signature n g) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) (x : Fin n → Bool) : scalarEval p w (scalarScore w x) = p.eval interpretation x

Evaluating scalarEval p w at scalarScore w x recovers p.eval interpretation x.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.scalarTranscript_scalarScore {n g : ℕ} (p : Program signature n g) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) (x : Fin n → Bool) : scalarTranscript p w (scalarScore w x) = transcript p x

Evaluating scalarTranscript p w at scalarScore w x recovers transcript p x.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.scalarReadout_scalarScore {n g : ℕ} {β : Type u_1} (p : Program signature n g) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) (readout : (Fin g → Bool) → β) (x : Fin n → Bool) : scalarReadout p w readout (scalarScore w x) = readout (p.eval interpretation x)

Evaluating scalarReadout p w readout at scalarScore w x recovers readout (p.eval interpretation x).

theorem Cslib.Circuits.Boolean.WeightedThreshold.piecesAtMost_scalarEval {n g : ℕ} (p : Program signature n g) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) : PiecesAtMost (scalarEval p w) (attainableTranscripts p).card

Theorem 4.1 (Piece bound for scalar-direction gate evaluation): when every gate reads inputs along w, scalarEval p w has at most (attainableTranscripts p).card pieces on ℝ.

theorem Cslib.Circuits.Boolean.WeightedThreshold.piecesAtMost_scalarTranscript {n g : ℕ} (p : Program signature n g) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) : PiecesAtMost (scalarTranscript p w) (attainableTranscripts p).card

Theorem 4.1 (Piece bound for scalar-direction transcripts): scalarTranscript p w has at most (attainableTranscripts p).card pieces on ℝ.

theorem Cslib.Circuits.Boolean.WeightedThreshold.piecesAtMost_scalarReadout {n g : ℕ} {β : Type u_1} (p : Program signature n g) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) (readout : (Fin g → Bool) → β) : PiecesAtMost (scalarReadout p w readout) (attainableTranscripts p).card

Theorem 4.1 (Piece bound for scalar-direction readouts): for any readout of the gate values, scalarReadout p w readout has at most (attainableTranscripts p).card pieces on ℝ.

theorem Cslib.Circuits.Boolean.WeightedThreshold.changesAtMost_scalarReadout {n g : ℕ} {β : Type u_1} (p : Program signature n g) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) (readout : (Fin g → Bool) → β) : ChangesAtMost (scalarReadout p w readout) ((attainableTranscripts p).card - 1)

Theorem 4.1 (Change bound for scalar-direction readouts): scalarReadout p w readout changes at most (attainableTranscripts p).card - 1 times along ℝ.

theorem Cslib.Circuits.Boolean.WeightedThreshold.length_le_succ_of_changesAtMost_of_isChain {α : Type u_1} {β : Type u_2} [Preorder α] {Φ : α → β} {T : ℕ} (hΦ : ChangesAtMost Φ T) {ts : List α} (hmono : List.IsChain (fun (x1 x2 : α) => x1 ≤ x2) ts) (halt : List.IsChain (fun (x1 x2 : β) => x1 ≠ x2) (List.map Φ ts)) : ts.length ≤ T + 1

Any ordered list ts along which Φ alternates between consecutive elements has length at most T + 1 whenever ChangesAtMost Φ T.

theorem Cslib.Circuits.Boolean.WeightedThreshold.length_le_card_attainableTranscripts_of_isChain {n g : ℕ} {β : Type u_1} (p : Program signature n g) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) (readout : (Fin g → Bool) → β) {xs : List (Fin n → Bool)} (hmono : List.IsChain (fun (x1 x2 : ℝ) => x1 ≤ x2) (List.map (scalarScore w) xs)) (halt : List.IsChain (fun (x1 x2 : β) => x1 ≠ x2) (List.map (fun (x : Fin n → Bool) => readout (p.eval interpretation x)) xs)) : xs.length ≤ (attainableTranscripts p).card

Theorem 4.1 (Alternating-run capacity bound): if xs : List (Fin n → Bool) has nondecreasing scalar scores along w and alternating readout values, then xs.length ≤ (attainableTranscripts p).card.

theorem Cslib.Circuits.Boolean.WeightedThreshold.length_le_sum_choose_of_isChain {n g : ℕ} {β : Type u_1} (p : Program signature n g) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) (readout : (Fin g → Bool) → β) {xs : List (Fin n → Bool)} (hmono : List.IsChain (fun (x1 x2 : ℝ) => x1 ≤ x2) (List.map (scalarScore w) xs)) (halt : List.IsChain (fun (x1 x2 : β) => x1 ≠ x2) (List.map (fun (x : Fin n → Bool) => readout (p.eval interpretation x)) xs)) : xs.length ≤ ∑ j ∈ Finset.range (inputActivity p + 1), (inputGates p).card.choose j

Theorem 4.1 (Input-activity run capacity bound): any score-ordered list of inputs with alternating readout values has length at most ∑ j ∈ range (inputActivity p + 1), q.choose j.

theorem Cslib.Circuits.Boolean.WeightedThreshold.length_le_sum_choose_gateActivity_of_isChain {n g : ℕ} {β : Type u_1} (p : Program signature n g) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) (readout : (Fin g → Bool) → β) {xs : List (Fin n → Bool)} (hmono : List.IsChain (fun (x1 x2 : ℝ) => x1 ≤ x2) (List.map (scalarScore w) xs)) (halt : List.IsChain (fun (x1 x2 : β) => x1 ≠ x2) (List.map (fun (x : Fin n → Bool) => readout (p.eval interpretation x)) xs)) : xs.length ≤ ∑ j ∈ Finset.range (gateActivity p + 1), g.choose j

Theorem 4.1 (Gate-activity run capacity bound): any score-ordered list of inputs with alternating readout values has length at most ∑ j ∈ range (gateActivity p + 1), g.choose j.

Section 4.2: Scalar activity for two-sided rectangle-free functions

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_mul_max_card_attainableTranscripts_of_direction {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) {f : BooleanFunction n} {K : ℕ} (hreadout : ∀ (x : Fin n → Bool), readout (p.eval interpretation x) = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) : 2 ^ n < 4 * K ^ 2 * max 1 (4 * ((attainableTranscripts p).card - 1))

Corollary 4.2 (Sharp attainable-transcript capacity bound): if a single-direction threshold program computes a two-sided K-rectangle-free Boolean function f, then 2 ^ n < 4 * K ^ 2 * max 1 (4 * ((attainableTranscripts p).card - 1)).

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_mul_card_attainableTranscripts_of_direction {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) {f : BooleanFunction n} {K : ℕ} (hreadout : ∀ (x : Fin n → Bool), readout (p.eval interpretation x) = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) : 2 ^ n < 16 * K ^ 2 * (attainableTranscripts p).card

Corollary 4.2 (Attainable-transcript capacity bound): if a single-direction threshold program computes a two-sided K-rectangle-free Boolean function f, then 2 ^ n < 16 * K ^ 2 * (attainableTranscripts p).card.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_mul_sum_choose_of_direction {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) {f : BooleanFunction n} {K : ℕ} (hreadout : ∀ (x : Fin n → Bool), readout (p.eval interpretation x) = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) : 2 ^ n < 16 * K ^ 2 * ∑ j ∈ Finset.range (inputActivity p + 1), (inputGates p).card.choose j

Corollary 4.2 (Input-activity capacity bound): if a single-direction threshold program computes a two-sided K-rectangle-free Boolean function f, then 2 ^ n < 16 * K ^ 2 * ∑ j ∈ range (inputActivity p + 1), (inputGates p).card.choose j.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_mul_sum_choose_gateActivity_of_direction {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) (w : Fin n → ℝ) (hw : ∀ (j : Fin g), ∃ (c : ℝ), inputWeight p j = c • w) {f : BooleanFunction n} {K : ℕ} (hreadout : ∀ (x : Fin n → Bool), readout (p.eval interpretation x) = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) : 2 ^ n < 16 * K ^ 2 * ∑ j ∈ Finset.range (gateActivity p + 1), g.choose j

Corollary 4.2 (Gate-activity capacity bound): if a single-direction threshold program computes a two-sided K-rectangle-free Boolean function f, then 2 ^ n < 16 * K ^ 2 * ∑ j ∈ range (gateActivity p + 1), g.choose j.

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_two_pow_lt_mul_sum_choose_of_direction {n : ℕ} (c : Circuit signature n 1) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) (w : Fin n → ℝ) (hw : ∀ (j : Fin c.size), ∃ (a : ℝ), inputWeight c.program j = a • w) {f : BooleanFunction n} {K : ℕ} (hcomputes : ∀ (x : Fin n → Bool), c.eval interpretation x 0 = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) : 2 ^ n < 16 * K ^ 2 * ∑ j ∈ Finset.range (inputActivity c.program + 1), (inputGates c.program).card.choose j

Single-output circuit form of two_pow_lt_mul_sum_choose_of_direction.

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_two_pow_lt_mul_sum_choose_gateActivity_of_direction {n : ℕ} (c : Circuit signature n 1) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) (w : Fin n → ℝ) (hw : ∀ (j : Fin c.size), ∃ (a : ℝ), inputWeight c.program j = a • w) {f : BooleanFunction n} {K : ℕ} (hcomputes : ∀ (x : Fin n → Bool), c.eval interpretation x 0 = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) : 2 ^ n < 16 * K ^ 2 * ∑ j ∈ Finset.range (gateActivity c.program + 1), c.size.choose j

Single-output circuit form of two_pow_lt_mul_sum_choose_gateActivity_of_direction.