Bounded-observation extensionality — proof internals

This module extracts the information recorded by a bounded tape observation and a finite transducer snapshot. In particular, equal bounded work-tape observations determine the symbols read by the transition function and remain equal after applying the same write and move, provided both successor heads remain inside the observed window.

theorem Complexity.Tape.head_eq_of_boundedObs_eq {t u : Tape} {space : ℕ} (ht : t.head ≤ space) (hu : u.head ≤ space) (hobs : t.boundedObs space ht = u.boundedObs space hu) : t.head = u.head

Equal bounded observations have equal underlying head positions.

theorem Complexity.Tape.cells_eq_of_boundedObs_eq {t u : Tape} {space : ℕ} (ht : t.head ≤ space) (hu : u.head ≤ space) (hobs : t.boundedObs space ht = u.boundedObs space hu) (i : Fin (space + 1)) : t.cells ↑i = u.cells ↑i

Equal bounded observations agree on every cell in the observed window.

theorem Complexity.Tape.read_eq_of_boundedObs_eq {t u : Tape} {space : ℕ} (ht : t.head ≤ space) (hu : u.head ≤ space) (hobs : t.boundedObs space ht = u.boundedObs space hu) : t.read = u.read

Equal bounded observations read the same symbol.

theorem Complexity.Tape.boundedObs_writeAndMove_congr {t u : Tape} {space : ℕ} (ht : t.head ≤ space) (hu : u.head ≤ space) (hobs : t.boundedObs space ht = u.boundedObs space hu) (s : Γ) (d : Dir3) (ht' : (t.writeAndMove s d).head ≤ space) (hu' : (u.writeAndMove s d).head ≤ space) : (t.writeAndMove s d).boundedObs space ht' = (u.writeAndMove s d).boundedObs space hu'

Applying the same write and move to equal bounded observations produces equal successor observations, as long as both successor heads remain inside the same observed window.

theorem Complexity.TM.state_eq_of_transducerSnapshot_eq {k : ℕ} {tm : TM k} {inputLength space : ℕ} {c d : Cfg k tm.Q} (hc : c.WithinAuxSpace inputLength space) (hd : d.WithinAuxSpace inputLength space) (hsnap : tm.transducerSnapshot c inputLength space hc = tm.transducerSnapshot d inputLength space hd) : c.state = d.state

Equal transducer snapshots record the same machine state.

theorem Complexity.TM.input_head_eq_of_transducerSnapshot_eq {k : ℕ} {tm : TM k} {inputLength space : ℕ} {c d : Cfg k tm.Q} (hc : c.WithinAuxSpace inputLength space) (hd : d.WithinAuxSpace inputLength space) (hsnap : tm.transducerSnapshot c inputLength space hc = tm.transducerSnapshot d inputLength space hd) : c.input.head = d.input.head

Equal transducer snapshots record the same input-head position.

theorem Complexity.TM.input_read_eq_of_transducerSnapshot_eq {k : ℕ} {tm : TM k} {inputLength space : ℕ} {c d : Cfg k tm.Q} (hc : c.WithinAuxSpace inputLength space) (hd : d.WithinAuxSpace inputLength space) (hsnap : tm.transducerSnapshot c inputLength space hc = tm.transducerSnapshot d inputLength space hd) (hinput : c.input.cells = d.input.cells) : c.input.read = d.input.read

When two snapshotted configurations share their read-only input contents, equal snapshots make their input heads read the same symbol.

theorem Complexity.TM.work_boundedObs_eq_of_transducerSnapshot_eq {k : ℕ} {tm : TM k} {inputLength space : ℕ} {c d : Cfg k tm.Q} (hc : c.WithinAuxSpace inputLength space) (hd : d.WithinAuxSpace inputLength space) (hsnap : tm.transducerSnapshot c inputLength space hc = tm.transducerSnapshot d inputLength space hd) (i : Fin k) : (c.work i).boundedObs space ⋯ = (d.work i).boundedObs space ⋯

Equal transducer snapshots contain equal bounded observations of each work tape.

theorem Complexity.TM.work_head_eq_of_transducerSnapshot_eq {k : ℕ} {tm : TM k} {inputLength space : ℕ} {c d : Cfg k tm.Q} (hc : c.WithinAuxSpace inputLength space) (hd : d.WithinAuxSpace inputLength space) (hsnap : tm.transducerSnapshot c inputLength space hc = tm.transducerSnapshot d inputLength space hd) (i : Fin k) : (c.work i).head = (d.work i).head

Equal transducer snapshots record the same head position on each work tape.

theorem Complexity.TM.work_read_eq_of_transducerSnapshot_eq {k : ℕ} {tm : TM k} {inputLength space : ℕ} {c d : Cfg k tm.Q} (hc : c.WithinAuxSpace inputLength space) (hd : d.WithinAuxSpace inputLength space) (hsnap : tm.transducerSnapshot c inputLength space hc = tm.transducerSnapshot d inputLength space hd) (i : Fin k) : (c.work i).read = (d.work i).read

Equal transducer snapshots read the same symbol on each work tape.

theorem Complexity.TM.output_head_zero_eq_of_transducerSnapshot_eq {k : ℕ} {tm : TM k} {inputLength space : ℕ} {c d : Cfg k tm.Q} (hc : c.WithinAuxSpace inputLength space) (hd : d.WithinAuxSpace inputLength space) (hsnap : tm.transducerSnapshot c inputLength space hc = tm.transducerSnapshot d inputLength space hd) : decide (c.output.head = 0) = decide (d.output.head = 0)

Equal transducer snapshots have equal output-head zero flags.

theorem Complexity.TM.output_head_eq_zero_iff_of_transducerSnapshot_eq {k : ℕ} {tm : TM k} {inputLength space : ℕ} {c d : Cfg k tm.Q} (hc : c.WithinAuxSpace inputLength space) (hd : d.WithinAuxSpace inputLength space) (hsnap : tm.transducerSnapshot c inputLength space hc = tm.transducerSnapshot d inputLength space hd) : c.output.head = 0 ↔ d.output.head = 0

Equal transducer snapshots agree on whether the output head is at the exceptional immutable left-marker cell.

theorem Complexity.TM.output_read_eq_of_transducerSnapshot_eq {k : ℕ} {tm : TM k} {inputLength space : ℕ} {c d : Cfg k tm.Q} (hc : c.WithinAuxSpace inputLength space) (hd : d.WithinAuxSpace inputLength space) (hsnap : tm.transducerSnapshot c inputLength space hc = tm.transducerSnapshot d inputLength space hd) : c.output.read = d.output.read

Equal transducer snapshots read the same output symbol.