In-place multi-head machines

An in-place machine has one writable tape whose cells are exactly the n input cells, a finite tape alphabet Γ, h heads sharing those n cells, and a finite control Q. Moves past 0 or n - 1 clamp at the boundary (Move.apply), and when multiple heads write to the same cell in one step, the highest head index wins (writeHeads). Because native Turing.Cfg has a read-only input, separate unbounded work tapes, and a write-only output, this fixed-length shared-tape configuration map is formalized as a standalone finite dynamical system rather than an instance of Turing.Cfg/Turing.Action.

This module defines configurations (w, p, q) with w : Fin n → Γ, p : Fin h → Fin n, and q : Q, the one-step map Machine.step, and the finite set reach M n of configurations reachable from initial configurations M.init x (x : BitString n). It proves the configuration count |Γ|^n * n^h * |Q| (card_config), the bounds on (reach M n).card (reach_card_le_configs, reach_card_le_time under a halting-time bound, and reach_card_le_round for a machine that returns to an initial configuration every τ steps), and the conditional halting characterization after |Γ|^n * n^h * |Q| steps under absorbing halting states (iterate_card_halting): the configuration at step |Γ|^n * n^h * |Q| is halting if and only if the run ever halts, and equals the halting configuration whenever one is reached (non-halting runs may continue cycling).

The circuit theorems (inplace_fixed_power, inplace_fixed_power_optimized, inplace_configs_optimized, inplace_time_optimized, inplace_halting) apply fixed_power_encoded to the forward-invariant reachable set reach M n, assuming an encoding e : Config Q Γ n h → BitString w injective on reach M n, a circuit c computing M.step on e '' reach M n, and a circuit ι computing x ↦ e (M.init x) (charging c.size and ι.size rather than compiling M.δ into gates). In inplace_halting, the circuit outputs the encoded configuration after |Γ|^n * n^h * |Q| steps together with the semantic halting equivalence, not a separately costed single-bit halting test. Finally, for a machine whose rounds of τ steps realize P : BitString m → BitString m, round_lower_bound_of_hard and round_bounds_of_hard transfer any circuit lower bound for P^[T] to the (τ * T)-th step of M via an explicit output-wire projection tape : Fin m → Fin w satisfying ∀ x, e (M.init x) ∘ tape = x.

Main definitions

• Cslib.Circuits.Boolean.Iteration.InPlace.Move: clamped head moves (left, stay, right).
• Cslib.Circuits.Boolean.Iteration.InPlace.Machine: an in-place multi-head machine.
• Cslib.Circuits.Boolean.Iteration.InPlace.Config: machine configuration (w, p, q).
• Cslib.Circuits.Boolean.Iteration.InPlace.reach: configurations reachable from initial inputs.

Main results

• Cslib.Circuits.Boolean.Iteration.InPlace.reach_card_le_configs, Cslib.Circuits.Boolean.Iteration.InPlace.reach_card_le_time, Cslib.Circuits.Boolean.Iteration.InPlace.reach_card_le_round: reachable configuration bounds.
• Cslib.Circuits.Boolean.Iteration.InPlace.iterate_card_halting: after Fintype.card (Config Q Γ n h) steps under absorbing halting states, the configuration is halting iff the run ever halts, and equals the halting configuration when it does.
• Cslib.Circuits.Boolean.Iteration.InPlace.inplace_fixed_power_optimized, Cslib.Circuits.Boolean.Iteration.InPlace.inplace_configs_optimized, Cslib.Circuits.Boolean.Iteration.InPlace.inplace_time_optimized, Cslib.Circuits.Boolean.Iteration.InPlace.inplace_halting: square-root circuit bounds for in-place machines.
• Cslib.Circuits.Boolean.Iteration.InPlace.round_lower_bound_of_hard, Cslib.Circuits.Boolean.Iteration.InPlace.round_bounds_of_hard: transfer of round lower bounds and matching reachable-state upper bounds.

References

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

inductive Cslib.Circuits.Boolean.Iteration.InPlace.Move : Type

A head move. Moves past either end of the tape leave the head in place.

• left : Move
• stay : Move
• right : Move

@[instance_reducible]

instance Cslib.Circuits.Boolean.Iteration.InPlace.instDecidableEqMove : DecidableEq Move

def Cslib.Circuits.Boolean.Iteration.InPlace.Move.apply {n : ℕ} : Move → Fin n → Fin n

