IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.DeltaForcedNoEnumeration

   1import Mathlib.Logic.Basic
   2
   3namespace IndisputableMonolith.PRCGrow.DeltaForcedNoEnumeration
   4
   5/-- The constructive Cantor theorem: the binary-sequence space `ℕ → Bool` cannot be
   6δ-enumerated. This is the choice-free heart of `¬ DeltaForced ℝ`: a forced
   7(δ-enumerable) carrier cannot surject onto the binary sequences, so the continuum
   8is not forced. -/
   9theorem no_enumeration_seq : ¬ ∃ f : ℕ → (ℕ → Bool), Function.Surjective f := by
  10  rintro ⟨f, hf⟩
  11  obtain ⟨n, hn⟩ := hf (fun k => !(f k k))
  12  have := congrFun hn n
  13  simp at this
  14
  15end IndisputableMonolith.PRCGrow.DeltaForcedNoEnumeration
  16