Savitch's theorem for general space bounds

A nondeterministic machine whose computation paths on an input of length n visit at most S work cells is simulated by a deterministic machine within space O((S + log₂ n + 1) ^ 2): this is Savitch's theorem [Sav70]. No constructibility of S is assumed; as in Sipser's proof of Theorem 8.5 [Sip13], the machine tries growing bounds. The simulation runs Savitch's midpoint recursion with an explicit stack (Cslib.Reachability.Savitch.step) on the compact configuration graph of the machine (Turing.MultiTapeNTM.ConfigurationGraph), whose vertices omit the input. A vertex of the graph of radix B is stored as a word of W = O(log B) bits, so the stack of at most W frames has O(W ^ 2) bits. The input is never copied: the simulation is a query machine (Turing.QueryMachine), which reads one input bit per step, and the edge test at the bottom of the recursion needs exactly one input bit, at the input head of its source vertex.

The space bound S is not computed. The machine counts the input in binary and then tries the radices roundRadix State n j = 4 ^ j * startRadix State n of Turing.MultiTapeNTM.ConfigurationGraph.roundRadix in turn, the radices of Immerman's inductive counting for nondeterministic space; Sipser's proof of Theorem 8.5 likewise tries the space bounds 1, 2, 3, … and checks whether the machine uses more. In round j, a first recursion asks whether an overflowing vertex, one with a step leaving the radix, is reachable from the start vertex; if it is, the machine moves on to round j + 1. Otherwise every reachable view fits the radix, and a second recursion on the same graph asks whether an accepting halted vertex is reachable, which decides acceptance. A machine within space S has no reachable overflow from round 4 * S + 1 on (Turing.MultiTapeNTM.ConfigurationGraph.fits_roundRadix_of_runsInSpace), so every round has vertices of O(S + log₂ n + 1) bits. To have a single target, the graph on words gains a sink, the word of W ones: every target vertex steps to it (Turing.MultiTapeNTM.SquareSavitch.sinkReach_eq_true_iff).

The sublinear form of Savitch's theorem is the extension stated in the final paragraph of Section 8.4 of Sipser's third edition, just before Section 8.5 (p. 351): "We can extend Savitch's theorem to hold for sublinear space bounds down to f(n) ≥ log n." Sipser's Theorem 8.5 itself assumes f(n) ≥ n, and Arora and Barak's Theorem 4.14 assumes a space-constructible bound S(n) ≥ log n. In the extension, the machine has a read-only input tape, and the configurations of the machine on the input w record the state, the work tapes and the head positions but not w. Here these are the vertices of the compact configuration graph, and the query machine reads the one input bit an edge test needs. The sources state the theorem for languages decided by nondeterministic machines whose branches all halt; the statement here also covers machines that only recognize the problem (branches may run forever), arbitrary per-instance bounds without constructibility, and arbitrary instances under an encoding into List Bool.

Main definitions

• Turing.MultiTapeNTM.SquareSavitch.wordEdge: the edges of the graph on words, given the round mode and the input bit at the source.
• Turing.MultiTapeNTM.SquareSavitch.sinkReach: the recursion from the start vertex to the sink.
• Turing.MultiTapeNTM.SquareSavitch.machine: the deterministic query machine.
• Turing.MultiTapeNTM.SquareSavitch.Runtime: named runtime fields with generated encodings and certificates.

Main results

• Turing.MultiTapeNTM.SquareSavitch.sinkReach_true_iff, Turing.MultiTapeNTM.SquareSavitch.sinkReach_false_iff: the recursion decides reachable overflow, and without it acceptance.
• Turing.MultiTapeNTM.exists_decidableInTimeAndSpace_sq: Savitch's theorem: a problem recognized by a nondeterministic machine within space S is decided by a deterministic machine within space O((S + log₂ n + 1) ^ 2).
• Turing.MultiTapeNTM.SquareSavitch.exists_halted, Turing.MultiTapeNTM.SquareSavitch.length_encRuntime_le: the machine halts, and its states have O((S + log₂ n + 1) ^ 2) bits.

References

• W. J. Savitch, Relationships between nondeterministic and deterministic tape complexities; journal text not inspected (paywalled), so no theorem number or page is cited.
• M. Sipser, Introduction to the Theory of Computation, 3rd edition, Theorem 8.5 and its proof, and Section 8.4, final paragraph (p. 351)
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Theorem 4.14
• N. Immerman, Nondeterministic Space Is Closed under Complementation

The graph on words

