This note presents a minimal, Lean‑checked formalization of a trivial pancomputationalism result:

• Define an implementation relation as a homomorphism preserving state transitions (with an accessibility side condition).
• Show that every system implements itself via identity maps.
• Conclude that ∀P ∃C (Implements P C) by taking C = P.

Stronger claims require additional constraints (e.g., computational type, counterfactual robustness, restrictions on admissible witnesses) and are left for future work.

Lean 4 Proof (full)

-- lean/Tau/Pancomputational.lean
universe u₁ v₁ u₂ v₂ u v

namespace Tau

structure System (S : Type u) (I : Type v) where
  tau : S → I → S
  Acc : S → I → Prop

def Implements {S₁ : Type u₁} {I₁ : Type v₁} {S₂ : Type u₂} {I₂ : Type v₂}
  (P : System S₁ I₁) (C : System S₂ I₂) : Prop :=
  ∃ (f : S₁ → S₂) (g : I₁ → I₂),
    ∀ (s : S₁) (i : I₁), P.Acc s i → f (P.tau s i) = C.tau (f s) (g i)

theorem pancomputational_self {S : Type u} {I : Type v}
  (P : System S I) : Implements P P := by
  refine ⟨id, id, ?h⟩; intro s i _h; rfl

theorem pancomputational {S : Type u} {I : Type v}
  (P : System S I) : ∃ (C : System S I), Implements P C := by
  exact ⟨P, pancomputational_self P⟩

end Tau

Checked with Lean 4.22.0.

Laws as Programmer (Lean conditional)

Intuition: robustly programmable subsystems with non‑degenerate carriers witness a non‑trivial implementation.

Full Lean sources (non‑trivial framework and exemplar)

lean/Tau/NonTrivial.lean

import Tau.Pancomputational

/-!
Non‑trivial implementation framework (research scaffold)

Strengthens the trivial `Implements` relation by adding:
- An interpretation map on states/inputs
- A robustness requirement over an admissible input family
- A non‑degeneracy condition on witnesses (forbids trivial identity/constant maps)

We deliberately keep this parametric and proof‑oriented; a separate
certificate/checker module handles computable, finite cases.
-/

universe u₁ v₁ u₂ v₂ u v

namespace Tau

/-- Interpretation from physical to semantic variables (states/inputs). -/
structure Interpretation (S₁ : Type u₁) (I₁ : Type v₁) (S₂ : Type u₂) (I₂ : Type v₂) where
  f : S₁ → S₂
  g : I₁ → I₂

/-- Non‑degeneracy constraint forbidding trivial witnesses. Tunable. -/
def NonDegenerate {S₁ : Type u₁} {I₁ : Type v₁}
  (f : S₁ → S₁) (g : I₁ → I₁) : Prop :=
  (¬ ((∀ s, f s = s) ∧ (∀ i, g i = i))) ∧
  (∃ s₁ s₂, f s₁ ≠ f s₂) ∧ (∃ i₁ i₂, g i₁ ≠ g i₂)

/-- Robustness: homomorphism must hold for all admissible inputs in a family U. -/
def RobustImplements {S₁ : Type u₁} {I₁ : Type v₁} {S₂ : Type u₂} {I₂ : Type v₂}
  (P : System S₁ I₁) (C : System S₂ I₂)
  (U : S₁ → I₁ → Prop) (hU : ∀ s i, U s i → P.Acc s i)
  (f : S₁ → S₂) (g : I₁ → I₂) : Prop :=
  ∀ s i, U s i → f (P.tau s i) = C.tau (f s) (g i)

/-- Non‑trivial implementation combines robustness with non‑degeneracy. -/
def ImplementsNonTrivial {S₁ : Type u₁} {I₁ : Type v₁} {S₂ : Type u₂} {I₂ : Type v₂}
  (P : System S₁ I₁) (C : System S₂ I₂)
  (U : S₁ → I₁ → Prop) (hU : ∀ s i, U s i → P.Acc s i)
  : Prop :=
  ∃ (f : S₁ → S₂) (g : I₁ → I₂),
    RobustImplements P C U hU f g ∧
    (∃ (φ : S₁ → S₁) (γ : I₁ → I₁), NonDegenerate φ γ)

end Tau

lean/Tau/Certificates.lean

/-!
Finite certificate checker (scaffold)

