Exact reachability of the compact configuration graph

The invariant is an actual finite view whose radix registers equal the current ID. Arithmetic steps preserve this invariant, so malformed IDs cannot create spurious accepting paths. The forward implication only requires that source-reachable views fit the selected radix.

The overflow test (Turing.MultiTapeNTM.ConfigurationGraph.overflow) detects the represented views with a step leaving the radix. When no reachable vertex overflows, every source-reachable view fits the radix, so the graph is exact without any space bound on the source.

Main results

• Turing.MultiTapeNTM.ConfigurationGraph.accepts_iff_reachable_bad: exact native acceptance.
• Turing.MultiTapeNTM.ConfigurationGraph.overflow_vertexID: overflow means a step leaving the radix.
• Turing.MultiTapeNTM.ConfigurationGraph.fits_of_not_overflow: a graph without reachable overflow represents every reachable view.
• Turing.MultiTapeNTM.ConfigurationGraph.not_overflow_of_fits: conversely.

theorem Turing.MultiTapeNTM.ConfigurationGraph.radix_pos (D n : ℕ) : 0 < radix D n

theorem Turing.MultiTapeNTM.ConfigurationGraph.pos_of_fits {k B : ℕ} {r : Register k → ℕ} (hf : Fits B r) : 0 < B

A radix that fits some registers is positive.

theorem Turing.MultiTapeNTM.ConfigurationGraph.stateCode_injective {State : Type} [Fintype State] : Function.Injective stateCode

theorem Turing.MultiTapeNTM.ConfigurationGraph.outputCode_lt (w : List Bool) : outputCode w < 3

theorem Turing.MultiTapeNTM.ConfigurationGraph.outputCode_summary (w : List Bool) : outputCode (outputClass w) = outputCode w

theorem Turing.MultiTapeNTM.ConfigurationGraph.outputCode_append (w : List Bool) (b : Option Bool) : outputCode (outputClass (w ++ b.toList)) = outputStep (outputCode w) b

theorem Turing.MultiTapeNTM.ConfigurationGraph.outputCode_eq_one_iff {w : List Bool} : outputCode w = 1 ↔ w = [true]

theorem Turing.MultiTapeNTM.ConfigurationGraph.inputMove_eq {k : ℕ} {State : Type} (v : FiniteCfg k Bool State) (d : SignType) : inputMove v.input.length (↑v.inputPos) d = ↑(moveInputPos v.inputPos d)

The arithmetic input move agrees with native clamping.

theorem Turing.MultiTapeNTM.ConfigurationGraph.registers_step {k : ℕ} {State : Type} [Fintype State] (v : FiniteCfg k Bool State) (a : Action k Bool State) : registers (v.step a).summarizeOutput = nextRegisters v.input.length (registers v) a

The arithmetic tuple update agrees with the summarized finite view step.

theorem Turing.MultiTapeNTM.ConfigurationGraph.readRegisters_vertexID {k B : ℕ} {State : Type} [Fintype State] {v : FiniteCfg k Bool State} (hf : Fits B (registers v)) : readRegisters B (vertexID B v) = registers v

theorem Turing.MultiTapeNTM.ConfigurationGraph.vertexID_lt {k B : ℕ} {State : Type} [Fintype State] {v : FiniteCfg k Bool State} (hf : Fits B (registers v)) : vertexID B v < vertexBound B

theorem Turing.MultiTapeNTM.ConfigurationGraph.valid_vertexID {k B : ℕ} {State : Type} [Fintype State] {v : FiniteCfg k Bool State} (hf : Fits B (registers v)) : valid B v.input.length (vertexID B v) = true

theorem Turing.MultiTapeNTM.ConfigurationGraph.fitsB_eq_true {k B : ℕ} {r : Register k → ℕ} : fitsB B r = true ↔ Fits B r

theorem Turing.MultiTapeNTM.ConfigurationGraph.inputSymbol_query {k B : ℕ} {State : Type} [Fintype State] {v : FiniteCfg k Bool State} (hf : Fits B (registers v)) : inputSymbol v.input.length (↑v.inputPos) v.input[queryIndex B (vertexID B v)]? = v.inputSymbol

The sole queried symbol agrees with the native input head, including both blank boundaries.

theorem Turing.MultiTapeNTM.ConfigurationGraph.matchesEntry_iff {k : ℕ} {State : Type} [Fintype State] (v : FiniteCfg k Bool State) (symbol : Option Bool) (t : Instruction k State) : matchesEntry v.input.length (registers v) symbol t = true ↔ v.state = some t.1 ∧ inputSymbol v.input.length (↑v.inputPos) symbol = t.2.1 ∧ v.workTapeSymbols = t.2.2.1

theorem Turing.MultiTapeNTM.ConfigurationGraph.lt_vertexBound_of_valid {k : ℕ} {State : Type} [Fintype State] {B n u : ℕ} (h : valid B n u = true) : u < vertexBound B

Validity rejects every ID outside the ambient vertex range.

