# AMRAL × Lebesgue Universal Covering — Round 12
## Global Checkpoint Crystal and Multi-AI Shard Audit Protocol

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

---

# 0. 本輪摘要判定

Round 11 已把 global exhaustive proof 改寫為：

$$
\boxed{
\text{complete prefix-free frontier}
+
\text{independently verifiable shards}.
}
$$

Round 12 再進一步：

> 不只把每一輪結果存成研究摘要，而是把**整個 distributed proof state 本身**存成可恢復、可審計、可失效、可修正的 Checkpoint Crystal。

本輪完成：

1. machine-readable checkpoint schema；
2. proof-critical dependency fingerprint；
3. performance-only dependency separation；
4. append-only claim ledger；
5. audit ledger；
6. stale propagation；
7. local rejection / global aggregate invalidation；
8. append-only correction；
9. checkpoint sufficiency theorem；
10. multi-AI lagged audit protocol；
11. actual Round 11 reference proof-state transition dry run。

本輪判定：

$$
\boxed{
\text{DISTRIBUTED PROOF CHECKPOINT ABI: CLOSED}
}
$$

$$
\boxed{
\text{STALE / CORRECTION SEMANTICS: CLOSED}
}
$$

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

---

# 1. Checkpoint Crystal 不再只是摘要

過去 State Crystal 的用途：

> 用最少資訊讓下一個對話知道研究推到哪裡。

Round 12 增加第二層：

> 用最少但充分的**機器可讀 proof state**，讓任何 worker / AI / verifier 可以恢復 global computation，而不依賴過去 scheduler 歷史。

因此一個 checkpoint 包含：

$$
\boxed{
\mathsf{CP}
=
(
R,
T,
D,
\mathcal P,
\mathcal C,
\mathcal A,
G
)
}
$$

其中：

- $R$：root identity；
- $T$：target；
- $D$：dependency bundle；
- $\mathcal P$：current frontier；
- $\mathcal C$：claim ledger；
- $\mathcal A$：audit ledger；
- $G$：aggregate state。

---

# 2. Proof-critical dependencies

定義：

$$
D_{\rm proof}
$$

至少包含：

1. global root-domain hash；
2. target：
   $$
   T;
   $$
3. split-semantics hash；
4. geometry / common-core hash；
5. arithmetic-policy hash；
6. witness-catalog hash；
7. verifier-semantics hash；
8. certificate-format-semantics hash。

定義：

$$
\boxed{
H_{\rm dep}
=
H(D_{\rm proof}).
}
$$

每個 shard claim 都保存：

$$
H_{\rm dep}^{\rm claim}.
$$

---

# 3. Performance-only dependencies

以下資訊影響成本，但不影響 theorem meaning：

- scheduler；
- worker count；
- queue order；
- machine identity；
- wall-time limit；
- node cap；
- cache；
- priority score。

記為：

$$
D_{\rm perf}.
$$

它可以進 checkpoint，但：

$$
\boxed{
D_{\rm perf}
\text{ 不進 }H_{\rm dep}.
}
$$

所以換機器／換 scheduler 不會讓 valid shard 無謂 stale。

---

# 4. Dependency Eligibility Rule

claim：

$$
c
$$

只有在：

$$
\boxed{
H_{\rm dep}^{c}
=
H_{\rm dep}^{\rm current}
}
$$

時，才有資格進 final aggregate。

若不相等：

$$
\boxed{
\operatorname{status}_{\rm effective}(c)
=
\texttt{STALE}.
}
$$

不要求修改舊 claim file。

staleness 可以由 validator動態計算。

---

# 5. Stale-Safety Theorem

## 定理 5.1

若 finalizer只接受：

$$
H_{\rm dep}^{c}
=
H_{\rm dep}^{\rm current}
$$

的 claims，則任何 proof-critical dependency更新後，所有依賴舊語義的 claim 都無法靜默進入新的 final proof。

### 證明

舊 claim：

$$
H_{\rm dep}^{c}
=
H_{\rm old}.
$$

新 checkpoint：