noncomputable def Turing.MultiTapeNTM.SquareSavitch.target {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (overflowMode : Bool) (B n : ℕ) (symbol : Option Bool) (u : ℕ) : Bool

The targets of a round, given the input bit symbol at the vertex: the overflowing vertices in overflow mode, and the accepting halted vertices otherwise.

noncomputable def Turing.MultiTapeNTM.SquareSavitch.wordEdge {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (overflowMode : Bool) (B n : ℕ) (symbol : Option Bool) (u v : List Bool) : Bool

The edges of the graph on words, given the round mode and the input bit symbol at the source: the edges of the compact configuration graph between the values of the words, and an edge from every target vertex to the sink, the word of ones.

noncomputable def Turing.MultiTapeNTM.SquareSavitch.paramEdge {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (p : Bool × ℕ × ℕ × Option Bool) : List Bool → List Bool → Bool

The edges of the graph on words, with the round mode, the radix, the input length and the input bit as one parameter.

noncomputable def Turing.MultiTapeNTM.SquareSavitch.inputEdge {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (overflowMode : Bool) (B : ℕ) (w u v : List Bool) : Bool

The edges of the graph on words on the input w: the input bit is read at the input head of the source.

def Turing.MultiTapeNTM.SquareSavitch.Target {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (overflowMode : Bool) (B : ℕ) (w : List Bool) (u : ℕ) : Prop

The target test on an actual input, reading the bit at queryIndex.

noncomputable def Turing.MultiTapeNTM.SquareSavitch.sinkReach {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (overflowMode : Bool) (B : ℕ) (w : List Bool) : Bool

The recursion of a round: Savitch's midpoint recursion at depth W = vertexWidth k B on the graph on words of width W, from the start vertex to the sink.

def Turing.MultiTapeNTM.SquareSavitch.OverflowReachable {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (B : ℕ) (w : List Bool) : Prop

Some overflowing vertex is reachable in the graph of radix B.

Reachability of the sink

theorem Turing.MultiTapeNTM.SquareSavitch.vertexBound_le_ofBits_sink {k : ℕ} (B : ℕ) : ConfigurationGraph.vertexBound B ≤ MultiTapeTM.ofBits (List.replicate (ConfigurationGraph.vertexWidth k B) true)

No vertex is the sink.

theorem Turing.MultiTapeNTM.SquareSavitch.lt_vertexBound_of_target {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {B : ℕ} {overflowMode : Bool} {n u : ℕ} {symbol : Option Bool} (h : target ntm overflowMode B n symbol u = true) : u < ConfigurationGraph.vertexBound B

Every target is a vertex of the graph.

theorem Turing.MultiTapeNTM.SquareSavitch.reflTransGen_sink_iff {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {B : ℕ} {w : List Bool} {overflowMode : Bool} (hstart : ConfigurationGraph.startID ntm B < ConfigurationGraph.vertexBound B) : Relation.ReflTransGen (fun (a b : List Bool) => a.length = ConfigurationGraph.vertexWidth k B ∧ b.length = ConfigurationGraph.vertexWidth k B ∧ inputEdge ntm overflowMode B w a b = true) (Cslib.BitString.lowBits (ConfigurationGraph.vertexWidth k B) (ConfigurationGraph.startID ntm B)) (List.replicate (ConfigurationGraph.vertexWidth k B) true) ↔ ∃ (u : ℕ), Relation.ReflTransGen (ConfigurationGraph.Edge ntm B w) (ConfigurationGraph.startID ntm B) u ∧ Target ntm overflowMode B w u

The sink is reachable exactly when a target is. Along the graph on words of width W = vertexWidth k B, from the start vertex to the word of W ones.

theorem Turing.MultiTapeNTM.SquareSavitch.sinkReach_eq_true_iff {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {B : ℕ} {w : List Bool} {overflowMode : Bool} (hB : Fintype.card (Option State) + 1 < B) : sinkReach ntm overflowMode B w = true ↔ ∃ (u : ℕ), Relation.ReflTransGen (ConfigurationGraph.Edge ntm B w) (ConfigurationGraph.startID ntm B) u ∧ Target ntm overflowMode B w u

The recursion of a round decides whether a target is reachable, for every radix above the finite tags.

theorem Turing.MultiTapeNTM.SquareSavitch.sinkReach_true_iff {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {B : ℕ} {w : List Bool} (hB : Fintype.card (Option State) + 1 < B) : sinkReach ntm true B w = true ↔ OverflowReachable ntm B w

The overflow round decides reachable overflow.

theorem Turing.MultiTapeNTM.SquareSavitch.sinkReach_false_iff {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {B : ℕ} {w : List Bool} (hB : Fintype.card (Option State) + 1 < B) (hno : ¬OverflowReachable ntm B w) : sinkReach ntm false B w = true ↔ ntm.Accepts w

Without reachable overflow, the acceptance round decides acceptance.

theorem Turing.MultiTapeNTM.SquareSavitch.not_overflowReachable_of_runsInSpace {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} {S j : ℕ} (hs : ntm.RunsInSpace w S) (hj : 4 * S + 1 ≤ j) : ¬OverflowReachable ntm (ConfigurationGraph.roundRadix State w.length j) w

The late rounds have no reachable overflow: for a machine within space S, from round 4 * S + 1 on.

The query machine

@[reducible, inline]

abbrev Turing.MultiTapeNTM.SquareSavitch.encParam : Bool × ℕ × ℕ × Option Bool ↪ List Bool

The encoding of the parameter of the edge test: the round mode, the radix and the input length in binary, and the input bit read last.

structure Turing.MultiTapeNTM.SquareSavitch.EdgeParams : Type

Edge-test parameters, with the input bit read last.

• overflowMode : Bool

  Whether the round searches for overflow, rather than for acceptance.

• radix : ℕ

  Radix used to encode the simulated machine registers.

• inputLength : ℕ

  Length of the original read-only input.

• symbol : Option Bool

  Input bit just read, or none beyond the input.

structure Turing.MultiTapeNTM.SquareSavitch.RoundSetup : Type

The parameters and unary vertex width share one frame.

• params : EdgeParams

  Parameters shared by all edge tests in this round.

• width : ℕ

  Bit width of vertices, stored in unary.

structure Turing.MultiTapeNTM.SquareSavitch.SimulationRound : Type

A round of midpoint recursion.

• setup : RoundSetup

  Edge-test parameters and vertex width.

• recursion : Cslib.Reachability.Savitch.State

  Current continuation stack and recursion register.

structure Turing.MultiTapeNTM.SquareSavitch.Runtime : Type

The input counter, startup flag, and current simulation round.

• counter : ℕ

  Number of input bits counted; the input length after startup.

• started : Bool

  Whether input counting has finished and recursion has started.

• round : SimulationRound

  Current midpoint-recursion round.

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_fields_deg : MultiTapeTM.ComputableInDegree (fun (a : EdgeParams) => (a.overflowMode, a.radix, a.inputLength, a.symbol)) encEdgeParams encEdgeParamsFields 1 1

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_symbol_deg : MultiTapeTM.ComputableInDegree EdgeParams.symbol encEdgeParams (MultiTapeTM.encOption MultiTapeTM.encBool) 1 1

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_radix_inO : MultiTapeTM.ComputableInO EdgeParams.radix encEdgeParams MultiTapeTM.encNat (fun (a : EdgeParams) => (encEdgeParams a).length) fun (a : EdgeParams) => (encEdgeParams a).length

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Bool} {x1 x2 : γ → ℕ} {x3 : γ → Option Bool} (h0 : MultiTapeTM.ComputableInPolyTime x0 encIn MultiTapeTM.encBool) (h1 : MultiTapeTM.ComputableInPolyTime x1 encIn MultiTapeTM.encNat) (h2 : MultiTapeTM.ComputableInPolyTime x2 encIn MultiTapeTM.encNat) (h3 : MultiTapeTM.ComputableInPolyTime x3 encIn (MultiTapeTM.encOption MultiTapeTM.encBool)) : MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { overflowMode := x0 x, radix := x1 x, inputLength := x2 x, symbol := x3 x }) encIn encEdgeParams

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_inputLength_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → EdgeParams} : MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encEdgeParams → MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).inputLength) encIn✝ MultiTapeTM.encNat

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_overflowMode_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → EdgeParams} : MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encEdgeParams → MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).overflowMode) encIn✝ MultiTapeTM.encBool

@[simp]

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_apply (a : EdgeParams) : encEdgeParams a = encEdgeParamsFields (a.overflowMode, a.radix, a.inputLength, a.symbol)

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_symbol_inO : MultiTapeTM.ComputableInO EdgeParams.symbol encEdgeParams (MultiTapeTM.encOption MultiTapeTM.encBool) (fun (a : EdgeParams) => (encEdgeParams a).length) fun (a : EdgeParams) => (encEdgeParams a).length

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_radix_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → EdgeParams} : MultiTapeTM.ComputableInSpace g✝ encIn✝ encEdgeParams S✝ → MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).radix) encIn✝ MultiTapeTM.encNat S✝

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → Bool} {x1 x2 : γ → ℕ} {x3 : γ → Option Bool} (h0 : MultiTapeTM.ComputableInSpace x0 encIn MultiTapeTM.encBool budget) (h1 : MultiTapeTM.ComputableInSpace x1 encIn MultiTapeTM.encNat budget) (h2 : MultiTapeTM.ComputableInSpace x2 encIn MultiTapeTM.encNat budget) (h3 : MultiTapeTM.ComputableInSpace x3 encIn (MultiTapeTM.encOption MultiTapeTM.encBool) budget) : MultiTapeTM.ComputableInSpace (fun (x : γ) => { overflowMode := x0 x, radix := x1 x, inputLength := x2 x, symbol := x3 x }) encIn encEdgeParams budget

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_inputLength_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → EdgeParams} : MultiTapeTM.ComputableInSpace g✝ encIn✝ encEdgeParams S✝ → MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).inputLength) encIn✝ MultiTapeTM.encNat S✝

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_mk_deg : MultiTapeTM.ComputableInDegree (fun (p : Bool × ℕ × ℕ × Option Bool) => { overflowMode := p.1, radix := p.2.1, inputLength := p.2.2.1, symbol := p.2.2.2 }) encEdgeParamsFields encEdgeParams 1 1

