# AMRAL × Lebesgue Universal Covering — Round 31
## Cross-Backend Arithmetic Replay and First Publication-Candidate Shard

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

---

# 0. 本輪摘要

Round 30 已完成 marker70/$B_7$ whole shard 的 implementation-level A1：

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

但两套 verifier仍共享：

`mpmath.iv / libmp`.

Round 31 找到系统级第二 backend：

$$
\boxed{\text{libMPFR 4.2.2 + GMP}}
$$

并以直接 C ABI / `ctypes` 构造最小 directed-rounding wrapper。

本轮重新验证：

## MPFR root

$$
\boxed{
t_3,t_5,t_7
\text{ 与 Round28 directed intervals 全部 overlap PASS}.
}
$$

## MPFR marker70 upper

$$
\boxed{
U_{70}^{\rm MPFR}
=
0.8349075014501105
<
0.835.
}
$$

margin：

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

## MPFR full lower tree

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

inconclusive：

$$
\boxed{0}.
$$

minimum exact rational lower margin：

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

所以 marker70/$B_7$ whole shard现在具备：

1. emitter implementation；
2. independent A1 implementation；
3. mpmath/libmp backend；
4. independent libMPFR/GMP backend；
5. strict upper/lower inequalities全部通过。

因此 local shard状态升级：

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

注意：

$$
\boxed{
\text{publication-candidate shard}
\ne
\text{global theorem}.
}
$$

global：

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

仍未 certified。

---

# 1. Second arithmetic backend

环境中没有：

- gmpy2；
- python-flint；
- Arb Python binding。

但系统动态库包含：

$$
\boxed{\texttt{libmpfr.so.6}}
$$

与：

$$
\boxed{\texttt{libgmp.so.10}}.
$$

Round 31直接调用 C ABI。

---

# 2. Minimal MPFR trust surface

wrapper只暴露当前 proof真正需要的：

- exact integer / rational load；
- RNDD / RNDU；
- add/sub/mul/div；
- sqrt；
- sin；
- cos；
- acos；
- atan2；
- pi；
- comparison；
- exact dyadic endpoint extraction。

没有把整个 CAS当成 proof dependency。

---

# 3. Fraction → MPFR → Fraction rule

Round 30已发现：

$$
\text{exact rational}
\to
\text{binary64}
\to
\text{interval}
$$

会破坏超窄 interval。

Round 31固定：

$$
\boxed{
\text{exact Fraction}
\to
\text{MPFR directed}
\to
\text{exact dyadic Fraction}.
}
$$

任何 transcendental endpoint都以 MPFR dyadic value完整取回。

---

# 4. MPFR root replay

重新从：

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

做 monotone directed bisection。

得到 $d_\star$ interval width约：

$$
2.97\times10^{-67}.
$$

再重算：

$$
t_3,t_5,t_7.
$$

三者全部与 Round 28 mpmath/libmp intervals overlap：

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

---

# 5. MPFR marker upper

marker70仍使用：

- exact rational marker point；
- finite integer normals；
- rational half-plane outer polygon；
- exact rational polar hull / line intersections / shoelace。

唯一更换：

> Reuleaux support sector的 directed transcendental arithmetic全部由 MPFR重新计算。

结果：

$$
\boxed{
0.8349075014501105
}
$$

与 Round 29显示值一致。

---

# 6. Initial conservative marker false negative

第一版 MPFR marker verifier在 active sector之外额外加入相邻 Reuleaux pieces作为 upper candidates。

这仍是 one-sided safe upper，

但过度宽松：

$$
U\approx0.9201.
$$

所以 marker无法通过。

这不是 false proof，

只是 false negative / inconclusive。

修正：

> 只纳入 directed sector interval真正可能 active 的 pieces。

修正后 exact outer certificate PASS。

已记录：

`R31-MPFR-MARKER-001`.

---

# 7. MPFR lower replay semantics

Round 31 full lower verifier使用：

- MPFR reconstructed root；
- explicit topology；
- explicit witness split axes；
- defining-disk common-core geometry；
- independent support-candidate generator；
- fixed-grid integer rationalization；
- exact integer monotone hull；
- exact rational area comparison。

acceptance仍是：

$$
A_{\rm rational}
>
\frac{167}{200}.
$$

---

# 8. Full MPFR lower result

总 leaves：

$$
9278.
$$

PASS：

$$
\boxed{9278}.
$$

inconclusive：

$$
\boxed{0}.
$$

---

# 9. MPFR density distribution

$$
512:8174,
$$

$$
1024:869,
$$

$$
2048:163,
$$

$$
4096:56,
$$

$$
8192:12,
$$

$$
16384:4.
$$

与 Round 30 A1 implementation得到相同 density histogram。

这是因为 finite candidate policy相同，

但 core enclosure arithmetic backend不同。

---

# 10. Minimum MPFR margin

最薄：

```text
11010110100110101001110111
```

margin：

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

仍 strictly positive。

---

# 11. Cross-backend theorem state

现在同一个 local shard有：

## Backend A

`mpmath.iv / libmp`

Round 28 emitter + Round 30 A1。