Apply a clamped move to a head position.

structure Cslib.Circuits.Boolean.Iteration.InPlace.Machine (Q : Type u) (Γ : Type v) (h : ℕ) : Type (max u v)

An in-place machine with h heads. The transition reads the state, the symbols under the heads, and for each head whether it is on the first and on the last cell. It returns the new state, a symbol to write under each head, and a move for each head.

• δ : Q → (Fin h → Γ) → (Fin h → Bool) → (Fin h → Bool) → Q × (Fin h → Γ) × (Fin h → Move)

  The transition function returning the next state, written symbols, and head moves.

• start : Q

  The initial control state.

• halting : Q → Prop

  The halting predicate on control states.

• embed : Bool → Γ

  The input map from {0, 1} into Γ.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.Iteration.InPlace.Config (Q : Type u) (Γ : Type v) (n h : ℕ) : Type (max v u)

Configurations: tape contents, head positions, and control state.

def Cslib.Circuits.Boolean.Iteration.InPlace.writeHeads {Γ : Type v} {n h : ℕ} (w : Fin n → Γ) (p : Fin h → Fin n) (σ : Fin h → Γ) : Fin n → Γ

Write under the heads in order of increasing index, so the largest index wins.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.writeHeads_of_forall_ne {Γ : Type v} {n h : ℕ} (w : Fin n → Γ) (p : Fin h → Fin n) (σ : Fin h → Γ) (i : Fin n) (hi : ∀ (j : Fin h), p j ≠ i) : writeHeads w p σ i = w i

A cell under no head is unchanged.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.writeHeads_read {Γ : Type v} {n h : ℕ} (w : Fin n → Γ) (p : Fin h → Fin n) : (writeHeads w p fun (j : Fin h) => w (p j)) = w

Rewriting the symbols read leaves the tape unchanged.

def Cslib.Circuits.Boolean.Iteration.InPlace.Machine.step {Q : Type u} {Γ : Type v} {n h : ℕ} (M : Machine Q Γ h) (z : Config Q Γ n h) : Config Q Γ n h

The one-step map of an in-place machine.

def Cslib.Circuits.Boolean.Iteration.InPlace.Machine.init {Q : Type u} {Γ : Type v} {n h : ℕ} [NeZero n] (M : Machine Q Γ h) (x : BitString n) : Config Q Γ n h

The initial configuration: the input on the tape, every head on the first cell.

def Cslib.Circuits.Boolean.Iteration.InPlace.Machine.HaltingAbsorbing {Q : Type u} {Γ : Type v} {h : ℕ} (M : Machine Q Γ h) : Prop

Halting states are absorbing: they write the symbols read, do not move, and keep the state.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.Machine.step_of_halting {Q : Type u} {Γ : Type v} {n h : ℕ} {M : Machine Q Γ h} (hM : M.HaltingAbsorbing) (z : Config Q Γ n h) (hz : M.halting z.2.2) : M.step z = z

theorem Cslib.Circuits.Boolean.Iteration.InPlace.card_config {Q : Type u} {Γ : Type v} {n h : ℕ} [Fintype Q] [Fintype Γ] : Fintype.card (Config Q Γ n h) = Fintype.card Γ ^ n * n ^ h * Fintype.card Q

The number of configurations |Γ|^n * n^h * |Q|.

noncomputable def Cslib.Circuits.Boolean.Iteration.InPlace.reach {Q : Type u} {Γ : Type v} {h : ℕ} [Fintype Q] [Fintype Γ] (M : Machine Q Γ h) (n : ℕ) [NeZero n] : Finset (Config Q Γ n h)

The configurations reachable from some initial configuration.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.mem_reach {Q : Type u} {Γ : Type v} {n h : ℕ} [Fintype Q] [Fintype Γ] [NeZero n] (M : Machine Q Γ h) {z : Config Q Γ n h} : z ∈ reach M n ↔ ∃ (x : BitString n) (t : ℕ), M.step^[t] (M.init x) = z

theorem Cslib.Circuits.Boolean.Iteration.InPlace.init_mem_reach {Q : Type u} {Γ : Type v} {n h : ℕ} [Fintype Q] [Fintype Γ] [NeZero n] (M : Machine Q Γ h) (x : BitString n) : M.init x ∈ reach M n

