Threshold transcript trees and native scalar stages

A native weighted threshold program has a decision tree whose queries are native threshold lines reading only original inputs. It computes any output determined by the restricted transcript, has depth at most the number of input-reading gates, and has at most as many leaves as attained transcripts. Only nonempty answer branches are constructed.

The same tree gives a separable comparison tree for every split of the input coordinates by relabeling its queries. This preserves its exact structural depth and leaf count. All threshold comparisons retain the convention that equality returns true.

The circuit-to-tree construction is semantic and noncomputable; no efficient compiler is asserted.

In the other direction, ScalarStage.append emits a native adaptive scalar stage: one input-free indicator per supplied history pattern followed by one scalar query. A unique matching pattern selects its threshold; no match selects a baseline that can pad a terminated path with false. Earlier gate values and input coefficients are preserved. The helpers add no input-reading gates, and the query adds exactly one when its direct input vector is nonzero. With zero direct vector, zero selected thresholds and baseline one, the same stage recognizes whether any supplied pattern matches. These are stage-local results, not yet a whole-tree compiler or its global size/activity bound.

Main definitions

• Cslib.Circuits.Boolean.WeightedThreshold.gateQuery: a native input-only threshold line, with fixed earlier gate contributions absorbed into its threshold.
• Cslib.Circuits.Boolean.WeightedThreshold.inputOfSplit: assemble the two sides of an input.
• Cslib.Circuits.Boolean.WeightedThreshold.lineComparison: express an input-only threshold line as a separable comparison across a coordinate split.
• Cslib.Circuits.Boolean.WeightedThreshold.gateComparison: express a gate query with fixed earlier gate values as a separable comparison across a coordinate split.
• Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.prefixLine, .prefixBank, .queryLine, .append: native prefix indicators, their bank, a scalar query, and an adaptive stage.

Main results

• Cslib.Circuits.Boolean.WeightedThreshold.gateComparison_eval_eq, Cslib.Circuits.Boolean.WeightedThreshold.gateQuery_eval_eq: earlier gate values suffice to evaluate comparisons and queries.
• Cslib.Circuits.Boolean.WeightedThreshold.exists_linear_transcript_tree: a transcript determines a tree of native linear threshold queries, independent of any coordinate split.
• Cslib.Circuits.Boolean.WeightedThreshold.exists_transcript_tree: the corresponding separable comparison tree for any split.
• Cslib.Circuits.Boolean.WeightedThreshold.exists_gate_readout_tree: every fixed readout of the complete gate valuation is covered.
• Cslib.Circuits.Boolean.WeightedThreshold.exists_circuit_tree: designated gate outputs are computed simultaneously.
• Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.prefixLine_eval, .eval_append_last, .eval_append_of_match, .eval_append_of_no_match: indicator, selection and padding semantics.
• Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.eval_append_readout: the same constructor realizes the OR of its supplied pattern indicators without reading original inputs.
• Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.eval_append_castSucc, .inputWeight_append_castSucc, .inputWeight_append_flag, .inputWeight_append_last, .card_inputGates_append: preservation and exact direct-input cost of an emitted stage.

References

• Threshold Circuits as Decision Trees and Finite-State Programs, Lemma 3.1 and the stage construction in the proof of Theorem 4.1

def Cslib.Circuits.Boolean.WeightedThreshold.gateQuery {n g : ℕ} (p : Program signature n g) (gate : Fin g) (previous : Fin g → Bool) : Line signature n 0

With preceding gate values fixed, a gate is a native threshold line on original inputs. Its coefficients are aggregated by actual input wire, so cancelled slots contribute zero.

theorem Cslib.Circuits.Boolean.WeightedThreshold.gateQuery_eval_eq {n g : ℕ} (p : Program signature n g) (gate : Fin g) (previous : Fin g → Bool) (x : Fin n → Bool) (hprevious : ∀ j < gate, previous j = p.eval interpretation x j) : (gateQuery p gate previous).eval interpretation x Fin.elim0 = p.eval interpretation x gate