@[reducible, inline]

abbrev Turing.MultiTapeNTM.SquareSavitch.encEdgeParamsFields : Bool × ℕ × ℕ × Option Bool ↪ List Bool

The tuple of the fields of encEdgeParams.

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_overflowMode_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → EdgeParams} : MultiTapeTM.ComputableInSpace g✝ encIn✝ encEdgeParams S✝ → MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).overflowMode) encIn✝ MultiTapeTM.encBool S✝

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_radix_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → EdgeParams} : MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encEdgeParams → MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).radix) encIn✝ MultiTapeTM.encNat

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_inputLength_deg : MultiTapeTM.ComputableInDegree EdgeParams.inputLength encEdgeParams MultiTapeTM.encNat 1 1

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_radix_deg : MultiTapeTM.ComputableInDegree EdgeParams.radix encEdgeParams MultiTapeTM.encNat 1 1

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_symbol_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → EdgeParams} : MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encEdgeParams → MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).symbol) encIn✝ (MultiTapeTM.encOption MultiTapeTM.encBool)

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_overflowMode_inO : MultiTapeTM.ComputableInO EdgeParams.overflowMode encEdgeParams MultiTapeTM.encBool (fun (a : EdgeParams) => (encEdgeParams a).length) fun (a : EdgeParams) => (encEdgeParams a).length

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Bool} {T0 S0 x1 T1 S1 x2 T2 S2 : γ → ℕ} {x3 : γ → Option Bool} {T3 S3 : γ → ℕ} (h0 : MultiTapeTM.ComputableInO x0 encIn MultiTapeTM.encBool T0 S0) (h1 : MultiTapeTM.ComputableInO x1 encIn MultiTapeTM.encNat T1 S1) (h2 : MultiTapeTM.ComputableInO x2 encIn MultiTapeTM.encNat T2 S2) (h3 : MultiTapeTM.ComputableInO x3 encIn (MultiTapeTM.encOption MultiTapeTM.encBool) T3 S3) : MultiTapeTM.ComputableInO (fun (x : γ) => { overflowMode := x0 x, radix := x1 x, inputLength := x2 x, symbol := x3 x }) encIn encEdgeParams (fun (x : γ) => T0 x + (T1 x + (T2 x + T3 x))) fun (x : γ) => S0 x + (S1 x + (S2 x + S3 x))

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_overflowMode_deg : MultiTapeTM.ComputableInDegree EdgeParams.overflowMode encEdgeParams MultiTapeTM.encBool 1 1

def Turing.MultiTapeNTM.SquareSavitch.encEdgeParams : EdgeParams ↪ List Bool

Round mode, binary radix and input length followed by the optional input bit, in field order.

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_symbol_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → EdgeParams} : MultiTapeTM.ComputableInSpace g✝ encIn✝ encEdgeParams S✝ → MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).symbol) encIn✝ (MultiTapeTM.encOption MultiTapeTM.encBool) S✝

theorem Turing.MultiTapeNTM.SquareSavitch.encEdgeParams_inputLength_inO : MultiTapeTM.ComputableInO EdgeParams.inputLength encEdgeParams MultiTapeTM.encNat (fun (a : EdgeParams) => (encEdgeParams a).length) fun (a : EdgeParams) => (encEdgeParams a).length

theorem Turing.MultiTapeNTM.SquareSavitch.encRoundSetup_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → EdgeParams} {x1 : γ → ℕ} (h0 : MultiTapeTM.ComputableInSpace x0 encIn encEdgeParams budget) (h1 : MultiTapeTM.ComputableInSpace x1 encIn MultiTapeTM.encUnary budget) : MultiTapeTM.ComputableInSpace (fun (x : γ) => { params := x0 x, width := x1 x }) encIn encRoundSetup budget

theorem Turing.MultiTapeNTM.SquareSavitch.encRoundSetup_fields_deg : MultiTapeTM.ComputableInDegree (fun (a : RoundSetup) => (a.params, a.width)) encRoundSetup encRoundSetupFields 1 1

theorem Turing.MultiTapeNTM.SquareSavitch.encRoundSetup_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → EdgeParams} {T0 S0 x1 T1 S1 : γ → ℕ} (h0 : MultiTapeTM.ComputableInO x0 encIn encEdgeParams T0 S0) (h1 : MultiTapeTM.ComputableInO x1 encIn MultiTapeTM.encUnary T1 S1) : MultiTapeTM.ComputableInO (fun (x : γ) => { params := x0 x, width := x1 x }) encIn encRoundSetup (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Turing.MultiTapeNTM.SquareSavitch.encRoundSetup_params_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → RoundSetup} : MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encRoundSetup → MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).params) encIn✝ encEdgeParams

theorem Turing.MultiTapeNTM.SquareSavitch.encRoundSetup_params_deg : MultiTapeTM.ComputableInDegree RoundSetup.params encRoundSetup encEdgeParams 1 1