theorem Cslib.Circuits.Boolean.Iteration.InPlace.iterate_mem_reach {Q : Type u} {Γ : Type v} {n h : ℕ} [Fintype Q] [Fintype Γ] [NeZero n] (M : Machine Q Γ h) (x : BitString n) (t : ℕ) : M.step^[t] (M.init x) ∈ reach M n

theorem Cslib.Circuits.Boolean.Iteration.InPlace.step_mem_reach {Q : Type u} {Γ : Type v} {n h : ℕ} [Fintype Q] [Fintype Γ] [NeZero n] (M : Machine Q Γ h) {z : Config Q Γ n h} (hz : z ∈ reach M n) : M.step z ∈ reach M n

The reachable set is forward invariant.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.reach_card_le_configs {Q : Type u} {Γ : Type v} {n h : ℕ} [Fintype Q] [Fintype Γ] [NeZero n] (M : Machine Q Γ h) : (reach M n).card ≤ Fintype.card Γ ^ n * n ^ h * Fintype.card Q

Every configuration is counted in the configuration bound.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.reach_card_le_of_cover {Q : Type u} {Γ : Type v} {n h : ℕ} [Fintype Q] [Fintype Γ] [NeZero n] (M : Machine Q Γ h) (B : ℕ) (hcover : ∀ (x : BitString n) (t : ℕ), ∃ (y : BitString n), ∃ j < B, M.step^[t] (M.init x) = M.step^[j] (M.init y)) : (reach M n).card ≤ 2 ^ n * B

Reachable configurations are covered by the first B steps from every input.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.reach_card_le_time {Q : Type u} {Γ : Type v} {n h : ℕ} [Fintype Q] [Fintype Γ] [NeZero n] (M : Machine Q Γ h) (hM : M.HaltingAbsorbing) (t : ℕ) (ht : ∀ (x : BitString n), ∃ s ≤ t, M.halting (M.step^[s] (M.init x)).2.2) : (reach M n).card ≤ 2 ^ n * (t + 1)

Under a halting-time bound t, at most 2 ^ n * (t + 1) configurations are reachable.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.iterate_rounds {Q : Type u} {Γ : Type v} {n h : ℕ} [NeZero n] (M : Machine Q Γ h) (τ : ℕ) (P : BitString n → BitString n) (hround : ∀ (x : BitString n), M.step^[τ] (M.init x) = M.init (P x)) (x : BitString n) (m : ℕ) : M.step^[τ * m] (M.init x) = M.init (P^[m] x)

Running τ * m steps of a machine with rounds of length τ runs m rounds.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.reach_card_le_round {Q : Type u} {Γ : Type v} {n h : ℕ} [Fintype Q] [Fintype Γ] [NeZero n] (M : Machine Q Γ h) (τ : ℕ) (hτ : 0 < τ) (P : BitString n → BitString n) (hround : ∀ (x : BitString n), M.step^[τ] (M.init x) = M.init (P x)) : (reach M n).card ≤ 2 ^ n * τ

A machine that returns to an initial configuration every τ steps reaches at most 2 ^ n * τ configurations.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.iterate_card_halting {Q : Type u} {Γ : Type v} {n h : ℕ} [Fintype Q] [Fintype Γ] (M : Machine Q Γ h) (hM : M.HaltingAbsorbing) (z : Config Q Γ n h) : (M.halting (M.step^[Fintype.card (Config Q Γ n h)] z).2.2 ↔ ∃ (t : ℕ), M.halting (M.step^[t] z).2.2) ∧ ∀ (t : ℕ), M.halting (M.step^[t] z).2.2 → M.step^[Fintype.card (Config Q Γ n h)] z = M.step^[t] z

Under absorbing halting states, the configuration after |Γ|^n * n^h * |Q| steps is halting if and only if the run ever halts, and equals any halting configuration reached along the run.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.powerBudget_mono {w s M M' L : ℕ} (hM : M ≤ M') : powerBudget w s M L ≤ powerBudget w s M' L

The integer budget is monotone in the storage count.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.optimizedBudget_mono {w s M M' : ℕ} (hM : M ≤ M') : optimizedBudget w s M ≤ optimizedBudget w s M'

The real budget is monotone in the storage count.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.reach_card_le_two_pow {Q : Type u} {Γ : Type v} {n h : ℕ} [Fintype Q] [Fintype Γ] [NeZero n] {w : ℕ} (M : Machine Q Γ h) (e : Config Q Γ n h → BitString w) (he : Set.InjOn e ↑(reach M n)) : (reach M n).card ≤ 2 ^ w