Earlier gate values suffice to evaluate the input-only query; current and later values do not affect it because their coefficients vanish.

theorem Cslib.Circuits.Boolean.WeightedThreshold.exists_linear_transcript_tree {n g : ℕ} {β : Type u_1} (p : Program signature n g) (output : (Fin n → Bool) → β) (hout : ∀ (x y : Fin n → Bool), transcript p x = transcript p y → output x = output y) : ∃ (t : DecisionTree (Line signature n 0) β), (∀ (x : Fin n → Bool), (t.eval fun (q : Line signature n 0) => q.eval interpretation x Fin.elim0) = output x) ∧ t.depth ≤ (inputGates p).card ∧ t.leafCount ≤ (Finset.image (transcript p) Finset.univ).card

Any output determined by the restricted transcript has a native linear-query tree. The tree is independent of coordinate splits; its leaves count only attainable transcripts.

def Cslib.Circuits.Boolean.WeightedThreshold.inputOfSplit {n : ℕ} {L : Type u_2} {R : Type u_3} (split : Fin n ≃ L ⊕ R) (x : L → Bool) (y : R → Bool) : Fin n → Bool

Assemble the left and right input coordinates using their partition equivalence.

def Cslib.Circuits.Boolean.WeightedThreshold.lineComparison {n : ℕ} {L : Type u_2} {R : Type u_3} [Fintype L] [Fintype R] (q : Line signature n 0) (split : Fin n ≃ L ⊕ R) : SeparableComparison (L → Bool) (R → Bool)

A native input-only threshold line is separable across every coordinate split. Repeated argument slots are aggregated by actual input wire.

theorem Cslib.Circuits.Boolean.WeightedThreshold.lineComparison_eval {n : ℕ} {L : Type u_2} {R : Type u_3} [Fintype L] [Fintype R] (q : Line signature n 0) (split : Fin n ≃ L ⊕ R) (x : L → Bool) (y : R → Bool) : (lineComparison q split).eval x y = q.eval interpretation (inputOfSplit split x y) Fin.elim0

Splitting a native input-only line preserves its answer, including threshold equality.

def Cslib.Circuits.Boolean.WeightedThreshold.gateComparison {n g : ℕ} {L : Type u_2} {R : Type u_3} [Fintype L] [Fintype R] (p : Program signature n g) (split : Fin n ≃ L ⊕ R) (gate : Fin g) (previous : Fin g → Bool) : SeparableComparison (L → Bool) (R → Bool)

With preceding gate values fixed, the remaining gate equation is a separable comparison of its direct input contributions.

theorem Cslib.Circuits.Boolean.WeightedThreshold.gateComparison_eval_eq {n g : ℕ} {L : Type u_2} {R : Type u_3} [Fintype L] [Fintype R] (p : Program signature n g) (split : Fin n ≃ L ⊕ R) (gate : Fin g) (previous : Fin g → Bool) (x : L → Bool) (y : R → Bool) (hprevious : ∀ j < gate, previous j = p.eval interpretation (inputOfSplit split x y) j) : (gateComparison p split gate previous).eval x y = p.eval interpretation (inputOfSplit split x y) gate

Earlier gate values suffice to evaluate the comparison; current and later values do not affect it because their coefficients vanish.

theorem Cslib.Circuits.Boolean.WeightedThreshold.exists_transcript_tree {n g : ℕ} {β : Type u_1} {L : Type u_2} {R : Type u_3} (p : Program signature n g) (split : Fin n ≃ L ⊕ R) (output : (Fin n → Bool) → β) (hout : ∀ (x y : Fin n → Bool), transcript p x = transcript p y → output x = output y) : ∃ (t : DecisionTree (SeparableComparison (L → Bool) (R → Bool)) β), (∀ (x : L → Bool) (y : R → Bool), (t.eval fun (q : SeparableComparison (L → Bool) (R → Bool)) => q.eval x y) = output (inputOfSplit split x y)) ∧ t.depth ≤ (inputGates p).card ∧ t.leafCount ≤ (Finset.image (transcript p) Finset.univ).card

