Exact trial-boundary trace decomposition

This internal module identifies consecutive repeatBoundaryCfg values with one complete trial stride. It also decomposes a stride into its T simulation choices, T + 1 rewind choices, and final finish choice. Named index-alignment lemmas keep all dependent casts out of the outer correctness induction.

Main results

• NTM.repeatBoundaryCfg_succ — consecutive boundaries differ by one stride
• NTM.repeatStrideChoices_trace_split — split a stride into simulation and admin
• NTM.repeatAdminChoices_trace_split — split admin into rewind and finish
• NTM.repeatStrideChoices_trace_split_three — complete three-phase split

Consecutive boundary slices

theorem Complexity.NTM.repeatPrefixChoices_succ_prefix {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) (m : ℕ) (hm : m < k) (i : Fin (repeatAtTimeSteps m T)) : repeatPrefixChoices choices (m + 1) ⋯ (Fin.cast ⋯ (Fin.castLE ⋯ i)) = repeatPrefixChoices choices m ⋯ i

Restricting the successor-boundary choices to the old prefix recovers the old boundary choices exactly.

theorem Complexity.NTM.repeatPrefixChoices_succ_suffix {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) (m : ℕ) (hm : m < k) (s : Fin (repeatAtTimeStride T)) : repeatPrefixChoices choices (m + 1) ⋯ (Fin.cast ⋯ (Fin.natAdd (repeatAtTimeSteps m T) s)) = repeatStrideChoices choices ⟨m, hm⟩ s

The suffix between boundaries m and m+1 is exactly trial m's stride slice of the full choice string.

theorem Complexity.NTM.repeatBoundaryCfg_succ {n k T : ℕ} (tm : NTM n) (x : List Bool) (choices : Fin (repeatAtTimeSteps k T) → Bool) (m : ℕ) (hm : m < k) : tm.repeatBoundaryCfg x choices (m + 1) ⋯ = (tm.repeatAtTime k T).trace (repeatAtTimeStride T) (repeatStrideChoices choices ⟨m, hm⟩) (tm.repeatBoundaryCfg x choices m ⋯)

Advancing one trial boundary is exactly tracing one complete stride from the preceding boundary configuration.

Three-phase stride split

def Complexity.NTM.repeatRewindChoices {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) (j : Fin k) : Fin (T + 1) → Bool

Rewind choices are the first T + 1 administrative choices.

Equations

• Complexity.NTM.repeatRewindChoices choices j a = Complexity.NTM.repeatAdminChoices choices j ⟨↑a, ⋯⟩

def Complexity.NTM.repeatFinishChoice {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) (j : Fin k) : Bool

The final administrative choice drives the finish transition.

Equations

• Complexity.NTM.repeatFinishChoice choices j = Complexity.NTM.repeatAdminChoices choices j ⟨T + 1, ⋯⟩

@[simp]

theorem Complexity.NTM.repeatRewindChoices_apply {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) (j : Fin k) (a : Fin (T + 1)) : repeatRewindChoices choices j a = repeatAdminChoices choices j ⟨↑a, ⋯⟩

Prefix form of the rewind slice.

@[simp]

theorem Complexity.NTM.repeatFinishChoice_eq {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) (j : Fin k) : repeatFinishChoice choices j = repeatAdminChoices choices j ⟨T + 1, ⋯⟩

The finish choice is the last entry of the administrative slice.

theorem Complexity.NTM.repeatStrideChoices_split_simulation {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) (j : Fin k) (t : Fin T) : repeatStrideChoices choices j (Fin.cast ⋯ (Fin.castLE ⋯ t)) = repeatSimulationChoices choices j t

The simulation prefix obtained by splitting a stride is exactly repeatSimulationChoices.

theorem Complexity.NTM.repeatStrideChoices_split_admin {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) (j : Fin k) (a : Fin (T + 2)) : repeatStrideChoices choices j (Fin.cast ⋯ (Fin.natAdd T a)) = repeatAdminChoices choices j a

The suffix obtained by splitting a stride is exactly repeatAdminChoices.

theorem Complexity.NTM.repeatStrideChoices_trace_split {n k T : ℕ} (tm : NTM n) (choices : Fin (repeatAtTimeSteps k T) → Bool) (j : Fin k) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) : (tm.repeatAtTime k T).trace (repeatAtTimeStride T) (repeatStrideChoices choices j) C = (tm.repeatAtTime k T).trace (T + 2) (repeatAdminChoices choices j) ((tm.repeatAtTime k T).trace T (repeatSimulationChoices choices j) C)

A complete stride trace splits into the source-simulation trace followed by all T + 2 administrative choices.

theorem Complexity.NTM.repeatAdminChoices_trace_split {n k T : ℕ} (tm : NTM n) (choices : Fin (repeatAtTimeSteps k T) → Bool) (j : Fin k) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) : (tm.repeatAtTime k T).trace (T + 2) (repeatAdminChoices choices j) C = (tm.repeatAtTime k T).trace 1 (fun (x : Fin 1) => repeatFinishChoice choices j) ((tm.repeatAtTime k T).trace (T + 1) (repeatRewindChoices choices j) C)

The administrative trace splits into T + 1 fixed-rewind choices and one finish choice.

theorem Complexity.NTM.repeatStrideChoices_trace_split_three {n k T : ℕ} (tm : NTM n) (choices : Fin (repeatAtTimeSteps k T) → Bool) (j : Fin k) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) : (tm.repeatAtTime k T).trace (repeatAtTimeStride T) (repeatStrideChoices choices j) C = (tm.repeatAtTime k T).trace 1 (fun (x : Fin 1) => repeatFinishChoice choices j) ((tm.repeatAtTime k T).trace (T + 1) (repeatRewindChoices choices j) ((tm.repeatAtTime k T).trace T (repeatSimulationChoices choices j) C))

A complete trial stride is exactly simulation, then fixed rewind, then the single finish transition.