Iterating a round

Amplification runs a round logarithmically many times. On the algorithm's side that is an iteration of one FP function; on the abstract side it is Amplifier.iter. This module says the two agree, for any round function that computes its transformation.

Main results

• Complexity.iterate_encGraph — iterating the algorithm writes the iterated graph
• Complexity.iterate_mem_FP_encGraph — and the iteration is an FP function

theorem Complexity.iterate_encGraph {α : Type} [Fintype α] [DecidableEq α] {f : List Bool → List Bool} {T : ConstraintGraph α → ConstraintGraph α} (hstep : ∀ (G : ConstraintGraph α), f (encGraph G) = encGraph (T G)) (k : ℕ) (G : ConstraintGraph α) : f^[k] (encGraph G) = encGraph (T^[k] G)

Iterating the algorithm writes the iterated graph.

theorem Complexity.iterate_encGraph_amplifier {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] {f : List Bool → List Bool} (A : Amplifier α) (hstep : ∀ (G : ConstraintGraph α), f (encGraph G) = encGraph (A.transform G)) (k : ℕ) (G : ConstraintGraph α) : f^[k] (encGraph G) = encGraph (A.iter k G)

And it writes the amplifier's iterate.

theorem Complexity.iterate_mem_FP_encGraph {α : Type} [Fintype α] [DecidableEq α] {f init ruler width : List Bool → List Bool} {T : ConstraintGraph α → ConstraintGraph α} (hf : f ∈ FP) (hinit : init ∈ FP) (hruler : ruler ∈ FP) (hwidth : width ∈ FP) (hstep : ∀ (G : ConstraintGraph α), f (encGraph G) = encGraph (T G)) (hinitG : ∀ (z : List Bool), ∃ (G : ConstraintGraph α), init z = encGraph G) (hbound : ∀ (z : List Bool) (G : ConstraintGraph α), init z = encGraph G → ∀ n ≤ (ruler z).length, (encGraph (T^[n] G)).length ≤ (width z).length) : (fun (z : List Bool) => f^[(ruler z).length] (init z)) ∈ FP

The iteration is an FP function. The bound the iteration rule wants is supplied on the graphs, where the round's size bounds live, rather than on their encodings.