## Backend B

`libMPFR 4.2.2 / GMP`

Round 31 full replay。

两边都 independently证明：

- root；
- marker upper；
- every lower leaf。

所以 backend-specific silent rounding defect必须同时在两个不同 arithmetic stacks中产生相容错误，可信度显著提升。

这仍不是对两个 libraries的形式证明，

但符合本 program定义的 publication-candidate cross-backend gate。

---

# 12. MPFR backend pin

Round 31 pin：

## MPFR

resolved ELF：

```text
/usr/lib/x86_64-linux-gnu/libmpfr.so.6.2.2
```

SHA-256：

```text
4e3ccf5b442fc91054b0153140fe62939009f98ca1367f45de62376d5b18d28c
```

## GMP

```text
/usr/lib/x86_64-linux-gnu/libgmp.so.10.5.0
```

SHA-256：

```text
d15e1585c6c267296459570c8ac217ca9123044bcd4e896d2f686b32333445d2
```

wrapper与 replay scripts也全部 content-hashed。

---

# 13. Publication-candidate gate

Round 31定义 local：

`PUBLICATION-CANDIDATE-SHARD`

条件：

1. directed root/path two-backend replay；
2. upper marker two-backend replay；
3. lower tree independent implementation A1；
4. lower tree independent arithmetic backend replay；
5. every claimed inequality strict；
6. dependency hashes pinned。

marker70/B7：

$$
\boxed{
\text{ALL LOCAL CONDITIONS MET}.
}
$$

---

# 14. What publication-candidate means

它表示：

> 这个单独 shard 已经达到可进入正式 proof package / 外部审计的成熟度。

它不表示：

> Lebesgue lower bound 已经证明。

因为 global theorem还需要所有 root/base/shard obligations coverage。

---

# 15. Global geometry still incomplete

最新共同 budget：

$$
\Gamma_{B_7}(36)=51/77.
$$

已知较高 budget：

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

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

仍有 geometry residual。

所以一个 publication-candidate shard不能改变 global theorem status。

---

# 16. Bulk arithmetic migration queue

Round 31把 full-atlas cells拆成：

## Geometry complete

进入：

$$
\boxed{
\text{ARITHMETIC-MIGRATION QUEUE}.
}
$$

对每个依序：

1. explicit topology / axis streams；
2. directed root/path；
3. marker upper；
4. bulk lower migration；
5. implementation A1；
6. MPFR cross-backend；
7. publication-candidate promotion。

## Geometry residual

继续：

$$
B_7
$$

closure wave。

不应在 lift tree尚未 complete时浪费 full arithmetic migration成本。

---

# 17. Migration economics

Round 28 / 30 / 31已经显示：

> arithmetic migration本身未导致 geometry resplit。

对 marker70：

$$
\boxed{
0\text{ leaves require resplit}.
}
$$

所以目前合理推测：

> 多数已有较厚 margin的 geometry-complete shards可以直接 bulk migrate。

但这只是 engineering hypothesis，

必须逐 shard验证。

---

# 18. Cross-backend scope boundary

Round 31不宣称：

> MPFR implementation formally verified。

真正的数学 certificate仍依赖一个 software trust base。

当前做法：

1. shrink trust surface；
2. source/binary pin；
3. different libraries；
4. different implementations；
5. strict rational final comparisons。

这是 practical computer-assisted proof architecture，

不是 foundational formal verification。

---

# 19. Current local status lattice

marker70/B7：

`REFERENCE-COMPLETE`

↓

`ARITHMETICALLY-CLOSED-PROTOTYPE`

↓

`A1-VERIFIED-PINNED-PROTOTYPE`

↓

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

但 global：

$$
\boxed{
\texttt{THEOREM-READY=false}.
}
$$

---

# 20. Correction ledger

## R31-MPFR-MARKER-001

overly broad active-sector candidate set caused safe false-negative marker upper。

fixed。

## R31-BACKEND-LOCK-001

first ldconfig parsing helper generated an invalid `/` path and failed before manifest generation。

fixed；无 mathematical effect。

---

# 21. Round 32

## Bulk Publication-Candidate Migration and Global Residual Closure

下一轮开始两队并行：

### Arithmetic team

取 geometry-complete queue中最便宜的下一批 cells，

批量做：

- Round28 lower migration；
- Round29 marker upper；
- Round30 A1；
- Round31 MPFR cross-backend。

统计：

$$
\boxed{
\text{publication-candidate coverage fraction}.
}
$$

### Geometry team

只追 still-residual cells，

完成新的 common-budget：

$$
d=40,\ 42,\ldots
$$

closure wave。

最终目标：

> geometry coverage 与 publication-candidate arithmetic coverage开始在同一 atlas上汇合。

---

# 22. 最短交接

Round 31关闭了 marker70 shard最后一个 local arithmetic redundancy gate：

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

所以：

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

已经合理成立于 local shard scope。

接下来主要问题不再是：

> 这一片能不能严谨重播？

而是：

$$
\boxed{
\text{能不能把这种成熟度批量扩散到所有 final shards}.
}
$$

global theorem仍保持：

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