Any output determined by the restricted transcript has a separable comparison tree of depth at most the input-reading count and with at most one leaf per attainable transcript.

theorem Cslib.Circuits.Boolean.WeightedThreshold.exists_gate_readout_tree {n g : ℕ} {β : Type u_1} {L : Type u_2} {R : Type u_3} (p : Program signature n g) (split : Fin n ≃ L ⊕ R) (readout : (Fin g → Bool) → β) : ∃ (t : DecisionTree (SeparableComparison (L → Bool) (R → Bool)) β), (∀ (x : L → Bool) (y : R → Bool), (t.eval fun (q : SeparableComparison (L → Bool) (R → Bool)) => q.eval x y) = readout (p.eval interpretation (inputOfSplit split x y))) ∧ t.depth ≤ (inputGates p).card ∧ t.leafCount ≤ (Finset.image (transcript p) Finset.univ).card

A fixed readout of all native gate values satisfies the transcript-tree bounds.

theorem Cslib.Circuits.Boolean.WeightedThreshold.exists_circuit_tree {n : ℕ} {L : Type u_2} {R : Type u_3} {m : ℕ} (c : Circuit signature n m) (split : Fin n ≃ L ⊕ R) (houtputs : ∀ (output : Fin m), ∃ (gate : Fin c.size), c.outputs output = Wire.gate gate) : ∃ (t : DecisionTree (SeparableComparison (L → Bool) (R → Bool)) (Fin m → Bool)), (∀ (x : L → Bool) (y : R → Bool), (t.eval fun (q : SeparableComparison (L → Bool) (R → Bool)) => q.eval x y) = c.eval interpretation (inputOfSplit split x y)) ∧ t.depth ≤ (inputGates c.program).card ∧ t.leafCount ≤ (Finset.image (transcript c.program) Finset.univ).card

A circuit whose outputs select gates has a comparison tree computing all designated outputs simultaneously, under the same depth and attainable-transcript leaf bounds.

Native scalar stages selected by transcript prefixes

def Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.prefixLine {n g d : ℕ} (reads : Fin d → Fin g) (pattern : Fin d → Bool) : Line signature n g

A single input-free gate testing whether selected earlier gates match a Boolean pattern. The selection may repeat wires; an inconsistent pattern then evaluates to false.

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.prefixLine_eval {n g d : ℕ} (reads : Fin d → Fin g) (pattern : Fin d → Bool) (x : Fin n → Bool) (z : Fin g → Bool) : (prefixLine reads pattern).eval interpretation x z = decide ((fun (j : Fin d) => z (reads j)) = pattern)

The prefix gate tests equality of the selected history with the pattern.

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.prefixLine_inputWeight {n g d : ℕ} (reads : Fin d → Fin g) (pattern : Fin d → Bool) (i : Fin n) : lineWeight (prefixLine reads pattern) (Wire.input i) = 0

Prefix indicators have no coefficient on any original input.

def Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.prefixBank {n g d : ℕ} (p : Program signature n g) (reads : Fin d → Fin g) (m : ℕ) : (Fin m → Fin d → Bool) → Program signature n (g + m)

Append a bank of prefix indicators, all reading the original program's selected gates. The program index charges exactly one new gate per supplied pattern.

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.prefixBank_eval_castAdd {n g d m : ℕ} (p : Program signature n g) (reads : Fin d → Fin g) (patterns : Fin m → Fin d → Bool) (x : Fin n → Bool) (j : Fin g) : (prefixBank p reads m patterns).eval interpretation x (Fin.castAdd m j) = p.eval interpretation x j

Extending a program by a prefix bank preserves its earlier gate values.

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.prefixBank_eval_natAdd {n g d m : ℕ} (p : Program signature n g) (reads : Fin d → Fin g) (patterns : Fin m → Fin d → Bool) (x : Fin n → Bool) (i : Fin m) : (prefixBank p reads m patterns).eval interpretation x (Fin.natAdd g i) = decide ((fun (j : Fin d) => p.eval interpretation x (reads j)) = patterns i)

