Inner-product lower bounds for separable and bi-monotone comparison trees

A separable-comparison or bi-monotone-comparison tree computing the inner product modulo two on ι → Bool has leaf count L satisfying 2 ^ Fintype.card ι ≤ L ^ 2. This division-free form of L ≥ 2 ^ (Fintype.card ι / 2) follows from the generic leaf-rectangle theorem and the Hadamard rectangle bound. Query scores are arbitrary real functions; the result imposes no restriction on their magnitudes or on the tree depth, and does not require a threshold circuit model.

Combining the leaf bound with the structural leaf bounds in Leaves.lean and the partial binomial-sum estimates in Complexity/Foundations/Data/Nat/Choose/Real.lean yields internal-node, decision-list, bounded-rank, and bounded-energy lower bounds for inner product.

Main results

• Cslib.DecisionTree.two_pow_le_leafCount_sq_of_biMonotone_hadamardCode, Cslib.DecisionTree.two_pow_le_leafCount_sq_of_hadamardCode: the inner-product leaf bounds.
• Cslib.DecisionTree.two_pow_le_nodeCount_add_one_sq_of_hadamardCode: the internal-node bound.
• Cslib.DecisionTree.two_pow_le_depth_add_one_sq_of_isDecisionList_hadamardCode: the decision-list depth bound.
• Cslib.DecisionTree.two_pow_le_sum_choose_rank_sq_of_hadamardCode, Cslib.DecisionTree.le_rank_mul_logb_depth_of_hadamardCode, Cslib.DecisionTree.rank_mul_rpow_le_depth_of_hadamardCode: bounded-rank tradeoffs.
• Cslib.DecisionTree.two_pow_le_sum_choose_energy_sq_of_hadamardCode, Cslib.DecisionTree.le_energy_mul_logb_depth_of_hadamardCode, Cslib.DecisionTree.energy_mul_rpow_le_depth_of_hadamardCode: tree-energy tradeoffs.

References

• [Threshold Circuits as Decision Trees and Finite-State Programs, Corollaries 2.5, 2.7, and 2.8] [26]

