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 weighted sum weightedSum 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 weightedSum w (eval_eq_of_weightedSum_between, transcript_eq_of_weightedSum_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.

Conversely, a supplied ordered class index on the Boolean cube can be computed by real threshold comparisons along weightedSum w with the exact ordered-tree capacity (exists_scalarComparisonTree_iff). Scores may tie within a class; distinct ordered classes must have strictly separated scores. Relabelling integer queries preserves the tree shape, depth and true-answer energy. This supplies the real-score tree, not the subsequent compilation into a fixed number of native input-reading circuit stages.

Main definitions

• Cslib.Circuits.Boolean.WeightedThreshold.leInputs, Cslib.Circuits.Boolean.WeightedThreshold.scalarRep: inputs with scalar score at most t and a canonical representative input for t.
• 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 weightedSum w.

Main results

• Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_of_weightedSum_between, Cslib.Circuits.Boolean.WeightedThreshold.transcript_eq_of_weightedSum_between: order-convexity of gate evaluations and transcripts along weightedSum 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 weightedSum w.
• Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_mul_card_attainableTranscripts_of_direction, WeightedThreshold.two_pow_lt_mul_max_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).
• Cslib.Circuits.Boolean.WeightedThreshold.exists_scalarComparisonTree_iff: real threshold trees realizing a supplied ordered class index, with exact structural leaf count and bounded depth and true-answer energy.

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

theorem Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_of_weightedSum_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₁₂ : weightedSum w x₁ ≤ weightedSum w x₂) (h₂₃ : weightedSum w x₂ ≤ weightedSum 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, weightedSum w x₁ ≤ weightedSum w x₂ ≤ weightedSum 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_weightedSum_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₁₂ : weightedSum w x₁ ≤ weightedSum w x₂) (h₂₃ : weightedSum w x₂ ≤ weightedSum 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_weightedSum_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 : weightedSum w x₁ = weightedSum w x₂) : p.eval interpretation x₁ = p.eval interpretation x₂

Inputs with equal scalar score have identical gate evaluations.

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

The number of attainable transcripts of p is positive.

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.scalarRep {n : ℕ} (w : Fin n → ℝ) (t : ℝ) : Fin n → Bool

Representative input at scalar threshold t: an input in leInputs w t maximizing weightedSum w when leInputs w t is nonempty, and a global minimizer of weightedSum 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 weightedSum 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 weightedSum 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 weightedSum w.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.scalarEval_weightedSum {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 (weightedSum w x) = p.eval interpretation x

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

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.scalarTranscript_weightedSum {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 (weightedSum w x) = transcript p x

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

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.scalarReadout_weightedSum {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 (weightedSum w x) = readout (p.eval interpretation x)

Evaluating scalarReadout p w readout at weightedSum 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_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 (weightedSum 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 (weightedSum 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 (weightedSum 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.

Real-score realization of ordered class indices

theorem Cslib.Circuits.Boolean.WeightedThreshold.exists_scalarComparisonTree_iff {n : ℕ} (w : Fin n → ℝ) (index : (Fin n → Bool) → ℕ) (q e L : ℕ) (hbound : ∀ (x : Fin n → Bool), index x < L) (horder : ∀ (x y : Fin n → Bool), index x < index y → weightedSum w x < weightedSum w y) : (∃ (t : DecisionTree ℝ ℕ), t.leafCount = L ∧ t.depth ≤ q ∧ t.energy ≤ e ∧ ∀ (x : Fin n → Bool), (t.eval fun (θ : ℝ) => decide (θ ≤ weightedSum w x)) = index x) ↔ 0 < L ∧ L ≤ BitString.ballSize q e

Real-score realization of ordered query-activity capacity. Suppose index labels ordered score classes by natural numbers below L: whenever one label is smaller than another, every score in the first class is strictly below every score in the second. There is a tree of real comparisons θ ≤ weightedSum w x, with exactly L structural leaves, depth at most q, and true-answer energy at most e, returning index x on every input, exactly when 0 < L ≤ ballSize q e.

Scores may tie within a class. If every index below L occurs, every counted leaf is reachable; otherwise the exact structural leaf count can include unreachable leaves. No minimality of the supplied class partition is asserted. This is the real-score realization step in the proof of Theorem 4.1 of [26], not the native circuit compiler.