We avoid external finite set dependencies by carrying explicit
enumerations for states and inputs. The checker is expressed as a
proposition over these enumerations, suitable for computable instances
or interactive proofs.
-/

universe u v

namespace Tau

structure Finsys where
  S : Type u
  I : Type v
  states : List S
  inputs : List I
  tau : S → I → S
  Acc : S → I → Prop

structure Cert (P C : Finsys) where
  f : P.S → C.S
  g : P.I → C.I
  U : P.S → P.I → Prop
  totalU : ∀ s i, U s i → P.Acc s i

/-- Propositional checker over explicit finite enumerations. -/
def checkRobustProp (P C : Finsys) (c : Cert P C) : Prop :=
  ∀ s, s ∈ P.states → ∀ i, i ∈ P.inputs → c.U s i →
    c.f (P.tau s i) = C.tau (c.f s) (c.g i)

end Tau

lean/Tau/NonTrivialExemplar.lean

import Tau.Certificates

/-!
Non‑trivial exemplar: map a finite Mealy‑style P to a tiny cognitive
Moore‑style C via witnesses f,g and verify robustness over a finite U.
-/

namespace Tau

inductive PIn | a | b deriving DecidableEq
inductive PState | s0 | s1 | s2 deriving DecidableEq
open PIn PState

def P_tau : PState → PIn → PState
| s0, a => s1 | s0, b => s0 | s1, a => s1 | s1, b => s2 | s2, a => s1 | s2, b => s2
def P_Acc (_ : PState) (_ : PIn) : Prop := True

def P_sys : Finsys where
  S := PState; I := PIn
  states := [s0, s1, s2]
  inputs := [a, b]
  tau := P_tau
  Acc := P_Acc

inductive CIn | A | B deriving DecidableEq
inductive CState | start | seenA | yes deriving DecidableEq
open CIn CState

def C_tau : CState → CIn → CState
| start, A => seenA | start, B => start | seenA, A => seenA | seenA, B => yes | yes, A => seenA | yes, B => yes
def C_Acc (_ : CState) (_ : CIn) : Prop := True

def C_sys : Finsys where
  S := CState; I := CIn
  states := [start, seenA, yes]
  inputs := [A, B]
  tau := C_tau
  Acc := C_Acc

def f_w : PState → CState | s0 => start | s1 => seenA | s2 => yes
def g_w : PIn → CIn | PIn.a => CIn.A | PIn.b => CIn.B
def U_w (_s : PState) (_i : PIn) : Prop := True

theorem totalU_w : ∀ s i, U_w s i → P_sys.Acc s i := by intro; intros; trivial
def cert_w : Cert P_sys C_sys := { f := f_w, g := g_w, U := U_w, totalU := totalU_w }

theorem robust_ok : checkRobustProp P_sys C_sys cert_w := by
  intro s hs i hi _
  cases s <;> cases i <;> simp [P_sys, C_sys, cert_w, f_w, g_w, P_tau, C_tau]

end Tau

lean/Tau/Programmability.lean

import Tau.Pancomputational
import Tau.NonTrivial

/-! Programmability schema: robust witnesses imply non‑trivial implementation. -/

universe u₁ v₁ u₂ v₂

namespace Tau

def Programmable
  {S₁ : Type u₁} {I₁ : Type v₁} {S₂ : Type u₂} {I₂ : Type v₂}
  (P : System S₁ I₁) (C : System S₂ I₂)
  (U : S₁ → I₁ → Prop) (hU : ∀ s i, U s i → P.Acc s i) : Prop :=
  ∃ (f : S₁ → S₂) (g : I₁ → I₂), RobustImplements P C U hU f g

theorem implementsNonTrivial_of_programmable
  {S₁ : Type u₁} {I₁ : Type v₁} {S₂ : Type u₂} {I₂ : Type v₂}
  (P : System S₁ I₁) (C : System S₂ I₂)
  (U : S₁ → I₁ → Prop) (hU : ∀ s i, U s i → P.Acc s i)
  (hp : Programmable P C U hU)
  (nd : ∃ (φ : S₁ → S₁) (γ : I₁ → I₁), NonDegenerate φ γ)
  : ImplementsNonTrivial P C U hU := by
  rcases hp with ⟨f, g, hrob⟩; rcases nd with ⟨φ, γ, hnd⟩
  exact ⟨f, g, hrob, ⟨φ, γ, hnd⟩⟩