theorem Cslib.DecisionTree.two_pow_le_leafCount_sq_of_biMonotone_hadamardCode {ι : Type u_1} [Fintype ι] (t : DecisionTree (BiMonotoneComparison (ι → Bool) (ι → Bool)) Bool) (ht : ∀ (x y : ι → Bool), (t.eval fun (q : BiMonotoneComparison (ι → Bool) (ι → Bool)) => q.eval x y) = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ t.leafCount ^ 2

Computing inner product modulo two with a bi-monotone comparison tree requires the square of the leaf count to be at least the cardinality of the Boolean cube. The statement includes zero coordinates.

theorem Cslib.DecisionTree.two_pow_le_leafCount_sq_of_hadamardCode {ι : Type u_1} [Fintype ι] (t : DecisionTree (SeparableComparison (ι → Bool) (ι → Bool)) Bool) (ht : ∀ (x y : ι → Bool), (t.eval fun (q : SeparableComparison (ι → Bool) (ι → Bool)) => q.eval x y) = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ t.leafCount ^ 2

Computing inner product modulo two requires the square of the leaf count to be at least the cardinality of the Boolean cube. The statement includes zero coordinates.

theorem Cslib.DecisionTree.two_pow_le_nodeCount_add_one_sq_of_biMonotone_hadamardCode {ι : Type u_1} [Fintype ι] (t : DecisionTree (BiMonotoneComparison (ι → Bool) (ι → Bool)) Bool) (ht : ∀ (x y : ι → Bool), (t.eval fun (q : BiMonotoneComparison (ι → Bool) (ι → Bool)) => q.eval x y) = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ (t.nodeCount + 1) ^ 2

Every bi-monotone comparison tree computing inner product modulo two satisfies 2 ^ Fintype.card ι ≤ (nodeCount + 1) ^ 2.

theorem Cslib.DecisionTree.two_pow_le_nodeCount_add_one_sq_of_hadamardCode {ι : Type u_1} [Fintype ι] (t : DecisionTree (SeparableComparison (ι → Bool) (ι → Bool)) Bool) (ht : ∀ (x y : ι → Bool), (t.eval fun (q : SeparableComparison (ι → Bool) (ι → Bool)) => q.eval x y) = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ (t.nodeCount + 1) ^ 2

Every separable-comparison tree computing inner product modulo two satisfies 2 ^ Fintype.card ι ≤ (nodeCount + 1) ^ 2.

theorem Cslib.DecisionTree.two_pow_le_depth_add_one_sq_of_rank_le_one_hadamardCode {ι : Type u_1} [Fintype ι] (t : DecisionTree (SeparableComparison (ι → Bool) (ι → Bool)) Bool) (hr : t.rank ≤ 1) (ht : ∀ (x y : ι → Bool), (t.eval fun (q : SeparableComparison (ι → Bool) (ι → Bool)) => q.eval x y) = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ (t.depth + 1) ^ 2

Every separable-comparison tree of rank at most 1 computing inner product modulo two satisfies 2 ^ Fintype.card ι ≤ (depth + 1) ^ 2.

theorem Cslib.DecisionTree.two_pow_le_depth_add_one_sq_of_isDecisionList_hadamardCode {ι : Type u_1} [Fintype ι] (t : DecisionTree (SeparableComparison (ι → Bool) (ι → Bool)) Bool) (hl : t.IsDecisionList) (ht : ∀ (x y : ι → Bool), (t.eval fun (q : SeparableComparison (ι → Bool) (ι → Bool)) => q.eval x y) = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ (t.depth + 1) ^ 2

Every separable-comparison decision list computing inner product modulo two satisfies 2 ^ Fintype.card ι ≤ (depth + 1) ^ 2.

theorem Cslib.DecisionTree.two_pow_le_nodeCount_add_one_sq_of_isDecisionList_hadamardCode {ι : Type u_1} [Fintype ι] (t : DecisionTree (SeparableComparison (ι → Bool) (ι → Bool)) Bool) (_hl : t.IsDecisionList) (ht : ∀ (x y : ι → Bool), (t.eval fun (q : SeparableComparison (ι → Bool) (ι → Bool)) => q.eval x y) = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ (t.nodeCount + 1) ^ 2

Every separable-comparison decision list computing inner product modulo two satisfies 2 ^ Fintype.card ι ≤ (nodeCount + 1) ^ 2.

theorem Cslib.DecisionTree.two_pow_le_sum_choose_rank_sq_of_biMonotone_hadamardCode {ι : Type u_1} [Fintype ι] (t : DecisionTree (BiMonotoneComparison (ι → Bool) (ι → Bool)) Bool) (ht : ∀ (x y : ι → Bool), (t.eval fun (q : BiMonotoneComparison (ι → Bool) (ι → Bool)) => q.eval x y) = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ (∑ j ∈ Finset.range (t.rank + 1), t.depth.choose j) ^ 2

Every bi-monotone comparison tree computing inner product modulo two satisfies the binomial-sum rank-depth lower bound 2 ^ Fintype.card ι ≤ (∑ j ≤ rank, depth.choose j) ^ 2.

theorem Cslib.DecisionTree.two_pow_le_sum_choose_rank_sq_of_hadamardCode {ι : Type u_1} [Fintype ι] (t : DecisionTree (SeparableComparison (ι → Bool) (ι → Bool)) Bool) (ht : ∀ (x y : ι → Bool), (t.eval fun (q : SeparableComparison (ι → Bool) (ι → Bool)) => q.eval x y) = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ (∑ j ∈ Finset.range (t.rank + 1), t.depth.choose j) ^ 2

Every separable-comparison tree computing inner product modulo two satisfies the binomial-sum rank-depth lower bound 2 ^ Fintype.card ι ≤ (∑ j ≤ rank, depth.choose j) ^ 2.

theorem Cslib.DecisionTree.le_rank_mul_logb_depth_of_hadamardCode {ι : Type u_1} [Fintype ι] (t : DecisionTree (SeparableComparison (ι → Bool) (ι → Bool)) Bool) (ht : ∀ (x y : ι → Bool), (t.eval fun (q : SeparableComparison (ι → Bool) (ι → Bool)) => q.eval x y) = BitString.hadamardCode x y) : ↑(Fintype.card ι) / 2 ≤ ↑t.rank * Real.logb 2 (Real.exp 1 * ↑t.depth / ↑t.rank)

Logarithmic rank-depth tradeoff for a separable-comparison tree computing inner product modulo two. At rank zero, this forces Fintype.card ι = 0.

theorem Cslib.DecisionTree.rank_mul_rpow_le_depth_of_hadamardCode {ι : Type u_1} [Fintype ι] (t : DecisionTree (SeparableComparison (ι → Bool) (ι → Bool)) Bool) (ht : ∀ (x y : ι → Bool), (t.eval fun (q : SeparableComparison (ι → Bool) (ι → Bool)) => q.eval x y) = BitString.hadamardCode x y) : ↑t.rank / Real.exp 1 * 2 ^ (↑(Fintype.card ι) / (2 * ↑t.rank)) ≤ ↑t.depth

Depth lower bound in terms of rank for a separable-comparison tree computing inner product modulo two: (rank / exp 1) * 2 ^ (m / (2 * rank)) ≤ depth.

theorem Cslib.DecisionTree.two_pow_le_sum_choose_energy_sq_of_biMonotone_hadamardCode {ι : Type u_1} [Fintype ι] (t : DecisionTree (BiMonotoneComparison (ι → Bool) (ι → Bool)) Bool) (ht : ∀ (x y : ι → Bool), (t.eval fun (q : BiMonotoneComparison (ι → Bool) (ι → Bool)) => q.eval x y) = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ (∑ j ∈ Finset.range (t.energy + 1), t.depth.choose j) ^ 2

Every bi-monotone comparison tree computing inner product modulo two satisfies the binomial-sum energy-depth lower bound 2 ^ Fintype.card ι ≤ (∑ j ≤ energy, depth.choose j) ^ 2.

theorem Cslib.DecisionTree.two_pow_le_sum_choose_energy_sq_of_hadamardCode {ι : Type u_1} [Fintype ι] (t : DecisionTree (SeparableComparison (ι → Bool) (ι → Bool)) Bool) (ht : ∀ (x y : ι → Bool), (t.eval fun (q : SeparableComparison (ι → Bool) (ι → Bool)) => q.eval x y) = BitString.hadamardCode x y) : 2 ^ Fintype.card ι ≤ (∑ j ∈ Finset.range (t.energy + 1), t.depth.choose j) ^ 2

Every separable-comparison tree computing inner product modulo two satisfies the binomial-sum energy-depth lower bound 2 ^ Fintype.card ι ≤ (∑ j ≤ energy, depth.choose j) ^ 2.

theorem Cslib.DecisionTree.le_energy_mul_logb_depth_of_hadamardCode {ι : Type u_1} [Fintype ι] (t : DecisionTree (SeparableComparison (ι → Bool) (ι → Bool)) Bool) (ht : ∀ (x y : ι → Bool), (t.eval fun (q : SeparableComparison (ι → Bool) (ι → Bool)) => q.eval x y) = BitString.hadamardCode x y) : ↑(Fintype.card ι) / 2 ≤ ↑t.energy * Real.logb 2 (Real.exp 1 * ↑t.depth / ↑t.energy)

Logarithmic energy-depth tradeoff for a separable-comparison tree computing inner product modulo two. At energy zero, this forces Fintype.card ι = 0.

theorem Cslib.DecisionTree.energy_mul_rpow_le_depth_of_hadamardCode {ι : Type u_1} [Fintype ι] (t : DecisionTree (SeparableComparison (ι → Bool) (ι → Bool)) Bool) (ht : ∀ (x y : ι → Bool), (t.eval fun (q : SeparableComparison (ι → Bool) (ι → Bool)) => q.eval x y) = BitString.hadamardCode x y) : ↑t.energy / Real.exp 1 * 2 ^ (↑(Fintype.card ι) / (2 * ↑t.energy)) ≤ ↑t.depth

Depth lower bound in terms of energy for a separable-comparison tree computing inner product modulo two: (energy / exp 1) * 2 ^ (m / (2 * energy)) ≤ depth.