`TuringModel`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.ComputationBridge
domain: Complexity
line: 67 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Complexity.ComputationBridge on GitHub at line 67.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  64  Tr_linear : ∃ (c : ℝ), c > 0 ∧ ∀ n, n > 0 → Tr n ≥ c * n
  65
  66/-- The Turing model as a special case with zero recognition complexity. -/
  67structure TuringModel where
  68  /-- Turing time complexity -/
  69  T : ℕ → ℕ
  70  /-- Recognition complexity is zero in the Turing model. -/
  71  recognition_complexity : ℕ → ℕ
  72  recognition_free : ∀ n, recognition_complexity n = 0
  73
  74/-- Ledger-based computational model with explicit observation cost -/
  75
  76structure LedgerComputation where
  77  /-- State space (ledger configurations) -/
  78  states : Type
  79  /-- Evolution rule (double-entry updates) -/
  80  evolve : states → states
  81  /-- Input encoding into ledger -/
  82  encode : List Bool → states
  83  /-- Output protocol (measurement operations) -/
  84  measure : states → Finset (Fin n) → Bool
  85  /-- Evolution preserves closed-chain flux = 0 -/
  86  flux_conserved : ∀ s, evolve s = s  -- placeholder for actual conservation
  87  /-- Measurement requires Ω(n) queries for balanced-parity encoding -/
  88  measurement_bound : ∀ n M (hM : M.card < n),
  89    ¬(∀ b R, measure (encode (BalancedParityHidden.enc b R).toList) M = b)
  90
  91/-- SAT instance in ledger representation -/
  92structure SATLedger where
  93  /-- Number of variables -/
  94  n : ℕ
  95  /-- Number of clauses -/
  96  m : ℕ
  97  /-- Clause structure encoded in ledger -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.