Reachability and first-hitting-time circuits

Combining forest_transient_circuit with checkpoint_depth_circuit, cycle_label_circuit, and synthesis_navigation_given_flag yields a Boolean circuit on pair inputs z : BitString (n + n) returning both the reachability bit and the (n + 1)-bit first hitting time navigationBits f (inputLeft z) (inputRight z) within navigationBudget n c.size L gates (navigation_circuit), and within 13500000 * optimizedBudget n c.size (2 ^ n) gates at the balanced checkpoint parameter (reachability_hitting_time).

Main definitions

• Cslib.Circuits.Boolean.Iteration.navigationBudget: gate bound for the navigation circuit at checkpoint spacing L.

Main results

• Cslib.Circuits.Boolean.Iteration.navigation_circuit: synthesizes navigationBits within navigationBudget n c.size L gates.
• Cslib.Circuits.Boolean.Iteration.navigationBudget_le: bounds navigationBudget by 4500000 * powerBudget n s (2 ^ n) L.
• Cslib.Circuits.Boolean.Iteration.reachability_hitting_time: square-root-size circuit returning reachability and first hitting time.

References

• Adapted from lean/Proofs/NavigationCircuits.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

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

Gate bound for the combined reachability and first-hitting-time circuit at spacing L.

theorem Cslib.Circuits.Boolean.Iteration.navigation_circuit {n : ℕ} (c : Circuit signature n n) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature (n + n) (1 + (n + 1))), (out.Computes interpretation fun (z : Fin (n + n) → Bool) => navigationBits (c.eval interpretation) (inputLeft z) (inputRight z)) ∧ out.size ≤ navigationBudget n c.size L

Reachability and first hitting time at spacing L. Forest reachability plus depths, cycle labels, and word arithmetic compute navigationBits within navigationBudget n c.size L gates.

theorem Cslib.Circuits.Boolean.Iteration.navigationBudget_le (n s L : ℕ) : navigationBudget n s L ≤ 4500000 * powerBudget n s (2 ^ n) L

Every component of navigationBudget fits within 4500000 * powerBudget.

theorem Cslib.Circuits.Boolean.Iteration.reachability_hitting_time {n : ℕ} (c : Circuit signature n n) : ∃ (out : Circuit signature (n + n) (1 + (n + 1))), (∀ (z : Fin (n + n) → Bool), out.eval interpretation z 0 = true ↔ ∃ (t : ℕ), (c.eval interpretation)^[t] (inputLeft z) = inputRight z) ∧ (∀ (z : Fin (n + n) → Bool), out.eval interpretation z 0 = true → have t := (word fun (i : Fin (n + 1)) => out.eval interpretation z (Fin.natAdd 1 i)).toNat; (c.eval interpretation)^[t] (inputLeft z) = inputRight z ∧ (∀ j < t, (c.eval interpretation)^[j] (inputLeft z) ≠ inputRight z) ∧ t < 2 ^ n) ∧ ↑out.size ≤ 13500000 * optimizedBudget n c.size (2 ^ n)

Reachability and first hitting time, with an explicit optimized gate bound.