Inverting permutations and testing periodicity

The inverse of a permutation p of a finite type is the power p^[k! - 1], where k is the number of elements (iterate_factorial_pred_eq_symm). The fixed-power bound does not depend on the exponent, so a permutation computed by a circuit of size s has an inverse circuit within the same bound (permutation_inverse), also through a supplied encoding of an arbitrary finite type (permutation_inverse_encoded). Similarly, x is a periodic point exactly when f^[(2 ^ n)!] x = x, which one more equality test decides (periodicPts_circuit).

Main results

• Cslib.Circuits.Boolean.Iteration.permutation_inverse: inverting a permutation circuit.
• Cslib.Circuits.Boolean.Iteration.permutation_inverse_encoded: inverting through an encoding.
• Cslib.Circuits.Boolean.Iteration.periodicPts_circuit: deciding periodicity.

References

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

theorem Cslib.Circuits.Boolean.Iteration.iterate_factorial_pred_eq_symm {α : Type u} [Fintype α] (p : Equiv.Perm α) : (⇑p)^[(Fintype.card α).factorial - 1] = ⇑(Equiv.symm p)

The inverse of a permutation of a finite type is its (card α)! - 1-st power.

theorem Cslib.Circuits.Boolean.Iteration.permutation_inverse {n : ℕ} (c : Circuit signature n n) (p : Equiv.Perm (BitString n)) (hc : c.Computes interpretation ⇑p) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature n n), out.Computes interpretation ⇑(Equiv.symm p) ∧ out.size ≤ 40000 * powerBudget n c.size (2 ^ n) L

Permutation inversion. A permutation computed by a circuit of size s has an inverse circuit of size at most 40000 * powerBudget n s (2 ^ n) L.

theorem Cslib.Circuits.Boolean.Iteration.permutation_inverse_encoded {α : Type u} [Fintype α] {n : ℕ} (p : Equiv.Perm α) (e : α → BitString n) (he : Function.Injective e) (c : Circuit signature n n) (hc : ∀ (x : α), c.eval interpretation (e x) = e (p x)) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature n n), (∀ (x : α), out.eval interpretation (e x) = e ((Equiv.symm p) x)) ∧ out.size ≤ 40000 * powerBudget n c.size (Fintype.card α) L

Encoded permutation inversion. A permutation of a finite type of any universe, realized by a circuit on an injective encoding, has an inverse circuit whose storage term counts the type.

theorem Cslib.Circuits.Boolean.Iteration.periodicPts_circuit {n : ℕ} (c : Circuit signature n n) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature n 1), (∀ (x : Fin n → Bool), out.eval interpretation x 0 = true ↔ x ∈ Function.periodicPts (c.eval interpretation)) ∧ out.size ≤ 40000 * powerBudget n c.size (2 ^ n) L + (6 * n + 1)

Periodic points. Whether a state is periodic for a circuit's map is decided by one fixed power and an equality test.