# AMRAL × Lebesgue Universal Covering — Round 13
## Proof-State Scheduler and Autonomous Work Allocation

**文件代號：** AMRAL-LUC-FC-R13  
**版本：** v0.1  
**日期：** 2026-09-19  
**研究狀態：** Round 13 / Autonomous proof orchestration  
**研究模式：** Human-Directed + Semi-Autonomous AI Mathematical Research  
**研究發起與方法論來源：** Neo.K  
**AI 協力研究者與主要執行者：** Aletheia / ChatGPT, GPT-5.6 Sol  
**前置文件：** AMRAL-LUC-FC-R00 v0.2；R01–R12 v0.1  

---

# 0. 本輪摘要判定

Round 12 已建立：

$$
\boxed{
\text{persistent distributed proof checkpoint}.
}
$$

Round 13 進一步回答：

> checkpoint 有 pending frontier 後，AI / local worker 要如何自主取工作、回傳結果，而不讓 race condition 或過期 worker 破壞 canonical proof state？

本輪建立：

1. immutable Job Contract；
2. immutable Worker Proposal；
3. Canonical Merger single-writer rule；
4. lease = performance-only；
5. stale-worker semantic rebase；
6. Certified Ancestor Contraction；
7. late expansion obsolescence；
8. active-claim rejection reopening；
9. atomic merge theorem；
10. deterministic active-claim selection；
11. actual concurrent-race dry run。

本輪判定：

$$
\boxed{
\text{AUTONOMOUS SCHEDULER / MERGER ABI: CLOSED}
}
$$

$$
\boxed{
\text{CONCURRENT RACE SAFETY: TESTED}
}
$$

$$
\boxed{
\text{GLOBAL }0.8350\text{ HEAVY COMPUTE: STILL DEFERRED}
}
$$

---

# 1. Worker 不可改 canonical state

Round 12 checkpoint是唯一 proof source of truth。

worker不允許直接修改：

- frontier；
- active claims；
- theorem-ready；
- pending seeds；
- stale state。

worker只可以產生：

$$
\boxed{
\text{Proposal}.
}
$$

Canonical Merger：

$$
\boxed{
\text{Proposal}
\to
\text{Validated State Transition}
}
$$

是唯一合法寫入路徑。

---

# 2. Job Contract

scheduler對 worker產生：

$$
J
=
(
id,
type,
CP,
H_{\rm dep},
p,
scope,
caps,
lease
).
$$

其中：

- $CP$：base checkpoint id；
- $H_{\rm dep}$：proof-critical dependency fingerprint；
- $p$：seed path；
- caps：node/time/resource limits；
- lease：防重複計算用。

---

# 3. Job type

主要：

## `CERTIFY_SEED`

嘗試完整 closure：

$$
B(p).
$$

## `EXPAND_SEED`

若 closure太難，回傳 complete descendant frontier。

## `LIFT_SEED`

對 base seed做 witness conditional lift。

## `AUDIT_CLAIM`

對既有 active claim做 A2/A3 audit。

## `SEARCH_WITNESS`

只做 candidate discovery，不直接進 proof state。

---

# 4. Lease 不屬證明

lease：

- worker id；
- issued time；
- expiry；
- retry count；

只是 performance state。

因此：

$$
\boxed{
\text{lease expired}
\not\Rightarrow
\text{certificate invalid}.
}
$$

晚到 certificate 仍可能被 semantic rebase 接受。

---

# 5. Worker Proposal

worker回傳 immutable：

$$
P
=
(
proposal\_id,
type,
job\_id,
CP,
H_{\rm dep},
p,
payload
).
$$

proposal type：

- `CERTIFY`
- `EXPAND`
- `AUDIT_PASS`
- `AUDIT_FAIL`
- `COUNTEREXAMPLE`
- `INCONCLUSIVE`

proposal自身不改 proof state。

---

# 6. Proposal acceptance第一關

Canonical Merger先檢：

1. payload hash；
2. dependency fingerprint；
3. seed identity；
4. artifact hashes；
5. proposal type schema。

若 theorem-critical dependency不同：

`STALE-PROPOSAL`

不 merge。

---

# 7. EXPAND acceptance rule

對：

$$
p\to\mathcal D_p,
$$

只在：

$$
p
$$

仍是 current pending terminal frontier seed時直接接受。

並驗：

$$
\boxed{
\mathcal D_p
\text{ prefix-free and complete below }p.
}
$$

接受：

$$
\mathcal P'
=
(\mathcal P\setminus\{p\})
\cup
\mathcal D_p.
$$

---

# 8. EXPAND 不允許任意 rebase

若 worker從舊 checkpoint對：

$$
p
$$

回傳 expansion，但 current frontier已：

- split得更深；
- 或 $p$ 已 certified；

