From 975c93f6d2c3933396671ffc771dc9143d83719d Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 21:57:13 +0000 Subject: [PATCH 1/2] =?UTF-8?q?refactor(Machines):=20plain=20polynomial-ti?= =?UTF-8?q?me=20tape,=20configuration=20and=20NL=20=E2=8A=86=20P=20search?= =?UTF-8?q?=20rules=20(#862)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Plain ComputableInPolyTime rules for stack and bidirectional tapes, finite configurations (observations, fixed actions, initialization), list tail and emptiness, and the breadth-first search of Reachability (insertNew, expand, viewSucc), proved without the tidy calculus. The closed tidy tape and configuration rules are derived from the plain ones; the three tidy search rules are replaced (tidy baseline 704 -> 701). Co-Authored-By: Claude Opus 5.5 --- .../Complexity/LogSpace/Reachability.lean | 79 ++++---- .../Complexity/PolyTime/Configuration.lean | 173 +++++++++++++++--- .../MultiTape/Complexity/PolyTime/Tape.lean | 170 ++++++++++++++--- .../Turing/MultiTape/Complexity/Space.lean | 3 +- .../Internal/PolyTimeListPrimitives.lean | 16 ++ scripts/tidy_surface_baseline.json | 1 - 6 files changed, 342 insertions(+), 100 deletions(-) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean index 94e33e71ef..9ae13429e1 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean @@ -42,8 +42,8 @@ configuration graph, which has polynomially many vertices [Sipser, Section 8.4][ * `Turing.MultiTapeNTM.reflTransGen_viewSucc_iff`: the successor lists give the reachable views. * `Turing.MultiTapeNTM.searchAccepts_iff`: enough rounds decide acceptance. -* `Turing.MultiTapeNTM.computableTidilyInPolyTime_viewSucc`: the successors in polynomial time. -* `Turing.MultiTapeTM.ComputableTidilyInPolyTime.expand`: a round in polynomial time. +* `Turing.MultiTapeNTM.computableInPolyTime_viewSucc`: the successors in polynomial time. +* `Turing.MultiTapeTM.ComputableInPolyTime.expand`: a round in polynomial time. * `Turing.MultiTapeNTM.exists_computableInPolyTime_searchAccepts`: under a logarithmic space bound, enough rounds of breadth-first search run in polynomial time. @@ -133,12 +133,12 @@ end Turing.MultiTapeNTM /-! ### Breadth-first search in polynomial time -/ -namespace Turing.MultiTapeTM.ComputableTidilyInPolyTime +namespace Turing.MultiTapeTM.ComputableInPolyTime variable {α : Type} [DecidableEq α] {enc : α ↪ List Bool} /-- Appending an element unless it is already in the list is polynomial-time. -/ -theorem insertNew : ComputableTidilyInPolyTime +theorem insertNew : ComputableInPolyTime (fun p : List α × α => Cslib.Reachability.insertNew p.1 p.2) (encPair (encList enc) enc) (encList enc) := by have hmem (l : List α) (a : α) : decide (a ∈ l) = l.any fun b => decide (b = a) := by @@ -153,12 +153,12 @@ theorem insertNew : ComputableTidilyInPolyTime /-- **A round of breadth-first search is polynomial-time** when the successors are: the found elements and their successors are at most polynomially many and long. -/ -theorem expand {succ : α → List α} (hsucc : ComputableTidilyInPolyTime succ enc (encList enc)) : - ComputableTidilyInPolyTime (Cslib.Reachability.expand succ) (encList enc) (encList enc) := by - have hlist : ComputableTidilyInPolyTime (fun found : List α => found.flatMap succ) +theorem expand {succ : α → List α} (hsucc : ComputableInPolyTime succ enc (encList enc)) : + ComputableInPolyTime (Cslib.Reachability.expand succ) (encList enc) (encList enc) := by + have hlist : ComputableInPolyTime (fun found : List α => found.flatMap succ) (encList enc) (encList enc) := flatMapWithInput id' (hsucc.comp (snd _ _)) - have hstep : ComputableTidilyInPolyTime + have hstep : ComputableInPolyTime (fun p : (List α × List α) × α => Cslib.Reachability.insertNew p.1.2 p.2) (encPair (encPair (encList enc) (encList enc)) enc) (encList enc) := insertNew.comp (((snd _ _).comp (fst _ _)).prod (snd _ _)) @@ -176,7 +176,7 @@ theorem expand {succ : α → List α} (hsucc : ComputableTidilyInPolyTime succ length_frame] omega -end Turing.MultiTapeTM.ComputableTidilyInPolyTime +end Turing.MultiTapeTM.ComputableInPolyTime namespace Turing.MultiTapeNTM @@ -185,8 +185,8 @@ open MultiTapeTM variable {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} /-- **The successors of a view are polynomial-time.** -/ -theorem computableTidilyInPolyTime_viewSucc : - ComputableTidilyInPolyTime ntm.viewSucc encFiniteCfg (encList encFiniteCfg) := by +theorem computableInPolyTime_viewSucc : + ComputableInPolyTime ntm.viewSucc encFiniteCfg (encList encFiniteCfg) := by classical let key (finite : FiniteCfg k Bool State) : Option State × Option Bool × (Fin k → Option Bool) := (finite.state, finite.inputSymbol, finite.workTapeSymbols) @@ -200,16 +200,16 @@ theorem computableTidilyInPolyTime_viewSucc : funext finite rfl rw [heq] - refine ComputableTidilyInPolyTime.finite_cases + refine ComputableInPolyTime.finite_cases (tagEncoding := encPair (encFinite _) (encPair (encFinEnum _) (encFinEnum _))) ?_ fun tag => ?_ - · exact ComputableTidilyInPolyTime.finiteCfg_state.prod - (ComputableTidilyInPolyTime.finiteCfg_inputSymbol.prod - ComputableTidilyInPolyTime.finiteCfg_workTapeSymbols) + · exact ComputableInPolyTime.finiteCfg_state.prod + (ComputableInPolyTime.finiteCfg_inputSymbol.prod + ComputableInPolyTime.finiteCfg_workTapeSymbols) · rcases tag with ⟨_ | state, symbol, work⟩ - · exact ComputableTidilyInPolyTime.const [] - · exact ComputableTidilyInPolyTime.mapConst _ fun action _ => - ComputableInPolyTime.finiteCfg_summarizeOutput.tidy.comp - (ComputableTidilyInPolyTime.finiteCfg_step action) + · exact ComputableInPolyTime.const [] + · exact ComputableInPolyTime.mapConst _ fun action _ => + ComputableInPolyTime.finiteCfg_summarizeOutput.comp + (ComputableInPolyTime.finiteCfg_step action) /-- Under a logarithmic space bound, the number of rounds that decides acceptance is at most a polynomial in the input length. -/ @@ -244,20 +244,19 @@ theorem exists_computableInPolyTime_searchAccepts {α : Type} {enc : α ↪ List ComputableInPolyTime (fun a => ntm.searchAccepts (rounds a) (enc a)) enc encBool := by set D := 2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1) set rounds : α → ℕ := fun a => 2 * 2 ^ D * ((enc a).length + 1) ^ D - refine ⟨rounds, fun a => rounds_le k State c _, - ComputableTidilyInPolyTime.computableInPolyTime ?_⟩ + refine ⟨rounds, fun a => rounds_le k State c _, ?_⟩ -- the number of rounds in unary - have hcount : ComputableTidilyInPolyTime rounds enc encUnary := - ComputableTidilyInPolyTime.unary_mul.comp ((ComputableTidilyInPolyTime.const _).prod - ((ComputableTidilyInPolyTime.unary_pow D).comp (ComputableTidilyInPolyTime.unary_add.comp - ((ComputableTidilyInPolyTime.encoding_length enc).prod - (ComputableTidilyInPolyTime.const 1))))) - have hinit : ComputableTidilyInPolyTime (fun a => [ntm.initView (enc a)]) enc + have hcount : ComputableInPolyTime rounds enc encUnary := + ComputableInPolyTime.unary_mul.comp ((ComputableInPolyTime.const _).prod + ((ComputableInPolyTime.unary_pow D).comp (ComputableInPolyTime.unary_add.comp + ((ComputableInPolyTime.encoding_length enc).prod + (ComputableInPolyTime.const 1))))) + have hinit : ComputableInPolyTime (fun a => [ntm.initView (enc a)]) enc (encList encFiniteCfg) := - ComputableTidilyInPolyTime.cons' (ComputableTidilyInPolyTime.finiteCfg_init - (ComputableTidilyInPolyTime.of_eq (encIn := enc) (encMid := encBits) (f := fun a => enc a) + ComputableInPolyTime.cons' (ComputableInPolyTime.finiteCfg_init + (ComputableInPolyTime.of_eq (encIn := enc) (encOut := encBits) (f := fun a => enc a) fun _ => rfl) ntm.q₀) - (ComputableTidilyInPolyTime.const []) + (ComputableInPolyTime.const []) -- the found views are polynomially many, each of linear length set bound : α → ℕ := fun a => rounds a * (2 * viewLengthBound k State (enc a).length (c * (Nat.log2 (enc a).length + 1)) + 1) @@ -282,17 +281,17 @@ theorem exists_computableInPolyTime_searchAccepts {α : Type} {enc : α ↪ List refine (length_encList_le encFiniteCfg _ fun finite hf => length_encFiniteCfg_le (hs a) (hreach finite hf)).trans ?_ exact Nat.mul_le_mul_right _ hlen - have hsearch := ComputableTidilyInPolyTime.iterate hcount hinit - (ComputableTidilyInPolyTime.expand computableTidilyInPolyTime_viewSucc) hbound hstates - have htest : ComputableTidilyInPolyTime + have hsearch := ComputableInPolyTime.iterate hcount hinit + (ComputableInPolyTime.expand computableInPolyTime_viewSucc) hbound hstates + have htest : ComputableInPolyTime (fun finite : FiniteCfg k Bool State => decide (finite.state = none) && decide (finite.output = [true])) encFiniteCfg encBool := - ComputableTidilyInPolyTime.bool_and.comp - (((ComputableTidilyInPolyTime.of_finite fun state : Option State => - decide (state = none)).comp ComputableTidilyInPolyTime.finiteCfg_state).prod - (ComputableTidilyInPolyTime.decide_eq' ComputableTidilyInPolyTime.finiteCfg_output - (ComputableTidilyInPolyTime.const [true]))) - exact ComputableTidilyInPolyTime.anyWithInput hsearch - (htest.comp (ComputableTidilyInPolyTime.snd _ _)) + ComputableInPolyTime.bool_and.comp + (((ComputableInPolyTime.of_finite fun state : Option State => + decide (state = none)).comp ComputableInPolyTime.finiteCfg_state).prod + (ComputableInPolyTime.decide_eq' ComputableInPolyTime.finiteCfg_output + (ComputableInPolyTime.const [true]))) + exact ComputableInPolyTime.anyWithInput hsearch + (htest.comp (ComputableInPolyTime.snd _ _)) end Turing.MultiTapeNTM diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Configuration.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Configuration.lean index 78a99271bf..74fd9275ff 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Configuration.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Configuration.lean @@ -12,21 +12,26 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Poly public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Tape import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain /-! # Polynomial-time finite configuration operations -Ordinary structure construction, observations, fixed native actions and reply installation are -certified through the tidy functional calculus. Copying the input, work tapes, accumulated output -and every channel is charged by their encodings. These rules implement the interpreter; clients -of its eventual oracle-substitution theorem need no configuration bookkeeping. +Ordinary structure construction, observations, fixed native actions and initialization are +certified in plain polynomial time (`Turing.MultiTapeTM.ComputableInPolyTime`), by composition of +pair, list, table and tape rules. The tidy forms of the closed rules are derived from the plain +ones; channel operations for oracle configurations remain in the tidy calculus. Copying the +input, work tapes, accumulated output and every channel is charged by their encodings. ## Main results -* `Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteCfg_step`: execute a fixed native action. +* `Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_state`, `.finiteCfg_inputSymbol`, + `.finiteCfg_workTapeSymbols`, `.finiteCfg_output`: plain observations. +* `Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_step`: execute a fixed native action. +* `Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_init`: initialize finite storage. * `Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteConfig_step`, `.finiteConfig_receive`: local transitions and channel reset with a computed reply. -* `Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteConfig_init`: initialize finite storage. +* `Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteConfig_init`: initialize oracle storage. ## References @@ -36,7 +41,7 @@ Adapts Computability/Probabilistic/Configuration.lean on the cslib `crypto` bran @[expose] public section -namespace Turing.MultiTapeTM.ComputableTidilyInPolyTime +namespace Turing.MultiTapeTM.ComputableInPolyTime open Cslib.Turing MultiTapeMachine @@ -46,17 +51,17 @@ variable {k : ℕ} {State α : Type} [Finite State] {input : α ↪ List Bool} @[fun_prop] theorem finiteCfg_mk {word : α → List Bool} {state : α → Option State} {position : ∀ a, Fin ((word a).length + 2)} {work : α → Fin k → BiTape Bool} - {output : α → List Bool} (hword : ComputableTidilyInPolyTime word input encBits) - (hstate : ComputableTidilyInPolyTime state input (encFinite (Option State))) - (hposition : ComputableTidilyInPolyTime (fun a => (position a).val) input encUnary) - (hwork : ComputableTidilyInPolyTime work input (encPi (encBiTape encBool))) - (houtput : ComputableTidilyInPolyTime output input encBits) : - ComputableTidilyInPolyTime (fun a => + {output : α → List Bool} (hword : ComputableInPolyTime word input encBits) + (hstate : ComputableInPolyTime state input (encFinite (Option State))) + (hposition : ComputableInPolyTime (fun a => (position a).val) input encUnary) + (hwork : ComputableInPolyTime work input (encPi (encBiTape encBool))) + (houtput : ComputableInPolyTime output input encBits) : + ComputableInPolyTime (fun a => (⟨word a, state a, position a, work a, output a⟩ : FiniteCfg k Bool State)) input encFiniteCfg := (hword.prod (hstate.prod (hposition.prod (hwork.prod houtput)))).of_enc_eq (fun _ => rfl) -private theorem finiteCfg_parts : ComputableTidilyInPolyTime +private theorem finiteCfg_parts : ComputableInPolyTime (fun cfg : FiniteCfg k Bool State => (cfg.input, cfg.state, cfg.inputPos.val, cfg.workTapes, cfg.output)) encFiniteCfg (encPair encBits (encPair (encFinite (Option State)) @@ -64,39 +69,39 @@ private theorem finiteCfg_parts : ComputableTidilyInPolyTime /-- Read the stored input word. -/ @[fun_prop] -theorem finiteCfg_input : ComputableTidilyInPolyTime (FiniteCfg.input (k := k) (State := State)) +theorem finiteCfg_input : ComputableInPolyTime (FiniteCfg.input (k := k) (State := State)) encFiniteCfg encBits := finiteCfg_parts.fst' /-- Read the finite control. -/ @[fun_prop] -theorem finiteCfg_state : ComputableTidilyInPolyTime (FiniteCfg.state (k := k) (State := State)) +theorem finiteCfg_state : ComputableInPolyTime (FiniteCfg.state (k := k) (State := State)) encFiniteCfg (encFinite (Option State)) := finiteCfg_parts.snd'.fst' /-- Read the input head's unary position. -/ @[fun_prop] -theorem finiteCfg_inputPos : ComputableTidilyInPolyTime +theorem finiteCfg_inputPos : ComputableInPolyTime (fun cfg : FiniteCfg k Bool State => cfg.inputPos.val) encFiniteCfg encUnary := finiteCfg_parts.snd'.snd'.fst' /-- Read the complete family of work tapes. -/ @[fun_prop] -theorem finiteCfg_workTapes : ComputableTidilyInPolyTime +theorem finiteCfg_workTapes : ComputableInPolyTime (FiniteCfg.workTapes (k := k) (State := State)) encFiniteCfg (encPi (encBiTape encBool)) := finiteCfg_parts.snd'.snd'.snd'.fst' /-- Read all accumulated output. -/ @[fun_prop] -theorem finiteCfg_output : ComputableTidilyInPolyTime (FiniteCfg.output (k := k) (State := State)) +theorem finiteCfg_output : ComputableInPolyTime (FiniteCfg.output (k := k) (State := State)) encFiniteCfg encBits := finiteCfg_parts.snd'.snd'.snd'.snd' /-- Observe the read-only input, including both blank boundary cells. -/ @[fun_prop] -theorem finiteCfg_inputSymbol : ComputableTidilyInPolyTime +theorem finiteCfg_inputSymbol : ComputableInPolyTime (FiniteCfg.inputSymbol (k := k) (State := State)) encFiniteCfg (encFinEnum (Option Bool)) := by - have hlist : ComputableTidilyInPolyTime + have hlist : ComputableInPolyTime (fun cfg : FiniteCfg k Bool State => none :: cfg.input.map some) encFiniteCfg (encList (encFinEnum (Option Bool))) := by - have hsome : ComputableTidilyInPolyTime (some (α := Bool)) + have hsome : ComputableInPolyTime (some (α := Bool)) encBool (encFinEnum (Option Bool)) := of_finite _ exact (const none).cons' ((map hsome).comp (bitsToList.comp finiteCfg_input)) simpa only [Function.comp_def, List.getD_eq_getElem?_getD, @@ -105,14 +110,127 @@ theorem finiteCfg_inputSymbol : ComputableTidilyInPolyTime /-- Observe all work heads as a single fixed finite value. -/ @[fun_prop] -theorem finiteCfg_workTapeSymbols : ComputableTidilyInPolyTime +theorem finiteCfg_workTapeSymbols : ComputableInPolyTime (FiniteCfg.workTapeSymbols (k := k) (State := State)) encFiniteCfg (encFinEnum (Fin k → Option Bool)) := by - have hheads : ComputableTidilyInPolyTime + have hheads : ComputableInPolyTime (fun cfg : FiniteCfg k Bool State => fun tape => (cfg.workTapes tape).head) - encFiniteCfg (encPi (encOption encBool)) := by fun_prop + encFiniteCfg (encPi (encOption encBool)) := + pi fun tape => (biTape_head encBool).comp ((pi_apply _ tape).comp finiteCfg_workTapes) exact (of_finite id).comp hheads +/-- Clamped native input-head movement is efficient on the stored unary position. -/ +@[fun_prop] +theorem moveInputPos {word : α → List Bool} {position : ∀ a, Fin ((word a).length + 2)} + (hword : ComputableInPolyTime word input encBits) + (hposition : ComputableInPolyTime (fun a => (position a).val) input encUnary) + (move : SignType) : ComputableInPolyTime + (fun a => (Turing.moveInputPos (position a) move).val) input encUnary := by + cases move with + | neg => + apply (unary_sub.comp (hposition.prod (const 1))).of_enc_eq + intro a + apply congrArg encUnary + have h := val_moveInputPos_eq (position a) .neg + have hp := (position a).isLt + simp only [SignType.cast, Function.comp_def] at h ⊢ + lia + | zero => simpa using hposition + | pos => + -- `min x y = x - (x - y)` + have hnext := unary_add.comp (hposition.prod (const 1)) + have hlast := unary_add.comp ((length_bits.comp hword).prod (const 1)) + apply (unary_sub.comp (hnext.prod (unary_sub.comp (hnext.prod hlast)))).of_enc_eq + intro a + apply congrArg encUnary + have h := val_moveInputPos_eq (position a) .pos + simp only [SignType.cast, Function.comp_def] at h ⊢ + lia + +/-- Execute a fixed ordinary native action, including all retained storage. -/ +@[fun_prop] +theorem finiteCfg_step (action : Action k Bool State) : ComputableInPolyTime + (fun cfg : FiniteCfg k Bool State => cfg.step action) encFiniteCfg encFiniteCfg := by + refine finiteCfg_mk finiteCfg_input (const _) + (moveInputPos finiteCfg_input finiteCfg_inputPos action.inputTape) + (pi fun tape => biTape_step (action.workTapes tape) + ((pi_apply _ tape).comp finiteCfg_workTapes)) + (bitsAppend finiteCfg_output (const _)) + +/-- Initialize with the native input-head convention and blank work tapes. -/ +@[fun_prop] +theorem finiteCfg_init {word : α → List Bool} + (hword : ComputableInPolyTime word input encBits) (state : State) : + ComputableInPolyTime (fun a => FiniteCfg.init (k := k) state (word a)) + input encFiniteCfg := by + apply finiteCfg_mk hword (const _) + · simpa using (const (encIn := input) (encOut := encUnary) 1) + · exact const _ + · exact const _ + +end Turing.MultiTapeTM.ComputableInPolyTime + +namespace Turing.MultiTapeTM.ComputableTidilyInPolyTime + +open Cslib.Turing MultiTapeMachine + +variable {k : ℕ} {State α : Type} [Finite State] {input : α ↪ List Bool} + +/-- Assemble an ordinary configuration from its certified components. -/ +@[fun_prop] +theorem finiteCfg_mk {word : α → List Bool} {state : α → Option State} + {position : ∀ a, Fin ((word a).length + 2)} {work : α → Fin k → BiTape Bool} + {output : α → List Bool} (hword : ComputableTidilyInPolyTime word input encBits) + (hstate : ComputableTidilyInPolyTime state input (encFinite (Option State))) + (hposition : ComputableTidilyInPolyTime (fun a => (position a).val) input encUnary) + (hwork : ComputableTidilyInPolyTime work input (encPi (encBiTape encBool))) + (houtput : ComputableTidilyInPolyTime output input encBits) : + ComputableTidilyInPolyTime (fun a => + (⟨word a, state a, position a, work a, output a⟩ : FiniteCfg k Bool State)) + input encFiniteCfg := + (hword.prod (hstate.prod (hposition.prod (hwork.prod houtput)))).of_enc_eq (fun _ => rfl) + +/-- Read the stored input word. -/ +@[fun_prop] +theorem finiteCfg_input : ComputableTidilyInPolyTime (FiniteCfg.input (k := k) (State := State)) + encFiniteCfg encBits := ComputableInPolyTime.tidy ComputableInPolyTime.finiteCfg_input + +/-- Read the finite control. -/ +@[fun_prop] +theorem finiteCfg_state : ComputableTidilyInPolyTime (FiniteCfg.state (k := k) (State := State)) + encFiniteCfg (encFinite (Option State)) := + ComputableInPolyTime.tidy ComputableInPolyTime.finiteCfg_state + +/-- Read the input head's unary position. -/ +@[fun_prop] +theorem finiteCfg_inputPos : ComputableTidilyInPolyTime + (fun cfg : FiniteCfg k Bool State => cfg.inputPos.val) encFiniteCfg encUnary := + ComputableInPolyTime.tidy ComputableInPolyTime.finiteCfg_inputPos + +/-- Read the complete family of work tapes. -/ +@[fun_prop] +theorem finiteCfg_workTapes : ComputableTidilyInPolyTime + (FiniteCfg.workTapes (k := k) (State := State)) encFiniteCfg (encPi (encBiTape encBool)) := + ComputableInPolyTime.tidy ComputableInPolyTime.finiteCfg_workTapes + +/-- Read all accumulated output. -/ +@[fun_prop] +theorem finiteCfg_output : ComputableTidilyInPolyTime (FiniteCfg.output (k := k) (State := State)) + encFiniteCfg encBits := ComputableInPolyTime.tidy ComputableInPolyTime.finiteCfg_output + +/-- Observe the read-only input, including both blank boundary cells. -/ +@[fun_prop] +theorem finiteCfg_inputSymbol : ComputableTidilyInPolyTime + (FiniteCfg.inputSymbol (k := k) (State := State)) encFiniteCfg (encFinEnum (Option Bool)) := + ComputableInPolyTime.tidy ComputableInPolyTime.finiteCfg_inputSymbol + +/-- Observe all work heads as a single fixed finite value. -/ +@[fun_prop] +theorem finiteCfg_workTapeSymbols : ComputableTidilyInPolyTime + (FiniteCfg.workTapeSymbols (k := k) (State := State)) encFiniteCfg + (encFinEnum (Fin k → Option Bool)) := + ComputableInPolyTime.tidy ComputableInPolyTime.finiteCfg_workTapeSymbols + /-- Clamped native input-head movement is efficient on the stored unary position. -/ @[fun_prop] theorem moveInputPos {word : α → List Bool} {position : ∀ a, Fin ((word a).length + 2)} @@ -142,9 +260,8 @@ theorem moveInputPos {word : α → List Bool} {position : ∀ a, Fin ((word a). /-- Execute a fixed ordinary native action, including all retained storage. -/ @[fun_prop] theorem finiteCfg_step (action : Action k Bool State) : ComputableTidilyInPolyTime - (fun cfg : FiniteCfg k Bool State => cfg.step action) encFiniteCfg encFiniteCfg := by - unfold FiniteCfg.step - fun_prop + (fun cfg : FiniteCfg k Bool State => cfg.step action) encFiniteCfg encFiniteCfg := + ComputableInPolyTime.tidy (ComputableInPolyTime.finiteCfg_step action) /-- Initialize with the native input-head convention and blank work tapes. -/ @[fun_prop] diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Tape.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Tape.lean index 0cdd9a3eab..d45709c25f 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Tape.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Tape.lean @@ -9,20 +9,22 @@ module public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Tape public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain /-! # Polynomial-time operations on finite tape storage -The operations of cslib's existing tapes are certified by composition of list, option and pair -operations. They charge the complete stored tapes and accept any symbol encoding, including -infinite or empty alphabets. Finite-control interpreters can use these rules without building -new tape machines. +The operations of cslib's existing tapes are certified in plain polynomial time +(`Turing.MultiTapeTM.ComputableInPolyTime`) by composition of list, option and pair operations; +the tidy forms of the closed operations are derived from them. They charge the complete stored +tapes and accept any symbol encoding, including infinite or empty alphabets. Finite-control +interpreters can use these rules without building new tape machines. ## Main results -* `Turing.MultiTapeTM.ComputableTidilyInPolyTime.stackTape_cons`: prepend a computed cell, +* `Turing.MultiTapeTM.ComputableInPolyTime.stackTape_cons`: prepend a computed cell, retaining the stack's omission of trailing blanks. -* `Turing.MultiTapeTM.ComputableTidilyInPolyTime.biTape_moveLeft`, `.biTape_moveRight`, +* `Turing.MultiTapeTM.ComputableInPolyTime.biTape_moveLeft`, `.biTape_moveRight`, `.biTape_write`, `.biTape_step`: native tape operations with `fun_prop` certificates. * `Turing.MultiTapeTM.ComputableTidilyInPolyTime.biTape_mk₁`: load a computed list. @@ -35,7 +37,7 @@ instead of fixed finite tags. @[expose] public section -namespace Turing.MultiTapeTM.ComputableTidilyInPolyTime +namespace Turing.MultiTapeTM.ComputableInPolyTime open Cslib.Turing @@ -44,24 +46,140 @@ variable {Symbol α : Type} {input : α ↪ List Bool} {enc : Symbol ↪ List Bo /-- Reading the stored list is a change of view of the same encoded bits. -/ @[fun_prop] theorem stackTape_toList (enc : Symbol ↪ List Bool) : - ComputableTidilyInPolyTime StackTape.toList (encStackTape enc) (encList (encOption enc)) := + ComputableInPolyTime StackTape.toList (encStackTape enc) (encList (encOption enc)) := of_eq fun _ => rfl /-- Reading a stack head decodes the first cell, with a blank default. -/ @[fun_prop] theorem stackTape_head (enc : Symbol ↪ List Bool) : - ComputableTidilyInPolyTime StackTape.head (encStackTape enc) (encOption enc) := by + ComputableInPolyTime StackTape.head (encStackTape enc) (encOption enc) := by apply ((headD (encA := encOption enc) none).comp (stackTape_toList enc)).of_enc_eq intro tape cases tape with | mk values h => cases values <;> rfl -/-- Removing a stack head is the certified list-tail operation. -/ +/-- Removing a stack head is the list-tail operation. -/ @[fun_prop] theorem stackTape_tail (enc : Symbol ↪ List Bool) : - ComputableTidilyInPolyTime StackTape.tail (encStackTape enc) (encStackTape enc) := + ComputableInPolyTime StackTape.tail (encStackTape enc) (encStackTape enc) := ((tail (encA := encOption enc)).comp (stackTape_toList enc)).of_enc_eq (fun tape => by simp only [Function.comp_def, encStackTape_apply, StackTape.tail_toList]) +/-- Prepend a cell without requiring a default symbol or case analysis over the alphabet. -/ +@[fun_prop] +theorem stackTape_cons {symbol : α → Option Symbol} {tape : α → StackTape Symbol} + (hsymbol : ComputableInPolyTime symbol input (encOption enc)) + (htape : ComputableInPolyTime tape input (encStackTape enc)) : + ComputableInPolyTime (fun a => StackTape.cons (symbol a) (tape a)) input + (encStackTape enc) := by + have hcells := (stackTape_toList enc).comp htape + have hcond : ComputableInPolyTime (fun a => (symbol a).isSome || !(tape a).toList.isEmpty) + input encBool := + bool_or.comp ((optionIsSome hsymbol).prod + (bool_not.comp ((listIsEmpty (encA := encOption enc)).comp hcells))) + have hlist : ComputableInPolyTime + (fun a => if (symbol a).isSome || !(tape a).toList.isEmpty + then symbol a :: (tape a).toList else []) input (encList (encOption enc)) := + hcond.ite (cons' hsymbol hcells) (const []) + exact hlist.of_enc_eq (fun a => by rw [encStackTape_apply, StackTape.cons_toList]) + +/-- Map symbols to occupied cells with the list map. -/ +@[fun_prop] +theorem stackTape_mapSome (enc : Symbol ↪ List Bool) : + ComputableInPolyTime StackTape.mapSome (encList enc) (encStackTape enc) := + (map (optionSome enc)).of_enc_eq (fun _ => rfl) + +private theorem biTape_parts (enc : Symbol ↪ List Bool) : + ComputableInPolyTime (fun tape : BiTape Symbol => (tape.head, tape.left, tape.right)) + (encBiTape enc) (encPair (encOption enc) (encPair (encStackTape enc) (encStackTape enc))) := + of_eq fun _ => rfl + +/-- Assemble a tape from its computed head and two sides. -/ +@[fun_prop] +theorem biTape_mk {head : α → Option Symbol} {left right : α → StackTape Symbol} + (hhead : ComputableInPolyTime head input (encOption enc)) + (hleft : ComputableInPolyTime left input (encStackTape enc)) + (hright : ComputableInPolyTime right input (encStackTape enc)) : + ComputableInPolyTime (fun a => BiTape.mk (head a) (left a) (right a)) input + (encBiTape enc) := + (hhead.prod (hleft.prod hright)).of_enc_eq (fun _ => rfl) + +/-- Read the current cell of a computed tape. -/ +@[fun_prop] +theorem biTape_head (enc : Symbol ↪ List Bool) : + ComputableInPolyTime BiTape.head (encBiTape enc) (encOption enc) := + (biTape_parts enc).fst' + +/-- Extract the stored left side. -/ +@[fun_prop] +theorem biTape_left (enc : Symbol ↪ List Bool) : + ComputableInPolyTime BiTape.left (encBiTape enc) (encStackTape enc) := + (biTape_parts enc).snd'.fst' + +/-- Extract the stored right side. -/ +@[fun_prop] +theorem biTape_right (enc : Symbol ↪ List Bool) : + ComputableInPolyTime BiTape.right (encBiTape enc) (encStackTape enc) := + (biTape_parts enc).snd'.snd' + +/-- Move left by the stack operations. -/ +@[fun_prop] +theorem biTape_moveLeft (enc : Symbol ↪ List Bool) : + ComputableInPolyTime BiTape.moveLeft (encBiTape enc) (encBiTape enc) := by + unfold BiTape.moveLeft + fun_prop + +/-- Move right by the stack operations. -/ +@[fun_prop] +theorem biTape_moveRight (enc : Symbol ↪ List Bool) : + ComputableInPolyTime BiTape.moveRight (encBiTape enc) (encBiTape enc) := by + unfold BiTape.moveRight + fun_prop + +/-- Write a computed optional symbol, including blank erasure. -/ +@[fun_prop] +theorem biTape_write {tape : α → BiTape Symbol} {symbol : α → Option Symbol} + (htape : ComputableInPolyTime tape input (encBiTape enc)) + (hsymbol : ComputableInPolyTime symbol input (encOption enc)) : + ComputableInPolyTime (fun a => (tape a).write (symbol a)) input (encBiTape enc) := by + unfold BiTape.write + fun_prop + +/-- Execute a fixed native action, charging the full encoded tape. -/ +@[fun_prop] +theorem biTape_step (action : Option (Option Symbol) × SignType) + {tape : α → BiTape Symbol} + (htape : ComputableInPolyTime tape input (encBiTape enc)) : + ComputableInPolyTime (fun a => (tape a).step action) input (encBiTape enc) := by + rcases action with ⟨write, move⟩ + cases write <;> cases move <;> + simp only [BiTape.step, Option.elim_none, Option.elim_some] <;> fun_prop + +end Turing.MultiTapeTM.ComputableInPolyTime + +namespace Turing.MultiTapeTM.ComputableTidilyInPolyTime + +open Cslib.Turing + +variable {Symbol α : Type} {input : α ↪ List Bool} {enc : Symbol ↪ List Bool} + +/-- Reading the stored list is a change of view of the same encoded bits. -/ +@[fun_prop] +theorem stackTape_toList (enc : Symbol ↪ List Bool) : + ComputableTidilyInPolyTime StackTape.toList (encStackTape enc) (encList (encOption enc)) := + ComputableInPolyTime.tidy (ComputableInPolyTime.stackTape_toList enc) + +/-- Reading a stack head decodes the first cell, with a blank default. -/ +@[fun_prop] +theorem stackTape_head (enc : Symbol ↪ List Bool) : + ComputableTidilyInPolyTime StackTape.head (encStackTape enc) (encOption enc) := + ComputableInPolyTime.tidy (ComputableInPolyTime.stackTape_head enc) + +/-- Removing a stack head is the certified list-tail operation. -/ +@[fun_prop] +theorem stackTape_tail (enc : Symbol ↪ List Bool) : + ComputableTidilyInPolyTime StackTape.tail (encStackTape enc) (encStackTape enc) := + ComputableInPolyTime.tidy (ComputableInPolyTime.stackTape_tail enc) + /-- Prepend a cell without requiring a default symbol or case analysis over the alphabet. -/ @[fun_prop] theorem stackTape_cons {symbol : α → Option Symbol} {tape : α → StackTape Symbol} @@ -78,12 +196,7 @@ theorem stackTape_cons {symbol : α → Option Symbol} {tape : α → StackTape @[fun_prop] theorem stackTape_mapSome (enc : Symbol ↪ List Bool) : ComputableTidilyInPolyTime StackTape.mapSome (encList enc) (encStackTape enc) := - (map (optionSome enc)).of_enc_eq (fun _ => rfl) - -private theorem biTape_parts (enc : Symbol ↪ List Bool) : - ComputableTidilyInPolyTime (fun tape : BiTape Symbol => (tape.head, tape.left, tape.right)) - (encBiTape enc) (encPair (encOption enc) (encPair (encStackTape enc) (encStackTape enc))) := - of_eq fun _ => rfl + ComputableInPolyTime.tidy (ComputableInPolyTime.stackTape_mapSome enc) /-- Assemble a tape from its computed head and two sides. -/ @[fun_prop] @@ -99,33 +212,31 @@ theorem biTape_mk {head : α → Option Symbol} {left right : α → StackTape S @[fun_prop] theorem biTape_head (enc : Symbol ↪ List Bool) : ComputableTidilyInPolyTime BiTape.head (encBiTape enc) (encOption enc) := - (biTape_parts enc).fst' + ComputableInPolyTime.tidy (ComputableInPolyTime.biTape_head enc) /-- Extract the stored left side. -/ @[fun_prop] theorem biTape_left (enc : Symbol ↪ List Bool) : ComputableTidilyInPolyTime BiTape.left (encBiTape enc) (encStackTape enc) := - (biTape_parts enc).snd'.fst' + ComputableInPolyTime.tidy (ComputableInPolyTime.biTape_left enc) /-- Extract the stored right side. -/ @[fun_prop] theorem biTape_right (enc : Symbol ↪ List Bool) : ComputableTidilyInPolyTime BiTape.right (encBiTape enc) (encStackTape enc) := - (biTape_parts enc).snd'.snd' + ComputableInPolyTime.tidy (ComputableInPolyTime.biTape_right enc) /-- Move left by the existing stack operations. -/ @[fun_prop] theorem biTape_moveLeft (enc : Symbol ↪ List Bool) : - ComputableTidilyInPolyTime BiTape.moveLeft (encBiTape enc) (encBiTape enc) := by - unfold BiTape.moveLeft - fun_prop + ComputableTidilyInPolyTime BiTape.moveLeft (encBiTape enc) (encBiTape enc) := + ComputableInPolyTime.tidy (ComputableInPolyTime.biTape_moveLeft enc) /-- Move right by the existing stack operations. -/ @[fun_prop] theorem biTape_moveRight (enc : Symbol ↪ List Bool) : - ComputableTidilyInPolyTime BiTape.moveRight (encBiTape enc) (encBiTape enc) := by - unfold BiTape.moveRight - fun_prop + ComputableTidilyInPolyTime BiTape.moveRight (encBiTape enc) (encBiTape enc) := + ComputableInPolyTime.tidy (ComputableInPolyTime.biTape_moveRight enc) /-- Write a computed optional symbol, including blank erasure. -/ @[fun_prop] @@ -141,10 +252,9 @@ theorem biTape_write {tape : α → BiTape Symbol} {symbol : α → Option Symbo theorem biTape_step (action : Option (Option Symbol) × SignType) {tape : α → BiTape Symbol} (htape : ComputableTidilyInPolyTime tape input (encBiTape enc)) : - ComputableTidilyInPolyTime (fun a => (tape a).step action) input (encBiTape enc) := by - rcases action with ⟨write, move⟩ - cases write <;> cases move <;> - simp only [BiTape.step, Option.elim_none, Option.elim_some] <;> fun_prop + ComputableTidilyInPolyTime (fun a => (tape a).step action) input (encBiTape enc) := + (ComputableInPolyTime.tidy + (ComputableInPolyTime.biTape_step (enc := enc) action ComputableInPolyTime.id')).comp htape /-- Loading a list constructs a head and two stacks with no default symbol. -/ @[fun_prop] diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space.lean index e18b157ae8..acd8e191dc 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space.lean @@ -108,7 +108,8 @@ theorem outputClass : theorem finiteCfg_summarizeOutput {k : ℕ} {State : Type} [Finite State] : ComputableInPolyTime (FiniteCfg.summarizeOutput (k := k) (State := State)) encFiniteCfg encFiniteCfg := - ComputableTidilyInPolyTime.finiteCfg_summarizeOutput.computableInPolyTime + finiteCfg_mk finiteCfg_input finiteCfg_state finiteCfg_inputPos finiteCfg_workTapes + (outputClass.comp finiteCfg_output) end MultiTapeTM.ComputableInPolyTime diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeListPrimitives.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeListPrimitives.lean index 1d7ca6914a..9249e237a3 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeListPrimitives.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeListPrimitives.lean @@ -209,6 +209,22 @@ theorem bitsIsEmpty : ComputableInPolyTime List.isEmpty encBits encBool := by exact ⟨fun n => c * (n + 1), fun n => c * (n + 1), by fun_prop, by fun_prop, k, Q, hfinite, tm, fun word => htm word⟩ +/-- Drop the head of a list in any list encoding, reusing the encoding's linear-time machine. -/ +@[fun_prop] +theorem tail {α : Type} {encA : α ↪ List Bool} {encL : List α ↪ List Bool} + [ListEncoding encA encL] : ComputableInPolyTime (List.tail (α := α)) encL encL := by + obtain ⟨c, k, Q, hfinite, tm, htm⟩ := ListEncoding.tail (enc₁ := encA) (enc := encL) + exact ⟨fun n => c * (n + 1), fun n => c * (n + 1), by fun_prop, by fun_prop, + k, Q, hfinite, tm, fun word => htm word⟩ + +/-- Test a list in any list encoding for emptiness, reusing the encoding's linear-time machine. -/ +@[fun_prop] +theorem listIsEmpty {α : Type} {encA : α ↪ List Bool} {encL : List α ↪ List Bool} + [ListEncoding encA encL] : ComputableInPolyTime (List.isEmpty (α := α)) encL encBool := by + obtain ⟨c, k, Q, hfinite, tm, htm⟩ := ListEncoding.isEmpty (enc₁ := encA) (enc := encL) + exact ⟨fun n => c * (n + 1), fun n => c * (n + 1), by fun_prop, by fun_prop, + k, Q, hfinite, tm, fun word => htm word⟩ + private theorem rangeStepCertificate : ComputableInPolyTime (fun p : RangeState × Bool => rangeStep p.1 p.2) (encPair rangeEncoding encBool) rangeEncoding := by diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json index 06f1c636d8..7a800c4596 100644 --- a/scripts/tidy_surface_baseline.json +++ b/scripts/tidy_surface_baseline.json @@ -21,7 +21,6 @@ "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Compiler.lean": 1, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Routines.lean": 1, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/QueryMachine.lean": 9, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean": 3, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace.lean": 12, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace/Plain.lean": 4, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean": 19, From b7c78359e7a38fa25aa0108473ef3ec1eaeb7cbd Mon Sep 17 00:00:00 2001 From: Codex integration coordinator Date: Fri, 30 Oct 2026 11:36:57 -0400 Subject: [PATCH 2/2] style(Machines): use canonical tidy-baseline serialization Use the repository baseline_text formatter after the metadata-only union. Parsed entries remain identical at 690. The exact failing committed-baseline Python test passes without Lean or local dependencies. --- scripts/tidy_surface_baseline.json | 150 ++++++++++++++--------------- 1 file changed, 75 insertions(+), 75 deletions(-) diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json index 37773c4cf9..0ccd7185cf 100644 --- a/scripts/tidy_surface_baseline.json +++ b/scripts/tidy_surface_baseline.json @@ -1,77 +1,77 @@ { - "Complexity/Computability/Machines/ReadMachine/Tidy.lean": 2, - "Complexity/Computability/Machines/Turing/MultiTape/Combinators/Encoding.lean": 8, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Arith.lean": 2, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO.lean": 32, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Plain.lean": 2, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Degree.lean": 24, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Fold.lean": 2, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean": 19, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Bit.lean": 1, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean": 4, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean": 45, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Lists.lean": 14, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace.lean": 2, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram.lean": 11, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting/Callbacks.lean": 4, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting/Routines.lean": 34, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine.lean": 5, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Compiler.lean": 1, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Routines.lean": 1, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/QueryMachine.lean": 7, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace.lean": 12, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace/Plain.lean": 4, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean": 19, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Basic.lean": 27, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/BitString.lean": 31, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Configuration.lean": 18, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Finite.lean": 1, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Fold.lean": 7, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Int.lean": 13, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Int/Binary.lean": 24, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Iteration.lean": 7, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean": 66, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Membership.lean": 2, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat.lean": 17, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Binary.lean": 17, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/BinaryDiv.lean": 5, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Div.lean": 4, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Log.lean": 5, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Option.lean": 5, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Pi.lean": 6, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Plain.lean": 7, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Tape.lean": 14, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Primitives.lean": 9, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean": 15, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Streaming.lean": 14, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Translate.lean": 2, - "Complexity/Computability/Machines/Turing/MultiTape/Encodings/Basic.lean": 7, - "Complexity/Computability/Machines/Turing/MultiTape/Encodings/MultiPass.lean": 1, - "Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatPower.lean": 1, - "Complexity/Computability/Machines/Turing/MultiTape/Encodings/StreamFold.lean": 4, - "Complexity/Computability/Machines/Turing/MultiTape/Halting/Computable.lean": 5, - "Complexity/Computability/Machines/Turing/MultiTape/Halting/Rice.lean": 2, - "Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/QueryTake.lean": 2, - "Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean": 6, - "Complexity/Computability/Machines/Turing/MultiTape/Universal/Compose.lean": 7, - "Complexity/Computability/Machines/Turing/MultiTape/Universal/Decode.lean": 1, - "Complexity/Computability/Machines/Turing/MultiTape/Universal/InPlace.lean": 9, - "Complexity/Computability/Machines/Turing/MultiTape/Universal/Machine.lean": 2, - "Complexity/Computability/Machines/Turing/MultiTape/Universal/PolyTime.lean": 5, - "Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean": 2, - "Complexity/Computability/Probabilistic/Adaptive.lean": 5, - "Complexity/Computability/Probabilistic/CoinTape.lean": 5, - "Complexity/Computability/Probabilistic/Oracle.lean": 1, - "Complexity/Computability/Probabilistic/Oracle/Composition.lean": 12, - "Complexity/Computability/Probabilistic/Oracle/Iteration.lean": 3, - "Complexity/Computability/Probabilistic/Oracle/Normalization.lean": 4, - "Complexity/Computability/Probabilistic/Oracle/Parameter.lean": 2, - "Complexity/Computability/Probabilistic/Oracle/Substitution.lean": 2, - "Complexity/Computability/Probabilistic/Oracle/Tidy.lean": 18, - "Complexity/Computability/Probabilistic/OracleSimulation.lean": 1, - "Complexity/Computability/Probabilistic/PPT.lean": 1, - "Complexity/Computability/Probabilistic/PPT/Capture.lean": 4, - "Complexity/Computability/Probabilistic/Parameter.lean": 2, - "Complexity/Computability/Probabilistic/Presample.lean": 2, - "Complexity/Tactic/PolyTime.lean": 3 + "Complexity/Computability/Machines/ReadMachine/Tidy.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Combinators/Encoding.lean": 8, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Arith.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO.lean": 32, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Plain.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Degree.lean": 24, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Fold.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean": 19, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Bit.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean": 4, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean": 45, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Lists.lean": 14, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram.lean": 11, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting/Callbacks.lean": 4, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting/Routines.lean": 34, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine.lean": 5, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Compiler.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Routines.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/QueryMachine.lean": 7, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace.lean": 12, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace/Plain.lean": 4, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean": 19, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Basic.lean": 27, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/BitString.lean": 31, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Configuration.lean": 18, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Finite.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Fold.lean": 7, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Int.lean": 13, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Int/Binary.lean": 24, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Iteration.lean": 7, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean": 66, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Membership.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat.lean": 17, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Binary.lean": 17, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/BinaryDiv.lean": 5, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Div.lean": 4, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Log.lean": 5, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Option.lean": 5, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Pi.lean": 6, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Plain.lean": 7, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Tape.lean": 14, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Primitives.lean": 9, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean": 15, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Streaming.lean": 14, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Translate.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Encodings/Basic.lean": 7, + "Complexity/Computability/Machines/Turing/MultiTape/Encodings/MultiPass.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatPower.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Encodings/StreamFold.lean": 4, + "Complexity/Computability/Machines/Turing/MultiTape/Halting/Computable.lean": 5, + "Complexity/Computability/Machines/Turing/MultiTape/Halting/Rice.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/QueryTake.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean": 6, + "Complexity/Computability/Machines/Turing/MultiTape/Universal/Compose.lean": 7, + "Complexity/Computability/Machines/Turing/MultiTape/Universal/Decode.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Universal/InPlace.lean": 9, + "Complexity/Computability/Machines/Turing/MultiTape/Universal/Machine.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Universal/PolyTime.lean": 5, + "Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean": 2, + "Complexity/Computability/Probabilistic/Adaptive.lean": 5, + "Complexity/Computability/Probabilistic/CoinTape.lean": 5, + "Complexity/Computability/Probabilistic/Oracle.lean": 1, + "Complexity/Computability/Probabilistic/Oracle/Composition.lean": 12, + "Complexity/Computability/Probabilistic/Oracle/Iteration.lean": 3, + "Complexity/Computability/Probabilistic/Oracle/Normalization.lean": 4, + "Complexity/Computability/Probabilistic/Oracle/Parameter.lean": 2, + "Complexity/Computability/Probabilistic/Oracle/Substitution.lean": 2, + "Complexity/Computability/Probabilistic/Oracle/Tidy.lean": 18, + "Complexity/Computability/Probabilistic/OracleSimulation.lean": 1, + "Complexity/Computability/Probabilistic/PPT.lean": 1, + "Complexity/Computability/Probabilistic/PPT/Capture.lean": 4, + "Complexity/Computability/Probabilistic/Parameter.lean": 2, + "Complexity/Computability/Probabilistic/Presample.lean": 2, + "Complexity/Tactic/PolyTime.lean": 3 }