# AMRAL × Lebesgue Universal Covering — Round 14
## Semantic Rebase, Claim Dominance, and Proof-State Compaction

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

---

# 0. 本輪摘要判定

Round 12–13 已建立：

$$
\text{checkpoint}
\to
\text{worker proposals}
\to
\text{canonical merge}.
$$

真正長期運行後會出現新問題：

1. proof dependency只要 hash改變，是否所有舊 claim 都要重算？
2. 兩個 claim 都能證同一區域時，哪個應留在 hot state？
3. rejected / stale / obsolete / superseded 歷史累積幾百萬筆後，checkpoint 是否會無限膨脹？
4. 若把歷史移出 hot state，是否會破壞 theorem soundness？
5. 舊證據之後若又需要，如何安全 rehydrate？

Round 14 完成：

$$
\boxed{
\text{Semantic Compatibility}
}
$$

$$
\boxed{
\text{Claim Dominance}
}
$$

$$
\boxed{
\text{Minimal Active Proof Core}
}
$$

$$
\boxed{
\text{Hot / Cold Proof-State Compaction}.
}
$$

本輪主要結果：

- exact dependency hash equality降為 safe fast path，而非唯一合法路徑；
- margin credit可跨 target / scalar error budget做 semantic rebase；
- unused witness catalog extension不 stale舊 claim；
- 定義 claim capacity；
- 定義 claim dominance；
- 定義 active proof reachability；
- 證 hot-core compaction不改 current theorem-readiness；
- cold archive以 content hash + Merkle root綁定；
- 實際把 Round 13 reference checkpoint壓成 hot core + cold archive；
- machine-test semantic rebase success / failure boundary；
- machine-test archive rehydration。

本輪判定：

$$
\boxed{
\text{SEMANTIC REBASE LAYER: CLOSED}
}
$$

$$
\boxed{
\text{HOT/COLD PROOF COMPACTION: CLOSED}
}
$$

$$
\boxed{
\text{DESTRUCTIVE EVIDENCE DELETION: NOT AUTHORIZED}
}
$$

---

# 1. Round 12 的保守規則仍然正確

Round 12：

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

才直接接受 claim。

這是：

$$
\boxed{
\text{sound exact-identity fast path}.
}
$$

Round 14 不否定它。

問題只是：

> hash 不相等不代表數學上一定 incompatible。

所以新增：

$$
\boxed{
\text{semantic implication path}.
}
$$

---

# 2. Semantic compatibility relation

對 claim：

$$
c
$$

與 current proof obligation：

$$
O,
$$

寫：

$$
\boxed{
c\succeq_{\rm sem}O
}
$$

若 claim 的已證命題可邏輯推出 current obligation。

這必須由明確規則決定。

不能由模型「覺得差不多」決定。

---

# 3. Target monotonicity

若 claim證：

$$
\Phi(x)\ge T_c
$$

對其完整 domain成立，

則對任意：

$$
T'\le T_c
$$

自動有：

$$
\Phi(x)\ge T'.
$$

所以 target降低：

$$
\boxed{
\text{天然 semantic-compatible}.
}
$$

但 target提高需要 slack。

---

# 4. Scalar error-budget margin credit

reference leaf原始 one-sided quantity記：

$$
L.
$$

舊 verifier接受：

$$
L-e_c
\ge
T_c.
$$

令 worst verified slack：

$$
s_c
=
\min_{\rm leaves}
[
L-e_c-T_c
].
$$

因此：

$$
L
\ge
T_c+e_c+s_c
$$

對所有 leaves。

新 policy：

$$
e',
\qquad
T'.
$$

只要：

$$
T'+e'
\le
T_c+e_c+s_c,
$$

舊 raw witnesses仍足以證新 obligation。

---

# 5. Claim Capacity

定義：

