Turing_incomplete

formal source

 158  }
 159
 160/-- Turing incompleteness: the model ignores recognition cost -/
 161theorem Turing_incomplete (TM : TuringModel) :
 162  ∃ (problem : Type) (LC : LedgerComputation),
 163    -- The ledger model captures costs Turing ignores (existence of a hard measurement instance)
 164    (∃ (n : ℕ) (M : Finset (Fin n)) (hM : M.card < n),
 165      ¬ (∀ b R, LC.measure (LC.encode (BalancedParityHidden.enc b R).toList) M = b)) ∧
 166    -- Turing counts only evolution, not measurement
 167    TM.recognition_complexity = fun _ => 0 := by
 168  -- Witness: any problem with balanced-parity output
 169  let LC : LedgerComputation := {
 170    states := Unit  -- placeholder
 171    evolve := id
 172    encode := fun _ => ()
 173    measure := fun _ _ => false
 174    flux_conserved := fun _ => rfl
 175    measurement_bound := by
 176      intro n M hM
 177      -- Apply the balanced-parity lower bound
 178      classical
 179      intro h
 180      -- Instantiate the universal claim at `b = true` with any mask `R`.
 181      -- Our `measure` always returns `false`, so it cannot equal `true`.
 182      have h' := h true (fun _ => false)
 183      simpa using h'
 184  }
 185  use Unit, LC
 186  -- Provide a concrete hard instance using the bound and trivial size witness.
 187  refine ⟨?_, ?_⟩
 188  · refine ⟨1, (∅ : Finset (Fin 1)), by decide, ?_⟩
 189    -- Instantiate the universal impossibility from the `measurement_bound` field.
 190    simpa using (LC.measurement_bound 1 (∅) (by decide))
 191  · funext n