theorem Turing.MultiTapeNTM.SquareSavitch.encRoundSetup_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → EdgeParams} {x1 : γ → ℕ} (h0 : MultiTapeTM.ComputableInPolyTime x0 encIn encEdgeParams) (h1 : MultiTapeTM.ComputableInPolyTime x1 encIn MultiTapeTM.encUnary) : MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { params := x0 x, width := x1 x }) encIn encRoundSetup

theorem Turing.MultiTapeNTM.SquareSavitch.encRoundSetup_params_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → RoundSetup} : MultiTapeTM.ComputableInSpace g✝ encIn✝ encRoundSetup S✝ → MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).params) encIn✝ encEdgeParams S✝

theorem Turing.MultiTapeNTM.SquareSavitch.encRoundSetup_width_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → RoundSetup} : MultiTapeTM.ComputableInSpace g✝ encIn✝ encRoundSetup S✝ → MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).width) encIn✝ MultiTapeTM.encUnary S✝

@[simp]

theorem Turing.MultiTapeNTM.SquareSavitch.encRoundSetup_apply (a : RoundSetup) : encRoundSetup a = encRoundSetupFields (a.params, a.width)

theorem Turing.MultiTapeNTM.SquareSavitch.encRoundSetup_width_deg : MultiTapeTM.ComputableInDegree RoundSetup.width encRoundSetup MultiTapeTM.encUnary 1 1

theorem Turing.MultiTapeNTM.SquareSavitch.encRoundSetup_params_inO : MultiTapeTM.ComputableInO RoundSetup.params encRoundSetup encEdgeParams (fun (a : RoundSetup) => (encRoundSetup a).length) fun (a : RoundSetup) => (encRoundSetup a).length

theorem Turing.MultiTapeNTM.SquareSavitch.encRoundSetup_width_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → RoundSetup} : MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encRoundSetup → MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).width) encIn✝ MultiTapeTM.encUnary

def Turing.MultiTapeNTM.SquareSavitch.encRoundSetup : RoundSetup ↪ List Bool

Framed edge parameters followed by the unary vertex width.

@[reducible, inline]

abbrev Turing.MultiTapeNTM.SquareSavitch.encRoundSetupFields : EdgeParams × ℕ ↪ List Bool

The tuple of the fields of encRoundSetup.

theorem Turing.MultiTapeNTM.SquareSavitch.encRoundSetup_width_inO : MultiTapeTM.ComputableInO RoundSetup.width encRoundSetup MultiTapeTM.encUnary (fun (a : RoundSetup) => (encRoundSetup a).length) fun (a : RoundSetup) => (encRoundSetup a).length

theorem Turing.MultiTapeNTM.SquareSavitch.encRoundSetup_mk_deg : MultiTapeTM.ComputableInDegree (fun (p : EdgeParams × ℕ) => { params := p.1, width := p.2 }) encRoundSetupFields encRoundSetup 1 1

theorem Turing.MultiTapeNTM.SquareSavitch.encSimulationRound_setup_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → SimulationRound} : MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encSimulationRound → MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).setup) encIn✝ encRoundSetup

theorem Turing.MultiTapeNTM.SquareSavitch.encSimulationRound_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → RoundSetup} {x1 : γ → Cslib.Reachability.Savitch.State} (h0 : MultiTapeTM.ComputableInPolyTime x0 encIn encRoundSetup) (h1 : MultiTapeTM.ComputableInPolyTime x1 encIn Cslib.Reachability.Savitch.encState) : MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { setup := x0 x, recursion := x1 x }) encIn encSimulationRound

theorem Turing.MultiTapeNTM.SquareSavitch.encSimulationRound_recursion_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → SimulationRound} : MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encSimulationRound → MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).recursion) encIn✝ Cslib.Reachability.Savitch.encState

theorem Turing.MultiTapeNTM.SquareSavitch.encSimulationRound_setup_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → SimulationRound} : MultiTapeTM.ComputableInSpace g✝ encIn✝ encSimulationRound S✝ → MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).setup) encIn✝ encRoundSetup S✝

@[simp]

theorem Turing.MultiTapeNTM.SquareSavitch.encSimulationRound_apply (a : SimulationRound) : encSimulationRound a = encSimulationRoundFields (a.setup, a.recursion)

@[reducible, inline]

abbrev Turing.MultiTapeNTM.SquareSavitch.encSimulationRoundFields : RoundSetup × Cslib.Reachability.Savitch.State ↪ List Bool

The tuple of the fields of encSimulationRound.

theorem Turing.MultiTapeNTM.SquareSavitch.encSimulationRound_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → RoundSetup} {T0 S0 : γ → ℕ} {x1 : γ → Cslib.Reachability.Savitch.State} {T1 S1 : γ → ℕ} (h0 : MultiTapeTM.ComputableInO x0 encIn encRoundSetup T0 S0) (h1 : MultiTapeTM.ComputableInO x1 encIn Cslib.Reachability.Savitch.encState T1 S1) : MultiTapeTM.ComputableInO (fun (x : γ) => { setup := x0 x, recursion := x1 x }) encIn encSimulationRound (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Turing.MultiTapeNTM.SquareSavitch.encSimulationRound_recursion_inO : MultiTapeTM.ComputableInO SimulationRound.recursion encSimulationRound Cslib.Reachability.Savitch.encState (fun (a : SimulationRound) => (encSimulationRound a).length) fun (a : SimulationRound) => (encSimulationRound a).length

def Turing.MultiTapeNTM.SquareSavitch.encSimulationRound : SimulationRound ↪ List Bool

Framed round setup followed by the encoded recursion state.

theorem Turing.MultiTapeNTM.SquareSavitch.encSimulationRound_fields_deg : MultiTapeTM.ComputableInDegree (fun (a : SimulationRound) => (a.setup, a.recursion)) encSimulationRound encSimulationRoundFields 1 1

theorem Turing.MultiTapeNTM.SquareSavitch.encSimulationRound_recursion_deg : MultiTapeTM.ComputableInDegree SimulationRound.recursion encSimulationRound Cslib.Reachability.Savitch.encState 1 1

theorem Turing.MultiTapeNTM.SquareSavitch.encSimulationRound_setup_inO : MultiTapeTM.ComputableInO SimulationRound.setup encSimulationRound encRoundSetup (fun (a : SimulationRound) => (encSimulationRound a).length) fun (a : SimulationRound) => (encSimulationRound a).length

theorem Turing.MultiTapeNTM.SquareSavitch.encSimulationRound_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → RoundSetup} {x1 : γ → Cslib.Reachability.Savitch.State} (h0 : MultiTapeTM.ComputableInSpace x0 encIn encRoundSetup budget) (h1 : MultiTapeTM.ComputableInSpace x1 encIn Cslib.Reachability.Savitch.encState budget) : MultiTapeTM.ComputableInSpace (fun (x : γ) => { setup := x0 x, recursion := x1 x }) encIn encSimulationRound budget