The reachable set fits in the encoding width.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.inplace_fixed_power {Q : Type u} {Γ : Type v} {n h : ℕ} [Fintype Q] [Fintype Γ] [NeZero n] {w : ℕ} (M : Machine Q Γ h) (e : Config Q Γ n h → BitString w) (he : Set.InjOn e ↑(reach M n)) (c : Circuit signature w w) (hstep : ∀ z ∈ reach M n, c.eval interpretation (e z) = e (M.step z)) (ι : Circuit signature n w) (hι : ∀ (x : Fin n → Bool), ι.eval interpretation x = e (M.init x)) (R : ℕ) (hR : (reach M n).card ≤ R) (T L : ℕ) (hL : 0 < L) (hLw : L ≤ 2 ^ w) : ∃ (out : Circuit signature n w), (∀ (x : Fin n → Bool), out.eval interpretation x = e (M.step^[T] (M.init x))) ∧ out.size ≤ ι.size + 40000 * powerBudget w c.size R L

Every fixed power on the initial configurations, with any upper bound R on the number of reachable configurations in the storage term. The initial-encoding circuit ι is charged.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.inplace_fixed_power_optimized {Q : Type u} {Γ : Type v} {n h : ℕ} [Fintype Q] [Fintype Γ] [NeZero n] {w : ℕ} (M : Machine Q Γ h) (e : Config Q Γ n h → BitString w) (he : Set.InjOn e ↑(reach M n)) (c : Circuit signature w w) (hstep : ∀ z ∈ reach M n, c.eval interpretation (e z) = e (M.step z)) (ι : Circuit signature n w) (hι : ∀ (x : Fin n → Bool), ι.eval interpretation x = e (M.init x)) (R : ℕ) (hR : (reach M n).card ≤ R) (T : ℕ) : ∃ (out : Circuit signature n w), (∀ (x : Fin n → Bool), out.eval interpretation x = e (M.step^[T] (M.init x))) ∧ ↑out.size ≤ ↑ι.size + 120000 * optimizedBudget w c.size R

The square-root form, with any upper bound R on the number of reachable configurations.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.inplace_configs_optimized {Q : Type u} {Γ : Type v} {n h : ℕ} [Fintype Q] [Fintype Γ] [NeZero n] {w : ℕ} (M : Machine Q Γ h) (e : Config Q Γ n h → BitString w) (he : Set.InjOn e ↑(reach M n)) (c : Circuit signature w w) (hstep : ∀ z ∈ reach M n, c.eval interpretation (e z) = e (M.step z)) (ι : Circuit signature n w) (hι : ∀ (x : Fin n → Bool), ι.eval interpretation x = e (M.init x)) (T : ℕ) : ∃ (out : Circuit signature n w), (∀ (x : Fin n → Bool), out.eval interpretation x = e (M.step^[T] (M.init x))) ∧ ↑out.size ≤ ↑ι.size + 120000 * optimizedBudget w c.size (Fintype.card Γ ^ n * n ^ h * Fintype.card Q)

The alphabet bound: the storage term is the number of configurations.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.inplace_time_optimized {Q : Type u} {Γ : Type v} {n h : ℕ} [Fintype Q] [Fintype Γ] [NeZero n] {w : ℕ} (M : Machine Q Γ h) (hM : M.HaltingAbsorbing) (t : ℕ) (ht : ∀ (x : BitString n), ∃ s ≤ t, M.halting (M.step^[s] (M.init x)).2.2) (e : Config Q Γ n h → BitString w) (he : Set.InjOn e ↑(reach M n)) (c : Circuit signature w w) (hstep : ∀ z ∈ reach M n, c.eval interpretation (e z) = e (M.step z)) (ι : Circuit signature n w) (hι : ∀ (x : Fin n → Bool), ι.eval interpretation x = e (M.init x)) (T : ℕ) : ∃ (out : Circuit signature n w), (∀ (x : Fin n → Bool), out.eval interpretation x = e (M.step^[T] (M.init x))) ∧ ↑out.size ≤ ↑ι.size + 120000 * optimizedBudget w c.size (2 ^ n * (t + 1))

The time bound: under absorbing halting states and a halting time t, the storage term is 2 ^ n * (t + 1).

