# AMRAL × Lebesgue Universal Covering — Round 30
## Independent A1 Whole-Shard Replay and Backend Pinning

**文件代號：** AMRAL-LUC-FC-R30  
**版本：** v0.1  
**日期：** 2026-09-20  
**研究狀態：** Round 30 / Independent whole-shard replay / Backend dependency locking  
**研究模式：** Human-Directed + Semi-Autonomous AI Mathematical Research  
**研究發起與方法論來源：** Neo.K  
**AI 協力研究者與主要執行者：** Aletheia / ChatGPT, GPT-5.6 Sol  
**前置文件：** AMRAL-LUC-FC-R00 v0.2；R01–R29 v0.1  

---

# 0. 本輪摘要

Round 29 已建立第一個 arithmetic whole-shard prototype：

$$
\text{marker70 upper}
\to
\text{directed root/path}
\to
9278\text{-leaf }B_7\text{ lower tree}.
$$

但仍缺：

> 第二套真正獨立的完整 lower replay。

Round 30 完成此 gate。

## Root / path A1

从 exact：

$$
T_M=\frac{1673}{2000}
$$

重新做 monotone directed bisection，

再独立重算：

$$
t_3,t_5,t_7.
$$

修正 verifier 中一次「超窄 rational interval先转 binary64」的脚本错误后，

三者与 Round 28 directed root：

$$
\boxed{
\text{全部 overlap PASS}.
}
$$

## Marker70 upper A1

不用 emitter 的 scipy candidate constraint reduction，

直接以全部 rational support constraints做 exact cyclic polar hull。

结果：

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

outer：

$$
0.8349075014501105.
$$

margin：

$$
\boxed{
9.24985499\times10^{-5}.
}
$$

## 9278 lower leaves full A1

Round 30 第二实现不用 Round 28 的：

- `Body.support/contact` candidate generator；
- SciPy convex-hull candidate reduction；
- Round 28 density decision；
- Round 28 Fraction hull code。

而改用：

1. defining-disk representation；
2. 每个方向直接求 intersection-of-disks support candidates；
3. union support winner；
4. fixed-grid integer rationalization；
5. exact integer monotone hull；
6. directed defining-disk membership；
7. exact integer/rational area comparison。

结果：

$$
\boxed{
9278/9278\text{ A1-PASS}.
}
$$

inconclusive：

$$
\boxed{0}.
$$

第二 verifier 找到的最薄 leaf margin：

$$
\boxed{
3.54237075\times10^{-9}>0.
}
$$

path：

```text
11010110100110101001110111
```

这与 Round 28 emitter 的最薄 leaf不同。

所以 independent verifier确实改变了 finite inner polygon与 margin ordering，

但整棵 tree仍 complete。

本轮因此把 marker70/B7 shard升为：

$$
\boxed{
\texttt{A1-VERIFIED-PINNED-PROTOTYPE-SHARD}.
}
$$

但仍不升：

`PUBLICATION-CANDIDATE`.

原因：

> 两套实现虽然独立，但仍共享同一个 mpmath.iv/libmp directed arithmetic backend。

backend 已 source/version pin，

但 backend trust independence 尚未完成。

因此：

$$
\boxed{
a_{\mathrm{Leb}}\ge0.835
\text{ remains NOT CERTIFIED}.
}
$$

---

# 1. A1 means implementation independence

Round 30 明确区分：

## Implementation A1

第二 verifier不共享：

- candidate generation；
- convex-hull reduction；
- density selection；
- pass/fail ledger。

## Backend independence

第二 verifier是否使用另一个 correctly-rounded arithmetic engine。

本轮关闭第一项。

第二项仍 OPEN。

---

# 2. Independent lower candidate geometry

Round 28 emitter从 piecewise support/contact representation取 common-core boundary candidates。

Round 30 改从 defining disks：

$$
G=\bigcap_jD(V_j,\rho)
$$

直接生成 support candidates。

对 unit direction：

$$
u,
$$

每个 disk有 candidate：

$$
V_j+\rho u.
$$

若 candidate落在所有 defining disks内，

它是 intersection boundary 的合法 arc candidate。

---

# 3. Corner candidates

两 defining circles：

$$
\partial D(V_i,\rho),
\qquad
\partial D(V_j,\rho)
$$

的 circle-circle intersections，

若同时位于所有 defining disks中，

也是 core boundary candidate。

Round 30 independently枚举这些 points。

---