theorem existsNonDegenerate_of_two
  {S₁ : Type u₁} {I₁ : Type v₁}
  [DecidableEq S₁] [DecidableEq I₁]
  (Hs : ∃ s₁ s₂ : S₁, s₁ ≠ s₂)
  (Hi : ∃ i₁ i₂ : I₁, i₁ ≠ i₂)
  : ∃ (φ : S₁ → S₁) (γ : I₁ → I₁), NonDegenerate φ γ := by
  rcases Hs with ⟨s₁, s₂, hs⟩; rcases Hi with ⟨i₁, i₂, hi⟩
  let φ : S₁ → S₁ := fun x => if x = s₁ then s₂ else if x = s₂ then s₁ else x
  let γ : I₁ → I₁ := fun x => if x = i₁ then i₂ else if x = i₂ then i₁ else x
  have hφs1 : φ s₁ = s₂ := by simp [φ]
  have hφs2 : φ s₂ = s₁ := by simp [φ]
  have hφ_diff : φ s₁ ≠ φ s₂ := by intro h; have : s₂ = s₁ := by simpa [hφs1, hφs2] using h; exact hs this.symm
  have hγi1 : γ i₁ = i₂ := by simp [γ]
  have hγi2 : γ i₂ = i₁ := by simp [γ]
  have hγ_diff : γ i₁ ≠ γ i₂ := by intro h; have : i₂ = i₁ := by simpa [hγi1, hγi2] using h; exact hi this.symm
  have not_both_id : ¬ ((∀ s, φ s = s) ∧ (∀ i, γ i = i)) := by
    intro h; have hφ := h.left; have hφs1' : φ s₁ = s₁ := hφ s₁; have : s₂ = s₁ := by simpa [hφs1] using hφs1'; exact hs this.symm
  exact ⟨φ, γ, And.intro not_both_id (And.intro ⟨s₁, s₂, hφ_diff⟩ ⟨i₁, i₂, hγ_diff⟩)⟩

theorem implementsNonTrivial_of_programmable_two
  {S₁ : Type u₁} {I₁ : Type v₁} {S₂ : Type u₂} {I₂ : Type v₂}
  [DecidableEq S₁] [DecidableEq I₁]
  (P : System S₁ I₁) (C : System S₂ I₂)
  (U : S₁ → I₁ → Prop) (hU : ∀ s i, U s i → P.Acc s i)
  (hp : Programmable P C U hU)
  (Hs : ∃ s₁ s₂ : S₁, s₁ ≠ s₂)
  (Hi : ∃ i₁ i₂ : I₁, i₁ ≠ i₂)
  : ImplementsNonTrivial P C U hU := by
  obtain ⟨φ, γ, hnd⟩ := existsNonDegenerate_of_two (S₁:=S₁) (I₁:=I₁) Hs Hi
  exact implementsNonTrivial_of_programmable P C U hU hp ⟨φ, γ, hnd⟩

end Tau

This note presents a minimal, Lean‑checked formalization of a trivial pancomputationalism result:

• Define an implementation relation as a homomorphism preserving state transitions (with an accessibility side condition).
• Show that every system implements itself via identity maps.
• Conclude that ∀P ∃C (Implements P C) by taking C = P.

Stronger claims require additional constraints (e.g., computational type, counterfactual robustness, restrictions on admissible witnesses) and are left for future work.

Lean 4 Proof (excerpt)

-- lean/Tau/Pancomputational.lean
universe u₁ v₁ u₂ v₂ u v

namespace Tau

structure System (S : Type u) (I : Type v) where
  tau : S → I → S
  Acc : S → I → Prop

def Implements {S₁ : Type u₁} {I₁ : Type v₁} {S₂ : Type u₂} {I₂ : Type v₂}
  (P : System S₁ I₁) (C : System S₂ I₂) : Prop :=
  ∃ (f : S₁ → S₂) (g : I₁ → I₂),
    ∀ (s : S₁) (i : I₁), P.Acc s i → f (P.tau s i) = C.tau (f s) (g i)

theorem pancomputational_self {S : Type u} {I : Type v}
  (P : System S I) : Implements P P := by
  refine ⟨id, id, ?h⟩; intro s i _h; rfl

theorem pancomputational {S : Type u} {I : Type v}
  (P : System S I) : ∃ (C : System S I), Implements P C := by
  exact ⟨P, pancomputational_self P⟩

end Tau

Checked with Lean 4.22.0. See lean/Tau/Pancomputational.lean in this repo.