$$
H_{\rm dep}^{\rm current}
=
H_{\rm new}.
$$

若 proof-critical bundle改變，cryptographic canonical payload也改變：

$$
H_{\rm old}\ne H_{\rm new}
$$

除了 hash collision。

validator將其分類：

`STALE`

並排除。

Q.E.D.

---

# 6. Selective invalidation

不是每次 dependency change 都一定 stale 全部 shards。

可將 dependency拆成：

$$
D_{\rm global}
$$

與：

$$
D_{\rm local}(c).
$$

例如：

## Global

- target；
- root；
- split semantics；
- common arithmetic policy。

global change通常影響全部 claims。

## Witness-local

若某 shard只使用：

$$
B_7
$$

而另一些使用 Fourier witness，

修改 Fourier witness geometry只需 stale使用該 geometry hash的 claims。

因此 production 可進一步存：

```text
claim_dependency_hashes:
    global
    witness_ids_used
    geometry_modules_used
    arithmetic_policy
    verifier_modes_used
```

本輪 reference schema先使用單一 aggregate fingerprint。

---

# 7. Claim ledger

claim 永遠 append-only。

基本狀態：

## `EMITTED`

certificate bytes已存在。

## `VERIFIED-INDEPENDENT-REPLAY`

canonical independent verifier PASS。

## `REJECTED`

找到有效 failure。

## `STALE`

dependency不再 current。

## `SUPERSEDED`

被新 claim取代。

## `CORRECTED`

歷史標記；正式可用證據仍應是一條新的 verified claim。

---

# 8. Why append-only

不覆寫錯誤 shard 的理由：

1. 可追 correction ancestry；
2. 可重現當時錯在哪；
3. lagged verifier能引用原 claim；
4. future audit可比較；
5. 防止「修掉歷史後看起來從沒錯過」。

因此：

$$
\boxed{
\text{evidence history monotone}
}
$$

但：

$$
\boxed{
\text{belief / active status 可回退}.
}
$$

---

# 9. Claim supersession

若：

$$
c_2
$$

修正：

$$
c_1,
$$

則：

```text
c2.supersedes = c1.claim_id
```

active claim selection排除被 supersede 的 ancestor。

舊 claim仍保留在 ledger。

---

# 10. Audit ledger

audit record 至少：

```text
audit_id
claim_id
audit_level
verifier_hash
result
failure_class
counterexample
metrics
auditor
timestamp
```

audit 自身也 append-only。

---

# 11. Audit levels

本輪 formalize：

## A0 — Emitter Self-Check

不能單獨進 final theorem。

## A1 — Canonical Independent Replay

每個 final terminal shard必須至少一個：

$$
\boxed{
\text{A1 PASS}.
}
$$

checkpoint 的：

`theorem_ready`

把它當必要條件。

## A2 — Independent Implementation / Lagged AI

第二實作、第二 AI、lagged branch。

它不取代 A1。

## A3 — Adversarial Mathematical Audit

主動找：

- branch omission；
- false core；
- stale dependency；
- sign error；
- arithmetic mismatch；
- hidden symmetry assumption。

---

# 12. Multi-AI 不是 majority vote

如果：

- AI-A：PASS；
- AI-B：PASS；
- AI-C：FAIL，且給出 valid counterexample；

則結果：

$$
\boxed{
\text{FAIL}.
}
$$

不是：

$$
2:1\text{ PASS}.
$$

同理：

100 個 PASS也不會消除一個有效反例。

---

# 13. Lagged verifier

沿用 Round 00 設計：

secondary verifier預設落後 canonical：

$$
2\text{–}4
$$

rounds。

對 shard：

1. 先讀指定 checkpoint；
2. 不讀 future corrections；
3. 獨立重建；
4. 回傳 audit。

這降低 information contamination。

---

# 14. Checkpoint validity

checkpoint本身要滿足：

1. payload hash；
2. frontier prefix-free；
3. frontier complete；
4. dependency fingerprint internal consistency；
5. claim ids unique；
6. active claim selection deterministic；
7. every theorem-ready seed exactly one eligible active claim；
8. eligible claim有 A1 PASS；
9. no duplicate active coverage。

