Circuits for eventual behaviour

Questions about arbitrarily late times reduce to one fixed power. Two orbits are ever in the same state at the same time exactly when they are at time 2 ^ n (FunctionalGraph.exists_iterate_eq_iterate_iff), so synchronous coalescence costs two fixed powers and an equality test (synchronous_coalescence). A recognized target recurs arbitrarily late exactly when it is reachable from the cycle projection f^[(2 ^ n)!] x (recurring_target_circuit), and it holds from some time on exactly when its complement does not recur (eventually_always_target_circuit). Balancing the parameter gives the square-root bounds (synchronous_coalescence_optimized, recurring_target_optimized, eventually_always_target_optimized).

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 parameter choice; nothing here bounds the time to construct them.

Main results

• Cslib.Circuits.Boolean.Iteration.synchronous_coalescence, Cslib.Circuits.Boolean.Iteration.synchronous_coalescence_optimized: meeting orbits.
• Cslib.Circuits.Boolean.Iteration.recurring_target_circuit, Cslib.Circuits.Boolean.Iteration.recurring_target_optimized: recurring targets.
• Cslib.Circuits.Boolean.Iteration.eventually_always_target_circuit, Cslib.Circuits.Boolean.Iteration.eventually_always_target_optimized: eventually permanent targets.

References

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

theorem Cslib.Circuits.Boolean.Iteration.synchronous_coalescence {n : ℕ} (c : Circuit signature n n) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature (n + n) 1), (∀ (z : Fin (n + n) → Bool), out.eval interpretation z 0 = true ↔ ∃ (t : ℕ), ((c.eval interpretation)^[t] fun (i : Fin n) => z (Fin.castAdd n i)) = (c.eval interpretation)^[t] fun (i : Fin n) => z (Fin.natAdd n i)) ∧ out.size ≤ 80000 * powerBudget n c.size (2 ^ n) L + 6 * n + 1

Synchronous coalescence. For every 0 < L ≤ 2 ^ n, some circuit of size at most 80000 * powerBudget n c.size (2 ^ n) L + 6 * n + 1 decides, for two states given as the two halves of its input, whether their orbits are ever in the same state at the same time.

theorem Cslib.Circuits.Boolean.Iteration.synchronous_coalescence_optimized {n : ℕ} (c : Circuit signature n n) : ∃ (out : Circuit signature (n + n) 1), (∀ (z : Fin (n + n) → Bool), out.eval interpretation z 0 = true ↔ ∃ (t : ℕ), ((c.eval interpretation)^[t] fun (i : Fin n) => z (Fin.castAdd n i)) = (c.eval interpretation)^[t] fun (i : Fin n) => z (Fin.natAdd n i)) ∧ ↑out.size ≤ 240000 * optimizedBudget n c.size (2 ^ n) + 6 * ↑n + 1

Square-root synchronous coalescence.

theorem Cslib.Circuits.Boolean.Iteration.recurring_target_circuit {n : ℕ} (c : Circuit signature n n) (p : Circuit signature n 1) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature n 1), (∀ (x : Fin n → Bool), out.eval interpretation x 0 = true ↔ ∀ (a : ℕ), ∃ (t : ℕ), a ≤ t ∧ p.eval interpretation ((c.eval interpretation)^[t] x) 0 = true) ∧ out.size ≤ 80000 * powerBudget n (c.size + p.size + 4 * n) (2 ^ n) L + p.size

Recurring targets. For every 0 < L ≤ 2 ^ n, some circuit of size at most 80000 * powerBudget n (c.size + p.size + 4 * n) (2 ^ n) L + p.size decides whether the orbit of its input visits a state accepted by p at arbitrarily late times.

theorem Cslib.Circuits.Boolean.Iteration.exists_not_circuit {n : ℕ} (p : Circuit signature n 1) : ∃ (out : Circuit signature n 1), (∀ (x : Fin n → Bool), out.eval interpretation x 0 = !p.eval interpretation x 0) ∧ out.size ≤ p.size + 1

Negating a one-bit circuit costs one gate.

theorem Cslib.Circuits.Boolean.Iteration.eventually_always_target_circuit {n : ℕ} (c : Circuit signature n n) (p : Circuit signature n 1) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature n 1), (∀ (x : Fin n → Bool), out.eval interpretation x 0 = true ↔ ∃ (a : ℕ), ∀ (t : ℕ), a ≤ t → p.eval interpretation ((c.eval interpretation)^[t] x) 0 = true) ∧ out.size ≤ 80000 * powerBudget n (c.size + (p.size + 1) + 4 * n) (2 ^ n) L + p.size + 2

Eventually permanent targets. For every 0 < L ≤ 2 ^ n, some circuit of size at most 80000 * powerBudget n (c.size + (p.size + 1) + 4 * n) (2 ^ n) L + p.size + 2 decides whether the orbit of its input is accepted by p from some time on.

theorem Cslib.Circuits.Boolean.Iteration.recurring_target_optimized {n : ℕ} (c : Circuit signature n n) (p : Circuit signature n 1) : ∃ (out : Circuit signature n 1), (∀ (x : Fin n → Bool), out.eval interpretation x 0 = true ↔ ∀ (a : ℕ), ∃ (t : ℕ), a ≤ t ∧ p.eval interpretation ((c.eval interpretation)^[t] x) 0 = true) ∧ ↑out.size ≤ 240000 * optimizedBudget n (c.size + p.size + 4 * n) (2 ^ n) + ↑p.size

Square-root recurring targets.

theorem Cslib.Circuits.Boolean.Iteration.eventually_always_target_optimized {n : ℕ} (c : Circuit signature n n) (p : Circuit signature n 1) : ∃ (out : Circuit signature n 1), (∀ (x : Fin n → Bool), out.eval interpretation x 0 = true ↔ ∃ (a : ℕ), ∀ (t : ℕ), a ≤ t → p.eval interpretation ((c.eval interpretation)^[t] x) 0 = true) ∧ ↑out.size ≤ 240000 * optimizedBudget n (c.size + (p.size + 1) + 4 * n) (2 ^ n) + ↑p.size + 2

Square-root eventually permanent targets.