Native controller routines for inductive counting

The certificates charge the full encoded arguments and apply to every state, including malformed register contents. Width is supplied in unary: writing the binary register bound 2 ^ width then takes only linear space in that argument.

Unary conversion and fixed-list dispatch adapt the corresponding native tidy-calculus proofs.

Main results

• Turing.InductiveCounting.instruction_budget: the local controller instruction.
• Turing.InductiveCounting.advance_budget: the instruction with storage and rank checks.
• Turing.InductiveCounting.advance_inSpace: the complete routine on its encoded input tuple.
• Turing.InductiveCounting.query_budget: the explicit edge or bad-vertex request.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.6

theorem Turing.InductiveCounting.unaryToBinary_inSpace : MultiTapeTM.ComputableTidilyInSpace (fun (n : ℕ) => n) MultiTapeTM.encUnary MultiTapeTM.encNat fun (n : ℕ) => (MultiTapeTM.encUnary n).length

Converting a unary counter to binary needs only linear space.

theorem Turing.InductiveCounting.unaryTwoPow_inSpace : MultiTapeTM.ComputableTidilyInSpace (fun (n : ℕ) => 2 ^ n) MultiTapeTM.encUnary MultiTapeTM.encNat fun (n : ℕ) => (MultiTapeTM.encUnary n).length

Binary powers of two from unary exponents, without an exponential unary intermediate.

theorem Turing.InductiveCounting.stateData_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => stateData (s a)) enc (MultiTapeTM.encPair MultiTapeTM.encNat (MultiTapeTM.encPair (MultiTapeTM.encList MultiTapeTM.encNat) (MultiTapeTM.encPair MultiTapeTM.encBool MultiTapeTM.encBool))) S

Reading the encoded product underlying a controller state.

theorem Turing.InductiveCounting.phaseCode_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => phaseCode (s a).phase) enc MultiTapeTM.encNat S

Reading the finite instruction label as its fixed natural code.

theorem Turing.InductiveCounting.registers_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => registers (s a)) enc (MultiTapeTM.encList MultiTapeTM.encNat) S

Reading the ten binary registers.

theorem Turing.InductiveCounting.hit_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).hit) enc MultiTapeTM.encBool S

Reading the predicate flag.

theorem Turing.InductiveCounting.finalScan_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).finalScan) enc MultiTapeTM.encBool S

Reading the final-scan flag.

theorem Turing.InductiveCounting.register_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) (i : ℕ) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (List.drop i (registers (s a))).headD 0) enc MultiTapeTM.encNat S

A fixed register projection preserves the common budget.

theorem Turing.InductiveCounting.phaseCases_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {β : Type} {encB : β ↪ List Bool} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) (F : Cslib.InductiveCounting.Phase → α → β) (hF : ∀ (p : Cslib.InductiveCounting.Phase), MultiTapeTM.ComputableTidilyInSpace (F p) enc encB S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => F (s a).phase a) enc encB S

Case distinction on the finite phase, retaining an arbitrary common budget.

theorem Turing.InductiveCounting.state_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hp : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => phaseCode (s a).phase) enc MultiTapeTM.encNat S) (hround : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).round) enc MultiTapeTM.encNat S) (hcount : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).count) enc MultiTapeTM.encNat S) (htarget : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).target) enc MultiTapeTM.encNat S) (hnext : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).nextCount) enc MultiTapeTM.encNat S) (hcandidate : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).candidate) enc MultiTapeTM.encNat S) (hselected : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).selected) enc MultiTapeTM.encNat S) (hremaining : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).remaining) enc MultiTapeTM.encNat S) (hcurrent : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).current) enc MultiTapeTM.encNat S) (hguess : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).guess) enc MultiTapeTM.encNat S) (hbits : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).bits) enc MultiTapeTM.encNat S) (hhit : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).hit) enc MultiTapeTM.encBool S) (hfinal : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).finalScan) enc MultiTapeTM.encBool S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableTidilyInSpace s enc encState S

Constructing a state from its finite label, ten binary registers and two flags.

theorem Turing.InductiveCounting.round_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).round) enc MultiTapeTM.encNat S

Reading the round register preserves the common budget.

theorem Turing.InductiveCounting.count_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).count) enc MultiTapeTM.encNat S

Reading the count register preserves the common budget.

theorem Turing.InductiveCounting.target_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).target) enc MultiTapeTM.encNat S

Reading the target register preserves the common budget.

