TauLib · API Book III

TauLib.BookIII.Computation.TowerMachine

TauLib.BookIII.Computation.TowerMachine

τ-Tower Machine, TTM τ-Nativity, and Observable Transition.

Registry Cross-References

  • [III.D51] τ-Tower Machine – TTMConfig, ttm_step, ttm_check

  • [III.T30] TTM τ-Nativity – ttm_nativity_check

  • [III.D52] Observable Transition – observable_transition_check

Mathematical Content

III.D51 (τ-Tower Machine): The TTM at E₂: a state machine operating on τ-addresses. Configuration = (state, register_values, depth). Transitions are modular operations at primorial level k. Extends Book I’s TTM (I.D69) to the enriched E₂ setting.

III.T30 (TTM τ-Nativity): Program IS τ-address operating ON τ-addresses. Code = data = τ-address. No external representation needed: the machine’s program is itself a cylinder in ℤ̂_τ.

III.D52 (Observable Transition): The observable transition function δ^obs operates on bounded configurations. The Cook-Levin width W = 1 + m bounds the observable state at each step.

Tau.BookIII.Computation.TTMConfig

source structure Tau.BookIII.Computation.TTMConfig :Type

[III.D51] TTM configuration at E₂ level: state + register values at primorial depth k. The registers hold τ-addresses.

  • state : Denotation.TauIdx
  • reg_a : Denotation.TauIdx
  • reg_b : Denotation.TauIdx
  • depth : Denotation.TauIdx Instances For

Tau.BookIII.Computation.instReprTTMConfig

source instance Tau.BookIII.Computation.instReprTTMConfig :Repr TTMConfig

Equations

  • Tau.BookIII.Computation.instReprTTMConfig = { reprPrec := Tau.BookIII.Computation.instReprTTMConfig.repr }

Tau.BookIII.Computation.instReprTTMConfig.repr

source def Tau.BookIII.Computation.instReprTTMConfig.repr :TTMConfig → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Computation.instDecidableEqTTMConfig.decEq

source def Tau.BookIII.Computation.instDecidableEqTTMConfig.decEq (x✝ x✝¹ : TTMConfig) :Decidable (x✝ = x✝¹)

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Computation.instDecidableEqTTMConfig

source instance Tau.BookIII.Computation.instDecidableEqTTMConfig :DecidableEq TTMConfig

Equations

  • Tau.BookIII.Computation.instDecidableEqTTMConfig = Tau.BookIII.Computation.instDecidableEqTTMConfig.decEq

Tau.BookIII.Computation.instBEqTTMConfig.beq

source def Tau.BookIII.Computation.instBEqTTMConfig.beq :TTMConfig → TTMConfig → Bool

Equations

  • One or more equations did not get rendered due to their size.
  • Tau.BookIII.Computation.instBEqTTMConfig.beq x✝¹ x✝ = false Instances For

Tau.BookIII.Computation.instBEqTTMConfig

source instance Tau.BookIII.Computation.instBEqTTMConfig :BEq TTMConfig

Equations

  • Tau.BookIII.Computation.instBEqTTMConfig = { beq := Tau.BookIII.Computation.instBEqTTMConfig.beq }

Tau.BookIII.Computation.ttm_step

source def Tau.BookIII.Computation.ttm_step (cfg : TTMConfig) :TTMConfig

[III.D51] TTM transition: one step of computation at primorial level k. The transition is a modular operation determined by the state. Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Computation.ttm_run

source **def Tau.BookIII.Computation.ttm_run (cfg : TTMConfig)

(n : Denotation.TauIdx) :TTMConfig**

[III.D51] TTM multi-step: run n steps from initial configuration. Equations

  • Tau.BookIII.Computation.ttm_run cfg n = Tau.BookIII.Computation.ttm_run.go cfg n Instances For

Tau.BookIII.Computation.ttm_run.go

source@[irreducible]

**def Tau.BookIII.Computation.ttm_run.go (c : TTMConfig)

(fuel : ℕ) :TTMConfig**

