反事實與決策
把帳本分岔，然後做差分。
FDCS 層回答「如果……會怎樣」的方式，是把帳本分岔，並讓每個分支都在同一套稽核下執行。得到的答案條件於文件宣告了什麼 —— 而 Runtime 從不假裝不是這樣。
干預
- 硬干預
- 把一個值固定住。被干預的交易不再依賴它的來源。
- 軟干預
- 把一個值推一下。相依結構仍然存在，效果沿著它傳播。
這個區分不是修辭。硬干預會切斷相依圖上的邊，軟干預不會。它們回答不同的問題，也分開宣告。
干預衝突是驗證錯誤，不是執行時的意外。一份文件如果用兩種不相容的方式釘住同一筆交易，它會在執行前被拒絕。
分支差分帳
每個分支都是一本完整的帳，也都拿到一次完整的稽核。你之後讀到的是分支之間的差異，不是某個聲稱能總結它們的單一數字。
分支
一個沒過自己稽核的分支，會被當成「失敗的分支」回報。它不會被默默從比較裡刪掉，也不會讓那些通過的分支跟著失效。
固定點與時間
時間參照讓一筆交易可以依賴帳本較早的狀態。fixed_point_groups 在宣告的契約下疊代到收斂 —— 疊代上界與容忍度都寫在文件裡。
- 固定點收斂對任意非線性系統的形式證明
不確定性
離散不確定性精確傳播。連續不確定性使用決定性的 Halton 序列與 copula，所以重跑會得到同樣的數字 —— 這讓它可重現，但這並不讓它變成解析的。
- 決定性的 Halton 與 copula 取樣解析的連續推論
- 宣告的分支機率學習得到或客觀校準過的機率
決策
不確定性層之上有三種有限分析。
- 政策評分
- 每個宣告的政策在宣告的效用下被評分。
- 資訊價值
- 在你付錢取得一項觀測之前，它值多少。
- 有限序貫決策
- 有界時域的決策序列，精確求解而非近似。
「有限」是關鍵字。這些是對有界問題的精確答案，不是對無界問題的近似。
可識別性
E7 問的是：兩個不同的宣告結構，能不能用手上有的觀測區分開來？有時候不能，而 Runtime 會把這件事說出來。
- 有限觀測等價一般的統計可識別性
「在現有資料下這兩個模型觀測上等價」本身就是一個結果。從裡面挑一個當成答案回報，就不是了。
條件性住在哪裡
宣告值
宣告的機率、因果結構、成本、效用與觀測模型都是模型輸入。本頁每一個結論都條件於它們，而它們沒有任何一項是 Runtime 從世界推論出來的。