theorem Turing.InductiveCounting.nextCount_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).nextCount) enc MultiTapeTM.encNat S

Reading the nextCount register preserves the common budget.

theorem Turing.InductiveCounting.candidate_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).candidate) enc MultiTapeTM.encNat S

Reading the candidate register preserves the common budget.

theorem Turing.InductiveCounting.selected_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).selected) enc MultiTapeTM.encNat S

Reading the selected register preserves the common budget.

theorem Turing.InductiveCounting.remaining_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).remaining) enc MultiTapeTM.encNat S

Reading the remaining register preserves the common budget.

theorem Turing.InductiveCounting.current_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).current) enc MultiTapeTM.encNat S

Reading the current register preserves the common budget.

theorem Turing.InductiveCounting.guess_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).guess) enc MultiTapeTM.encNat S

Reading the guess register preserves the common budget.

theorem Turing.InductiveCounting.bits_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).bits) enc MultiTapeTM.encNat S

Reading the bits register preserves the common budget.

theorem Turing.InductiveCounting.halted_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => Cslib.InductiveCounting.halted (s a)) enc MultiTapeTM.encBool S

Halt detection reads only the finite phase.

theorem Turing.InductiveCounting.accepting_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => (s a).phase == Cslib.InductiveCounting.Phase.accept) enc MultiTapeTM.encBool S

Acceptance detection reads only the finite phase.

theorem Turing.InductiveCounting.widthBinary_budget {α : Type} {enc : α ↪ List Bool} {S width : α → ℕ} (hw : MultiTapeTM.ComputableTidilyInSpace width enc MultiTapeTM.encUnary S) : MultiTapeTM.ComputableTidilyInSpace width enc MultiTapeTM.encNat S

A unary width can also be used as a binary register in the same budget.

theorem Turing.InductiveCounting.registerBound_budget {α : Type} {enc : α ↪ List Bool} {S N width : α → ℕ} (hN : MultiTapeTM.ComputableTidilyInSpace N enc MultiTapeTM.encNat S) (hw : MultiTapeTM.ComputableTidilyInSpace width enc MultiTapeTM.encUnary S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => Cslib.InductiveCounting.registerBound (N a) (width a)) enc MultiTapeTM.encNat S

The complete register bound, with unary width, uses linear space on all inputs.

theorem Turing.InductiveCounting.instruction_budget {α : Type} {enc : α ↪ List Bool} {S N width source : α → ℕ} {s : α → Cslib.InductiveCounting.State} {answer choice : α → Bool} (hN : MultiTapeTM.ComputableTidilyInSpace N enc MultiTapeTM.encNat S) (hw : MultiTapeTM.ComputableTidilyInSpace width enc MultiTapeTM.encNat S) (hsource : MultiTapeTM.ComputableTidilyInSpace source enc MultiTapeTM.encNat S) (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) (hanswer : MultiTapeTM.ComputableTidilyInSpace answer enc MultiTapeTM.encBool S) (hchoice : MultiTapeTM.ComputableTidilyInSpace choice enc MultiTapeTM.encBool S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => Cslib.InductiveCounting.instruction (N a) (width a) (source a) (s a) (answer a) (choice a)) enc encState S

A native certificate for the underlying local instruction, with no validity assumption.

theorem Turing.InductiveCounting.candidateCost_budget {α : Type} {enc : α ↪ List Bool} {S N width : α → ℕ} (hN : MultiTapeTM.ComputableTidilyInSpace N enc MultiTapeTM.encNat S) (hw : MultiTapeTM.ComputableTidilyInSpace width enc MultiTapeTM.encNat S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => Cslib.InductiveCounting.candidateCost (N a) (width a)) enc MultiTapeTM.encNat S

The candidate cost is a fixed arithmetic expression in the supplied parameters.

theorem Turing.InductiveCounting.targetCost_budget {α : Type} {enc : α ↪ List Bool} {S N width : α → ℕ} (hN : MultiTapeTM.ComputableTidilyInSpace N enc MultiTapeTM.encNat S) (hw : MultiTapeTM.ComputableTidilyInSpace width enc MultiTapeTM.encNat S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => Cslib.InductiveCounting.targetCost (N a) (width a)) enc MultiTapeTM.encNat S

The target cost uses a fixed number of binary arithmetic operations.