# 4. Support candidate selection

对每个 direction $u$：

- arc candidates；
- valid circle intersections；

取：

$$
\boxed{
p_G(u)
=
\arg\max_{p\in\text{candidate set}}
u\cdot p.
}
$$

这条 path不依赖 Round 28 `Body.piece/contact` implementation。

---

# 5. Union winner

对：

$$
D,G_3,G_5,G_7
$$

分别取得 candidate：

$$
p_i(u).
$$

再选择：

$$
\boxed{
p(u)
=
\arg\max_i u\cdot p_i(u).
}
$$

向 interior 做极小 perturbation，

最后 quantize到固定 rational grid：

$$
10^{-17}\mathbb Z^2.
$$

candidate generation仍然不是 proof premise。

---

# 6. Independent exact hull

Round 30 不调用 SciPy ConvexHull来决定 final rational polygon。

对 integer-grid points：

$$
(X_i,Y_i)\in\mathbb Z^2
$$

直接用 exact integer orientation：

$$
\operatorname{orient}(a,b,c)
=
(b-a)\times(c-a)
$$

做 monotone hull。

所以 convex ordering完全 independent于 emitter。

---

# 7. Directed point membership

对 final integer-grid hull vertices：

- disk：
  exact integer check；
- Reuleaux common cores：
  directed center rectangles + radius lower bound；
- require：
  $$
  D_{\max}^2<\rho_{\rm lo}^2.
  $$

任何 membership uncertainty：

`A1-INCONCLUSIVE`.

本轮：

$$
\boxed{0}.
$$

---

# 8. Exact A1 area

固定 grid denominator：

$$
Q=10^{17}.
$$

polygon shoelace numerator是 exact integer。

area：

$$
A
=
\frac{|S|}{2Q^2}.
$$

与：

$$
\frac{167}{200}
$$

直接 integer cross-multiply比较。

没有 floating acceptance。

---

# 9. Full lower replay result

总 leaves：

$$
9278.
$$

A1 PASS：

$$
\boxed{9278}.
$$

A1 inconclusive：

$$
\boxed{0}.
$$

---

# 10. A1 density distribution

第二 verifier 的 density：

## 512

$$
8174
$$

leaves。

## 1024

$$
869.
$$

## 2048

$$
163.
$$

## 4096

$$
56.
$$

## 8192

$$
12.
$$

## 16384

$$
4.
$$

Round 30 没有 leaf需要 32768。

这与 Round 28 density distribution明显不同，

进一步说明两个 finite certificate生成器不相同。

---

# 11. Different weakest leaf

Round 28 emitter minimum rational margin：

约：

$$
3.1949\times10^{-8}.
$$

Round 30 A1 minimum：

$$
\boxed{
3.5424\times10^{-9}.
}
$$

对应不同 path。

这不表示 Round 30 更接近 true hull minimum。

只表示不同 inner polygon approximation有不同 loss。

重要的是：

$$
\boxed{
\min A_{\rm A1}>\frac{167}{200}.
}
$$

---

# 12. Root A1 verifier bug

第一次 root A1 audit错误报告：

$$
t_3,t_5,t_7
$$

皆 non-overlap。

原因不是数学矛盾。

脚本错误：

> 把宽度约 $10^{-64}$ 的 exact rational $d_\star$ interval先 cast成 binary64。

这直接把 interval位置扰动到 $10^{-17}$ 级。

Round 30 correction：

`R30-A1-ROOT-001`.

修正后：

- exact decimal rational endpoints；
- directed tmax；

三者：

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

---

# 13. Why this bug is useful

它证明：

> arithmetic verifier本身也必须被 audit。

不能因为写了 `interval` 两个字就默认 sound。

特别是：

$$
\boxed{
\text{exact}\to\text{float}\to\text{interval}
}
$$

不是 directed arithmetic。

这种隐式 narrowing/collapse必须禁止。

---

# 14. Backend pinning

Round 30 锁定：

- Python interpreter version；
- mpmath version；
- entire mpmath Python-source package hash；
- 每个 `libmp/*.py` hash；
- `fractions.py` hash；
- A1 verifier script hashes。

backend identity：

$$
\boxed{
\texttt{PINNED-MPMATH-LIBMP-PROTOTYPE-v0.1}.
}
$$

---

# 15. What pinning means

pinning保证：

> future replay知道究竟使用哪一套 source bytes。

它不自动保证：