Each newly appended bank gate computes its own pattern indicator.

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.prefixBank_inputWeight_castAdd {n g d m : ℕ} (p : Program signature n g) (reads : Fin d → Fin g) (patterns : Fin m → Fin d → Bool) (j : Fin g) (i : Fin n) : inputWeight (prefixBank p reads m patterns) (Fin.castAdd m j) i = inputWeight p j i

A prefix bank preserves the effective input coefficients of every earlier gate.

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.prefixBank_inputWeight_natAdd {n g d m : ℕ} (p : Program signature n g) (reads : Fin d → Fin g) (patterns : Fin m → Fin d → Bool) (i : Fin n) (j : Fin m) : inputWeight (prefixBank p reads m patterns) (Fin.natAdd g j) i = 0

Every new bank gate has zero direct input vector, including with repeated history wires.

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.card_inputGates_prefixBank {n g d m : ℕ} (p : Program signature n g) (reads : Fin d → Fin g) (patterns : Fin m → Fin d → Bool) : (inputGates (prefixBank p reads m patterns)).card = (inputGates p).card

Appending any prefix bank adds no input-reading gates.

def Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.queryLine {n g m : ℕ} (w : Fin n → ℝ) (flags : Fin m → Fin g) (adjust : Fin m → ℝ) (baseline : ℝ) : Line signature n g

A native scalar query with direct input vector w, plus a weighted sum of earlier flags.

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.queryLine_eval {n g m : ℕ} (w : Fin n → ℝ) (flags : Fin m → Fin g) (adjust : Fin m → ℝ) (baseline : ℝ) (x : Fin n → Bool) (z : Fin g → Bool) : (queryLine w flags adjust baseline).eval interpretation x z = decide (baseline ≤ ∑ i : Fin n, w i * ↑(x i).toNat + ∑ j : Fin m, adjust j * ↑(z (flags j)).toNat)

The query line evaluates the direct input score plus its flag adjustments.

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.queryLine_inputWeight {n g m : ℕ} (w : Fin n → ℝ) (flags : Fin m → Fin g) (adjust : Fin m → ℝ) (baseline : ℝ) (i : Fin n) : lineWeight (queryLine w flags adjust baseline) (Wire.input i) = w i

The effective coefficient on an original input is exactly the supplied coefficient.

def Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.append {n g d m : ℕ} (p : Program signature n g) (reads : Fin d → Fin g) (patterns : Fin m → Fin d → Bool) (w : Fin n → ℝ) (thresholds : Fin m → ℝ) (baseline : ℝ) : Program signature n (g + m + 1)

Append one adaptive scalar stage: a bank of m prefix indicators and one query. A matching pattern contributes baseline - threshold, so a unique match selects that threshold. No match leaves the baseline unchanged. The output gate is Fin.last (g + m).

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.eval_append_castSucc {n g d m : ℕ} (p : Program signature n g) (reads : Fin d → Fin g) (patterns : Fin m → Fin d → Bool) (w : Fin n → ℝ) (thresholds : Fin m → ℝ) (baseline : ℝ) (x : Fin n → Bool) (j : Fin g) : (append p reads patterns w thresholds baseline).eval interpretation x (Fin.castAdd m j).castSucc = p.eval interpretation x j

Appending a scalar stage preserves every earlier gate value.

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.eval_append_last {n g d m : ℕ} (p : Program signature n g) (reads : Fin d → Fin g) (patterns : Fin m → Fin d → Bool) (w : Fin n → ℝ) (thresholds : Fin m → ℝ) (baseline : ℝ) (x : Fin n → Bool) : (append p reads patterns w thresholds baseline).eval interpretation x (Fin.last (g + m)) = decide (baseline ≤ ∑ i : Fin n, w i * ↑(x i).toNat + ∑ a : Fin m, (baseline - thresholds a) * ↑(decide ((fun (j : Fin d) => p.eval interpretation x (reads j)) = patterns a)).toNat)