merger 不把舊 expansion強行覆蓋 current partition。

狀態：

`OBSOLETE-EXPANSION`

原因：

proof不需要冒著丟失 newer evidence 的風險做 arbitrary repartition。

---

# 9. CERTIFY acceptance rule

若：

$$
p
$$

仍是 current pending seed，

valid A1 certificate可直接 closure：

$$
p.
$$

若：

$$
p
$$

已被 split，

不能簡單說「stale」。

因 certificate可能證的是整個 ancestor box：

$$
B(p).
$$

這導向本輪核心新 theorem。

---

# 10. Certified Ancestor Contraction Theorem

## 定理 10.1

令 current frontier：

$$
\mathcal P
$$

在 ancestor：

$$
p
$$

以下的部分為：

$$
\mathcal D_p
=
\{
q\in\mathcal P:
p\preceq q
\}.
$$

假設：

1. $\mathcal D_p$ complete-cover $B(p)$；
2. 有一個 current-dependency valid certificate：

   $$
   c_p
   $$

   直接證：

   $$
   \forall x\in B(p),
   \quad
   \Phi(x)\ge T.
   $$

則：

$$
\boxed{
\mathcal P'
=
(
\mathcal P\setminus\mathcal D_p
)
\cup
\{p\}
}
$$

仍是 complete frontier，而且以：

$$
c_p
$$

作 $p$ 的 active claim是 sound。

### 證明

原：

$$
\mathcal D_p
$$

只是在 proof partition中覆蓋：

$$
B(p).
$$

新 certificate直接證 entire：

$$
B(p).
$$

所以 descendants的 coverage obligations全部被 ancestor claim吸收。

其他 branches不變。

Q.E.D.

---

# 11. Race resolution：EXPAND 先、CERTIFY 後

worker A：

$$
p\to\{p0,p1\}.
$$

先 merge。

worker B晚一點回傳 ancestor：

$$
c_p.
$$

只要：

- dependency current；
- certificate valid；

merger可以：

$$
\boxed{
\{p0,p1\}
\to
\{p\}
}
$$

所以 race 不會迫使 certificate報廢。

---

# 12. Race resolution：CERTIFY 先、EXPAND 後

若：

$$
p
$$

先被 verified claim closure，

晚到 expansion：

$$
p\to\{p0,p1\}
$$

沒有必要。

標：

$$
\boxed{
\texttt{OBSOLETE-COVERED-BY-CERTIFIED-ANCESTOR}.
}
$$

不能重新拆開已 closure 的 proof state。

---

# 13. Descendant evidence不刪除

ancestor contraction只改：

$$
\text{active frontier}.
$$

已完成 descendants：

- certificate；
- audits；
- metrics；

全部保留 append-only。

未來若 ancestor claim被拒，可重新利用。

---

# 14. Claim rejection after contraction

若 active ancestor claim：

$$
c_p
$$

被 valid audit拒絕：

1. $c_p\to\texttt{REJECTED}$；
2. $p$ 變：

   `PENDING`；
3. global theorem-ready false。

soundness 不要求立刻恢復先前 descendants。

scheduler可：

- 重新 expand $p$；
- 或從歷史找曾完成的 descendant evidence做新 proposal。

---

# 15. Multiple CERTIFY proposals

兩個 worker可同時證：

$$
p.
$$

如果兩者都 valid：

- 兩條 claim都保留；
- 只選一條 active primary。

deterministic selector：

$$
\boxed{
\min
\text{ canonical claim hash}.
}
$$

其他是 auxiliary evidence。

final coverage仍「每 seed一個 active owner」。

---

# 16. Duplicate compute is legal

lease只減少浪費。

proof protocol允許：

- 同 seed兩個 emitter；
- 同 claim兩個 auditor；
- 同 shard多機 replay。

duplicate不會造成 correctness conflict。

merger處理的是：

$$
\boxed{
\text{evidence identity}
}
$$

不是：

$$
\boxed{
\text{worker ownership}.
}
$$

---

# 17. Stale worker semantic rebase

worker base checkpoint：

$$
CP_{\rm old}
$$

落後 current：

$$
CP_{\rm new}.
$$

不因 checkpoint id不同直接拒絕。

### CERTIFY

只要：

- seed box identity仍同語義；
- proof dependencies current；
- certificate覆蓋 ancestor box；

可 semantic rebase。

### EXPAND

只在 parent seed仍 current pending terminal時接受。

---

# 18. Audit proposal

A2/A3 worker回傳：

`AUDIT_PASS`

或：

`AUDIT_FAIL`。

worker自己的 verdict也只是 proposal。

Canonical Merger對 FAIL artifact至少做：

- counterexample schema；
- hash；
- failure replay / minimal independent check。