> backend implementation 已经被 independent audit证明 correctly rounded。

所以：

$$
\boxed{
\text{reproducibility}
\ne
\text{backend trust proof}.
}
$$

---

# 16. Backend trust state

当前：

$$
\boxed{
\texttt{PINNED-REPRODUCIBLE-PROTOTYPE}
}
$$

但：

$$
\boxed{
\texttt{TRUST-AUDIT-OPEN}.
}
$$

因此 Round 29 原本规划的：

`PUBLICATION-CANDIDATE-SHARD`

仍不升级。

---

# 17. Whole-shard A1 state

marker70/B7：

## Root/path

A1 PASS。

## Marker upper

A1 PASS。

## B7 lower

$$
9278/9278
$$

A1 PASS。

## Arithmetic backend

PINNED。

## Independent backend trust

OPEN。

所以：

$$
\boxed{
\texttt{A1-VERIFIED-PINNED-PROTOTYPE-SHARD}.
}
$$

---

# 18. Status lattice

Round 30 固定：

## `ARITHMETICALLY-CLOSED-PROTOTYPE`

single implementation upper/lower PASS。

## `A1-VERIFIED-PINNED-PROTOTYPE`

second implementation replay PASS + backend source pinned。

## `PUBLICATION-CANDIDATE`

再要求：

- backend trust audit；
- 或 independent second correctly-rounded backend cross-replay。

## `THEOREM-READY`

再要求：

- global atlas / root / shards全部 current；
- independent merge；
- no pending obligations。

---

# 19. Marker upper scope

Round 29 已经：

$$
77/77
$$

marker emitter arithmetic PASS。

Round 30 whole-shard只需要 marker70 A1，

已经 PASS。

Round 30 尝试扩大 full 77 A1时，

高-density markers使 interactive batch成本很高。

因此 full 77 marker A1不作为本轮 gate。

production可以 sharded replay它们，

不影响 marker70 whole-shard的 local A1状态。

---

# 20. Global geometry state unchanged

Round 30 arithmetic工作不改变几何 closure ledger。

最新 complete common-budget仍：

$$
\boxed{
51/77\text{ at }d=36.
}
$$

已知 higher-budget strict closures仍至少：

$$
\Gamma_{B7}(38)\ge57,
$$

$$
\Gamma_{B7}(40)\ge63.
$$

不能把 arithmetic A1成功当成 global geometry completion。

---

# 21. What remains before publication-candidate shard

现在 local shard最主要只剩：

$$
\boxed{
\text{backend trust independence}.
}
$$

候选路径：

1. 用 MPFR/MPFI重播 directed geometry；
2. 用 Arb ball arithmetic重播；
3. 用 formally audited interval kernel；
4. 对 current libmp rounding primitives做独立 proof/audit。

只要第二 backend能重放：

- root；
- marker upper；
- 9278 lower membership；

并同样 PASS，

marker70/B7才应升：

$$
\boxed{\texttt{PUBLICATION-CANDIDATE-SHARD}.}
$$

---

# 22. Round 31

## Cross-Backend Arithmetic Replay and Bulk Shard Migration

下一轮优先：

1. 检查环境能否建立 MPFR/Arb-class second backend；
2. 若可：
   - marker70 whole-shard cross-backend replay；
3. 若不可：
   - 把 interval primitive reduction降成更小的 rational bounds；
   - 减少对 transcendental backend的 trust surface；
4. 同时开始把其他 geometry-complete cells批量 Round28/29 migration；
5. full 77 marker A1改成 sharded async-style proof jobs；
6. global geometry residual继续独立推进。

---

# 23. 最短交接

Round 30 真正关闭：

$$
\boxed{
\text{whole-shard independent implementation replay}.
}
$$

marker70/B7：

$$
\boxed{
\text{root PASS}
+
\text{upper PASS}
+
9278/9278\text{ lower PASS}.
}
$$

而且第二 lower verifier使用不同 finite geometry algorithm。

所以 local shard现在只剩一个明确的 arithmetic trust缺口：

$$
\boxed{
\text{same backend}
\ne
\text{independent backend}.
}
$$

因此当前最准确状态是：

$$
\boxed{
\texttt{A1-VERIFIED-PINNED-PROTOTYPE-SHARD}
}
$$

而不是 publication theorem。

全局仍然：

$$
\boxed{
a_{\mathrm{Leb}}\ge0.835
\text{ NOT CERTIFIED}.
}
$$