---

# 15. Theorem-Ready State

對 current frontier：

$$
\mathcal P,
$$

如果對每個：

$$
p\in\mathcal P
$$

恰有一條 active claim：

$$
c_p
$$

使：

1. dependency current；
2. status：
   `VERIFIED-INDEPENDENT-REPLAY`；
3. 至少一個 A1 PASS；
4. 無 newer rejection / supersession；
5. frontier complete；

則：

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

這只代表：

> checkpoint 所宣告的 scope 已完整 certified。

scope仍可能是 Round 10 local reference，而非全球 Lebesgue theorem。

---

# 16. Scope is proof-critical metadata

永遠必須保存：

```text
scope
global_lebesgue_claim
```

Round 12 reference：

```text
scope = ROUND10-LOCAL-REFERENCE-SHARDS
global_lebesgue_claim = false
```

所以即使：

`theorem_ready=true`

也不能被誤讀成：

$$
a_{\mathrm{Leb}}\ge0.835.
$$

---

# 17. Checkpoint Sufficiency Theorem

## 定理 17.1

若 checkpoint 保存：

1. root identity；
2. current complete frontier；
3. current proof dependencies；
4. complete shard claims + certificate hashes；
5. pending frontier；
6. deterministic split semantics；

則為了**繼續或驗證 proof computation**，不需要 scheduler history。

### 理由

complete seeds：

- 可由 certificate hash重新取得證據；
- 可獨立 replay。

pending seeds：

- seed path + root + split semantics足以重建 box；
- 可重新派給任意 worker。

歷史：

- 哪台機器跑過；
- 先跑哪個 seed；
- 曾經排隊幾次；

都不影響 domain coverage。

所以：

$$
\boxed{
\text{checkpoint crystal 是 global proof continuation 的充分狀態}.
}
$$

---

# 18. Local rejection propagation

若：

$$
c_B
$$

只覆蓋 shard-B seeds，而 audit證其錯誤：

$$
c_B\to\texttt{REJECTED},
$$

則：

- shard-A claim仍可保留；
- shard-C claim仍可保留；
- B seeds變 pending；
- global aggregate不再 theorem-ready；
- global merge hash / Merkle summary stale。

所以 invalidation是：

$$
\boxed{
\text{local evidence invalidation}
+
\text{global aggregate invalidation}.
}
$$

不是全系統重算。

---

# 19. Correction propagation

若 corrected claim：

$$
c_B'
$$

被 append，且：

$$
c_B'.supersedes=c_B,
$$

並通過 current A1 audit，

則 B seeds重新有 eligible active claim。

如果其餘 seeds一直 valid：

$$
\boxed{
\text{global theorem-ready 可恢復}.
}
$$

不必重驗與 correction沒有依賴關係的 sibling certificate bytes。

final merger仍應重新計算 global aggregate summary / Merkle root。

---

# 20. Proof-critical change propagation

若 arithmetic policy：

$$
A_1
\to
A_2,
$$

且所有 shards原本都依賴：

$$
A_1,
$$

則：

$$
\boxed{
\text{全部舊 claims effective status = STALE}.
}
$$

checkpoint變：

`NOT-THEOREM-READY`

直到重新驗證／重發 compatible claims。

---

# 21. Performance-only change

若只有：

$$
\text{scheduler v1}
\to
\text{scheduler v2},
$$

而 proof-critical bundle不變，

則：

$$
H_{\rm dep}
$$

不變。

所有 valid shard claims保持 eligible。

所以：

$$
\boxed{
\text{換 scheduler 不需要重證。}
}
$$

---

# 22. Reference checkpoint dry run

Round 12以 Round 11 的 reference sharded proof為 source。

frontier：

$$
\boxed{
\{00,01,10,11\}
}
$$

shards：

- A：$\{00,11\}$；
- B：$\{01\}$；
- C：$\{10\}$。

全部已有 Round 11 independent replay PASS。

---

# 23. Reference Checkpoint V1