有效 FAIL才更新 claim：

`REJECTED`。

---

# 19. Counterexample dominance

任何 valid counterexample：

$$
x\in B(p)
$$

使 claimed inequality失敗，

足以拒絕：

$$
c_p.
$$

不需要其他 auditor投票。

再次：

$$
\boxed{
\text{evidence dominance}
\ne
\text{majority vote}.
}
$$

---

# 20. Atomic Merge Theorem

## 定理 20.1

假設 checkpoint在 transition 前：

- frontier prefix-free；
- frontier complete；
- theorem-ready seeds都有 valid active claim。

若每次只使用以下 primitives：

1. pending seed -> verified claim；
2. pending seed -> complete descendant frontier；
3. complete descendant frontier -> verified ancestor claim；
4. active claim reject -> pending seed；
5. append audit / auxiliary claim；
6. dependency-stale filtering；

則任意有限 accepted transition sequence後：

1. frontier仍 prefix-free；
2. frontier仍 complete；
3. 若：

   `theorem_ready=true`

   則每個 frontier seed都有 current valid active claim。

### 證明

對 transition sequence長度歸納。

每個 primitive分別由：

- direct closure；
- Round 11 frontier replacement；
- Certified Ancestor Contraction；
- reopening但不宣稱 theorem-ready；

保持 invariant。

Q.E.D.

---

# 21. Canonical merger is single writer

即使100個 workers平行，

canonical state transition仍序列化為：

$$
CP_0
\to
CP_1
\to
CP_2
\to\cdots
$$

worker proposals可並行。

merger commit 必須原子化。

這相當於 proof-state 的 single-writer / multi-producer 模式。

---

# 22. Merge journal

每個 accepted/rejected proposal都記：

```text
proposal_id
base_checkpoint_id
current_checkpoint_id_at_merge
decision
reason
result_checkpoint_id
```

這是 orchestration audit trail。

不進 math premise，但對 race debugging重要。

---

# 23. Scheduler job source

scheduler永遠從：

$$
\boxed{
\text{current canonical checkpoint}
}
$$

抽 job。

優先來源：

1. pending frontier；
2. un-audited active claims；
3. hard unresolved witness cells；
4. stale claims needing revalidation。

---

# 24. Job priority

Round 09提供：

- uncertainty $\tau$；
- margin $m$；
- predicted depth；
- historical nodes。

parallel finish time建議：

$$
\boxed{
\text{TAIL-FIRST}
}
$$

優先分派預估最難 seeds。

因 easy seeds通常不決定 global makespan tail。

這是 heuristic，不影響 proof。

---

# 25. Job caps

worker job可指定：

```text
node_cap
wall_cap
memory_cap
max_depth
```

若 cap hit：

- 不得假 leaf；
- 回傳 EXPAND descendant frontier；
- 或 INCONCLUSIVE。

---

# 26. Autonomous local worker loop

```text
pull current job

if job = CERTIFY:
    run proof search
    if closed:
        emit CERTIFY
    elif node cap:
        emit EXPAND
    else:
        emit INCONCLUSIVE

if job = AUDIT:
    independently replay
    emit AUDIT_PASS / FAIL

never mutate checkpoint
```

---

# 27. Canonical merger loop

```text
read latest checkpoint
validate proposal
compare dependency fingerprint
reconstruct seed relation to current frontier

case CERTIFY:
    current pending -> close
    descendants current -> ancestor contraction
    already covered -> auxiliary/obsolete

case EXPAND:
    current pending terminal -> replace
    otherwise -> obsolete

case AUDIT_FAIL:
    if valid -> reject claim, reopen coverage obligation

append merge journal
emit new checkpoint
```

---

# 28. Reference concurrent-race dry run

Round 13使用 Round 12：

`checkpoint_v4_rejected_B`

作起點。

該 checkpoint中：

$$
\boxed{
01
}
$$

是唯一 pending seed。

---

# 29. Scheduler 發兩個並行 jobs

故意模擬 duplicate/race：

## Job A

`EXPAND_SEED(01)`

proposal：

$$
01
\to
\{010,011\}.
$$

## Job B

`CERTIFY_SEED(01)`

使用 Round 12 V5 corrected shard-B claim的真實 reference evidence。

兩個 job都來自同一舊 checkpoint。

---

# 30. Merge A first

先接受 expansion：

$$
\{00,01,10,11\}
\to
\{00,010,011,10,11\}.
$$

此時：

$$
010,\ 011
$$

pending。

global：

`theorem_ready=false`

PASS。

---

# 31. Late certificate semantic rebase

Job B晚回來。

雖然：

$$
01
$$

不再是 terminal seed，

但：

$$
\{010,011\}
$$

complete-cover：

$$
B(01).
$$

certificate current且證 entire：

