Explicit bounds for the shallow-circuit recurrence

These elementary natural-number inequalities keep the size proof separate from the circuit construction. All constants are independent of the input length and the integer root scale.

theorem Complexity.Shallow.exp_mul_bound {k a b x y : ℕ} (hx : x ≤ 2 ^ (a * k)) (hy : y ≤ 2 ^ (b * k)) : x * y ≤ 2 ^ ((a + b) * k)

theorem Complexity.Shallow.exp_add_bound {k a b x y : ℕ} (hk : 1 ≤ k) (hx : x ≤ 2 ^ (a * k)) (hy : y ≤ 2 ^ (b * k)) : x + y ≤ 2 ^ ((a + b + 1) * k)

theorem Complexity.Shallow.exp_const_bound (c k : ℕ) (hk : 1 ≤ k) : c ≤ 2 ^ (c * k)

theorem Complexity.Shallow.construction_size_bound {k n U V B N A D E : ℕ} (hk : 1 ≤ k) (hn : n ≤ 2 ^ (N * k)) (hu : U ≤ A * k) (hv : V ≤ 2 ^ (D * k)) (hb : B ≤ 2 ^ (E * k)) : 1 + (n + 1) * (1 + 3 ^ U * (n + 1) * (2 + V * (B + 2))) ≤ 2 ^ ((2 * A + 2 * N + D + E + 8) * k)

A bound for the entire finite construction, with only its three summary parameters: input count, sum of moduli, and sum of squared moduli.

theorem Complexity.Shallow.sum_sq_moduli_bound {r C k : ℕ} (hk : 1 ≤ k) (m : Fin r → ℕ) (hm : ∀ (i : Fin r), m i ≤ C * k) : ∑ i : Fin r, m i ^ 2 ≤ 2 ^ ((r + 2 * C + 2) * k)

Polynomial factors in the moduli fit into the exponential envelope.

theorem Complexity.Shallow.pair_size_bound {n d k m : ℕ} (hk : 1 ≤ k) (hn : n ≤ k ^ (d + 2)) (hm : k ≤ m) : 2 * (n / m + 1) ≤ (4 * k) ^ (d + 1)

Two blocks fit into the smaller instance used by the depth induction.