建立：

`checkpoint_v1.json`

狀態：

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

但 scope：

$$
\boxed{
\texttt{ROUND10-LOCAL-REFERENCE-SHARDS}
}
$$

以及：

$$
\boxed{
\texttt{global\_lebesgue\_claim}=false.
}
$$

---

# 24. Transition V2：performance-only

只改：

$$
\text{scheduler hash}.
$$

proof-critical fingerprint不變。

validator：

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

PASS。

---

# 25. Transition V3：proof-critical arithmetic change

將：

$$
e_{\rm fp}=10^{-8}
$$

的 reference policy改成：

$$
2\times10^{-8}
$$

而不重發 shards。

new dependency fingerprint改變。

舊三 shard claims全部：

$$
\boxed{
\texttt{STALE}.
}
$$

frontier四個 seeds全部 pending。

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

PASS。

---

# 26. Transition V4：local shard rejection

在原 proof dependencies下，把 shard-B claim標：

`REJECTED`

siblings A/C保留。

結果：

- seeds：

  $$
  00,10,11
  $$

  仍有有效 claims；

- seed：

  $$
  01
  $$

  pending；

- aggregate：

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

PASS。

---

# 27. Transition V5：append-only correction

新增：

`claim-shard-B-v2-corrected`

並：

```text
supersedes = claim-shard-B-v1
```

新 claim有 A1 PASS。

舊 rejected claim仍留在 ledger。

validator重新得到：

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

PASS。

---

# 28. Reference transition summary

Round 12 實際 machine test得到：

| State | Change | theorem_ready |
|---|---|---:|
| V1 | baseline | `true` |
| V2 | scheduler only | `true` |
| V3 | arithmetic proof dependency | `false` |
| V4 | shard-B rejected | `false` |
| V5 | append corrected B claim | `true` |

因此：

$$
\boxed{
\text{stale / rejection / correction semantics 實際跑通。}
}
$$

---

# 29. Persistent checkpoint naming

建議 production：

```text
AMRAL_LUC_FC_CP_<target>_<sequence>_<short-hash>.json
```

例如：

```text
AMRAL_LUC_FC_CP_08350_000127_ab12cd34.json
```

每次 checkpoint append。

不要覆寫唯一的：

`latest.json`

作為唯一歷史。

可另有：

`LATEST_POINTER.json`

只當方便導航。

---

# 30. Checkpoint lineage

每個：

$$
\mathsf{CP}_n
$$

保存：

```text
checkpoint_id
parent_checkpoint_id
```

形成：

$$
\boxed{
\text{append-only checkpoint DAG / chain}.
}
$$

若有兩個 worker同時從同 checkpoint分叉，

可存在：

$$
CP_{n+1}^{(A)},
\qquad
CP_{n+1}^{(B)}.
$$

之後 merge成：

$$
CP_{n+2}.
$$

merge必須解：

- seed ownership；
- duplicate claims；
- supersession；
- dependency compatibility。

---

# 31. Multi-AI audit output destination

canonical proof state：

`99_State_Crystals`

secondary AI audit artifacts：

`01_Verification_Expansion`

audit文件命名：

```text
AUDIT_<checkpoint_id>_<shard_id>_<auditor>_<hash>.json
```

canonical conversation ingest audit後：

- 不直接覆寫 shard；
- append audit ledger；
- 必要時 append correction claim；
- 產生新 checkpoint crystal。

---

# 32. Mandatory claim ancestry

任何 correction至少要記：

```text
claim_id
supersedes
reason
source_certificate_hash
new_certificate_hash
audit_ids
```

若只是 dependency重驗、不改 bytes：

`new_certificate_hash`

可以相同，

但 claim id與 audit evidence必須新。

---

# 33. Stale aggregate

任何 terminal claim stale / rejected時：

global aggregate必須標：

$$
\boxed{
\texttt{NOT-THEOREM-READY}
}
$$

即使：

- 99.999% seeds仍 verified；
- 只剩一個 tiny seed。

coverage proof沒有百分比通融。

---

