Weighted threshold transcripts as linear-query trees

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.

This construction is semantic and noncomputable; no efficient compiler is asserted.

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.

Main results

• 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.

References

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

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.