theorem Turing.MultiTapeNTM.SquareSavitch.encSimulationRound_recursion_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → SimulationRound} : MultiTapeTM.ComputableInSpace g✝ encIn✝ encSimulationRound S✝ → MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).recursion) encIn✝ Cslib.Reachability.Savitch.encState S✝

theorem Turing.MultiTapeNTM.SquareSavitch.encSimulationRound_setup_deg : MultiTapeTM.ComputableInDegree SimulationRound.setup encSimulationRound encRoundSetup 1 1

theorem Turing.MultiTapeNTM.SquareSavitch.encSimulationRound_mk_deg : MultiTapeTM.ComputableInDegree (fun (p : RoundSetup × Cslib.Reachability.Savitch.State) => { setup := p.1, recursion := p.2 }) encSimulationRoundFields encSimulationRound 1 1

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_round_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Runtime} : MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encRuntime → MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).round) encIn✝ encSimulationRound

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 T0 S0 : γ → ℕ} {x1 : γ → Bool} {T1 S1 : γ → ℕ} {x2 : γ → SimulationRound} {T2 S2 : γ → ℕ} (h0 : MultiTapeTM.ComputableInO x0 encIn MultiTapeTM.encNat T0 S0) (h1 : MultiTapeTM.ComputableInO x1 encIn MultiTapeTM.encBool T1 S1) (h2 : MultiTapeTM.ComputableInO x2 encIn encSimulationRound T2 S2) : MultiTapeTM.ComputableInO (fun (x : γ) => { counter := x0 x, started := x1 x, round := x2 x }) encIn encRuntime (fun (x : γ) => T0 x + (T1 x + T2 x)) fun (x : γ) => S0 x + (S1 x + S2 x)

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_counter_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Runtime} : MultiTapeTM.ComputableInSpace g✝ encIn✝ encRuntime S✝ → MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).counter) encIn✝ MultiTapeTM.encNat S✝

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_round_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Runtime} : MultiTapeTM.ComputableInSpace g✝ encIn✝ encRuntime S✝ → MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).round) encIn✝ encSimulationRound S✝

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_round_inO : MultiTapeTM.ComputableInO Runtime.round encRuntime encSimulationRound (fun (a : Runtime) => (encRuntime a).length) fun (a : Runtime) => (encRuntime a).length

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_counter_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Runtime} : MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encRuntime → MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).counter) encIn✝ MultiTapeTM.encNat

@[reducible, inline]

abbrev Turing.MultiTapeNTM.SquareSavitch.encRuntimeFields : ℕ × Bool × SimulationRound ↪ List Bool

The tuple of the fields of encRuntime.

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → ℕ} {x1 : γ → Bool} {x2 : γ → SimulationRound} (h0 : MultiTapeTM.ComputableInPolyTime x0 encIn MultiTapeTM.encNat) (h1 : MultiTapeTM.ComputableInPolyTime x1 encIn MultiTapeTM.encBool) (h2 : MultiTapeTM.ComputableInPolyTime x2 encIn encSimulationRound) : MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { counter := x0 x, started := x1 x, round := x2 x }) encIn encRuntime

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget x0 : γ → ℕ} {x1 : γ → Bool} {x2 : γ → SimulationRound} (h0 : MultiTapeTM.ComputableInSpace x0 encIn MultiTapeTM.encNat budget) (h1 : MultiTapeTM.ComputableInSpace x1 encIn MultiTapeTM.encBool budget) (h2 : MultiTapeTM.ComputableInSpace x2 encIn encSimulationRound budget) : MultiTapeTM.ComputableInSpace (fun (x : γ) => { counter := x0 x, started := x1 x, round := x2 x }) encIn encRuntime budget

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_counter_deg : MultiTapeTM.ComputableInDegree Runtime.counter encRuntime MultiTapeTM.encNat 1 1

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_started_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Runtime} : MultiTapeTM.ComputableInSpace g✝ encIn✝ encRuntime S✝ → MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).started) encIn✝ MultiTapeTM.encBool S✝

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_mk_deg : MultiTapeTM.ComputableInDegree (fun (p : ℕ × Bool × SimulationRound) => { counter := p.1, started := p.2.1, round := p.2.2 }) encRuntimeFields encRuntime 1 1

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_round_deg : MultiTapeTM.ComputableInDegree Runtime.round encRuntime encSimulationRound 1 1

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_counter_inO : MultiTapeTM.ComputableInO Runtime.counter encRuntime MultiTapeTM.encNat (fun (a : Runtime) => (encRuntime a).length) fun (a : Runtime) => (encRuntime a).length

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_started_deg : MultiTapeTM.ComputableInDegree Runtime.started encRuntime MultiTapeTM.encBool 1 1

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_started_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Runtime} : MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encRuntime → MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).started) encIn✝ MultiTapeTM.encBool

def Turing.MultiTapeNTM.SquareSavitch.encRuntime : Runtime ↪ List Bool

Binary counter, startup bit and simulation round, in field order.

@[simp]

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_apply (a : Runtime) : encRuntime a = encRuntimeFields (a.counter, a.started, a.round)

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_started_inO : MultiTapeTM.ComputableInO Runtime.started encRuntime MultiTapeTM.encBool (fun (a : Runtime) => (encRuntime a).length) fun (a : Runtime) => (encRuntime a).length

theorem Turing.MultiTapeNTM.SquareSavitch.encRuntime_fields_deg : MultiTapeTM.ComputableInDegree (fun (a : Runtime) => (a.counter, a.started, a.round)) encRuntime encRuntimeFields 1 1

def Turing.MultiTapeNTM.SquareSavitch.SimulationRound.ofRound (q : ((Bool × ℕ × ℕ × Option Bool) × ℕ) × Cslib.Reachability.Savitch.State) : SimulationRound

Enter the named runtime representation at the generic Savitch round boundary.

