TuringModel
The TuringModel structure defines the classical Turing computation model by specifying a time complexity function T together with a recognition complexity function forced to zero. Researchers studying ledger-based complexity separations would cite this as the zero-recognition baseline case. The declaration is a bare structure definition whose third field is an axiom enforcing the vanishing of recognition cost for every input.
claimA Turing model consists of functions $T : ℕ → ℕ$ and $C : ℕ → ℕ$ such that $C(n) = 0$ for every natural number $n$, where $T$ records Turing time complexity and $C$ records recognition complexity.
background
This declaration sits inside a scaffold module that explores hypothetical ledger-based dual complexity (computation versus recognition) and possible P versus NP separations. The module states explicitly that its results rely on model assumptions, are not part of the verified certificate chain, and should not be cited as proven mathematics. Recognition cost is supplied by upstream definitions: ObserverForcing.cost equates the cost of a recognition event to the J-cost of its state, while MultiplicativeRecognizerL4.cost gives the derived cost of a comparator on positive ratios. Breath1024.T supplies the fundamental period type used for timing.
proof idea
The declaration is a structure definition. It introduces the three fields T for time complexity, recognition_complexity for the recognition map, and the axiom recognition_free that sets the map to zero at every natural number. No lemmas, tactics, or upstream results are applied inside the definition itself.
why it matters in Recognition Science
TuringModel supplies the turing_special_case field of CompleteModel, permitting reduction to the classical Turing setting when recognition costs are neglected. It is used by the Turing_incomplete theorem to exhibit the existence of measurement instances that the Turing model cannot capture. The definition therefore marks the zero-recognition baseline inside the exploratory ledger framework, underscoring the information-theoretic barrier created by balanced-parity encoding.
scope and limits
- Does not claim to resolve P versus NP.
- Does not belong to the verified certificate chain.
- Does not apply to models with nonzero recognition cost.
- Does not supply unconditional theorems.
formal statement (Lean)
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