Square-root-size reachability circuits via compressed checkpoint forests

Combining synthesis_transient_forest_reachability with checkpoint_depth_circuit, exists_forest_circuit_tables, and cycle_label_circuit yields a Boolean circuit of size O(powerBudget n c.size (2 ^ n) L) that decides reachability ∃ t, f^[t] x = y for all pairs of states (x, y) (forest_reachability_circuit). Optimizing the checkpoint spacing L yields the square-root-size bound O(optimizedBudget n c.size (2 ^ n)) (forest_reachability_optimized).

Main results

• Cslib.Circuits.Boolean.Iteration.forest_dictionary_cost_le: bounds dictionaryCost by a constant multiple of powerBudget.
• Cslib.Circuits.Boolean.Iteration.transientForestCost_le: bounds transientForestCost by a constant multiple of powerBudget.
• Cslib.Circuits.Boolean.Iteration.forest_transient_circuit: decides reachability to transient targets within 4000000 * powerBudget n c.size (2 ^ n) L gates.
• Cslib.Circuits.Boolean.Iteration.forest_reachability_circuit: decides general reachability within 4500000 * powerBudget n c.size (2 ^ n) L gates.
• Cslib.Circuits.Boolean.Iteration.forest_reachability_optimized: decides general reachability within 13500000 * optimizedBudget n c.size (2 ^ n) gates.

References

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

theorem Cslib.Circuits.Boolean.Iteration.forest_dictionary_cost_le (n s v M Q L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) (hv : v ≤ 4 * n + 5) (hM : M ≤ 2 * (2 ^ n / L)) (hQ : Q ≤ 2 * L + 2) : dictionaryCost n v M Q ≤ 1500000 * powerBudget n s (2 ^ n) L

Every shared dictionary lookup in the compressed-forest query fits within powerBudget.

theorem Cslib.Circuits.Boolean.Iteration.transientForestCost_le (n s d M E L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) (hd : d ≤ 50000 * powerBudget n s (2 ^ n) L) (hM : M ≤ 2 * (2 ^ n / L)) (hE : E ≤ 2 * (2 ^ n / L)) : transientForestCost n s d M E L ≤ 4000000 * powerBudget n s (2 ^ n) L

The transient compressed-forest query budget is bounded by 4000000 * powerBudget.

theorem Cslib.Circuits.Boolean.Iteration.forest_transient_circuit {n : ℕ} (c : Circuit signature n n) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature (n + n) 1), (∀ (z : BitString (n + n)), 0 < FunctionalGraph.transientDepth (c.eval interpretation) (inputRight z) → (out.eval interpretation z 0 = true ↔ ∃ (t : ℕ), (c.eval interpretation)^[t] (inputLeft z) = inputRight z)) ∧ out.size ≤ 4000000 * powerBudget n c.size (2 ^ n) L

Transient reachability. For transient targets, reachability has the same checkpoint tradeoff as a single fixed iterate.

theorem Cslib.Circuits.Boolean.Iteration.forest_reachability_circuit {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] (inputLeft z) = inputRight z) ∧ out.size ≤ 4500000 * powerBudget n c.size (2 ^ n) L

General reachability. Combining compressed-forest ancestry for transient targets with canonical cycle representatives for periodic targets decides reachability for all pairs (x, y) within 4500000 * powerBudget n c.size (2 ^ n) L gates.

theorem Cslib.Circuits.Boolean.Iteration.forest_reachability_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] (inputLeft z) = inputRight z) ∧ ↑out.size ≤ 13500000 * optimizedBudget n c.size (2 ^ n)

Square-root reachability. Optimizing the checkpoint parameter L gives a circuit of size at most 13500000 * optimizedBudget n c.size (2 ^ n) deciding reachability for all state pairs.