# 34. Partial progress metrics

雖不能把 99% 當 theorem，

checkpoint可以報：

```text
verified_seed_count
pending_seed_count
verified_domain_weight_estimate
verified_nodes
pending_nodes_estimate
hard_shards
```

這些是 progress metadata。

不進 final proof premise。

---

# 35. Global $0.8350$ production checkpoint

真正 heavy run應建立：

```text
scope = GLOBAL-F3-BASE-ATLAS-T08350
global_lebesgue_claim = conditional
```

在 complete base + witness certificate全部完成前：

```text
global_lebesgue_claim = false
aggregate_status = IN-PROGRESS
```

只有 final independent merge + publication arithmetic gate通過後才升：

```text
global_lebesgue_claim = true
```

---

# 36. Publication gate

本輪建議 final：

$$
a_{\mathrm{Leb}}\ge0.8350
$$

宣告至少需要：

1. complete global frontier；
2. every terminal seed exactly one active claim；
3. all active claim dependencies current；
4. every active claim A1 PASS；
5. no active reject/stale；
6. global merge PASS；
7. forest identities；
8. publication-grade arithmetic theorem；
9. source / certificate hashes；
10. correction ancestry complete。

A2/A3 額外提高可信度，但不以投票取代 hard gates。

---

# 37. Files produced in Round 12

本輪 package包含：

- canonical Round 12 MD；
- State Crystal；
- checkpoint JSON schema；
- Multi-AI audit protocol；
- checkpoint validator；
- state-transition demo；
- reference checkpoint V1–V5；
- transition summary；
- source Round 11 shard metadata needed by demo；
- validation report。

---

# 38. COMPUTE-DEFERRED

## C12-1

把 global：

$$
T=0.835
$$

heavy run的 current frontier真正寫成 checkpoint crystal。

## C12-2

讓 lagged verifier chat開始接 shard audit jobs。

## C12-3

建立 automatic stale detection against：

- geometry hash；
- arithmetic hash；
- witness hash；
- verifier hash。

## C12-4

把本地端 worker輸出直接 ingest成 claim ledger。

---

# 39. Round 13 指定題目

## AMRAL-LUC-FC-R13
### Proof-State Scheduler and Autonomous Work Allocation

若 heavy global compute尚未回來：

下一輪可把 checkpoint直接變成 autonomous scheduler interface：

1. 從 pending frontier估 cost；
2. 分派 base-atlas job / B7 lift job；
3. 自動選 local / cloud / secondary AI；
4. 依 node cap回收 descendant frontier；
5. 自動更新 checkpoint；
6. 不讓任何 worker直接改 canonical truth；
7. canonical merger是唯一 state transition authority。

如果 global compute已回來：

直接 ingest真實 checkpoint。

---

# 40. Reproducibility checklist

## Checkpoint schema

`IMPLEMENTED`

## Dependency fingerprint

`IMPLEMENTED`

## Stale-safety semantics

`PROVED + TESTED`

## Performance-only non-invalidation

`TESTED`

## Local rejection propagation

`TESTED`

## Append-only correction

`TESTED`

## Multi-AI audit protocol

`SPECIFIED`

## Reference checkpoint transition V1–V5

`PASS`

## Global $0.8350$ checkpoint

`COMPUTE-DEFERRED`

---

# 41. 最短交接結論

Round 12 把「雲端同步結晶法」從研究記憶提升為：

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

現在一個 checkpoint crystal 已能回答：

- global root 是什麼；
- frontier在哪；
- 哪些 shard已證；
- 哪些 pending；
- 每個 claim依賴哪個 proof version；
- 哪些 stale；
- 哪些被拒；
- 哪些是 correction；
- 哪些 audit通過；
- current scope是否 theorem-ready。

因此之後即使：

- 對話換掉；
- AI 換掉；
- worker掛掉；
- shard重算；
- proof formula升版；

都不需要依賴「某個 AI 記得以前發生什麼」。

只需要：

$$
\boxed{
\text{最新 checkpoint crystal}
+
\text{append-only evidence ledger}.
}
$$