$$
\boxed{
\operatorname{Cap}_{e'}(c)
=
T_c+s_c+e_c-e'.
}
$$

則：

$$
\boxed{
T'
\le
\operatorname{Cap}_{e'}(c)
}
$$

是 scalar-error semantic migration的充分條件。

---

# 6. Margin credit ledger

future production claim建議永遠保存：

```text
proved_threshold
verified_error_budget
worst_verified_slack
raw_lower_witness_policy
```

不要只存：

```text
PASS
```

因為：

$$
\boxed{
\text{slack 是未來 semantic rebase 的可用資產}.
}
$$

---

# 7. Reference capacity example

Round 11 local reference：

old：

$$
T_c=0.835,
$$

$$
e_c=10^{-8}.
$$

三個 active shard worst slacks：

## A

$$
s_A
=
3.8698779558643537\times10^{-7}.
$$

## B

$$
s_B
=
9.574949350055206\times10^{-7}.
$$

## C

$$
s_C
=
3.545377508240577\times10^{-7}.
$$

若新 error budget：

$$
e'=2\times10^{-8},
$$

容量：

$$
\operatorname{Cap}(A)
\approx
0.8350003769877956,
$$

$$
\operatorname{Cap}(B)
\approx
0.8350009474949350,
$$

$$
\operatorname{Cap}(C)
\approx
0.8350003445377508.
$$

因此同一 local reference proof在這個 stricter error policy下的 aggregate capacity：

$$
\boxed{
T_{\rm cap}^{\rm ref}
\approx
0.8350003445377508.
}
$$

再次：

$$
\boxed{
\text{這只是 Round 10/11 local reference scope，
不是 global Lebesgue lower bound}.
}
$$

---

# 8. Target + arithmetic simultaneous migration

Round 14 actual test：

從：

$$
T=0.835,
\qquad
e=10^{-8}
$$

遷移到：

$$
\boxed{
T'=0.8350001,
\qquad
e'=2\times10^{-8}.
}
$$

三個 active claim全都仍有正 margin credit。

所以：

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

within reference scope。

---

# 9. Migration boundary test

再推到：

$$
T''=0.8350004
$$

with：

$$
e'=2\times10^{-8}.
$$

此時至少 A / C capacity不足。

所以：

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

這證 semantic validator不是：

> dependency mismatch一律放行。

而是真的受 margin boundary限制。

---

# 10. Witness catalog extension

claim只依賴實際被 certificate使用的 witnesses。

若：

$$
W_c
=
\{B_7\}
$$

而 current catalog：

$$
W'
=
\{B_7,B_9,\text{Fourier dictionary}\},
$$

則：

$$
\boxed{
W_c\subseteq W'
}
$$

所以 catalog extension 不影響舊 claim。

因此：

> 新增 search candidates 不應讓已證 shard stale。

---

# 11. Witness mutation

若：

$$
B_7
$$

的 geometry semantics / normalization改變，

則使用：

$$
B_7
$$

的舊 claim不能僅靠 catalog superset規則重用。

需要：

- geometry exact identity；
- 或 explicit migration theorem；
- 或 revalidation。

---

# 12. Local dependency closure

production claim不應只綁整個巨大 global dependency bundle。

應保存：

$$
\boxed{
D(c)
=
\text{claim actually used dependencies}.
}
$$

例如：

- geometry modules used；
- witness ids used；
- arithmetic mode used；
- proof modes used；
- verifier semantics used。

global新增一個完全無關 module：

$$
\notin D(c)
$$

不應 stale claim。

---

# 13. Domain semantic rebase

若 claim證 ancestor：

$$
B(p)
$$

而 current obligation是 descendant：

$$
B(q),
$$

其中：

$$
p\preceq q,
$$

則：

$$
B(q)\subseteq B(p).
$$

所以 ancestor claim：

$$
\boxed{
\text{dominates descendant obligation}.
}
$$

這是 Round 13 Certified Ancestor Contraction的 dependency-level generalization。

---

# 14. Descendant evidence不是 ancestor claim

反向：

$$
q\succeq p
$$

時，單一：

$$
B(q)
$$

claim不能證：

$$
B(p).
$$

需要一個 complete descendant claim set：

$$
\mathcal C_p
$$

覆蓋：

$$
B(p).
$$

所以：

$$
\boxed{
\text{single-claim dominance}
}
$$

與：

$$
\boxed{
\text{claim-set coverage}
}
$$

必須分開。

---

# 15. Claim Dominance

定義 current policy：

$$
\Pi.
$$

claim：

$$
c_1
$$

dominates：

$$
c_2,
$$

寫：

$$
c_1\succeq_\Pi c_2,
$$

若：

1. $c_1$ domain覆蓋 $c_2$ current-needed domain；
2. $c_1$ semantic capacity至少不低於 $c_2$；
3. $c_1$ local dependency set current-compatible；
4. $c_1$ 具有 required A1 evidence。

則：

$$
\boxed{
c_2
\text{ 不需要留在 hot active proof core}.
}
$$

但不能刪除 cold evidence。

---

# 16. Same-seed dominance

同一 seed：

$$
p,
$$

兩 claim：

$$
c_1,c_2.
$$

若：

$$
\operatorname{Cap}(c_1)
\ge
\operatorname{Cap}(c_2)
$$

且：

$$
D(c_1)
\subseteq D(c_2)
$$

在 compatibility 意義下，

則 active primary應優先：

$$
c_1.
$$

如果 capacity相同，用 canonical certificate hash tie-break。

---

# 17. Rejected claim 永不 dominate

即使 rejected claim：

- threshold更高；
- slack更大；

也不能作 active dominance source。

必須先有 current valid audit state。

---

# 18. Active Evidence Graph

定義完整 proof history graph：

$$
G=(V,E).
$$

nodes包括：

- checkpoints；
- claims；
- audits；
- certificates；
- policies；
- witnesses；
- proposals；
- corrections。

current theorem實際只依賴其中一個 reachable subgraph：

$$
\boxed{
G_{\rm live}.
}
$$

---

# 19. Minimal Active Proof Core

Round 14定義 hot core至少保留：

1. scope；
2. root identity；
3. current target / semantic policy；
4. current frontier；
5. current primary active claims；
6.每個 primary claim的：
   - certificate hash；
   - proved threshold；
   - error budget；
   - worst slack；
   - local dependencies；
   - A1 evidence summary；
7. pending seeds；
8. cold archive root。

這足以回答：

> current scope 是否 theorem-ready？

---

# 20. Cold Evidence Archive

移出 hot state：

- rejected claims；
- superseded claims；
- stale claims；
- obsolete proposals；
- old orchestration journal；
- old checkpoints；
- auxiliary duplicate verified claims；
- old scheduler metrics。

它們仍是：

$$
\boxed{
\text{immutable content-addressed evidence}.
}
$$

---

# 21. Garbage Collection 的定義

本輪：

$$
\boxed{
\text{GC}
=
\text{hot-state eviction}.
}
$$

不是：

$$
\boxed{
\text{physical deletion}.
}
$$

所以使用者仍能：

- 查 correction ancestry；
- rehydrate old descendants；
- audit historical failure。

---

# 22. Hot-Core Compaction Theorem

## 定理 22.1

令 full state：

$$
S
$$

與 compact state：

$$
H
$$

具有相同：

1. current scope/root；
2. current semantic policy；
3. current frontier；
4. current active coverage claims；
5. theorem-critical A1 evidence。

則 current：

$$
\texttt{theorem\_ready}(S)
$$

與：

$$
\texttt{theorem\_ready}(H)
$$

相同。

### 證明

theorem-ready predicate只量化 current frontier obligations。

每個 obligation是否 closure只依賴 current semantic-compatible active claim與 required verifier evidence。

歷史：

- rejected；
- superseded；
- obsolete；
- scheduler；

不出現在 current proof implication中。

因此移到 cold archive不改 predicate。

Q.E.D.

---

# 23. Archive Merkle Binding

cold archive每個 object：

$$
o_i
$$

有：

$$
h_i=H(o_i).
$$

再建立：

$$
\boxed{
H_{\rm archive}
=
\operatorname{MerkleRoot}(h_1,\ldots,h_n).
}
$$

hot core保存：

- archive manifest hash；
- archive Merkle root。

---

# 24. Archive 不自動恢復 proof

即使 cold archive中有一個昔日 verified claim：

也不能因為 rehydrate就自動 active。

必須重新判：

1. status / supersession；
2. semantic compatibility；
3. current audit requirement；
4. domain relation。

archive只證：

> 這是當時那份 evidence。

不是：

> 它現在仍然有效。

---

# 25. Rejection after compaction

若 hot active claim：

$$
c
$$

之後被拒：

1. $c$ 失效；
2. seed pending；
3. theorem-ready false；
4. merger可從 cold archive找：
   - old descendant certificates；
   - auxiliary duplicate claims；
5. rehydrate；
6. semantic validate；
7. append新 active transition。

因此 GC不阻止 recovery。

---

# 26. Reference hot/cold compaction

來源：

Round 13 final reference checkpoint。

full source包含：

- active A；
- rejected B-v1；
- active corrected B-v2；
- active C；
- 5 audit records；
- orchestration race ledger；
- aggregate metadata。

Round 14 hot core只保留：

$$
\boxed{
A,\ B\text{-v2},\ C
}
$$

三個 active evidence summaries，

plus：

- frontier；
- semantic policy；
- archive binding。

完整 Round 13 source checkpoint移入 immutable cold archive snapshot。

---

# 27. Archive rehydration test

Round 14 machine test：

1. 驗 archive object SHA-256；
2. 從 cold snapshot讀回：

   `claim-shard-B-v1`；
3. 確認其歷史狀態仍為：

   `REJECTED`；
4. certificate hash保持一致。

PASS。

---

# 28. Compaction size note

reference checkpoint本身很小，所以 size reduction不是本輪主要 benchmark。

production幾百萬 history records時，差異才重要。

真正 invariant是：

$$
\boxed{
|H_{\rm hot}|
\propto
\text{current frontier + active claims}
}
$$

而不是：

$$
\boxed{
\text{total historical events}.
}
$$

---

# 29. Semantic validator actual test

Round 14 actual tests：

## Baseline

$$
T=0.835,
\quad
e=10^{-8}.
$$

Ready：

`true`.

## Stricter arithmetic + slightly higher target

$$
T=0.8350001,
\quad
e=2\times10^{-8},
$$

plus catalog extension：

$$
B_9.
$$

Ready：

`true`.

## Beyond margin capacity

$$
T=0.8350004,
\quad
e=2\times10^{-8}.
$$

Ready：

`false`.

## Catalog-only extension

原 target / error，catalog加入：

- $B_9$；
- Round 02 Fourier dictionary。

Ready：

`true`.

全部 PASS。

---

# 30. Round 12 strengthening ledger

Round 12 rule：

`dependency hash mismatch -> stale`

保留為：

`SAFE-CONSERVATIVE`.

Round 14新增：

`R12-STRENGTHENING-001`

內容：

> hash mismatch可進 explicit semantic migration；沒有 migration proof時仍 stale。

所以沒有降低 safety bar。

---

# 31. Semantic Migration Registry

future checkpoint建議保存：

```text
migration_rule_id
source_semantics
target_semantics
preconditions
proof_reference
verifier
```

只有 registry中的 rule可被 canonical merger自動使用。

AI不能臨時口頭發明 migration。

---

# 32. Registered rules in Round 14

## `TARGET-MONOTONICITY-V0.1`

$$
T'\le T.
$$

## `SCALAR-ERROR-MARGIN-CREDIT-V0.1`

$$
T'+e'
\le T+e+s.
$$

## `WITNESS-CATALOG-SUPERSET-V0.1`

claim used witnesses：

$$
\subseteq
$$

current catalog。

## `ANCESTOR-DOMAIN-COVERAGE-V0.1`

verified ancestor domain covers descendant obligation。

---

# 33. What is NOT automatically compatible

- arbitrary geometry rewrite；
- new support convention；
- changed reflection semantics；
- changed normalization；
- different floating model without error implication；
- witness replaced by non-equivalent shape；
- target raised beyond margin；
- larger root domain。

這些需要新 proof。

---

# 34. Hot archive policy

建議 hot state保留：

```text
current checkpoint header
current frontier
pending seeds
primary active claim summaries
active A1 audit refs
unresolved FAIL tombstones
migration registry
cold archive root
```

其他全部可冷凍。

---

# 35. Tombstones

如果某歷史 record雖已移 cold，但 current state仍需知道：

> 此 claim不能復活

hot只需保留小 tombstone：

```text
claim_id
status = REJECTED | SUPERSEDED | STALE-BLOCKED
reason_hash
archive_locator
```

避免 full record回 hot。

---

# 36. Proof-State Garbage Collection Safety

可 hot-evict：

- superseded；
- rejected full bodies；
- old audit details；
- obsolete proposals；
- scheduler events。

不可 hot-evict且沒有 replacement summary：

- current active claim；
- current pending seed；
- unresolved current FAIL；
- current semantic policy；
- migration rule used by active claim；
- certificate hash / A1 evidence needed by active claim。

---

# 37. Physical retention

本輪不處理：

- 幾年後可否真的刪 raw certificate；
- storage quota；
- legal retention。

default：

$$
\boxed{
\text{archive forever until separate governance decision}.
}
$$

---

# 38. COMPUTE-DEFERRED

## C14-1

把 future global $0.835$ checkpoint改成 hot-core格式。

## C14-2

每個 claim保存 margin credit。

## C14-3

建立 migration registry validator。

## C14-4

cold archive按月／每 N checkpoints封 immutable pack。

## C14-5

建立 archive rehydration CLI。

---

# 39. Round 15 指定題目

## AMRAL-LUC-FC-R15
### Global Proof Capacity and Threshold Ladder Automation

Round 14得到每個 claim的：

$$
\operatorname{Cap}(c).
$$

下一輪可以把它升成：

> 在不用重算全部 shards的情況下，current global proof state最多能把 target往上推到哪裡？

對 global frontier：

$$
\boxed{
T_{\rm capacity}
=
\min_{p\in\mathcal P}
\max_{c\text{ covers }p}
\operatorname{Cap}(c).
}
$$

這可以自動：

1. 找 bottleneck shards；
2. 決定下一個 target；
3. 只重算限制 target的 shards；
4. 建 adaptive lower-bound ladder。

如果 global compute尚未開始，先用 reference proof做完整 capacity scheduler prototype。

---

# 40. Reproducibility checklist

## Semantic compatibility

`FORMALIZED`

## Scalar margin migration

`PROVED`

## Witness catalog extension

`PROVED`

## Claim dominance

`FORMALIZED`

## Minimal active proof core

`FORMALIZED`

## Hot-core compaction theorem

`PROVED`

## Cold archive binding

`IMPLEMENTED`

## Archive rehydration

`PASS`

## Semantic rebase boundary tests

`PASS`

## Destructive evidence deletion

`NOT AUTHORIZED`

---

# 41. 最短交接結論

Round 14 解決兩個長期運行問題。

第一：

$$
\boxed{
\text{hash mismatch}
\not\Rightarrow
\text{必然重算}.
}
$$

只要有明確 implication，例如：

$$
T'+e'
\le T+e+s,
$$

舊 claim 可以合法 semantic rebase。

第二：

$$
\boxed{
\text{proof history可以一直長，
hot checkpoint不用一直長}.
}
$$

current theorem只依賴 Minimal Active Proof Core。

其餘 evidence移入 content-addressed cold archive。

所以 AMRAL distributed proof state現在不只：

- 正確；
- 可並發；
- 可恢復；

也開始具備：

$$
\boxed{
\text{長時間可維護性}.
}
$$