TLC は与えた有限インスタンス（固定スレッド数 T、固定木 高さ H・幅 N、固定 MaxCommits）に対してのみ exhaustive。
インスタンスを大きくし続けても「∀T・∀木」には到達しない（無限後退）。
本デッキは、有限 TLC 結果を無限族の主張へ持ち上げる議論をまとめる
（出典: doc/parameterized_cutoff.md）。
| 軸 | 到達点 | 機構 |
|---|---|---|
| 木（高さ・幅） | ∀ 木形の定理 | 構造カットオフ（catamorphism 簡約）: H=3, N=2 へ簡約 → TLC で網羅放電 |
スレッド T | ∀T は強根拠つき予想（定理にしない） | 恒等フリー safety + contention bound まで網羅 + σ-飽和の測定 |
| 活性 (livelock-free) | ∀N のranking 論証 | oldest-tag ランキング関数（スレッドカットオフ不要）+ 残存 1 補題 |
読み方: 「∀ 木形・全スレッド数」は 「木については証明済み／スレッドについては強根拠つき予想」と読む。
パラメータ化検証は一般に決定不能（Apt–Kozen 1986）なので、機械化していない ∀T 定理は主張しない。
すべての bundle / unbundle 遷移は木上の畳み込み (catamorphism)である。
(* bundle は部分木を ↓ 下向きに畳む *)
bundle(n) = collect( linkage[n], { bundle(c) : c ∈ children(n) } )
(* unbundle は祖先鎖を ↑ 上向きに畳む（priority root が base case）*)
unbundle(n) = extract( linkage[n], unbundle(parent(n)) ){linkage[n]} と、直接の畳み込み近傍
（bundle なら子、unbundle なら親）の畳み込み結果のみ。結合関数は木の高さ・子の個数に依存しない。
子は対称集約（[c ↦ linkage[c]], ∀ c …）と単調な「全子完了」閾値を通じてのみ現れる。
要点: 「アクションが2レベルしか触らない」ではない（SnapshotForUnbundle は
祖先鎖全体を一度に読む；inner bundle は孫に届く）。要点は、その層越えアクセスが
高さ一様な局所ステップを持つ畳み込みであること。だから下の深さ帰納がアルゴリズム再構成なしで通る。
| アクション | linkage footprint | 役割 |
|---|---|---|
BundlePhase1 (collect) | self + 各直接子（孫は非葉子の再帰 inner-bundle 経由のみ） | bundle↓ |
BundlePhase3 (per-child CAS) | self + 直接子（1アクション1子） | bundle↓ |
UnbundleWalk / UnbundleCASLoop / UnbundleCASChild | self + 直接親 / 1祖先 + root anchor / self + 直接親 | unbundle↑ |
BundlePhase2/4, CommitTryCAS, CommitGrand | self のみ（root anchor 読みを含む） | local |
全アクションの footprint ⊆ {self} ∪ {直接畳み込み近傍} ∪ {root anchor}。obligation #1 放電済。
is_bundle_root ⇔ 全子 bundled）は子集合上の単調閾値。
ゆえに N ≥ 2 子の任意挙動は、子 3..N を子 2 に潰すことで 2 子挙動でシミュレートできる。
2 子で幅依存の 3 パターンが既に出る: 一方完了/他方保留・同一子で 2 スレッド競合・別々の子で 2 スレッド。3 子目は反復のみ。
SnapshotConsistency, BundleChainValid, NoPriorityLoss,
GrandAlwaysPriority, MissingPropagation, TerminalPayloadCheck, …）は、
任意の高さ H・任意の幅 N の木で成立 ⇔ H=3（root + 内部 1 + 葉）かつ N=2 のインスタンスで成立。
H 帰納。役割は leaf / internal / root の 3 種のみで、H=3 が全役割と両畳み込み方向を内部ノードで行使。H≥4 は同じ一様ステップの追加だけで新規役割相互作用なし。N を 2 に簡約。帰結: H=3, N=2, superfine の網羅 TLC 実行は、木軸については
無限木族に対する safety 不変条件の完全な証明を構成する（単に検査した個別インスタンスではなく、
カットオフの base case として Lemma 1–2 が全 H, N へ持ち上げる）。
T 定理にしないか + 恒等フリー safety∀T 定理は主張しない（意図的スコープ）。 パラメータ化検証は一般に決定不能（Apt–Kozen 1986）。
機械化した ∀T 証明（guided TLAPS の Spec(T) ⊑ Spec(3) simulation、または別途検証したスレッドフリー抽象 CAS モデル）は将来課題。
代わりに 3 つの機械検査可能な要素で 強根拠つき予想として支える: ① 恒等フリー safety（本スライド）、② contention bound まで網羅、③ σ-飽和の測定（次スライド）。
| A | 構造述語. 全 safety 不変条件（SnapshotConsistency, NoPriorityLoss, BundleChainValid, BundledByCorrect, GrandAlwaysPriority, MissingPropagation, TerminalPayloadCheck）は bundle-tree linkage（hasPriority/bundledBy/sub[·]/missing）と payload count 上の述語。priorityTag も serial も読まない＝スレッドに言及しない。 |
| B | per-node CAS 直列化. linkage[n] は成功 CAS でのみ変化 → 任意 T で各ノードの履歴は単一の直列値列。gate は どのスレッドが CAS を試みるかを制限するだけ（priorityTag を書く、linkage は書かない）→ 安全違反を作り出せない。 |
| C | 恒等は uniquifier のみ. スレッド恒等は Lamport serial = counter·Base + tid の低位 uniquifier としてのみ状態に現れる。GenSerial で counter が因果順を支配、tid は因果的に並行なイベントの tie-break のみ（順序依存データ独立性, Lazić 1999）。 |
⇒ スレッド対称性は意味論的に成立（安全状態は恒等の任意置換で不変）。
ただし TLC SYMMETRY 縮約としては適用不可: TagOlder の tid-<（Lamport tie-break）は Threads を順序付き自然数に強制するが、
TLC SYMMETRY はmodel-value 集合を要求し、両者は排他（TLC は SYMMETRY Permutations(Threads) を拒否）。
ゆえに下の実行はすべて symmetry 縮約なしの raw。なお対称性は置換のみでスレッド数を減らさない（symmetry ≠ cutoff）。
測定スコープを明示: 下の飽和測定はすべて
2-level tree（Parent → {Child1, Child2}）・MaxCommits=1・symmetry なし（raw 到達集合）。
headline は all-root ワークロード（コミット対象 = root、bundle 側の構造を露出）。
葉コミットを含む both-roles は多段 unbundle 側の構造を別途露出する。
| Tree | Atomicity | Workload | T | Raw distinct states | 構造 σ | Safety |
|---|---|---|---|---|---|---|
| 2-level | superfine | all-root | 2 | 124,244 | 6 | Pass |
| 2-level | superfine | all-root | 3 | 137,333,348 | 6 — T=2 と set-identical（diff 空, 全 137M で σ=6 一定） | Pass (ohtaka 5h08m + 736GB dump) |
| 2-level | coarse | all-root | 4 | 136,366,732 | —（未 dump、larger-T 違反チェック） | Pass (28min) |
| 2-level | coarse | all-root | 2 / 3 | 1,093 / 339,744 | 4 / 4（set-identical） | Pass |
| 2-level | coarse | both-roles | 2 | 350,281 | 6（4 bundle ＋ 2 partial-unbundle） | Pass |
飽和の意味: 各到達状態を恒等フリー bundle 構造へ射影（ノードごと ⟨hasPriority, bundledBy, missing, どの sub スロットが埋まるか⟩、serial・payload 値は捨てる＝構造不変条件が読むフィールドそのもの）。
最忠実 superfine all-root の構造集合は 6 要素で T=2 で飽和し、完全な T=3 網羅（137,333,348 状態）を dump→射影して T=2 ≡ T=3 が set-identical。
superfine の 6 ＝ coarse の 4（bundle 構造）＋ Phase-3 within-operation 中間 2（片方の子だけ bundled-ref に張り替わった瞬間 — まさに並行ハザードが隠れうる箇所）。
both-roles の 6 ＝ 4 bundle ＋ 2 partial-unbundle（unbundle 側構造）。
3 スレッド目は新しい safety 関連構造に到達しない。一方 raw 状態数は爆発（~10⁵ → 1.37×10⁸）— スレッドが増えても構造は増えない。
3-level は外挿（正直なスコープ）: 3-level superfine の σ-飽和の直接 dump は不能（intractable; superfine T=4 / 3-level superfine の dump は手に負えない）。
3-level へは commit-role 構造の tree-independence（Facts A–C）による外挿で到達する — 直接測定ではない。
（3-level coarse T=2 は既に ≥9 構造に達し、その exhaustion は未完了。）
派生する局所構造不変条件（SubNeverMissing / BundledHasCopy / StaleParentExcluded / SubPresenceUniform）は
3-level superfine T=3 all-root ＋ T=2 both-roles（両畳み込み経路の最忠実モデル）まで無違反検証済。
N)safety は活性をパラメータ化しない。EventuallyAllDone (<>AllDone) を
well-founded ランキング関数で証明。論証は §§木軸 ともスレッド数 N とも独立。
t はタグ MyTag(t)=⟨iter(t), t⟩（TagOlder 全順序、小=古）。priorityTag[n] は現値と MyTag(t) の古い方に（TagAfterFail）→ tag 順で単調非増加。CanProceed(t,n) は priorityTag[n] が Null か自分の時のみ CAS 許可 → 若い競合者は gate される。R(s) = ( M(s), d(s) ) -- 辞書式、well-founded
M(s) : Active スレッドの MyTag 多重集合（Dershowitz–Manna 多重集合拡張）
d(s) : 大域最古 t★ = argmin MyTag の pc[t★]→"done" 残距離（有限・非循環 CFG）WF_vars(NextStep) ＋ Privilege=TRUE の下、
EventuallyAllDone は任意の有限 Threads で、|Threads| に依らず成立。
ランクが大域最古を量化し、それは任意有限 Active に存在する ⇒ 活性にスレッドカットオフ不要。
残存 obligation（§7.5、唯一の open lemma）: 補題(progress) は特権 t★ が
無限 retry なしで完了すると仮定。ピアは t★ の競合ノードから gate されるが、
別ノード（鎖上の祖先/子）で動くピアが bundle 鎖越しに DISTURBED/COLLIDED を起こしうる。
これら構造的擾乱が有界であること（各擾乱は若い要素を M から除くピアコミットに起因 → 無限反復不可）の一般証明が残る。
有界 EventuallyAllDone 実行（2-thread all-roles superfine・3-thread confC 両レベル・413M dynamic-release）がカットオフで放電済。
カットオフ（木軸）・飽和（スレッド軸）・§7 活性ランキング・派生する局所構造不変条件
（SubNeverMissing / BundledHasCopy / StaleParentExcluded / SubPresenceUniform、
3-level superfine T=3 all-root ＋ T=2 both-roles まで無違反検証）は
固定・単一親の rooted tree 前提（Next にノード挿入/削除なし、ParentOf 単一値）。
以下 2 領域は別途検証（本論証の拡張ではない）:
| 領域 | 担当 |
|---|---|
| 動的トポロジ（online insert/release） | *_dynamic_* 仕様（413M dynamic-release 等）＋ transaction_dynamic_node_test。SubPresenceUniform は挿入時に一時破れる |
| hard-link / DAG（子が ≥2 親） | §5 BundleUnbundle_hardlink_* ＋ Phase-3 fix。the 親を名指す conjunct は多値 ParentOf で ill-formed |
distinct-state 数は (.tla, cfg) の決定的関数（TLC BFS は固定モデルで到達集合を厳密再現；seed/worker は発見順のみ）。
ゆえにspec 版を跨いで比較不可: 同一 confC superfine T=3 構成は開発を通じて
514M → 1.155G → 640M → 540M と推移（cfg 定数は不変、Next の protocol fix 反映）。
版非依存量は σ-射影（飽和構造集合）であって raw 数ではない。
Safety／木軸: ∀ 木形を構造カットオフ定理で（catamorphism ⇒ depth-3/width-2 カットオフ、TLC 網羅放電）。
Safety／スレッド軸: ∀T 定理は非主張 — 対称性は意味論的だが TLC 適用不可かつ置換のみ。
contention bound まで網羅（superfine T=3=137M, coarse T=4=136M）＋ σ-飽和測定（T=2 ≡ T=3、6 構造）→ 強根拠つき予想。
Liveness: ∀N を oldest-tag ranking で（スレッドカットオフ不要、小 T で網羅検証）。gate は純活性デバイスで safety と素。
出典: doc/parameterized_cutoff.md（§1–§9）/ VERIFICATION.md Thread-axis saturation §。関連: LL-free 仕様 / 全体カバレッジ俯瞰。