theorem Cslib.Circuits.Boolean.Iteration.InPlace.inplace_halting {Q : Type u} {Γ : Type v} {n h : ℕ} [Fintype Q] [Fintype Γ] [NeZero n] {w : ℕ} (M : Machine Q Γ h) (hM : M.HaltingAbsorbing) (e : Config Q Γ n h → BitString w) (he : Set.InjOn e ↑(reach M n)) (c : Circuit signature w w) (hstep : ∀ z ∈ reach M n, c.eval interpretation (e z) = e (M.step z)) (ι : Circuit signature n w) (hι : ∀ (x : Fin n → Bool), ι.eval interpretation x = e (M.init x)) : ∃ (out : Circuit signature n w) (final : BitString n → Config Q Γ n h), (∀ (x : Fin n → Bool), out.eval interpretation x = e (final x) ∧ (M.halting (final x).2.2 ↔ ∃ (t : ℕ), M.halting (M.step^[t] (M.init x)).2.2) ∧ ∀ (t : ℕ), M.halting (M.step^[t] (M.init x)).2.2 → final x = M.step^[t] (M.init x)) ∧ ↑out.size ≤ ↑ι.size + 120000 * optimizedBudget w c.size (Fintype.card Γ ^ n * n ^ h * Fintype.card Q)

Halting, the halting state, and the final configuration of a machine that need not halt: one circuit returns the encoding of the configuration after |Γ|^n * n^h * |Q| steps. It is a halting configuration exactly when the run halts, and it is then the final configuration.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.round_lower_bound_of_hard {Q : Type u} {Γ : Type v} {h m w : ℕ} [NeZero m] (M : Machine Q Γ h) (τ T q : ℕ) (P : BitString m → BitString m) (hround : ∀ (x : BitString m), M.step^[τ] (M.init x) = M.init (P x)) (e : Config Q Γ m h → BitString w) (tape : Fin m → Fin w) (htape : ∀ (x : BitString m), e (M.init x) ∘ tape = x) (hhard : ∀ (d : Circuit signature m m), d.Computes interpretation P^[T] → q < d.size) (out : Circuit signature m w) (hout : ∀ (x : Fin m → Bool), out.eval interpretation x = e (M.step^[τ * T] (M.init x))) : q < out.size

A machine whose rounds of τ steps apply a map P : BitString m → BitString m, and whose encoding exposes the input word of an initial configuration as a projection, inherits any circuit lower bound for P^[T]: if every circuit computing P^[T] has size strictly greater than q, then every circuit computing the (τ * T)-th step from M.init has size strictly greater than q.

theorem Cslib.Circuits.Boolean.Iteration.InPlace.round_bounds_of_hard {Q : Type u} {Γ : Type v} {h m w : ℕ} [NeZero m] (M : Machine Q Γ h) [Fintype Q] [Fintype Γ] (τ T q : ℕ) (hτ : 0 < τ) (P : BitString m → BitString m) (hround : ∀ (x : BitString m), M.step^[τ] (M.init x) = M.init (P x)) (e : Config Q Γ m h → BitString w) (he : Set.InjOn e ↑(reach M m)) (tape : Fin m → Fin w) (htape : ∀ (x : BitString m), e (M.init x) ∘ tape = x) (hhard : ∀ (d : Circuit signature m m), d.Computes interpretation P^[T] → q < d.size) (c : Circuit signature w w) (hstep : ∀ z ∈ reach M m, c.eval interpretation (e z) = e (M.step z)) (ι : Circuit signature m w) (hι : ∀ (x : Fin m → Bool), ι.eval interpretation x = e (M.init x)) : (∀ (out : Circuit signature m w), (∀ (x : Fin m → Bool), out.eval interpretation x = e (M.step^[τ * T] (M.init x))) → q < out.size) ∧ ∀ (T' : ℕ), ∃ (out : Circuit signature m w), (∀ (x : Fin m → Bool), out.eval interpretation x = e (M.step^[T'] (M.init x))) ∧ ↑out.size ≤ ↑ι.size + 120000 * optimizedBudget w c.size (2 ^ m * τ)

Both sides for a round machine: any circuit lower bound q for P^[T] transfers to the (τ * T)-th step of M, while every step T' has a circuit within the reachable-set upper bound 2 ^ m * τ, given an encoded step circuit.