theorem Turing.InductiveCounting.roundCost_budget {α : Type} {enc : α ↪ List Bool} {S N width : α → ℕ} (hN : MultiTapeTM.ComputableTidilyInSpace N enc MultiTapeTM.encNat S) (hw : MultiTapeTM.ComputableTidilyInSpace width enc MultiTapeTM.encNat S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => Cslib.InductiveCounting.roundCost (N a) (width a)) enc MultiTapeTM.encNat S

The round cost uses a fixed number of binary arithmetic operations.

theorem Turing.InductiveCounting.rank_budget {α : Type} {enc : α ↪ List Bool} {S N width : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hN : MultiTapeTM.ComputableTidilyInSpace N enc MultiTapeTM.encNat S) (hw : MultiTapeTM.ComputableTidilyInSpace width enc MultiTapeTM.encNat S) (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => Cslib.InductiveCounting.rank (N a) (width a) (s a)) enc MultiTapeTM.encNat S

The full progress measure is computed in the common budget on arbitrary states.

theorem Turing.InductiveCounting.bounded_budget {α : Type} {enc : α ↪ List Bool} {S N width : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hN : MultiTapeTM.ComputableTidilyInSpace N enc MultiTapeTM.encNat S) (hw : MultiTapeTM.ComputableTidilyInSpace width enc MultiTapeTM.encUnary S) (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => decide (Cslib.InductiveCounting.Bounded (N a) (width a) (s a))) enc MultiTapeTM.encBool S

All ten storage checks are executable within the budget, including on malformed states.

theorem Turing.InductiveCounting.advance_budget {α : Type} {enc : α ↪ List Bool} {S N width source : α → ℕ} {s : α → Cslib.InductiveCounting.State} {answer choice : α → Bool} (hN : MultiTapeTM.ComputableTidilyInSpace N enc MultiTapeTM.encNat S) (hw : MultiTapeTM.ComputableTidilyInSpace width enc MultiTapeTM.encUnary S) (hsource : MultiTapeTM.ComputableTidilyInSpace source enc MultiTapeTM.encNat S) (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) (hanswer : MultiTapeTM.ComputableTidilyInSpace answer enc MultiTapeTM.encBool S) (hchoice : MultiTapeTM.ComputableTidilyInSpace choice enc MultiTapeTM.encBool S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => Cslib.InductiveCounting.advance (N a) (width a) (source a) (s a) (answer a) (choice a)) enc encState S

One checked controller step: this certificate includes both the complete storage test and the comparison of the old and new ranks. Width is unary, so the bound remains linear on all arguments, without any register-validity hypothesis.

theorem Turing.InductiveCounting.initial_budget {α : Type} {enc : α ↪ List Bool} {S N source : α → ℕ} (hN : MultiTapeTM.ComputableTidilyInSpace N enc MultiTapeTM.encNat S) (hsource : MultiTapeTM.ComputableTidilyInSpace source enc MultiTapeTM.encNat S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => Cslib.InductiveCounting.initial (N a) (source a)) enc encState S

Initializing the controller includes its source-range check.

def Turing.InductiveCounting.queryData : Cslib.InductiveCounting.Query → Bool × ℕ × ℕ

Tagged binary data for one edge or bad-vertex request.

theorem Turing.InductiveCounting.queryData_injective : Function.Injective queryData

def Turing.InductiveCounting.encQuery : Cslib.InductiveCounting.Query ↪ List Bool

An oracle request stores its tag and at most two binary vertices.

theorem Turing.InductiveCounting.query_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {s : α → Cslib.InductiveCounting.State} (hs : MultiTapeTM.ComputableTidilyInSpace s enc encState S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableTidilyInSpace (fun (a : α) => Cslib.InductiveCounting.query (s a)) enc (MultiTapeTM.encOption encQuery) S

The explicit request, including the finite-phase and final-scan selection.

def Turing.InductiveCounting.encAdvanceInput : ℕ × ℕ × ℕ × Cslib.InductiveCounting.State × Bool × Bool ↪ List Bool

Full routine inputs: N, unary width, source, state, answer and choice.

theorem Turing.InductiveCounting.advance_inSpace : MultiTapeTM.ComputableTidilyInSpace (fun (a : ℕ × ℕ × ℕ × Cslib.InductiveCounting.State × Bool × Bool) => Cslib.InductiveCounting.advance a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2.1 a.2.2.2.2.2) encAdvanceInput encState fun (a : ℕ × ℕ × ℕ × Cslib.InductiveCounting.State × Bool × Bool) => (encAdvanceInput a).length

An unconditional native linear-space certificate for the complete checked routine.