Encoded state spaces and burn-in

The fixed-power bound applies to a map f on any finite invariant set S of a type in any universe, given an injective bit encoding e of S and a Boolean circuit realizing f on the encodings (fixed_power_encoded). All computation is charged on the encoding; no gate evaluates f itself. Its storage term counts |S|.

After a burn-in of d steps, computed by a separate circuit, every orbit lies in the image of f^[d], so the storage term of the remaining steps counts only that image (fixed_power_image).

Main results

• Cslib.Circuits.Boolean.Iteration.fixed_power_encoded: fixed powers through an encoding.
• Cslib.Circuits.Boolean.Iteration.fixed_power_image: fixed powers after a burn-in.

References

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

theorem Cslib.Circuits.Boolean.Iteration.iterate_encoded {α : Type u} {n : ℕ} (f : α → α) (S : Finset α) (e : α → BitString n) (c : Circuit signature n n) (hS : ∀ x ∈ S, f x ∈ S) (hstep : ∀ x ∈ S, c.eval interpretation (e x) = e (f x)) {x : α} (hx : x ∈ S) (T : ℕ) : (c.eval interpretation)^[T] (e x) = e (f^[T] x)

A circuit realizing f on the encodings of an invariant set realizes its powers.

theorem Cslib.Circuits.Boolean.Iteration.fixed_power_encoded {α : Type u} {n : ℕ} (f : α → α) (S : Finset α) (e : α → BitString n) (he : Set.InjOn e ↑S) (c : Circuit signature n n) (hS : ∀ x ∈ S, f x ∈ S) (hstep : ∀ x ∈ S, c.eval interpretation (e x) = e (f x)) (T L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature n n), (∀ x ∈ S, out.eval interpretation (e x) = e (f^[T] x)) ∧ out.size ≤ 40000 * powerBudget n c.size S.card L

Encoded fixed powers. If an injective encoding e of a finite invariant set S of an arbitrary type is realized by a circuit c, then for every exponent T and 0 < L ≤ 2 ^ n some circuit of size at most 40000 * powerBudget n c.size S.card L realizes f^[T] on S.

theorem Cslib.Circuits.Boolean.Iteration.fixed_power_image {n : ℕ} (c burn : Circuit signature n n) (d T L : ℕ) (hburn : burn.Computes interpretation (c.eval interpretation)^[d]) (hdT : d ≤ T) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature n n), out.Computes interpretation (c.eval interpretation)^[T] ∧ out.size ≤ burn.size + 40000 * powerBudget n c.size (Finset.image (c.eval interpretation)^[d] Finset.univ).card L

Fixed powers after a burn-in. Given a circuit for d ≤ T steps, the remaining T - d steps cost the fixed-power bound with storage term the size of the image of f^[d].