theorem Turing.MultiTapeNTM.ConfigurationGraph.lt_vertexBound_of_edgeWithSymbol {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {B n u v : ℕ} {symbol : Option Bool} (h : edgeWithSymbol ntm B n u v symbol = true) : u < vertexBound B ∧ v < vertexBound B

Every successful local edge query stays inside the finite ambient graph.

theorem Turing.MultiTapeNTM.ConfigurationGraph.edge_sound {k B : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {v : FiniteCfg k Bool State} {u : ℕ} (hf : Fits B (registers v)) (he : Edge ntm B v.input (vertexID B v) u) : ∃ (v' : FiniteCfg k Bool State), ntm.ViewStep v v' ∧ v'.input = v.input ∧ u = vertexID B v' ∧ Fits B (registers v')

An edge out of a represented vertex has an actual native view successor.

theorem Turing.MultiTapeNTM.ConfigurationGraph.edge_complete {k B : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {v v' : FiniteCfg k Bool State} (hf : Fits B (registers v)) (hf' : Fits B (registers v')) (he : ntm.ViewStep v v') : Edge ntm B v.input (vertexID B v) (vertexID B v')

Every fitting native view edge is an edge of the compact graph.

theorem Turing.MultiTapeNTM.ConfigurationGraph.vertexID_init {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) (B : ℕ) (w : List Bool) : vertexID B (ntm.initView w) = startID ntm B

Initial storage has an input-length-only ID.

theorem Turing.MultiTapeNTM.ConfigurationGraph.input_of_reachable {k : ℕ} {State : Type} {ntm : MultiTapeNTM k Bool State} {w : List Bool} {v : FiniteCfg k Bool State} (h : Relation.ReflTransGen ntm.ViewStep (ntm.initView w) v) : v.input = w

Views reachable on one input retain precisely that input.

theorem Turing.MultiTapeNTM.ConfigurationGraph.reachable_iff {k B : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} (hfit : ∀ (v : FiniteCfg k Bool State), Relation.ReflTransGen ntm.ViewStep (ntm.initView w) v → Fits B (registers v)) (u : ℕ) : Relation.ReflTransGen (Edge ntm B w) (startID ntm B) u ↔ ∃ (v : FiniteCfg k Bool State), Relation.ReflTransGen ntm.ViewStep (ntm.initView w) v ∧ u = vertexID B v

Exact graph reachability, provided all source-reachable views fit the radix.

theorem Turing.MultiTapeNTM.ConfigurationGraph.bad_vertexID {k B : ℕ} {State : Type} [Fintype State] {v : FiniteCfg k Bool State} (hf : Fits B (registers v)) : bad B v.input.length (vertexID B v) = true ↔ v.state = none ∧ v.output = [true]

bad has exactly the native accepting-halt meaning on represented vertices.

theorem Turing.MultiTapeNTM.ConfigurationGraph.accepts_iff_reachable_bad {k B : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} (hfit : ∀ (v : FiniteCfg k Bool State), Relation.ReflTransGen ntm.ViewStep (ntm.initView w) v → Fits B (registers v)) : ntm.Accepts w ↔ ∃ (u : ℕ), Relation.ReflTransGen (Edge ntm B w) (startID ntm B) u ∧ bad B w.length u = true

Native acceptance is exactly reachability of a bad vertex. No totality or time bound on the source machine is used; the only assumption is that its reachable registers fit the radix.

theorem Turing.MultiTapeNTM.ConfigurationGraph.overflow_vertexID {k B : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {v : FiniteCfg k Bool State} (hf : Fits B (registers v)) : Overflow ntm B v.input (vertexID B v) ↔ ∃ (v' : FiniteCfg k Bool State), ntm.ViewStep v v' ∧ ¬Fits B (registers v')

Overflow means a step leaving the radix: a represented view overflows exactly when one of its source steps reaches a view that does not fit.

theorem Turing.MultiTapeNTM.ConfigurationGraph.fits_of_not_overflow {k B : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} (hstart : Fits B (registers (ntm.initView w))) (hno : ∀ (u : ℕ), Relation.ReflTransGen (Edge ntm B w) (startID ntm B) u → ¬Overflow ntm B w u) (v : FiniteCfg k Bool State) (hv : Relation.ReflTransGen ntm.ViewStep (ntm.initView w) v) : Fits B (registers v)

A graph without reachable overflow is exact: if the start view fits and no vertex reachable in the graph overflows, then every source-reachable view fits the radix.

theorem Turing.MultiTapeNTM.ConfigurationGraph.not_overflow_of_fits {k B : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} (hfit : ∀ (v : FiniteCfg k Bool State), Relation.ReflTransGen ntm.ViewStep (ntm.initView w) v → Fits B (registers v)) (u : ℕ) (hu : Relation.ReflTransGen (Edge ntm B w) (startID ntm B) u) : ¬Overflow ntm B w u

Conversely, when every source-reachable view fits the radix, no reachable vertex overflows.