TuringModel
plain-language theorem explainer
The Turing model structure encodes classical computation by forcing recognition complexity to vanish for every input size. Researchers studying ledger dual-complexity models would reference it to recover the standard Turing case from the full recognition-aware setting. The declaration consists of a structure with three fields and no additional proof obligations.
Claim. A Turing model comprises a time-complexity function $T : ℕ → ℕ$, a recognition-complexity function $r : ℕ → ℕ$, and the assertion that $r(n) = 0$ for every natural number $n$.
background
The ComputationBridge module is labeled as a scaffold for exploring hypothetical implications of ledger-style computation versus recognition, distinct from the verified RS chain. Recognition complexity here is set to zero, in contrast to the J-cost of recognition events supplied by ObserverForcing.cost. The upstream MultiplicativeRecognizerL4.cost defines derived costs on positive ratios, while Breath1024.T supplies the period type used throughout.
proof idea
The declaration is a structure definition introducing the three fields directly. No tactics or lemmas are applied; the recognition_free field simply asserts the zero function.
why it matters
It supplies the turing_special_case field inside the CompleteModel structure and is invoked by the Turing_incomplete theorem to exhibit problems where ledger measurement exceeds Turing evolution. The module documentation positions it within a hypothetical P versus NP framework based on balanced-parity encoding, but explicitly warns that the results are exploratory and not part of the certificate chain. It addresses the question of whether classical models omit essential recognition costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.