Transient depths by binary search

A threshold μ < 2 ^ n is found with one query μ ≤ v per binary digit: keep the largest candidate below μ found so far (searchBelow), and output one more than it, or zero (searchBelow_result). Given circuits for the queries, this costs n + 1 queries and a few word operations per digit (synthesis_threshold).

For the transient depth, the query transientDepth f x ≤ v asks whether f^[v] x is periodic: one input-time iteration and one periodicity test. This gives transient depths in at most 200000 * (n + 1) ^ 2 * powerBudget n s (2 ^ n) L gates (depth_circuit), and 600000 * (n + 1) ^ 2 * optimizedBudget n s (2 ^ n) balanced (depth_circuit_optimized). The dictionary construction of Iteration.Depth avoids the factor (n + 1) ^ 2.

The circuits are native De Morgan circuits: every NOT, AND and OR gate and every constant is charged, while wiring and fanout are free. They exist for each L; nothing here bounds the time to construct them.

Main definitions

• Cslib.Circuits.Boolean.Iteration.searchBelow: the binary search for a threshold.
• Cslib.Circuits.Boolean.Iteration.depthBudget: the gate count of the search for depths.

Main results

• Cslib.Circuits.Boolean.Iteration.searchBelow_result: the search finds the threshold.
• Cslib.Circuits.Boolean.Iteration.synthesis_threshold: its gate count.
• Cslib.Circuits.Boolean.Iteration.depth_circuit, Cslib.Circuits.Boolean.Iteration.depth_circuit_optimized: transient depths.

References

• Adapted from lean/Proofs/{BinarySearch,DepthCircuit}.lean in S. Schlesinger, Square-root circuit bounds for iterated functions, whose balanced bound has the constant 3000000.

def Cslib.Circuits.Boolean.Iteration.searchBelow (n μ : ℕ) : ℕ → ℕ

After j digits, the largest value of the form searchBelow n μ j' + 2 ^ (n - j' - 1) below μ, built from the most significant of n digits.

theorem Cslib.Circuits.Boolean.Iteration.searchBelow_bounds (n μ : ℕ) (hμ : μ ≤ 2 ^ n) (j : ℕ) (hj : j ≤ n) : (μ = 0 → searchBelow n μ j = 0) ∧ (0 < μ → searchBelow n μ j < μ ∧ μ ≤ searchBelow n μ j + 2 ^ (n - j))

theorem Cslib.Circuits.Boolean.Iteration.searchBelow_lt (n μ j : ℕ) (hμ : μ < 2 ^ n) (hj : j ≤ n) : searchBelow n μ j < 2 ^ n

theorem Cslib.Circuits.Boolean.Iteration.searchBelow_result (n μ : ℕ) (hμ : μ ≤ 2 ^ n) : (if μ = 0 then 0 else searchBelow n μ n + 1) = μ

Binary search. One more than the last candidate below μ, or zero, is μ.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_threshold {a : ℕ} (s : Set (BooleanFunction a)) (μ : BitString a → ℕ) (n C : ℕ) (hμ : ∀ (x : BitString a), μ x < 2 ^ n) (hc : ∀ (b : Bool), (fun (x : BitString a) => b) ∈ s) (query : ∀ (src : Set (BooleanFunction a)), s ⊆ src → ∀ (value : BitString a → BitVec (n + 2)), wordWires value ⊆ src → Synthesis interpretation src {fun (x : BitString a) => decide (μ x ≤ (value x).toNat)} C) : Synthesis interpretation s (wordWires fun (x : BitString a) => BitVec.ofNat (n + 2) (μ x)) ((n + 1) * (C + 16 * (n + 3)))

Threshold search. If μ x < 2 ^ n and, from any family of available sources containing s, every available (n + 2)-bit word v gives the query μ x ≤ v within C gates, then μ x in n + 2 bits costs n + 1 queries and 16 * (n + 3) gates per query for the word operations.

def Cslib.Circuits.Boolean.Iteration.depthBudget (n s L : ℕ) : ℕ

The gate count of the threshold search for transient depths.

theorem Cslib.Circuits.Boolean.Iteration.depth_circuit {n : ℕ} (c : Circuit signature n n) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature n (n + 2)), (∀ (x : Fin n → Bool), word (out.eval interpretation x) = BitVec.ofNat (n + 2) (FunctionalGraph.transientDepth (c.eval interpretation) x)) ∧ out.size ≤ depthBudget n c.size L

Transient depths by binary search. For every 0 < L ≤ 2 ^ n, some circuit of size at most depthBudget n c.size L computes the transient depth of every state in n + 2 bits.

theorem Cslib.Circuits.Boolean.Iteration.depthBudget_le (n s L : ℕ) : depthBudget n s L ≤ 200000 * (n + 1) ^ 2 * powerBudget n s (2 ^ n) L

The threshold search costs at most a factor (n + 1) ^ 2 more than a fixed power.

theorem Cslib.Circuits.Boolean.Iteration.depth_circuit_optimized {n : ℕ} (c : Circuit signature n n) : ∃ (out : Circuit signature n (n + 2)), (∀ (x : Fin n → Bool), word (out.eval interpretation x) = BitVec.ofNat (n + 2) (FunctionalGraph.transientDepth (c.eval interpretation) x)) ∧ ↑out.size ≤ 600000 * (↑n + 1) ^ 2 * optimizedBudget n c.size (2 ^ n)

Square-root transient depths by binary search. Some circuit of size at most 600000 * (n + 1) ^ 2 * optimizedBudget n c.size (2 ^ n) computes the transient depth of every state in n + 2 bits.