Exact semantics of the emitted query, without assuming distinct or reachable patterns.

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.eval_append_of_match {n g d m : ℕ} (p : Program signature n g) (reads : Fin d → Fin g) (patterns : Fin m → Fin d → Bool) (w : Fin n → ℝ) (thresholds : Fin m → ℝ) (baseline : ℝ) (x : Fin n → Bool) (a : Fin m) (hinj : Function.Injective patterns) (hmatch : (fun (j : Fin d) => p.eval interpretation x (reads j)) = patterns a) : (append p reads patterns w thresholds baseline).eval interpretation x (Fin.last (g + m)) = decide (thresholds a ≤ ∑ i : Fin n, w i * ↑(x i).toNat)

A unique matching prefix selects its threshold, with equality returning true.

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.eval_append_of_no_match {n g d m : ℕ} (p : Program signature n g) (reads : Fin d → Fin g) (patterns : Fin m → Fin d → Bool) (w : Fin n → ℝ) (thresholds : Fin m → ℝ) (baseline : ℝ) (x : Fin n → Bool) (hmiss : ∀ (a : Fin m), (fun (j : Fin d) => p.eval interpretation x (reads j)) ≠ patterns a) (hscore : ∑ i : Fin n, w i * ↑(x i).toNat < baseline) : (append p reads patterns w thresholds baseline).eval interpretation x (Fin.last (g + m)) = false

No matching live prefix pads the transcript with false when the score is below baseline.

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.eval_append_readout {n g d m : ℕ} (p : Program signature n g) (reads : Fin d → Fin g) (patterns : Fin m → Fin d → Bool) (x : Fin n → Bool) : (append p reads patterns (fun (x : Fin n) => 0) (fun (x : Fin m) => 0) 1).eval interpretation x (Fin.last (g + m)) = decide (∃ (a : Fin m), (fun (j : Fin d) => p.eval interpretation x (reads j)) = patterns a)

With zero direct vector and selected thresholds, baseline one computes the OR of the pattern indicators. This input-free readout uses the same stage constructor and permits repeated patterns as well as an empty accepting bank.

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.inputWeight_append_castSucc {n g d m : ℕ} (p : Program signature n g) (reads : Fin d → Fin g) (patterns : Fin m → Fin d → Bool) (w : Fin n → ℝ) (thresholds : Fin m → ℝ) (baseline : ℝ) (j : Fin g) (i : Fin n) : inputWeight (append p reads patterns w thresholds baseline) (Fin.castAdd m j).castSucc i = inputWeight p j i

The scalar stage preserves all prior direct input coefficients.

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.inputWeight_append_flag {n g d m : ℕ} (p : Program signature n g) (reads : Fin d → Fin g) (patterns : Fin m → Fin d → Bool) (w : Fin n → ℝ) (thresholds : Fin m → ℝ) (baseline : ℝ) (j : Fin m) (i : Fin n) : inputWeight (append p reads patterns w thresholds baseline) (Fin.natAdd g j).castSucc i = 0

The helper gates of a scalar stage have zero direct input coefficients.

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.inputWeight_append_last {n g d m : ℕ} (p : Program signature n g) (reads : Fin d → Fin g) (patterns : Fin m → Fin d → Bool) (w : Fin n → ℝ) (thresholds : Fin m → ℝ) (baseline : ℝ) (i : Fin n) : inputWeight (append p reads patterns w thresholds baseline) (Fin.last (g + m)) i = w i

The new query's direct input vector is exactly w.

theorem Cslib.Circuits.Boolean.WeightedThreshold.ScalarStage.card_inputGates_append {n g d m : ℕ} (p : Program signature n g) (reads : Fin d → Fin g) (patterns : Fin m → Fin d → Bool) (w : Fin n → ℝ) (thresholds : Fin m → ℝ) (baseline : ℝ) : (inputGates (append p reads patterns w thresholds baseline)).card = (inputGates p).card + if w = 0 then 0 else 1

A scalar stage adds exactly one input-reading gate when w ≠ 0, and none when w = 0. Its program index counts m + 1 new gates; the m prefix helpers are input-free.