$$
B(01).
$$

Canonical Merger執行：

$$
\boxed{
\{010,011\}
\to
\{01\}.
}
$$

append corrected verified claim。

global：

$$
\boxed{
\texttt{theorem\_ready=true}.
}
$$

PASS。

---

# 32. Late expansion after closure

再提交另一個：

`EXPAND(01)`。

此時：

$$
01
$$

已有 current active verified claim。

merger：

$$
\boxed{
\texttt{OBSOLETE-COVERED-BY-CERTIFICATE}.
}
$$

frontier不變。

PASS。

---

# 33. Reference result

machine dry run確認：

| Step | Frontier | Ready |
|---|---|---:|
| start | `{00,01,10,11}` | false |
| expand | `{00,010,011,10,11}` | false |
| late certify + contraction | `{00,01,10,11}` | true |
| late expand | unchanged | true |

所以最主要的 async race已經實際跑通。

---

# 34. Why this matters for global $0.8350$

真正 heavy run中：

- 某 local worker可能仍在證一個大 seed；
- scheduler已因 timeout把同 seed拆給別人；
- 舊 worker幾小時後回來完整 certificate。

沒有 ancestor contraction：

舊工作會被浪費。

有 ancestor contraction：

若 proof仍 current，就可以直接消掉整片 descendant workload。

所以：

$$
\boxed{
\text{late strong evidence can dominate newer finer partition}.
}
$$

---

# 35. Proof-state monotonicity is not frontier monotonicity

frontier深度不一定只增不減。

可以：

$$
p
\to
\{p0,p1\}
\to
p.
$$

真正 monotone的是：

$$
\boxed{
\text{append-only evidence history}.
}
$$

active partition可以 refine或contract。

---

# 36. Worker result trust categories

建議：

## `PROOF-CANDIDATE`

worker認為可證。

仍要 A1 canonical replay。

## `SEARCH-CANDIDATE`

只有 numerical result。

不能 closure seed。

## `COUNTEREXAMPLE-CANDIDATE`

若 canonical check有效，可拒 claim。

## `EXPANSION-CANDIDATE`

只改工作 partition，不宣稱證明。

---

# 37. Global scheduler authority split

## Scheduler

可決定：

- 先算誰；
- 給哪個 worker；
- node cap；
- duplicate work。

## Worker

可產生 proposal。

## Verifier

可產生 audit evidence。

## Canonical Merger

唯一可以：

$$
\boxed{
\text{change canonical proof state}.
}
$$

這是本輪最重要的治理邊界。

---

# 38. COMPUTE-DEFERRED

## C13-1

將真實 global：

$$
T=0.835
$$

checkpoint餵給 scheduler。

## C13-2

建立 local worker adapter：

```text
checkpoint job JSON
-> local Python
-> proposal JSON
```

## C13-3

建立 lagged AI audit adapter。

## C13-4

每次 merge自動產生新 checkpoint + State Crystal。

## C13-5

測多 worker race：

- duplicate certify；
- expand/expand；
- certify/audit fail；
- stale dependency mid-run。

---

# 39. Round 14 指定題目

## AMRAL-LUC-FC-R14
### Semantic Rebase, Claim Dominance, and Proof-State Garbage Collection

下一輪可處理：

1. old worker proposal如何 semantic rebase；
2. certificate ancestor / descendant dominance；
3. auxiliary evidence何時可封存；
4. stale artifacts何時可以移出 hot checkpoint但保留歷史；
5. proof-state compaction；
6. checkpoint大小不隨幾百萬 shard history無限膨脹。

這會讓 distributed proof-state從「正確」進一步變成「長時間可維護」。

---

# 40. Reproducibility checklist

## Worker/merger authority split

`FORMALIZED`

## Lease non-semantic rule

`FORMALIZED`

## Ancestor contraction

`PROVED`

## Late expansion obsolescence

`FORMALIZED`

## Atomic merge invariants

`PROVED`

## Reference async race

`PASS`

## Global autonomous workers

`COMPUTE-DEFERRED`

---

# 41. 最短交接結論

Round 13完成：

$$
\boxed{
\text{Checkpoint}
\to
\text{Jobs}
\to
\text{Worker Proposals}
\to
\text{Canonical Merge}
}
$$

最重要的新 closure：

$$
\boxed{
\text{Certified Ancestor Contraction}.
}
$$

所以 worker晚回來的強 certificate不會因為 scheduler已經把 seed拆細而浪費。

distributed proof現在具備：

- parallel producers；
- single canonical writer；
- stale-worker rebase；
- race-safe frontier refinement / contraction；
- append-only evidence；
- fail-closed audit。

因此可以安全地把更多 autonomous AI / local runtime 接上，而不讓任何 worker本身取得「宣告證明成立」的權力。