noncomputable def Turing.MultiTapeNTM.SquareSavitch.initRound {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (overflowMode : Bool) (B n : ℕ) : ((Bool × ℕ × ℕ × Option Bool) × ℕ) × Cslib.Reachability.Savitch.State

The first state of a round of the given mode and radix, on inputs of length n: the call at depth W from the start vertex to the sink. The start vertex is written as the binary digits of its value plus 2 ^ W, without the last one (Turing.MultiTapeTM.bits_add_two_pow).

def Turing.MultiTapeNTM.SquareSavitch.idle : ((Bool × ℕ × ℕ × Option Bool) × ℕ) × Cslib.Reachability.Savitch.State

The round held while the input is counted.

def Turing.MultiTapeNTM.SquareSavitch.callSource (st : Cslib.Reachability.Savitch.State) : List Bool

The source of the pending call, if any.

def Turing.MultiTapeNTM.SquareSavitch.returned (st : Cslib.Reachability.Savitch.State) : Bool

The recursion has returned its value.

def Turing.MultiTapeNTM.SquareSavitch.restarts (s : Runtime) : Bool

The round has returned, and it is an overflow round: the next round starts.

noncomputable def Turing.MultiTapeNTM.SquareSavitch.query (k : ℕ) (s : Runtime) : ℕ

The input bit to read: the next input position while counting, then the input head of the source of the pending call.

noncomputable def Turing.MultiTapeNTM.SquareSavitch.next {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (p : Runtime × Option Bool) : Runtime

A step of the machine, given the input bit read: count the input until its end, then start the overflow round of the first radix. An overflow round that returns true starts the overflow round of the next radix; one that returns false starts the acceptance round of the same radix. Other steps run the recursion, with the bit read as the input bit of the edge test.

def Turing.MultiTapeNTM.SquareSavitch.halted (s : Runtime) : Bool

The machine halts once an acceptance round has returned.

def Turing.MultiTapeNTM.SquareSavitch.finish (s : Runtime) : List Bool

The answer: the value returned by the recursion.

noncomputable def Turing.MultiTapeNTM.SquareSavitch.machine {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) : QueryMachine Runtime

The deterministic simulation, as a query machine: count the input, then run Savitch's recursion on the graphs on words of growing radix, reading the input bit of each edge test.

The runs of the machine

theorem Turing.MultiTapeNTM.SquareSavitch.step_congr {e₁ e₂ : List Bool → List Bool → Bool} {W : ℕ} {st : Cslib.Reachability.Savitch.State} (h : ∀ (u v : List Bool), st.reg = Cslib.Reachability.Savitch.Reg.call 0 u v → e₁ u v = e₂ u v) : Cslib.Reachability.Savitch.step e₁ W st = Cslib.Reachability.Savitch.step e₂ W st

The step of the recursion only uses the edge test at a call at level 0.

theorem Turing.MultiTapeNTM.SquareSavitch.output_eq {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} (w : List Bool) (t : ℕ) : (machine ntm).output w t = finish ((machine ntm).run w t)

The machine emits nothing before its final answer.

theorem Turing.MultiTapeNTM.SquareSavitch.run_of_le {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} (w : List Bool) {t : ℕ} (ht : t ≤ w.length) : (machine ntm).run w t = { counter := t, started := false, round := SimulationRound.ofRound idle }

While counting, the machine holds the number of input bits read.

theorem Turing.MultiTapeNTM.SquareSavitch.run_length_succ {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} (w : List Bool) : (machine ntm).run w (w.length + 1) = { counter := w.length, started := true, round := SimulationRound.ofRound (initRound ntm true (ConfigurationGraph.startRadix State w.length) w.length) }

At the end of the input, the machine starts the overflow round of the first radix.

theorem Turing.MultiTapeNTM.SquareSavitch.returned_eq_true_iff {st : Cslib.Reachability.Savitch.State} : returned st = true ↔ ∃ (b : Bool), st = { stack := [], reg := Cslib.Reachability.Savitch.Reg.ret b }

The value of a returned recursion is the value of its register.

theorem Turing.MultiTapeNTM.SquareSavitch.step_round {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} (w : List Bool) {mode : Bool} {B : ℕ} {symbol : Option Bool} {st : Cslib.Reachability.Savitch.State} (h : returned st = false) : (machine ntm).step w { counter := w.length, started := true, round := SimulationRound.ofRound (((mode, B, w.length, symbol), ConfigurationGraph.vertexWidth k B), st) } = { counter := w.length, started := true, round := SimulationRound.ofRound (((mode, B, w.length, w[ConfigurationGraph.queryIndex B (MultiTapeTM.ofBits (callSource st))]?), ConfigurationGraph.vertexWidth k B), Cslib.Reachability.Savitch.step (inputEdge ntm mode B w) (ConfigurationGraph.vertexWidth k B) st) }

A step of a round that has not returned runs the recursion, with the input bit at the source of the pending call.

theorem Turing.MultiTapeNTM.SquareSavitch.step_restart {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} (w : List Bool) {B : ℕ} {symbol : Option Bool} {b : Bool} : (machine ntm).step w { counter := w.length, started := true, round := SimulationRound.ofRound (((true, B, w.length, symbol), ConfigurationGraph.vertexWidth k B), { stack := [], reg := Cslib.Reachability.Savitch.Reg.ret b }) } = { counter := w.length, started := true, round := SimulationRound.ofRound (initRound ntm b (if b = true then 4 * B else B) w.length) }

A returned overflow round starts the next round: the overflow round of the next radix if it returned true, and the acceptance round of the same radix otherwise.

theorem Turing.MultiTapeNTM.SquareSavitch.halted_round {k : ℕ} (w : List Bool) {B : ℕ} {symbol : Option Bool} {b : Bool} : halted { counter := w.length, started := true, round := SimulationRound.ofRound (((false, B, w.length, symbol), ConfigurationGraph.vertexWidth k B), { stack := [], reg := Cslib.Reachability.Savitch.Reg.ret b }) } = true

A returned acceptance round has halted.

theorem Turing.MultiTapeNTM.SquareSavitch.initRound_snd {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} (w : List Bool) {mode : Bool} {B : ℕ} (hB : Fintype.card (Option State) + 1 < B) : (initRound ntm mode B w.length).2 = { stack := [], reg := Cslib.Reachability.Savitch.Reg.call (ConfigurationGraph.vertexWidth k B) (Cslib.BitString.lowBits (ConfigurationGraph.vertexWidth k B) (ConfigurationGraph.startID ntm B)) (List.replicate (ConfigurationGraph.vertexWidth k B) true) }

The first state of a round, once the start vertex is known to have a word.

theorem Turing.MultiTapeNTM.SquareSavitch.ret_eq_sinkReach {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} (w : List Bool) {mode : Bool} {B : ℕ} (hB : Fintype.card (Option State) + 1 < B) {i : ℕ} {b : Bool} (h : (Cslib.Reachability.Savitch.step (inputEdge ntm mode B w) (ConfigurationGraph.vertexWidth k B))^[i] (initRound ntm mode B w.length).2 = { stack := [], reg := Cslib.Reachability.Savitch.Reg.ret b }) : b = sinkReach ntm mode B w

A returned round holds the value of its recursion.

theorem Turing.MultiTapeNTM.SquareSavitch.exists_run_returned {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} (w : List Bool) {mode : Bool} {B t₀ : ℕ} (hB : Fintype.card (Option State) + 1 < B) (h₀ : (machine ntm).run w t₀ = { counter := w.length, started := true, round := SimulationRound.ofRound (initRound ntm mode B w.length) }) : ∃ (t : ℕ) (symbol : Option Bool), (machine ntm).run w t = { counter := w.length, started := true, round := SimulationRound.ofRound (((mode, B, w.length, symbol), ConfigurationGraph.vertexWidth k B), { stack := [], reg := Cslib.Reachability.Savitch.Reg.ret (sinkReach ntm mode B w) }) }

A round runs to its return: from the first state of a round, the machine runs the recursion until it returns the value sinkReach.

def Turing.MultiTapeNTM.SquareSavitch.RunState {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} (w : List Bool) (s : Runtime) : Prop

The states of a run: counting the input, or a round of radix roundRadix State n j, after overflow rounds that found overflow at every earlier radix. An acceptance round has no reachable overflow at its radix.

theorem Turing.MultiTapeNTM.SquareSavitch.runState_step {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} (w : List Bool) {s : Runtime} (h : RunState w s) : RunState w ((machine ntm).step w s)

The machine keeps the states of a run.

theorem Turing.MultiTapeNTM.SquareSavitch.runState_run {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} (w : List Bool) (t : ℕ) : RunState w ((machine ntm).run w t)

Every state of the run is a state of a run.

theorem Turing.MultiTapeNTM.SquareSavitch.answer_iff_of_halted {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} (w : List Bool) {s : Runtime} (h : RunState w s) (hh : halted s = true) : s.round.recursion.reg.toPair.2 = true ↔ ntm.Accepts w

A halted machine has decided acceptance.

theorem Turing.MultiTapeNTM.SquareSavitch.halted_or_next_round {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} (w : List Bool) {j t₀ : ℕ} (h₀ : (machine ntm).run w t₀ = { counter := w.length, started := true, round := SimulationRound.ofRound (initRound ntm true (ConfigurationGraph.roundRadix State w.length j) w.length) }) : (∃ (t : ℕ), halted ((machine ntm).run w t) = true) ∨ OverflowReachable ntm (ConfigurationGraph.roundRadix State w.length j) w ∧ ∃ (t₁ : ℕ), (machine ntm).run w t₁ = { counter := w.length, started := true, round := SimulationRound.ofRound (initRound ntm true (ConfigurationGraph.roundRadix State w.length (j + 1)) w.length) }

A returned overflow round leads to a halted machine or to the overflow round of the next radix, after reachable overflow.

theorem Turing.MultiTapeNTM.SquareSavitch.exists_halted {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} (w : List Bool) {S : ℕ} (hs : ntm.RunsInSpace w S) : ∃ (t : ℕ), halted ((machine ntm).run w t) = true

The machine halts on the inputs of a machine within some space bound.

The size of the states

theorem Turing.MultiTapeNTM.SquareSavitch.le_of_overflowReachable {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} {S j : ℕ} (hs : ntm.RunsInSpace w S) (hlt : ∀ j' < j, OverflowReachable ntm (ConfigurationGraph.roundRadix State w.length j') w) : j ≤ 4 * S + 1

A run within space S stays below round 4 * S + 1.

theorem Turing.MultiTapeNTM.SquareSavitch.invariant_iterate_initRound {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} {mode : Bool} {B : ℕ} (hB : Fintype.card (Option State) + 1 < B) (i : ℕ) : Cslib.Reachability.Savitch.Invariant (ConfigurationGraph.vertexWidth k B) (ConfigurationGraph.vertexWidth k B) ((Cslib.Reachability.Savitch.step (inputEdge ntm mode B w) (ConfigurationGraph.vertexWidth k B))^[i] (initRound ntm mode B w.length).2)

The states of the recursion satisfy the invariant of a run at depth W.

theorem Turing.MultiTapeNTM.SquareSavitch.length_encRuntime (s : Runtime) : (encRuntime s).length = 2 * (MultiTapeTM.encNat s.counter).length + 8 * (MultiTapeTM.encNat s.round.setup.params.radix).length + 8 * (MultiTapeTM.encNat s.round.setup.params.inputLength).length + 4 * ((MultiTapeTM.encOption MultiTapeTM.encBool) s.round.setup.params.symbol).length + 2 * s.round.setup.width + 27 + (Cslib.Reachability.Savitch.encState s.round.recursion).length

The runtime's framing cost, separated from the encoded recursion state.

noncomputable def Turing.MultiTapeNTM.SquareSavitch.widthConst (k : ℕ) (State : Type) [Fintype State] : ℕ

The constant factor of the width of the vertices in the rounds of a run.

noncomputable def Turing.MultiTapeNTM.SquareSavitch.sizeConst (k : ℕ) (State : Type) [Fintype State] : ℕ

The constant of the bound on the states of the machine.

theorem Turing.MultiTapeNTM.SquareSavitch.length_encRuntime_le {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} {S : ℕ} (hs : ntm.RunsInSpace w S) {s : Runtime} (h : RunState w s) : (encRuntime s).length ≤ sizeConst k State * (S + w.length.log2 + 1) ^ 2

The states of a run have O((S + log₂ n + 1) ^ 2) bits, for a machine within space S.

The parts of the machine in linear space

theorem Turing.MultiTapeNTM.SquareSavitch.stateFields_inSpace : MultiTapeTM.ComputableInSpace (fun (st : Cslib.Reachability.Savitch.State) => (st.stack, st.reg.toPair)) Cslib.Reachability.Savitch.encState (MultiTapeTM.encPair (MultiTapeTM.encList Cslib.Reachability.Savitch.encFrame) (MultiTapeTM.encPair (MultiTapeTM.encOption Cslib.Reachability.Savitch.encCall) MultiTapeTM.encBool)) fun (st : Cslib.Reachability.Savitch.State) => (Cslib.Reachability.Savitch.encState st).length

The fields of a state of the recursion, as pairs.

theorem Turing.MultiTapeNTM.SquareSavitch.budget_stack {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {st : α → Cslib.Reachability.Savitch.State} (h : MultiTapeTM.ComputableInSpace st enc Cslib.Reachability.Savitch.encState S) : MultiTapeTM.ComputableInSpace (fun (a : α) => (st a).stack) enc (MultiTapeTM.encList Cslib.Reachability.Savitch.encFrame) S

The stack, within a budget.

theorem Turing.MultiTapeNTM.SquareSavitch.budget_reg {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {st : α → Cslib.Reachability.Savitch.State} (h : MultiTapeTM.ComputableInSpace st enc Cslib.Reachability.Savitch.encState S) : MultiTapeTM.ComputableInSpace (fun (a : α) => (st a).reg.toPair) enc (MultiTapeTM.encPair (MultiTapeTM.encOption Cslib.Reachability.Savitch.encCall) MultiTapeTM.encBool) S

The register as a pair, within a budget.

theorem Turing.MultiTapeNTM.SquareSavitch.budget_callSource {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {st : α → Cslib.Reachability.Savitch.State} (h : MultiTapeTM.ComputableInSpace st enc Cslib.Reachability.Savitch.encState S) : MultiTapeTM.ComputableInSpace (fun (a : α) => MultiTapeTM.ofBits (callSource (st a))) enc MultiTapeTM.encNat S

The value of the source of the pending call, within a budget.

theorem Turing.MultiTapeNTM.SquareSavitch.budget_returned {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {st : α → Cslib.Reachability.Savitch.State} (h : MultiTapeTM.ComputableInSpace st enc Cslib.Reachability.Savitch.encState S) : MultiTapeTM.ComputableInSpace (fun (a : α) => returned (st a)) enc MultiTapeTM.encBool S

Whether the recursion has returned, within a budget.

theorem Turing.MultiTapeNTM.SquareSavitch.query_inSpace {k : ℕ} : MultiTapeTM.ComputableInSpace (query k) encRuntime MultiTapeTM.encNat fun (s : Runtime) => (encRuntime s).length

The input position to read, in space linear in the state.

theorem Turing.MultiTapeNTM.SquareSavitch.halted_inSpace : MultiTapeTM.ComputableInSpace halted encRuntime MultiTapeTM.encBool fun (s : Runtime) => (encRuntime s).length

The halting test, in space linear in the state.

theorem Turing.MultiTapeNTM.SquareSavitch.restarts_inSpace : MultiTapeTM.ComputableInSpace restarts encRuntime MultiTapeTM.encBool fun (s : Runtime) => (encRuntime s).length

The restart test, in space linear in the state.

theorem Turing.MultiTapeNTM.SquareSavitch.finish_inSpace : MultiTapeTM.ComputableInSpace finish encRuntime MultiTapeTM.encBits fun (s : Runtime) => (encRuntime s).length

The answer, in space linear in the state.

theorem Turing.MultiTapeNTM.SquareSavitch.paramEdge_inSpace {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) : MultiTapeTM.ComputableInSpace (fun (q : (Bool × ℕ × ℕ × Option Bool) × List Bool × List Bool) => paramEdge ntm q.1 q.2.1 q.2.2) (MultiTapeTM.encPair encParam (MultiTapeTM.encPair MultiTapeTM.encBits MultiTapeTM.encBits)) MultiTapeTM.encBool fun (q : (Bool × ℕ × ℕ × Option Bool) × List Bool × List Bool) => ((MultiTapeTM.encPair encParam (MultiTapeTM.encPair MultiTapeTM.encBits MultiTapeTM.encBits)) q).length

The edge test of the graph on words, in linear space.

theorem Turing.MultiTapeNTM.SquareSavitch.roundStep_inSpace {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) : MultiTapeTM.ComputableInSpace (Cslib.Reachability.Savitch.roundStep (paramEdge ntm)) (Cslib.Reachability.Savitch.encRound encParam) (Cslib.Reachability.Savitch.encRound encParam) fun (q : ((Bool × ℕ × ℕ × Option Bool) × ℕ) × Cslib.Reachability.Savitch.State) => ((Cslib.Reachability.Savitch.encRound encParam) q).length

A round of the recursion on the graph on words, in space linear in the round.

theorem Turing.MultiTapeNTM.SquareSavitch.initRound_budget {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {mode : α → Bool} {B n : α → ℕ} (hmode : MultiTapeTM.ComputableInSpace mode enc MultiTapeTM.encBool S) (hB : MultiTapeTM.ComputableInSpace B enc MultiTapeTM.encNat S) (hn : MultiTapeTM.ComputableInSpace n enc MultiTapeTM.encNat S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableInSpace (fun (a : α) => initRound ntm (mode a) (B a) (n a)) enc (Cslib.Reachability.Savitch.encRound encParam) S

The first state of a round, from the mode, the radix and the input length, within a budget.

theorem Turing.MultiTapeNTM.SquareSavitch.startRadix_budget {State : Type} [Fintype State] {α : Type} {enc : α ↪ List Bool} {S n : α → ℕ} (hn : MultiTapeTM.ComputableInSpace n enc MultiTapeTM.encNat S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableInSpace (fun (a : α) => ConfigurationGraph.startRadix State (n a)) enc MultiTapeTM.encNat S

The first radix, within a budget.

theorem Turing.MultiTapeNTM.SquareSavitch.next_inSpace {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) : MultiTapeTM.ComputableInSpace (next ntm) (MultiTapeTM.encPair encRuntime (MultiTapeTM.encOption MultiTapeTM.encBool)) encRuntime fun (p : Runtime × Option Bool) => ((MultiTapeTM.encPair encRuntime (MultiTapeTM.encOption MultiTapeTM.encBool)) p).length

A step of the machine, in space linear in the state and the bit read.

theorem Turing.MultiTapeNTM.exists_decidableInTimeAndSpace_sq {α : Type} {enc : α ↪ List Bool} {A : Set α} {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {S : α → ℕ} (hA : ntm.RecognizesInSpace enc A S) : ∃ (t : α → ℕ) (c : ℕ), MultiTapeTM.DecidableInTimeAndSpace A enc t fun (a : α) => c * (S a + (enc a).length.log2 + 1) ^ 2

Savitch's theorem [Sav70], for general space bounds. No constructibility is assumed: the machine tries growing bounds, as in Sipser's proof of Theorem 8.5 [Sip13]. A problem recognized by a nondeterministic machine whose computation paths on enc a visit at most S a work cells, and whose branches need not halt, is decided by a deterministic machine within space O((S a + log₂ |enc a| + 1) ^ 2): Savitch's midpoint recursion on the compact configuration graphs of the machine of growing radix (Turing.MultiTapeNTM.SquareSavitch.machine).