How to Reproduce

1. Install elan (Lean toolchain manager).
2. In the repo root: cd lean.
3. Build and check: lake build and lean Tau/Pancomputational.lean.

Discussion

This formalization captures a “self‑implementation” result. It can serve as a baseline for richer theorems: adding constraints on admissible implementations, requiring specific computational types, or formalizing counterfactual robustness.

Undecidability of Consciousness (Informal)

Under a computationalist reading where “is conscious” is modeled as a non‑trivial property of a computation’s extensional behavior, determining whether an arbitrary program/system is conscious is undecidable by Rice’s Theorem. Any total procedure deciding such a property for all programs would imply a decision procedure for all non‑trivial semantic properties, which is impossible. This pushes us toward conditional, axiomatic, or approximate criteria rather than a universal decision test.

• Assumption: Consciousness is a non‑trivial property of computed function/behavior (extensional).
• Claim: There is no total algorithm that decides “conscious?” for every program/system.
• Caveat: Specific definitions of consciousness may be computable on bounded models, but generally fail to be both faithful and tractable.

Black‑Hole Consciousness (Conditional Possibility)

If consciousness exists at all and is realized by some class of computations, then, assuming sufficiently rich physical substrates can implement those computations, there is no principled barrier to a black hole (or any complex physical system) implementing them. This is a conditional possibility claim, not a physical assertion.

• Assume: (i) Consciousness is realized by some computations C_cog; (ii) rich physical systems can implement computations in C_cog (with appropriate counterfactual robustness); (iii) black holes exist as physical systems.
• Then: It is possible that some black hole implements a conscious computation.
• Probability gloss: If a non‑zero prior mass is placed on black‑hole implementations of C_cog, consciousness has non‑zero probability in such systems, likely very low, but not logically excluded.

This section is an epistemic/axiomatic argument. It does not claim present‑day physics predicts consciousness in black holes; it shows how, under explicit assumptions, the possibility follows.

Visuals

Three compact diagrams illustrate the key ideas.

1) Implementation Flow (Trivial Pancomputationalism)

2) Rice’s Theorem Intuition (Undecidability)

3) Black‑Hole Consciousness (Conditional)

Laws as Programmer (Lean conditional)

We formalize the intuition “the laws of physics can program a subsystem” as a conditional theorem. Define Programmable P C U hU to mean there exist witnesses f, g such that RobustImplements P C U hU f g holds (homomorphism over a family of admissible inputs U). Then:

-- lean/Tau/Programmability.lean
def Programmable (P C U hU) : Prop := ∃ f g, RobustImplements P C U hU f g

theorem implementsNonTrivial_of_programmable
  (hp : Programmable P C U hU)
  (nd : ∃ φ γ, NonDegenerate φ γ)
  : ImplementsNonTrivial P C U hU

-- With ≥2 distinct states/inputs (and DecidableEq), we can build φ, γ
theorem implementsNonTrivial_of_programmable_two ... : ImplementsNonTrivial P C U hU

Read: if a physical subsystem can be robustly “programmed” (via boundary/initial conditions) to realize a target computation, and its carriers admit simple non‑degeneracy, then it non‑trivially implements that computation. See lean/Tau/Programmability.lean. For black‑hole computing context, see Lloyd & Ng, Black Hole Computers (Scientific American).

FAQ

Why is this the “trivial” case?
Because the proof witnesses implementation with identity maps (f = id, g = id), showing any system implements itself. That establishes ∀P ∃C Implements(P, C) by taking C = P, but says nothing about cognitive status or robustness.

What would a “non‑trivial” case look like?
Add constraints that forbid degenerate witnesses and demand meaningful structure, e.g., C ∈ a cognitive class, counterfactual robustness over rich inputs, non‑trivial information/representation properties, or (non)injectivity/surjectivity of maps. Proving existence under those constraints is far harder and generally assumption‑dependent.

Why is consciousness “typically” undecidable?
Modeling “is conscious” as a non‑trivial semantic property of computations brings Rice’s Theorem to bear: any such property over programs is undecidable in general, so no total algorithm can decide it for all systems.

When can it be decidable?
Under strong restrictions—finite/bounded models, domain‑specific computable proxies, or certified witnesses—decision procedures exist. These are context‑limited or sufficient tests; they do not yield a universal decider.

See also: Why “Consciousness?” Is Typically Undecidable.