Equations

  • Tau.BookIII.Computation.ttm_run.go c fuel = if fuel = 0 then c else Tau.BookIII.Computation.ttm_run.go (Tau.BookIII.Computation.ttm_step c) (fuel - 1) Instances For

Tau.BookIII.Computation.ttm_check

source def Tau.BookIII.Computation.ttm_check (bound db : Denotation.TauIdx) :Bool

[III.D51] TTM check: transitions preserve validity (registers stay within primorial range). Equations

  • Tau.BookIII.Computation.ttm_check bound db = Tau.BookIII.Computation.ttm_check.go bound db 0 0 1 ((bound + 1) * (bound + 1) * (db + 1)) Instances For

Tau.BookIII.Computation.ttm_check.go

source@[irreducible]

**def Tau.BookIII.Computation.ttm_check.go (bound db : Denotation.TauIdx)

(a b k fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Computation.ttm_nativity_check

source def Tau.BookIII.Computation.ttm_nativity_check (bound db : Denotation.TauIdx) :Bool

[III.T30] TTM τ-nativity check: program IS τ-address. The machine’s transition function is determined by the registers themselves (no external instruction tape). Code = data. Equations

  • Tau.BookIII.Computation.ttm_nativity_check bound db = Tau.BookIII.Computation.ttm_nativity_check.go bound db 0 1 ((bound + 1) * (db + 1)) Instances For

Tau.BookIII.Computation.ttm_nativity_check.go

source@[irreducible]

**def Tau.BookIII.Computation.ttm_nativity_check.go (bound db : Denotation.TauIdx)

(x k fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Computation.observable_width

source def Tau.BookIII.Computation.observable_width :Denotation.TauIdx

[III.D52] Observable width: the number of register bits visible at each step. W = 1 + m where m = number of registers (here m = 2). Equations

  • Tau.BookIII.Computation.observable_width = 3 Instances For

Tau.BookIII.Computation.observable_transition_check

source def Tau.BookIII.Computation.observable_transition_check (bound db : Denotation.TauIdx) :Bool

[III.D52] Observable transition check: the observable state at each step is bounded by the Cook-Levin width. Equations

  • Tau.BookIII.Computation.observable_transition_check bound db = Tau.BookIII.Computation.observable_transition_check.go bound db 0 1 ((bound + 1) * (db + 1)) Instances For

Tau.BookIII.Computation.observable_transition_check.go

source@[irreducible]

**def Tau.BookIII.Computation.observable_transition_check.go (bound db : Denotation.TauIdx)

(x k fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Computation.ttm_5_3

source theorem Tau.BookIII.Computation.ttm_5_3 :ttm_check 5 3 = true

Tau.BookIII.Computation.ttm_nativity_10_3

source theorem Tau.BookIII.Computation.ttm_nativity_10_3 :ttm_nativity_check 10 3 = true

Tau.BookIII.Computation.observable_10_3

source theorem Tau.BookIII.Computation.observable_10_3 :observable_transition_check 10 3 = true

Tau.BookIII.Computation.ttm_preserves_depth

source theorem Tau.BookIII.Computation.ttm_preserves_depth (cfg : TTMConfig) :(ttm_step cfg).depth = cfg.depth

[III.D51] Structural: TTM step preserves depth.

Tau.BookIII.Computation.ttm_depth_0

source theorem Tau.BookIII.Computation.ttm_depth_0 :(ttm_step { state := 0, reg_a := 42, reg_b := 7, depth := 0 }).depth = 0

[III.D51] Structural: TTM at depth 0 (Prim(0)=1, all ops mod 1).

Tau.BookIII.Computation.code_is_data

source theorem Tau.BookIII.Computation.code_is_data :(ttm_step { state := 0, reg_a := 7, reg_b := 7, depth := 3 }).reg_a = (7 + 7) % 30

[III.T30] Structural: code=data (self-application).

Tau.BookIII.Computation.obs_width

source theorem Tau.BookIII.Computation.obs_width :observable_width = 3

[III.D52] Structural: observable width is 3.